1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
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"
revision 1
bottle do
sha1 "ce3cd69caaa5644f23db06dba5a1b558badca8ad" => :yosemite
sha1 "8157fc67f29852e133e1e17f28530388a0f99d00" => :mavericks
sha1 "c6d0c8b66e676f4f7eae63b4fe9b3a40e5a6a36c" => :mountain_lion
end
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"
option "without-stdlib", "Don't install the Agda standard library"
option "with-malonzo-ffi",
"Include the MAlonzo backend's FFI (depends on the standard library)"
depends_on "cabal-install" => :build
depends_on "ghc"
depends_on "gmp"
depends_on "bdw-gc" if build.with? "epic-backend"
depends_on "emacs" => :optional
head do
resource "stdlib" do
url "https://github.com/agda/agda-stdlib.git", :branch => "master"
end
end
resource "stdlib" do
url "https://github.com/agda/agda-stdlib/archive/v0.9.tar.gz"
sha1 "f39d5685ab2dc47758c87d9068047fce6b4b99a1"
end
def install
if build.with? "epic-backend"
epic_flag = "-fepic"
else
epic_flag = "-f-epic"
end
# install Agda core
cabal_sandbox do
cabal_install_tools "alex", "happy", "cpphs"
if build.with? "epic-backend"
cabal_install "--prefix=#{prefix}", "epic"
end
cabal_install "--only-dependencies", epic_flag
cabal_install "--prefix=#{prefix}", epic_flag
end
cabal_clean_lib
if build.with? "stdlib"
resource("stdlib").stage prefix/"agda-stdlib"
# install the standard library's helper tools
cd prefix/"agda-stdlib" do
cabal_sandbox do
cabal_install "--only-dependencies"
cabal_install "--prefix=#{prefix/"agda-stdlib"}"
system prefix/"agda-stdlib"/"bin"/"GenerateEverything"
end
cabal_clean_lib
end
# install the standard library's FFI bindings for the MAlonzo backend
if build.with? "malonzo-ffi"
cd prefix/"agda-stdlib"/"ffi" do
cabal_install "--user"
end
end
# generate the standard library's documentation and vim highlighting files
cd prefix/"agda-stdlib" do
system bin/"agda", "-i", ".", "-i", "src", "--html", "--vim", "README.agda"
end
end
# byte-compile and install Agda's included emacs mode
if build.with? "emacs"
system bin/"agda-mode", "setup"
system bin/"agda-mode", "compile"
end
end
test do
# run Agda's built-in test suite
system bin/"agda", "--test"
# typecheck and compile a simple module
test_file_path = testpath/"simple-test.agda"
test_file_path.write <<-EOS.undent
{-# OPTIONS --without-K #-}
module simple-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", test_file_path
system bin/"agda", "--js", "--safe", test_file_path
# typecheck, compile, and run a program that uses the standard library
if build.with? "stdlib" and build.with? "malonzo-ffi"
test_file_path = testpath/"stdlib-test.agda"
test_file_path.write <<-EOS.undent
module stdlib-test where
open import Data.String
open import Function
open import IO
main : _
main = run $ putStr "Hello, world!"
EOS
system bin/"agda", "-i", testpath, "-i", prefix/"agda-stdlib"/"src",
"-c", test_file_path
assert_equal `testpath/"stdlib-test"`, "Hello, world!"
end
end
end
|
