2015-01-21 05:10:45 +00:00
|
|
|
require "language/haskell"
|
|
|
|
|
|
|
|
|
|
class Agda < Formula
|
|
|
|
|
include Language::Haskell::Cabal
|
|
|
|
|
|
|
|
|
|
homepage "http://wiki.portal.chalmers.se/agda/"
|
|
|
|
|
url "http://hackage.haskell.org/package/Agda-2.4.2.2/Agda-2.4.2.2.tar.gz"
|
|
|
|
|
sha1 "fbdf7df3d5a036e683210ac7ccf4f8ec0c9fea05"
|
|
|
|
|
|
2015-01-23 05:10:47 +00:00
|
|
|
bottle do
|
|
|
|
|
sha1 "d0827796e1d0ac2ba33ef73c8bec7f99ee95b02a" => :yosemite
|
|
|
|
|
sha1 "7e49026d601135596b830b4a6b7032e463b1a51c" => :mavericks
|
|
|
|
|
sha1 "0db7eb99ae43f17dc0509dbbf48341c20c534ef4" => :mountain_lion
|
|
|
|
|
end
|
|
|
|
|
|
2015-01-21 05:10:45 +00:00
|
|
|
devel do
|
|
|
|
|
url "https://github.com/agda/agda.git", :branch => "maint-2.4.2"
|
|
|
|
|
version "2.4.2.3-beta"
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
head "https://github.com/agda/agda.git", :branch => "master"
|
|
|
|
|
|
|
|
|
|
option "without-epic-backend", "Exclude the 'epic' compiler backend"
|
|
|
|
|
|
|
|
|
|
depends_on "ghc" => :build
|
|
|
|
|
depends_on "cabal-install" => :build
|
|
|
|
|
depends_on "gmp"
|
|
|
|
|
depends_on "bdw-gc" if build.with? "epic-backend"
|
|
|
|
|
|
|
|
|
|
def install
|
|
|
|
|
if build.with? "epic-backend"
|
|
|
|
|
epic_flag = "-fepic"
|
|
|
|
|
else
|
|
|
|
|
epic_flag = "-f-epic"
|
|
|
|
|
end
|
|
|
|
|
cabal_sandbox do
|
|
|
|
|
cabal_install_tools "alex", "happy", "cpphs"
|
|
|
|
|
cabal_install "--only-dependencies", epic_flag
|
|
|
|
|
cabal_install "--prefix=#{prefix}", epic_flag
|
|
|
|
|
end
|
|
|
|
|
cabal_clean_lib
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
test do
|
|
|
|
|
# run Agda's built-in test suite
|
|
|
|
|
system bin/"agda", "--test"
|
|
|
|
|
|
|
|
|
|
# typecheck and compile a simple module
|
|
|
|
|
path = testpath/"test.agda"
|
|
|
|
|
path.write <<-EOS.undent
|
|
|
|
|
module test where
|
|
|
|
|
open import Agda.Primitive
|
|
|
|
|
infixr 6 _::_
|
|
|
|
|
data List {i} (A : Set i) : Set i where
|
|
|
|
|
[] : List A
|
|
|
|
|
_::_ : A -> List A -> List A
|
|
|
|
|
snoc : forall {i} {A : Set i} -> List A -> A -> List A
|
|
|
|
|
snoc [] x = x :: []
|
|
|
|
|
snoc (x :: xs) y = x :: (snoc xs y)
|
|
|
|
|
EOS
|
|
|
|
|
system bin/"agda", "-c", "--no-main", "--safe", "--without-K", path
|
|
|
|
|
end
|
|
|
|
|
end
|
