From 3efe23a44c0a70a779083674992a70e20bf73edf Mon Sep 17 00:00:00 2001 From: Michael Cho Date: Sun, 23 Mar 2025 18:41:37 -0400 Subject: [PATCH 1/5] coq: rename to `rocq` --- .github/autobump.txt | 2 +- Formula/c/coq.rb | 90 -------------------------------------------- formula_renames.json | 1 + 3 files changed, 2 insertions(+), 91 deletions(-) delete mode 100644 Formula/c/coq.rb diff --git a/.github/autobump.txt b/.github/autobump.txt index 10ff7ca0ac37c..9c3dd0fa98e41 100644 --- a/.github/autobump.txt +++ b/.github/autobump.txt @@ -615,7 +615,6 @@ cookiecutter copa copier copilot -coq core-lightning coredns coreutils @@ -2977,6 +2976,7 @@ robin-map roblox-ts robot-framework rocksdb +rocq rogcat rojo rollup diff --git a/Formula/c/coq.rb b/Formula/c/coq.rb deleted file mode 100644 index 35bc8d6ec2339..0000000000000 --- a/Formula/c/coq.rb +++ /dev/null @@ -1,90 +0,0 @@ -class Coq < Formula - desc "Proof assistant for higher-order logic" - homepage "https://coq.inria.fr/" - url "https://github.com/coq/coq/releases/download/V8.20.1/coq-8.20.1.tar.gz" - sha256 "09ad238cc7930d59564b032be2a8a1fd10d6ef845364d739072d04090a6d3cc2" - license "LGPL-2.1-only" - head "https://github.com/coq/coq.git", branch: "master" - - livecheck do - url :stable - regex(/^v?(\d+(?:\.\d+)+)$/i) - end - - bottle do - sha256 arm64_sequoia: "65a6d3984df7191476d584bf10ad5a20f7f5b79985f3b2550ede68ee9c84204c" - sha256 arm64_sonoma: "f0fbf43c5369353ec0b2ca64b5132bb81b34c1ed2e3dc3e51aefb35232807873" - sha256 arm64_ventura: "6a647ecd4b7562cac8cf430dc897db55cad68aa2f41f727491c9d25a9528f1da" - sha256 sonoma: "37910c96de115af903170ebc56447092de187c4e1eda11c44be0fdc77bf0881e" - sha256 ventura: "3d1168df2643f5ab98fd7a721ca12bd3dff10f447918d6f3962d1867abfdc1ff" - sha256 arm64_linux: "1d2e24d6e8d829cf454df015d3b03a86e0779639825b5cfe60800bcc03fe6d3f" - sha256 x86_64_linux: "df412ed51c3f13261aa40bd9cccf2544ffcc6993ede2371f334e63d0ad8ff473" - end - - depends_on "dune" => :build - depends_on "gmp" - depends_on "ocaml" - depends_on "ocaml-findlib" - depends_on "ocaml-zarith" - - uses_from_macos "m4" => :build - uses_from_macos "unzip" => :build - - def install - # Work around for https://github.com/Homebrew/homebrew-test-bot/issues/805 - if ENV["HOMEBREW_GITHUB_ACTIONS"] && !(Formula["ocaml-findlib"].etc/"findlib.conf").exist? - ENV["OCAMLFIND_CONF"] = Formula["ocaml-findlib"].opt_libexec/"findlib.conf" - end - ENV.prepend_path "OCAMLPATH", Formula["ocaml-zarith"].opt_lib/"ocaml" - ENV.prepend_path "OCAMLPATH", Formula["ocaml-findlib"].opt_lib/"ocaml" - system "./configure", "-prefix", prefix, - "-mandir", man, - "-libdir", HOMEBREW_PREFIX/"lib/ocaml/coq", - "-docdir", pkgshare/"latex" - system "make", "dunestrap" - system "dune", "build", "-p", "coq-core,coq-stdlib,coqide-server,coq" - system "dune", "install", "--prefix=#{prefix}", - "--mandir=#{man}", - "--libdir=#{lib}/ocaml", - "coq-core", - "coq-stdlib", - "coqide-server", - "coq" - end - - test do - # Work around for https://github.com/Homebrew/homebrew-test-bot/issues/805 - if ENV["HOMEBREW_GITHUB_ACTIONS"] && !(Formula["ocaml-findlib"].etc/"findlib.conf").exist? - ENV["OCAMLFIND_CONF"] = Formula["ocaml-findlib"].opt_libexec/"findlib.conf" - end - (testpath/"testing.v").write <<~EOS - Require Coq.micromega.Lia. - Require Coq.ZArith.ZArith. - - Inductive nat : Set := - | O : nat - | S : nat -> nat. - Fixpoint add (n m: nat) : nat := - match n with - | O => m - | S n' => S (add n' m) - end. - Lemma add_O_r : forall (n: nat), add n O = n. - Proof. - intros n; induction n; simpl; auto; rewrite IHn; auto. - Qed. - - Import Coq.micromega.Lia. - Import Coq.ZArith.ZArith. - Open Scope Z. - Lemma add_O_r_Z : forall (n: Z), n + 0 = n. - Proof. - intros; lia. - Qed. - EOS - system bin/"coqc", testpath/"testing.v" - # test ability to find plugin files - output = shell_output("#{Formula["ocaml-findlib"].bin}/ocamlfind query coq-core.plugins.ltac") - assert_equal "#{HOMEBREW_PREFIX}/lib/ocaml/coq-core/plugins/ltac", output.chomp - end -end diff --git a/formula_renames.json b/formula_renames.json index 380477d5e15fb..b46f33a9e98ed 100644 --- a/formula_renames.json +++ b/formula_renames.json @@ -21,6 +21,7 @@ "cloog018": "cloog", "cloudflare-wrangler2": "cloudflare-wrangler", "commonmark": "cmark", + "coq": "rocq", "corepack": "node", "cppformat": "fmt", "crystal-lang": "crystal", From 9b44b81661074934fe2a82932902b4ff46a24b5a Mon Sep 17 00:00:00 2001 From: Michael Cho Date: Sun, 23 Mar 2025 22:04:13 -0400 Subject: [PATCH 2/5] rocq 9.0.0 (renamed formula) --- Formula/r/rocq.rb | 103 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 103 insertions(+) create mode 100644 Formula/r/rocq.rb diff --git a/Formula/r/rocq.rb b/Formula/r/rocq.rb new file mode 100644 index 0000000000000..793993078cf33 --- /dev/null +++ b/Formula/r/rocq.rb @@ -0,0 +1,103 @@ +class Rocq < Formula + desc "Proof assistant for higher-order logic" + homepage "https://rocq-prover.org/" + license "LGPL-2.1-only" + + stable do + url "https://github.com/coq/coq/releases/download/V9.0.0/rocq-9.0.0.tar.gz" + sha256 "82f86646fd3d047f760837648195c73374beee667b1c9592d31c5426e3b43a51" + + resource "stdlib" do + url "https://github.com/coq/stdlib/releases/download/V9.0.0/stdlib-9.0.0.tar.gz" + sha256 "1ab6adc42dfc651ddc909604bae1a54ff5623cda837f93677a8b12aab9eec711" + end + end + + livecheck do + url :stable + regex(/^v?(\d+(?:\.\d+)+)$/i) + end + + head do + url "https://github.com/coq/coq.git", branch: "master" + + resource "stdlib" do + url "https://github.com/coq/stdlib.git", branch: "master" + end + end + + depends_on "dune" => :build + depends_on "gmp" + depends_on "ocaml" + depends_on "ocaml-findlib" + depends_on "ocaml-zarith" + + uses_from_macos "m4" => :build + uses_from_macos "unzip" => :build + + def install + # Work around for https://github.com/Homebrew/homebrew-test-bot/issues/805 + if ENV["HOMEBREW_GITHUB_ACTIONS"] && !(Formula["ocaml-findlib"].etc/"findlib.conf").exist? + ENV["OCAMLFIND_CONF"] = Formula["ocaml-findlib"].opt_libexec/"findlib.conf" + end + ENV.prepend_path "OCAMLPATH", Formula["ocaml-zarith"].opt_lib/"ocaml" + ENV.prepend_path "OCAMLPATH", Formula["ocaml-findlib"].opt_lib/"ocaml" + + packages = %w[rocq-runtime coq-core rocq-core coq coqide-server] + + system "./configure", "-prefix", prefix, + "-mandir", man, + "-libdir", HOMEBREW_PREFIX/"lib/ocaml/coq", + "-docdir", pkgshare/"latex" + system "make", "dunestrap" + system "dune", "build", "-p", packages.join(",") + system "dune", "install", "--prefix=#{prefix}", + "--mandir=#{man}", + "--libdir=#{lib}/ocaml", + "--docdir=#{doc.parent}", + *packages + + resource("stdlib").stage do + ENV.prepend_path "PATH", bin + ENV["ROCQLIB"] = lib/"ocaml/coq" + system "make" + system "make", "install" + end + end + + test do + # Work around for https://github.com/Homebrew/homebrew-test-bot/issues/805 + if ENV["HOMEBREW_GITHUB_ACTIONS"] && !(Formula["ocaml-findlib"].etc/"findlib.conf").exist? + ENV["OCAMLFIND_CONF"] = Formula["ocaml-findlib"].opt_libexec/"findlib.conf" + end + (testpath/"testing.v").write <<~EOS + Require Stdlib.micromega.Lia. + Require Stdlib.ZArith.ZArith. + + Inductive nat : Set := + | O : nat + | S : nat -> nat. + Fixpoint add (n m: nat) : nat := + match n with + | O => m + | S n' => S (add n' m) + end. + Lemma add_O_r : forall (n: nat), add n O = n. + Proof. + intros n; induction n; simpl; auto; rewrite IHn; auto. + Qed. + + Import Stdlib.micromega.Lia. + Import Stdlib.ZArith.ZArith. + Open Scope Z. + Lemma add_O_r_Z : forall (n: Z), n + 0 = n. + Proof. + intros; lia. + Qed. + EOS + system bin/"rocq", "compile", testpath/"testing.v" + # test ability to find plugin files + output = shell_output("#{Formula["ocaml-findlib"].bin}/ocamlfind query rocq-runtime.plugins.ltac") + assert_equal "#{HOMEBREW_PREFIX}/lib/ocaml/rocq-runtime/plugins/ltac", output.chomp + end +end From 32e38279bb98aedb0c02dc21313fa4bbba290563 Mon Sep 17 00:00:00 2001 From: Michael Cho Date: Mon, 24 Mar 2025 18:10:43 -0400 Subject: [PATCH 3/5] rocq-elpi 2.5.0 (new formula) --- Formula/r/rocq-elpi.rb | 85 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 Formula/r/rocq-elpi.rb diff --git a/Formula/r/rocq-elpi.rb b/Formula/r/rocq-elpi.rb new file mode 100644 index 0000000000000..c188481ddf8b0 --- /dev/null +++ b/Formula/r/rocq-elpi.rb @@ -0,0 +1,85 @@ +class RocqElpi < Formula + desc "Elpi extension language for Coq" + homepage "https://github.com/LPCIC/coq-elpi" + # Update resources based on https://github.com/LPCIC/coq-elpi/blob/v#{version}/rocq-elpi.opam#L18-L26 + url "https://github.com/LPCIC/coq-elpi/releases/download/v2.5.0/rocq-elpi-2.5.0.tar.gz" + sha256 "0352cee8fc0a0224f8d8043d7c0f4daf217842e0dc46d5795537bdec737006ae" + license "LGPL-2.1-or-later" + + livecheck do + url :stable + regex(/^v?(\d+(?:\.\d+)+)$/i) + end + + depends_on "dune" => :build + depends_on "ocaml" => :build + depends_on "opam" => :build + depends_on "ocaml-findlib" + depends_on "rocq" + + # NOTE: Resources are just used to provide version numbers for `opam install` + # since we hit a build error when trying to install from tarball directly. + # The result is similar to using `--deps-only` in other formulae. We can't + # run that here as it installs a duplicate copy of `rocq`. + + resource "elpi" do + url "https://raw.githubusercontent.com/LPCIC/elpi/refs/tags/v2.0.7/elpi.opam" + sha256 "25a4d6bafd404d6067bd95227e7bd29de82d887f3789ac80ade7489b995edc1f" + end + + resource "ppx_optcomp" do + url "https://raw.githubusercontent.com/janestreet/ppx_optcomp/refs/tags/v0.17.0/ppx_optcomp.opam" + sha256 "9ddda7e28dabea043a0187acf3d0ff378084e0ef75c9e2003bd0350b83f4dd41" + end + + def install + with_env(OPAMROOT: buildpath/".opam", OPAMYES: "1", OPAMNODEPEXTS: "1", OPAMNOSELFUPGRADE: "1") do + system "opam", "init", "--disable-sandboxing", "--no-setup" + system "opam", "install", "elpi.#{resource("elpi").version}", "ppx_optcomp.v#{resource("ppx_optcomp").version}" + end + + # Move packages needed at runtime into libexec + libexec.install buildpath.glob(".opam/default/*") + inreplace [libexec/"lib/findlib.conf", libexec/"lib/toplevel/topfind"], buildpath/".opam/default", libexec + + # Replace findlib package with formula + inreplace libexec/"lib/toplevel/topfind", libexec/"lib/findlib", Formula["ocaml-findlib"].opt_lib/"ocaml/findlib" + rm_r(libexec/"lib/findlib") + + ENV["OCAMLFIND_CONF"] = libexec/"lib/findlib.conf" + system "make", "dune-files" + system "dune", "build", "-p", name, "@install" + system "dune", "install", name, "--prefix=#{prefix}", + "--libdir=#{lib}/ocaml", + "--mandir=#{man}", + "--docdir=#{doc.parent}" + pkgshare.install "examples/example_data_base.v" + end + + def caveats + <<~CAVEATS + Rocq needs the path to ML files installed inside `#{opt_libexec}/lib`. + This can be done by passing `-I #{opt_libexec}/lib` as an argument. + Alternatively, you can add the directory to OCAMLPATH, e.g. + export OCAMLPATH="#{opt_libexec}/lib:$OCAMLPATH" + or use the included findlib configuration file, e.g. + export OCAMLFIND_CONF="#{opt_libexec}/lib/findlib.conf" + CAVEATS + end + + test do + ENV["OCAMLFIND_CONF"] = libexec/"lib/findlib.conf" + cp pkgshare/"example_data_base.v", testpath + space = " " + assert_equal <<~EOS, shell_output("#{Formula["rocq"].bin}/rocq compile example_data_base.v") + The Db contains [phone_prefix USA 1] + Phone prefix for USA is 1 + The Db contains#{space} + [phone_prefix USA 1, phone_prefix France 33, phone_prefix Italy 39] + Phone prefix for France is 33 + sweet! + brr + yummy! + EOS + end +end From 50e37a1345df7828c80aac53dd148ba2e56a8ebb Mon Sep 17 00:00:00 2001 From: Michael Cho Date: Mon, 24 Mar 2025 23:05:36 -0400 Subject: [PATCH 4/5] coq-hierarchy-builder 1.8.1 (new formula) --- Formula/c/coq-hierarchy-builder.rb | 49 ++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 Formula/c/coq-hierarchy-builder.rb diff --git a/Formula/c/coq-hierarchy-builder.rb b/Formula/c/coq-hierarchy-builder.rb new file mode 100644 index 0000000000000..8d690458deb9e --- /dev/null +++ b/Formula/c/coq-hierarchy-builder.rb @@ -0,0 +1,49 @@ +class CoqHierarchyBuilder < Formula + desc "High level commands to declare a hierarchy based on packed classes" + homepage "https://github.com/math-comp/hierarchy-builder" + url "https://github.com/math-comp/hierarchy-builder/releases/download/v1.8.1/hierarchy-builder-1.8.1.tar.gz" + sha256 "9295185ac7e6c2222951a0706edeeb0de23763939ca033a3956d23c0f6c30fe8" + license "MIT" + + livecheck do + url :stable + regex(/^v?(\d+(?:\.\d+)+)$/i) + end + + depends_on "rocq" + depends_on "rocq-elpi" + + def install + ENV["OCAMLFIND_CONF"] = Formula["rocq-elpi"].libexec/"lib/findlib.conf" + system "make", "build" + system "make", "install", "HB_INSTALLDIR=#{bin}", "COQLIB=#{lib}/ocaml/coq" + end + + test do + (testpath/"test.v").write <<~EOS + From HB Require Import structures. + From Stdlib Require Import ssreflect ZArith. + + HB.mixin Record IsAddComoid A := { + zero : A; + add : A -> A -> A; + addrA : forall x y z, add x (add y z) = add (add x y) z; + addrC : forall x y, add x y = add y x; + add0r : forall x, add zero x = x; + }. + + HB.structure Definition AddComoid := { A of IsAddComoid A }. + + Notation "0" := zero. + Infix "+" := add. + + Check forall (M : AddComoid.type) (x : M), x + x = 0. + EOS + + ENV["OCAMLFIND_CONF"] = Formula["rocq-elpi"].libexec/"lib/findlib.conf" + assert_equal <<~EOS, shell_output("#{Formula["rocq"].bin}/rocq compile test.v") + forall (M : AddComoid.type) (x : M), x + x = 0 + : Prop + EOS + end +end From 5c3f7f53a33af824daed9962976dafe8581a4dc7 Mon Sep 17 00:00:00 2001 From: Michael Cho Date: Mon, 24 Mar 2025 23:36:30 -0400 Subject: [PATCH 5/5] math-comp 2.3.0 --- Formula/m/math-comp.rb | 47 ++++++++++++++++-------------------------- 1 file changed, 18 insertions(+), 29 deletions(-) diff --git a/Formula/m/math-comp.rb b/Formula/m/math-comp.rb index f6f355276d852..d380bc25e52c7 100644 --- a/Formula/m/math-comp.rb +++ b/Formula/m/math-comp.rb @@ -1,10 +1,9 @@ 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/refs/tags/mathcomp-1.19.0.tar.gz" - sha256 "786db902d904347f2108ffceae15ba29037ff8e63a6c58b87928f08671456394" + url "https://github.com/math-comp/math-comp/archive/refs/tags/mathcomp-2.3.0.tar.gz" + sha256 "19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec" license "CECILL-B" - revision 6 head "https://github.com/math-comp/math-comp.git", branch: "master" bottle do @@ -19,37 +18,28 @@ class MathComp < Formula depends_on "ocaml" => :build depends_on "ocaml-findlib" => :build - depends_on "coq" + depends_on "coq-hierarchy-builder" + depends_on "rocq" + depends_on "rocq-elpi" def install - # Work around for https://github.com/Homebrew/homebrew-test-bot/issues/805 - if ENV["HOMEBREW_GITHUB_ACTIONS"] && !(Formula["ocaml-findlib"].etc/"findlib.conf").exist? - ENV["OCAMLFIND_CONF"] = Formula["ocaml-findlib"].opt_libexec/"findlib.conf" - end - - 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"]}" - + ENV["OCAMLFIND_CONF"] = Formula["rocq-elpi"].libexec/"lib/findlib.conf" + + args = [] + if build.stable? + args += %w[-C mathcomp] + (buildpath/"mathcomp/Makefile.coq.local").write "COQLIB=#{lib}/ocaml/coq\n" + elisp.install "mathcomp/ssreflect/pg-ssr.el" + else + (buildpath/"Makefile.coq.local").append_lines "COQLIB=#{lib}/ocaml/coq\n" elisp.install "ssreflect/pg-ssr.el" end - doc.install Dir["docs/*"] + system "make", *args + system "make", *args, "install" end test do - # Work around for https://github.com/Homebrew/homebrew-test-bot/issues/805 - if ENV["HOMEBREW_GITHUB_ACTIONS"] && !(Formula["ocaml-findlib"].etc/"findlib.conf").exist? - ENV["OCAMLFIND_CONF"] = Formula["ocaml-findlib"].opt_libexec/"findlib.conf" - end - (testpath/"testing.v").write <<~EOS From mathcomp Require Import ssreflect seq. @@ -60,8 +50,7 @@ def install 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)) + ENV["OCAMLFIND_CONF"] = Formula["rocq-elpi"].libexec/"lib/findlib.conf" + assert_match(/\Atest\s+: forall/, shell_output("#{Formula["rocq"].bin}/rocq compile testing.v")) end end