7a4dabfc1a
This restores 1.8 hash rockets because they look nicer with e.g. `depends_on :foo => :bar`
190 lines
5 KiB
Ruby
190 lines
5 KiB
Ruby
require "language/haskell"
|
||
|
||
class Agda < Formula
|
||
include Language::Haskell::Cabal
|
||
|
||
desc "Dependently typed functional programming language"
|
||
homepage "http://wiki.portal.chalmers.se/agda/"
|
||
|
||
stable do
|
||
url "https://github.com/agda/agda/archive/v2.5.1.1.tar.gz"
|
||
sha256 "a0e23cbbcfd5a7e182d52efb9302c1c35085594fa650234806f6b0d90c7fe8d8"
|
||
|
||
resource "stdlib" do
|
||
url "https://github.com/agda/agda-stdlib/archive/v0.12.tar.gz"
|
||
sha256 "2fddbc6d08e74c6205075704f40c550fc40137dee44e6b22b2e08ddee1410e87"
|
||
end
|
||
end
|
||
|
||
bottle do
|
||
revision 1
|
||
sha256 "da0d064f704833f7594a2ece28d5aec82fdda17105d8059c955dd8e5f523270a" => :el_capitan
|
||
sha256 "4898eb5092dea5fb56a4c65cae2ff9eada1026f05901bb3056425b786dbb7d1e" => :yosemite
|
||
sha256 "c7a55550e0e9f4a440ceaa9a3348334a1eb792e3b9eb25e13d8dec643c06dab3" => :mavericks
|
||
end
|
||
|
||
head do
|
||
url "https://github.com/agda/agda.git"
|
||
|
||
resource "stdlib" do
|
||
url "https://github.com/agda/agda-stdlib.git"
|
||
end
|
||
end
|
||
|
||
deprecated_option "without-malonzo" => "without-ghc"
|
||
|
||
option "without-stdlib", "Don't install the Agda standard library"
|
||
option "without-ghc", "Disable the GHC backend"
|
||
|
||
depends_on "ghc" => :recommended
|
||
if build.with? "ghc"
|
||
depends_on "cabal-install"
|
||
else
|
||
depends_on "ghc" => :build
|
||
depends_on "cabal-install" => :build
|
||
end
|
||
|
||
depends_on :emacs => ["23.4", :recommended]
|
||
|
||
def install
|
||
# install Agda core
|
||
install_cabal_package :using => ["alex", "happy", "cpphs"]
|
||
|
||
if build.with? "stdlib"
|
||
resource("stdlib").stage lib/"agda"
|
||
|
||
# generate the standard library's bytecode
|
||
cd lib/"agda" do
|
||
cabal_sandbox :home => buildpath, :keep_lib => true do
|
||
cabal_install "--only-dependencies"
|
||
cabal_install
|
||
system "GenerateEverything"
|
||
end
|
||
end
|
||
|
||
# generate the standard library's documentation and vim highlighting files
|
||
cd lib/"agda" do
|
||
system bin/"agda", "-i", ".", "-i", "src", "--html", "--vim", "README.agda"
|
||
end
|
||
end
|
||
|
||
# compile the included Emacs mode
|
||
if build.with? "emacs"
|
||
system bin/"agda-mode", "compile"
|
||
elisp.install_symlink Dir["#{share}/*/Agda-#{version}/emacs-mode/*"]
|
||
end
|
||
end
|
||
|
||
def caveats
|
||
s = ""
|
||
|
||
if build.with? "stdlib"
|
||
s += <<-EOS.undent
|
||
To use the Agda standard library by default:
|
||
mkdir -p ~/.agda
|
||
echo #{HOMEBREW_PREFIX}/lib/agda/standard-library.agda-lib >>~/.agda/libraries
|
||
echo standard-library >>~/.agda/defaults
|
||
EOS
|
||
end
|
||
|
||
s
|
||
end
|
||
|
||
test do
|
||
simpletest = testpath/"SimpleTest.agda"
|
||
simpletest.write <<-EOS.undent
|
||
module SimpleTest where
|
||
|
||
data ℕ : Set where
|
||
zero : ℕ
|
||
suc : ℕ → ℕ
|
||
|
||
infixl 6 _+_
|
||
_+_ : ℕ → ℕ → ℕ
|
||
zero + n = n
|
||
suc m + n = suc (m + n)
|
||
|
||
infix 4 _≡_
|
||
data _≡_ {A : Set} (x : A) : A → Set where
|
||
refl : x ≡ x
|
||
|
||
cong : ∀ {A B : Set} (f : A → B) {x y} → x ≡ y → f x ≡ f y
|
||
cong f refl = refl
|
||
|
||
+-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
|
||
+-assoc zero _ _ = refl
|
||
+-assoc (suc m) n o = cong suc (+-assoc m n o)
|
||
EOS
|
||
|
||
stdlibtest = testpath/"StdlibTest.agda"
|
||
stdlibtest.write <<-EOS.undent
|
||
module StdlibTest where
|
||
|
||
open import Data.Nat
|
||
open import Relation.Binary.PropositionalEquality
|
||
|
||
+-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
|
||
+-assoc zero _ _ = refl
|
||
+-assoc (suc m) n o = cong suc (+-assoc m n o)
|
||
EOS
|
||
|
||
iotest = testpath/"IOTest.agda"
|
||
iotest.write <<-EOS.undent
|
||
module IOTest where
|
||
|
||
open import Agda.Builtin.IO
|
||
open import Agda.Builtin.Unit
|
||
|
||
postulate
|
||
return : ∀ {A : Set} → A → IO A
|
||
|
||
{-# COMPILED return (\\_ -> return) #-}
|
||
|
||
main : _
|
||
main = return tt
|
||
EOS
|
||
|
||
stdlibiotest = testpath/"StdlibIOTest.agda"
|
||
stdlibiotest.write <<-EOS.undent
|
||
module StdlibIOTest where
|
||
|
||
open import IO
|
||
|
||
main : _
|
||
main = run (putStr "Hello, world!")
|
||
EOS
|
||
|
||
# run Agda's built-in test suite
|
||
system bin/"agda", "--test"
|
||
|
||
# typecheck a simple module
|
||
system bin/"agda", simpletest
|
||
|
||
# typecheck a module that uses the standard library
|
||
if build.with? "stdlib"
|
||
system bin/"agda", "-i", lib/"agda"/"src", stdlibtest
|
||
end
|
||
|
||
# compile a simple module using the JS backend
|
||
system bin/"agda", "--js", simpletest
|
||
|
||
# test the GHC backend
|
||
if build.with? "ghc"
|
||
cabal_sandbox do
|
||
cabal_install "text"
|
||
dbpath = Dir["#{testpath}/.cabal-sandbox/*-packages.conf.d"].first
|
||
dbopt = "--ghc-flag=-package-db=#{dbpath}"
|
||
|
||
# compile and run a simple program
|
||
system bin/"agda", "-c", dbopt, iotest
|
||
assert_equal "", shell_output(testpath/"IOTest")
|
||
|
||
# compile and run a program that uses the standard library
|
||
if build.with? "stdlib"
|
||
system bin/"agda", "-c", "-i", lib/"agda"/"src", dbopt, stdlibiotest
|
||
assert_equal "Hello, world!", shell_output(testpath/"StdlibIOTest")
|
||
end
|
||
end
|
||
end
|
||
end
|
||
end
|