homebrew-core/Formula/agda.rb

187 lines
5.0 KiB
Ruby
Raw Blame History

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

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://hackage.haskell.org/package/Agda-2.5.2/Agda-2.5.2.tar.gz"
sha256 "d812cec3bf7f03c4b27248572475c7e060154102771a8434cc11ba89f5691439"
resource "stdlib" do
url "https://github.com/agda/agda-stdlib/archive/v0.13.tar.gz"
sha256 "e7cffc2b8b168c3584b6d1e760d2b49850835444e4777caa69eb29b3677ef8bb"
end
end
bottle do
sha256 "4de53fe05b8d9fc11d9e5955165a957c3c6bfcbf45dc28afba1c8fff80f5cece" => :sierra
sha256 "33acce2fc1b974f8d2438844402676b96de01034d120036cb8a3a429ee9fa095" => :el_capitan
sha256 "5061c16954c5af7f38e51fe07e9e2eb9923be90c62ba6e699102936da81a329a" => :yosemite
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
# 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", "ieee754"
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