2015-01-21 05:10:45 +00:00
|
|
|
require "language/haskell"
|
|
|
|
|
|
|
|
class Agda < Formula
|
|
|
|
include Language::Haskell::Cabal
|
2015-05-19 00:00:59 +00:00
|
|
|
desc "Dependently typed functional programming language"
|
2015-01-21 05:10:45 +00:00
|
|
|
homepage "http://wiki.portal.chalmers.se/agda/"
|
2015-11-01 19:22:02 +00:00
|
|
|
revision 1
|
|
|
|
|
|
|
|
stable do
|
|
|
|
url "https://github.com/agda/agda/archive/2.4.2.4.tar.gz"
|
|
|
|
sha256 "0147f8a1395a69bee1e7a452682094e45c83126233f9864544b8a14f956ce8c3"
|
|
|
|
# fix compilation of the included Emacs mode
|
|
|
|
# merged upstream in https://github.com/agda/agda/pull/1700
|
|
|
|
patch :DATA
|
|
|
|
end
|
2015-01-21 05:10:45 +00:00
|
|
|
|
2015-01-23 05:10:47 +00:00
|
|
|
bottle do
|
2015-11-02 04:34:00 +00:00
|
|
|
sha256 "91f67965e6a349b98b785aa189e80203321e8bd3e0b190fa4079ea5722c60813" => :el_capitan
|
|
|
|
sha256 "1fb3c63041d1b77395b44c7cd30c25a55dde4a8915103869209e5764358650d4" => :yosemite
|
|
|
|
sha256 "45030e84681d5460fe1c4458f5578b5757a2cc55fe2d09d034665acf10f16f5c" => :mavericks
|
2015-01-23 05:10:47 +00:00
|
|
|
end
|
|
|
|
|
2015-10-25 13:46:32 +00:00
|
|
|
head do
|
|
|
|
url "https://github.com/agda/agda.git", :branch => "master"
|
|
|
|
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.git",
|
|
|
|
:tag => "v0.11",
|
|
|
|
:revision => "8602c29a7627eb001344cf50e6b74f880fb6bf18"
|
|
|
|
end
|
2015-01-21 05:10:45 +00:00
|
|
|
|
2015-02-09 20:46:31 +00:00
|
|
|
option "without-stdlib", "Don't install the Agda standard library"
|
2015-10-25 13:46:32 +00:00
|
|
|
option "without-malonzo", "Disable the MAlonzo backend"
|
2015-01-21 05:10:45 +00:00
|
|
|
|
2015-10-25 13:46:32 +00:00
|
|
|
if build.with? "malonzo"
|
|
|
|
depends_on "ghc"
|
|
|
|
else
|
|
|
|
depends_on "ghc" => :build
|
|
|
|
end
|
2015-01-21 05:10:45 +00:00
|
|
|
depends_on "cabal-install" => :build
|
2015-04-30 05:48:53 +00:00
|
|
|
|
2015-01-21 05:10:45 +00:00
|
|
|
depends_on "gmp"
|
2015-11-04 12:46:04 +00:00
|
|
|
depends_on :emacs => ["21.1", :recommended]
|
2015-02-09 20:46:31 +00:00
|
|
|
|
2015-05-29 02:30:10 +00:00
|
|
|
setup_ghc_compilers
|
|
|
|
|
2015-01-21 05:10:45 +00:00
|
|
|
def install
|
2015-02-09 20:46:31 +00:00
|
|
|
# install Agda core
|
2015-01-21 05:10:45 +00:00
|
|
|
cabal_sandbox do
|
|
|
|
cabal_install_tools "alex", "happy", "cpphs"
|
2015-07-19 17:51:43 +00:00
|
|
|
cabal_install "--only-dependencies"
|
|
|
|
cabal_install "--prefix=#{prefix}"
|
2015-01-21 05:10:45 +00:00
|
|
|
end
|
|
|
|
cabal_clean_lib
|
2015-02-09 20:46:31 +00:00
|
|
|
|
|
|
|
if build.with? "stdlib"
|
|
|
|
resource("stdlib").stage prefix/"agda-stdlib"
|
|
|
|
|
2015-10-25 13:46:32 +00:00
|
|
|
# generate the standard library's bytecode
|
2015-02-09 20:46:31 +00:00
|
|
|
cd prefix/"agda-stdlib" do
|
|
|
|
cabal_sandbox do
|
|
|
|
cabal_install "--only-dependencies"
|
2015-10-25 13:46:32 +00:00
|
|
|
cabal_install
|
|
|
|
system "GenerateEverything"
|
2015-02-09 20:46:31 +00:00
|
|
|
end
|
2015-10-25 13:46:32 +00:00
|
|
|
rm_rf [".cabal", "dist"]
|
2015-02-09 20:46:31 +00:00
|
|
|
end
|
|
|
|
|
|
|
|
# install the standard library's FFI bindings for the MAlonzo backend
|
2015-10-25 13:46:32 +00:00
|
|
|
# in a dedicated GHC package database
|
|
|
|
if build.with? "malonzo"
|
|
|
|
db_path = prefix/"agda-stdlib"/"ffi"/"package.conf.d"
|
|
|
|
|
|
|
|
mkdir db_path
|
|
|
|
system "ghc-pkg", "--package-db=#{db_path}", "recache"
|
|
|
|
|
2015-02-09 20:46:31 +00:00
|
|
|
cd prefix/"agda-stdlib"/"ffi" do
|
2015-10-25 13:46:32 +00:00
|
|
|
cabal_sandbox do
|
|
|
|
system "cabal", "--ignore-sandbox", "install", "--package-db=#{db_path}",
|
|
|
|
"--prefix=#{prefix/"agda-stdlib"/"ffi"}"
|
|
|
|
end
|
|
|
|
rm_rf [".cabal", "dist"]
|
2015-02-09 20:46:31 +00:00
|
|
|
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
|
|
|
|
|
2015-10-25 13:46:32 +00:00
|
|
|
# compile the included Emacs mode
|
2015-02-09 20:46:31 +00:00
|
|
|
if build.with? "emacs"
|
|
|
|
system bin/"agda-mode", "compile"
|
2015-11-01 19:22:02 +00:00
|
|
|
elisp.install Dir["#{share}/*/Agda-#{version}/emacs-mode/*"]
|
2015-02-09 20:46:31 +00:00
|
|
|
end
|
2015-01-21 05:10:45 +00:00
|
|
|
end
|
|
|
|
|
2015-10-25 13:46:32 +00:00
|
|
|
def caveats
|
|
|
|
s = ""
|
|
|
|
|
|
|
|
if build.with? "stdlib"
|
|
|
|
s += <<-EOS.undent
|
|
|
|
To use the Agda standard library, point Agda to the following include dir:
|
|
|
|
#{prefix/"agda-stdlib"/"src"}
|
|
|
|
EOS
|
|
|
|
|
|
|
|
if build.with? "malonzo"
|
|
|
|
s += <<-EOS.undent
|
|
|
|
|
|
|
|
To use the FFI bindings for the MAlonzo backend, give Agda the following option:
|
|
|
|
--ghc-flag=-package-db=#{prefix/"agda-stdlib"/"ffi"/"package.conf.d"}
|
|
|
|
EOS
|
|
|
|
end
|
|
|
|
end
|
|
|
|
|
|
|
|
s
|
|
|
|
end
|
|
|
|
|
2015-01-21 05:10:45 +00:00
|
|
|
test do
|
|
|
|
# run Agda's built-in test suite
|
|
|
|
system bin/"agda", "--test"
|
|
|
|
|
|
|
|
# typecheck and compile a simple module
|
2015-02-09 20:46:31 +00:00
|
|
|
test_file_path = testpath/"simple-test.agda"
|
|
|
|
test_file_path.write <<-EOS.undent
|
|
|
|
{-# OPTIONS --without-K #-}
|
|
|
|
module simple-test where
|
2015-01-21 05:10:45 +00:00
|
|
|
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
|
2015-10-25 13:46:32 +00:00
|
|
|
if build.with? "malonzo"
|
|
|
|
system bin/"agda", "-c", "--no-main", "--safe", test_file_path
|
|
|
|
end
|
2015-02-09 20:46:31 +00:00
|
|
|
system bin/"agda", "--js", "--safe", test_file_path
|
|
|
|
|
|
|
|
# typecheck, compile, and run a program that uses the standard library
|
2015-10-25 13:46:32 +00:00
|
|
|
if build.with?("stdlib") && build.with?("malonzo")
|
2015-02-09 20:46:31 +00:00
|
|
|
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",
|
2015-10-25 13:46:32 +00:00
|
|
|
"--ghc-flag=-package-db=#{prefix/"agda-stdlib"/"ffi"/"package.conf.d"}",
|
2015-02-09 20:46:31 +00:00
|
|
|
"-c", test_file_path
|
2015-10-25 13:46:32 +00:00
|
|
|
assert_equal "Hello, world!", shell_output("#{testpath/"stdlib-test"}")
|
2015-02-09 20:46:31 +00:00
|
|
|
end
|
2015-01-21 05:10:45 +00:00
|
|
|
end
|
|
|
|
end
|
2015-10-25 13:46:32 +00:00
|
|
|
|
|
|
|
__END__
|
|
|
|
diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el
|
|
|
|
index 04604ee..f6b3122 100644
|
|
|
|
--- a/src/data/emacs-mode/agda2-mode.el
|
|
|
|
+++ b/src/data/emacs-mode/agda2-mode.el
|
|
|
|
@@ -20,6 +20,7 @@ Note that the same version of the Agda executable must be used.")
|
|
|
|
(require 'time-date)
|
|
|
|
(require 'eri)
|
|
|
|
(require 'annotation)
|
|
|
|
+(require 'fontset)
|
|
|
|
(require 'agda-input)
|
|
|
|
(require 'agda2)
|
|
|
|
(require 'agda2-highlight)
|