homebrew-core/Formula/math-comp.rb
2018-10-31 13:19:31 -04:00

52 lines
1.6 KiB
Ruby

class MathComp < Formula
desc "Mathematical Components for the Coq proof assistant"
homepage "https://math-comp.github.io/math-comp/"
url "https://github.com/math-comp/math-comp/archive/mathcomp-1.7.0.tar.gz"
sha256 "69c01e99aad618fa9a0bb4a19af00827c505b8205816eb590e51abca49f4ef17"
revision 3
head "https://github.com/math-comp/math-comp.git"
bottle do
cellar :any_skip_relocation
sha256 "4b767eb03faffb0318d2757b1cb5ecd74ce630081dfd3fadf546c9378b5c8736" => :mojave
sha256 "b59397f2aa9112bcebac0fa50c0a5e78c7f80a21b99875065e09aa0c3879db50" => :high_sierra
sha256 "6870a4cbcf0d55293b9bf8f8c00376204184ffaa15d1c920b06eafc450686ec7" => :sierra
end
depends_on "ocaml" => :build
depends_on "coq"
def install
coqlib = "#{lib}/coq/"
(buildpath/"mathcomp/Makefile.coq.local").write <<~EOS
COQLIB=#{coqlib}
EOS
cd "mathcomp" do
system "make", "Makefile.coq"
system "make", "-f", "Makefile.coq", "MAKEFLAGS=#{ENV["MAKEFLAGS"]}"
system "make", "install", "MAKEFLAGS=#{ENV["MAKEFLAGS"]}"
elisp.install "ssreflect/pg-ssr.el"
end
doc.install Dir["docs/*"]
end
test do
(testpath/"testing.v").write <<~EOS
From mathcomp Require Import ssreflect seq.
Parameter T: Type.
Theorem test (s1 s2: seq T): size (s1 ++ s2) = size s1 + size s2.
Proof. by elim : s1 =>//= x s1 ->. Qed.
Check test.
EOS
coqc = Formula["coq"].opt_bin/"coqc"
cmd = "#{coqc} -R #{lib}/coq/user-contrib/mathcomp mathcomp testing.v"
assert_match /\Atest\s+: forall/, shell_output(cmd)
end
end