rocq 9.0.0 (renamed formula) #216253
+192
−55
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -21,6 +21,7 @@ | |
| "cloog018": "cloog", | ||
| "cloudflare-wrangler2": "cloudflare-wrangler", | ||
| "commonmark": "cmark", | ||
| "coq": "rocq", | ||
| "corepack": "node", | ||
| "cppformat": "fmt", | ||
| "crystal-lang": "crystal", | ||
|
|
||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There is now a 2.4.0 release: https://github.com/math-comp/math-comp/releases/tag/mathcomp-2.4.0