math-comp 1.6.4
rename from ssreflect Closes #23561. Signed-off-by: ilovezfs <ilovezfs@icloud.com>master
Kasumi Hanazuki
ilovezfs
parent
b5c5520113
commit
67f69ba9e0
|
|
@ -0,0 +1 @@
|
|||
../Formula/math-comp.rb
|
||||
|
|
@ -0,0 +1 @@
|
|||
../Formula/math-comp.rb
|
||||
|
|
@ -0,0 +1,46 @@
|
|||
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.6.4.tar.gz"
|
||||
sha256 "c672a4237f708b5f03f1feed9de37f98ef5c331819047e1f71b5762dcd92b262"
|
||||
head "https://github.com/math-comp/math-comp.git"
|
||||
|
||||
depends_on "ocaml" => :build
|
||||
depends_on "coq"
|
||||
|
||||
def install
|
||||
coqbin = "#{Formula["coq"].opt_bin}/"
|
||||
coqlib = "#{lib}/coq/"
|
||||
|
||||
(buildpath/"mathcomp/Makefile.coq.local").write <<~EOS
|
||||
COQLIB=#{coqlib}
|
||||
EOS
|
||||
|
||||
cd "mathcomp" do
|
||||
system "make", "MAKEFLAGS=#{ENV["MAKEFLAGS"]}", "COQBIN=#{coqbin}"
|
||||
system "make", "install", "MAKEFLAGS=#{ENV["MAKEFLAGS"]}", "COQBIN=#{coqbin}"
|
||||
|
||||
elisp.install "ssreflect/pg-ssr.el"
|
||||
end
|
||||
|
||||
system "make", "-C", "htmldoc", "COQBIN=#{coqbin}" if build.head?
|
||||
|
||||
doc.install Dir["htmldoc/*"]
|
||||
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
|
||||
|
|
@ -1,125 +0,0 @@
|
|||
class Camlp5TransitionalModeRequirement < Requirement
|
||||
fatal true
|
||||
|
||||
satisfy(:build_env => false) { !Tab.for_name("camlp5").with?("strict") }
|
||||
|
||||
def message; <<~EOS
|
||||
camlp5 must be compiled in transitional mode (instead of --strict mode):
|
||||
brew install camlp5
|
||||
EOS
|
||||
end
|
||||
end
|
||||
|
||||
class Ssreflect < Formula
|
||||
desc "Virtual package provided by libssreflect-coq"
|
||||
homepage "https://math-comp.github.io/math-comp/"
|
||||
url "http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.tar.gz"
|
||||
sha256 "bad978693d1bfd0a89586a34678bcc244e3b7efba6431e0f83d8e1ae8f82a142"
|
||||
revision 3
|
||||
|
||||
bottle do
|
||||
sha256 "952d4dbbbb3599a901814892769fd42b2a86fc72544100d7abba42fbca56df0f" => :high_sierra
|
||||
sha256 "d2bb5472dc0339957be0f11efe89fdc9c367a0ab0d4458cb80c7829eec31fd7d" => :sierra
|
||||
sha256 "8bb36558561b6e9f95f65f13278add1cb5aaec4596b7b9010fc1abbaa4fc049d" => :el_capitan
|
||||
sha256 "4e818fc061186ff528dea4aae58db36fb8358152527185f6150b71cdf2b4c598" => :yosemite
|
||||
end
|
||||
|
||||
option "with-doc", "Install HTML documents"
|
||||
option "without-static", "Build without static linking"
|
||||
|
||||
depends_on "ocaml"
|
||||
depends_on "menhir" => :build
|
||||
depends_on "camlp5" => :build # needed for building Coq 8.4
|
||||
depends_on Camlp5TransitionalModeRequirement # same requirement as in Coq formula
|
||||
|
||||
resource "coq84" do
|
||||
url "https://coq.inria.fr/distrib/V8.4pl6/files/coq-8.4pl6.tar.gz"
|
||||
sha256 "a540a231a9970a49353ca039f3544616ff86a208966ab1c593779ae13c91ebd6"
|
||||
end
|
||||
|
||||
# Fix an ill-formatted ocamldoc comment.
|
||||
patch :DATA
|
||||
|
||||
def install
|
||||
ENV["OCAMLPARAM"] = "safe-string=0,_" # OCaml 4.06.0 compat
|
||||
|
||||
resource("coq84").stage do
|
||||
system "./configure", "-prefix", libexec/"coq",
|
||||
"-camlp5dir", Formula["camlp5"].opt_lib/"ocaml/camlp5",
|
||||
"-coqide", "no",
|
||||
"-with-doc", "no",
|
||||
# Prevent warning 31 (module is linked twice in the
|
||||
# same executable) from being a fatal error, which
|
||||
# would otherwise be the default as of ocaml 4.03.0;
|
||||
# note that "-custom" is the default value of
|
||||
# coqrunbyteflags, and is necessary, so don't just
|
||||
# overwrite it with "-warn-error -a"
|
||||
"-coqrunbyteflags", "-warn-error -a -custom"
|
||||
|
||||
system "make", "VERBOSE=1", "world"
|
||||
ENV.deparallelize { system "make", "install" }
|
||||
end
|
||||
|
||||
ENV.prepend_path "PATH", libexec/"coq/bin"
|
||||
ENV.deparallelize
|
||||
|
||||
# Enable static linking.
|
||||
if build.with? "static"
|
||||
inreplace "Make" do |s|
|
||||
s.gsub! /#\-custom/, "-custom"
|
||||
s.gsub! /#SSRCOQ/, "SSRCOQ"
|
||||
end
|
||||
end
|
||||
|
||||
args = %W[
|
||||
COQBIN=#{libexec}/coq/bin/
|
||||
COQLIBINSTALL=lib/coq/user-contrib
|
||||
COQDOCINSTALL=share/doc
|
||||
DSTROOT=#{prefix}/
|
||||
]
|
||||
system "make", *args
|
||||
system "make", "install", *args
|
||||
if build.with? "doc"
|
||||
system "make", "-f", "Makefile.coq", "html", *args
|
||||
system "make", "-f", "Makefile.coq", "mlihtml", *args
|
||||
system "make", "-f", "Makefile.coq", "install-doc", *args
|
||||
end
|
||||
bin.install "bin/ssrcoq.byte", "bin/ssrcoq" if build.with? "static"
|
||||
pkgshare.install "pg-ssr.el"
|
||||
end
|
||||
|
||||
test do
|
||||
(testpath/"helloworld.v").write <<~EOS
|
||||
Add LoadPath "#{lib}/coq/user-contrib/Ssreflect" as Ssreflect.
|
||||
Require Import Ssreflect.ssreflect.
|
||||
Variable P:Prop.
|
||||
|
||||
Theorem helloworld: P -> P.
|
||||
Proof.
|
||||
done.
|
||||
Qed.
|
||||
|
||||
Check helloworld.
|
||||
EOS
|
||||
(testpath/"expected").write <<~EOS
|
||||
helloworld
|
||||
: P -> P
|
||||
EOS
|
||||
assert_equal File.read(testpath/"expected"), pipe_output("#{bin}/ssrcoq -compile helloworld")
|
||||
end
|
||||
end
|
||||
|
||||
__END__
|
||||
diff --git a/src/ssrmatching.mli b/src/ssrmatching.mli
|
||||
index fd2e835..1d9d15b 100644
|
||||
--- a/src/ssrmatching.mli
|
||||
+++ b/src/ssrmatching.mli
|
||||
@@ -77,7 +77,7 @@ val interp_cpattern :
|
||||
pattern
|
||||
|
||||
(** The set of occurrences to be matched. The boolean is set to true
|
||||
- * to signal the complement of this set (i.e. {-1 3}) *)
|
||||
+ * to signal the complement of this set (i.e. \{-1 3\}) *)
|
||||
type occ = (bool * int list) option
|
||||
|
||||
(** Substitution function. The [int] argument is the number of binders
|
||||
|
|
@ -165,6 +165,7 @@
|
|||
"sonar": "sonarqube",
|
||||
"speedtest_cli": "speedtest-cli",
|
||||
"srtp@1.5": "srtp@1.6",
|
||||
"ssreflect": "math-comp",
|
||||
"stash-cli": "atlassian-cli",
|
||||
"subversion18": "subversion@1.8",
|
||||
"swig2": "swig@2",
|
||||
|
|
|
|||
Loading…
Reference in New Issue