Skip to content

Support for Rocq 9.2 #40

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
RalfJung merged 16 commits into from
Aug 7, 2026
Merged

Support for Rocq 9.2 #40

Show file tree
Hide file tree
Changes from 12 commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
671623d
update dependencies
skylee03 Jul 16, 2026
b17ed11
recover support for coq
skylee03 Aug 6, 2026
6d3ac0f
add version restrictions for rocq-prover and rocq-runtime
skylee03 Aug 6, 2026
53628dc
require rocq-core instead
skylee03 Aug 6, 2026
9a38ddb
require rocq-stdlib
skylee03 Aug 6, 2026
58ea8fa
add coq-core to support coq_makefile
skylee03 Aug 6, 2026
0af2756
remove max version
skylee03 Aug 6, 2026
3302586
remove coq dependency
skylee03 Aug 6, 2026
1dc9d4d
replace legacy Coq commands with Rocq commands
skylee03 Aug 6, 2026
f0bea7e
remove coq-core
skylee03 Aug 6, 2026
73c1aaa
update CI dependencies
skylee03 Aug 6, 2026
7213df7
update CI mathcomp images
skylee03 Aug 6, 2026
a101935
apply template
skylee03 Aug 6, 2026
36df460
replace legacy Coq dependencies manually
skylee03 Aug 6, 2026
a7e5fdb
update CI scripts manually
skylee03 Aug 6, 2026
f6d7a8f
remove instructions to install dependencies (rocq-community/templates…
skylee03 Aug 7, 2026
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
14 changes: 4 additions & 10 deletions .github/workflows/docker-action.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,16 +17,10 @@ jobs:
strategy:
matrix:
image:
- 'mathcomp/mathcomp-dev:coq-dev'
- 'mathcomp/mathcomp:2.2.0-coq-8.19'
- 'mathcomp/mathcomp:2.1.0-coq-8.18'
- 'mathcomp/mathcomp:2.0.0-coq-8.17'
- 'mathcomp/mathcomp:1.17.0-coq-8.17'
- 'mathcomp/mathcomp:1.16.0-coq-8.17'
- 'mathcomp/mathcomp:1.15.0-coq-8.16'
- 'mathcomp/mathcomp:1.14.0-coq-8.15'
- 'mathcomp/mathcomp:1.13.0-coq-8.15'
- 'mathcomp/mathcomp:1.12.0-coq-8.14'
- 'mathcomp/mathcomp-dev:rocq-prover-dev'
- 'mathcomp/mathcomp:2.6.0-rocq-prover-9.2'
- 'mathcomp/mathcomp:2.6.0-rocq-prover-9.1'
- 'mathcomp/mathcomp:2.6.0-rocq-prover-9.0'
fail-fast: false
steps:
- uses: actions/checkout@v3
Expand Down
2 changes: 1 addition & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ dist:

doc: clean-doc manual.pdf
- mkdir -p $(DOC)
coqdoc $(COQDOCFLAGS) -R theories Autosubst -R examples/plain Plain \
rocq doc $(COQDOCFLAGS) -R theories Autosubst -R examples/plain Plain \
-R examples/ssr Ssr $(THEORIES) $(EXAMPLES_PLAIN) $(EXAMPLES_SSR)
cp $(EXTRA_DIR)resources/* $(DOC)
cp manual.pdf $(DOC)
Expand Down
5 changes: 3 additions & 2 deletions coq-autosubst-ci.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ synopsis: "Autosubst (CI only)"

build: [make "-j%{jobs}%" "all"]
depends: [
"coq"
"coq-mathcomp-ssreflect"
"rocq-core"
"rocq-stdlib"
"rocq-mathcomp-ssreflect"
]
3 changes: 2 additions & 1 deletion coq-autosubst.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,8 @@ substitutions."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {(>= "8.14" & < "8.21~") | (= "dev")}
"rocq-core"
"rocq-stdlib"
]
Comment thread
skylee03 marked this conversation as resolved.

tags: [
Expand Down
2 changes: 1 addition & 1 deletion examples/plain/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ all: $(COQMAKEFILE)
+$(MAKE) -f $(COQMAKEFILE) all

$(COQMAKEFILE): Makefile $(VS)
coq_makefile -R $(LIB) Autosubst -R . Plain $(VS) -o $(COQMAKEFILE)
rocq makefile -R $(LIB) Autosubst -R . Plain $(VS) -o $(COQMAKEFILE)

clean: $(COQMAKEFILE)
-$(COQMAKE) clean
Expand Down
2 changes: 1 addition & 1 deletion examples/ssr/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ all: $(COQMAKEFILE)
+$(MAKE) -f $(COQMAKEFILE) all

$(COQMAKEFILE): Makefile $(VS)
coq_makefile -R $(LIB) Autosubst $(VS) -R . Ssr -o $(COQMAKEFILE)
rocq makefile -R $(LIB) Autosubst $(VS) -R . Ssr -o $(COQMAKEFILE)

clean: $(COQMAKEFILE)
-$(COQMAKE) clean
Expand Down
20 changes: 4 additions & 16 deletions meta.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,25 +50,13 @@ supported_coq_versions:
opam: '{(>= "8.14" & < "8.21~") | (= "dev")}'
Comment thread
skylee03 marked this conversation as resolved.
Outdated

tested_coq_opam_versions:
- version: 'coq-dev'
- version: 'rocq-prover-dev'
repo: 'mathcomp/mathcomp-dev'
- version: '2.2.0-coq-8.19'
- version: '2.6.0-rocq-prover-9.2'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.18'
- version: '2.6.0-rocq-prover-9.1'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '1.17.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '1.16.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '1.15.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '1.14.0-coq-8.15'
repo: 'mathcomp/mathcomp'
- version: '1.13.0-coq-8.15'
repo: 'mathcomp/mathcomp'
- version: '1.12.0-coq-8.14'
- version: '2.6.0-rocq-prover-9.0'
repo: 'mathcomp/mathcomp'

namespace: Autosubst
Expand Down
2 changes: 1 addition & 1 deletion theories/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ all: $(COQMAKEFILE)
+$(MAKE) -f $(COQMAKEFILE) all

$(COQMAKEFILE): Makefile $(VS)
coq_makefile -R $(LIB) Autosubst $(VS) -o $(COQMAKEFILE)
rocq makefile -R $(LIB) Autosubst $(VS) -o $(COQMAKEFILE)

install: $(COQMAKEFILE)
$(COQMAKE) install
Expand Down
Loading