Skip to content

Update meta.yml and require Rocq 9.0 #124

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
pi8027 merged 1 commit into from
Mar 25, 2026
Merged

Update meta.yml and require Rocq 9.0 #124

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions .github/workflows/docker-action.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,8 @@ jobs:
strategy:
matrix:
image:
- 'mathcomp/mathcomp:2.4.0-coq-8.20'
- 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
- 'mathcomp/mathcomp:2.4.0-rocq-prover-9.1'
- 'mathcomp/mathcomp:2.5.0-coq-8.20'
- 'mathcomp/mathcomp:2.5.0-rocq-prover-9.0'
- 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1'
- 'mathcomp/mathcomp-dev:rocq-prover-9.0'
Expand Down
4 changes: 1 addition & 3 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,10 @@ KNOWNTARGETS := Makefile.coq
# on them always get rebuilt
KNOWNFILES := Makefile _CoqProject

COQMAKEFILE?=$(shell command -v coq_makefile || echo "$(COQBIN)rocq makefile")

.DEFAULT_GOAL := invoke-coqmakefile

Makefile.coq: Makefile _CoqProject
$(COQMAKEFILE) -f _CoqProject -o Makefile.coq
$(COQBIN)rocq makefile -f _CoqProject -o Makefile.coq

invoke-coqmakefile: Makefile.coq
$(MAKE) --no-print-directory -f Makefile.coq $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
Expand Down
4 changes: 2 additions & 2 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ coefficients range over commutative rings and integral domains.
- Author(s):
- Pierre-Yves Strub (initial)
- License: [CeCILL-B Free Software License Agreement](CeCILL-B)
- Compatible Rocq/Coq versions: 8.20 or later
- Compatible Rocq/Coq versions: 9.0 or later
- Additional dependencies:
- [MathComp](https://math-comp.github.io) ssreflect 2.4 or later
- [MathComp](https://math-comp.github.io) algebra
Expand All @@ -37,7 +37,7 @@ is via [OPAM](https://opam.ocaml.org/doc/Install.html):

```shell
opam repo add rocq-released https://rocq-prover.org/opam/released
opam install coq-mathcomp-multinomials
opam install rocq-mathcomp-multinomials
```

To instead build and install manually, you need to make sure that all the
Expand Down
3 changes: 0 additions & 3 deletions coq-mathcomp-multinomials.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,3 @@
# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"
maintainer: "pierre-yves@strub.nu"
version: "dev"
Expand Down
14 changes: 5 additions & 9 deletions meta.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
---
fullname: A Multivariate polynomial Library for the Mathematical Components Library
shortname: multinomials
opam_name: coq-mathcomp-multinomials
opam_name: rocq-mathcomp-multinomials
organization: math-comp
action: true

Expand All @@ -25,20 +25,16 @@ license:
file: CeCILL-B

supported_coq_versions:
text: 8.20 or later
opam: '{>= "8.20"}'
text: 9.0 or later
opam: '{>= "9.0"}'

tested_coq_nix_versions:

tested_coq_opam_versions:
- version: '2.4.0-coq-8.20'
repo: 'mathcomp/mathcomp'
- version: '2.4.0-rocq-prover-9.0'
repo: 'mathcomp/mathcomp'
- version: '2.4.0-rocq-prover-9.1'
repo: 'mathcomp/mathcomp'
- version: '2.5.0-coq-8.20'
repo: 'mathcomp/mathcomp'
- version: '2.5.0-rocq-prover-9.0'
repo: 'mathcomp/mathcomp'
- version: '2.5.0-rocq-prover-9.1'
Expand All @@ -52,12 +48,12 @@ tested_coq_opam_versions:

dependencies:
- opam:
name: coq-mathcomp-ssreflect
name: rocq-mathcomp-ssreflect
version: '{>= "2.4"}'
description: |-
[MathComp](https://math-comp.github.io) ssreflect 2.4 or later
- opam:
name: coq-mathcomp-algebra
name: rocq-mathcomp-algebra
description: |-
[MathComp](https://math-comp.github.io) algebra
- opam:
Expand Down
10 changes: 6 additions & 4 deletions rocq-mathcomp-multinomials.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"
maintainer: "pierre-yves@strub.nu"
version: "dev"
Expand All @@ -16,10 +19,9 @@ coefficients range over commutative rings and integral domains."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
("coq" {>= "8.20" & < "8.21~"}
| "rocq-core" {>= "9.0"})
"coq-mathcomp-ssreflect" {>= "2.4"}
"coq-mathcomp-algebra"
"rocq-core" {>= "9.0"}
Copy link
Copy Markdown
Member Author

@pi8027 pi8027 Mar 24, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Apparently, the Rocq-community templates don't let us replace coq with rocq-core here yet.

Copy link
Copy Markdown
Member Author

@pi8027 pi8027 Mar 24, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Related issue: rocq-community/templates#142

"rocq-mathcomp-ssreflect" {>= "2.4"}
"rocq-mathcomp-algebra"
"coq-mathcomp-bigenough"
"coq-mathcomp-finmap"
]
Expand Down
Loading