Bug 293506
| Summary: | math/coq, math/rocq: Update to 9.1.1 | ||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| Product: | Ports & Packages | Reporter: | Laurent Chardon <laurent.chardon> | ||||||||
| Component: | Individual Port(s) | Assignee: | Laurent Chardon <laurent> | ||||||||
| Status: | New --- | ||||||||||
| Severity: | Affects Only Me | CC: | diizzy, laurent, thierry | ||||||||
| Priority: | --- | ||||||||||
| Version: | Latest | ||||||||||
| Hardware: | Any | ||||||||||
| OS: | Any | ||||||||||
| URL: | https://rocq-prover.org/doc/v9.1/refman/changes.html#changes-in-9-1-1 | ||||||||||
| Bug Depends on: | 286813 | ||||||||||
| Bug Blocks: | |||||||||||
| Attachments: |
|
||||||||||
Should use DISTVERSION and have DISTVERSIONPREFIX before it https://docs.freebsd.org/en/books/porters-handbook/book/#makefile-versions Why is SA_DIR defined? and used before being defined? Stray line, +#OCAML_LDLIBS= ${OCAML_SITELIBDIR}/coq-core Created attachment 268901 [details]
Update math/coq 8.20.1 to math/rocq 9.1.1 with changes from dizzy
(In reply to Daniel Engberg from comment #1) Thanks for the review! I'll add you to the Reviewd by: line. I changed to DISTVERSION and removed the commented line. I’ve kept SA_DIR as-is because it follows the established convention for OCaml ports. There are currently 44 ports using this pattern, and for example devel/ocaml-base does the same. Using SA_DIR before its declaration is safe here since it is only referenced in lazily-evaluated variables (=), not in immediate evaluations (:=). Reordering it would trigger portclippy warnings. Created attachment 268902 [details]
Update math/coq 8.20.1 to math/rocq 9.1.1 + changes from diizzy + fix typo
Fix typo in diizzy's name (sorry!)
I'm seeing this during build, "skipping make_git_revision: git not found" Does it do something funny / stupid if git is available? Other than that, LGTM! (In reply to Daniel Engberg from comment #5) If comes from rocq-9.1.1/dev/tools/make_git_revision.sh and is harmless, whether git is found or not. It's meant to generate git information if inside the development repo of rocq. If not, as in our case, we get either "kipping make_git_revision: git not found" if git is not installed, or "skipping make_git_revision: git dir not found" if it is. |
Created attachment 268423 [details] Update math/coq 8.20.1 to math/rocq 9.1.1 Update coq from 8.20.1 to 9.1.1 Rename coq to rocq to follow upstream name change Take maintainership portlint: OK portclippy: OK poudriere: OK This version of rocq requires an update to devel/ocaml-dune