Skip to content

Commit f6df88c

Browse files
proux01proux01
committed
Enable compilation without the coq shim on Rocq 9.0
1 parent c3593bc commit f6df88c

File tree

115 files changed

+916
-843
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

115 files changed

+916
-843
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ jobs:
2525
- uses: actions/checkout@v3
2626
- uses: coq-community/docker-coq-action@v1
2727
with:
28-
opam_file: 'coq-elpi.opam'
28+
opam_file: 'rocq-elpi.opam'
2929
custom_image: ${{ matrix.image }}
3030
export: 'OPAMWITHTEST OPAMIGNORECONSTRAINTS OPAMVERBOSE' # space-separated list of variables
3131
env:

‎.github/workflows/doc.yml‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,13 +34,15 @@ jobs:
3434
opam repo add coq-dev https://coq.inria.fr/opam/core-dev
3535
opam repo add extra-dev https://coq.inria.fr/opam/extra-dev
3636
opam update
37-
opam install coq-serapi.8.20.0+0.20.0 ./coq-elpi.opam coq-core.8.20.0
37+
opam install coq-serapi.8.20.0+0.20.0 ./rocq-elpi.opam coq-core.8.20.0
3838
sudo apt-get update
3939
sudo apt-get install python3-pip -y
4040
pip3 install git+https://github.com/cpitclaudel/alectryon.git@c8ab1ec
4141
4242
- name: build doc
43-
run: opam exec -- make doc COQ_ELPI_ALREADY_INSTALLED=1
43+
run: |
44+
opam exec -- make dune-files
45+
opam exec -- make doc COQ_ELPI_ALREADY_INSTALLED=1
4446
4547
- name: Save artifact
4648
uses: actions/upload-artifact@v4

‎.github/workflows/nix-action-coq-8.20.yml‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -189,7 +189,6 @@ jobs:
189189
coq-elpi:
190190
needs:
191191
- coq
192-
- stdlib
193192
runs-on: ubuntu-latest
194193
steps:
195194
- name: Determine which commit to initially checkout
@@ -241,10 +240,6 @@ jobs:
241240
name: 'Building/fetching previous CI target: coq'
242241
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
243242
--argstr job "coq"
244-
- if: steps.stepCheck.outputs.status == 'built'
245-
name: 'Building/fetching previous CI target: stdlib'
246-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
247-
--argstr job "stdlib"
248243
- if: steps.stepCheck.outputs.status == 'built'
249244
name: Building/fetching current CI target
250245
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"

‎.github/workflows/nix-action-coq-master.yml‎

Lines changed: 0 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,6 @@ jobs:
118118
coq-elpi:
119119
needs:
120120
- coq
121-
- stdlib
122121
runs-on: ubuntu-latest
123122
steps:
124123
- name: Determine which commit to initially checkout
@@ -170,72 +169,10 @@ jobs:
170169
name: 'Building/fetching previous CI target: coq'
171170
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
172171
--argstr job "coq"
173-
- if: steps.stepCheck.outputs.status == 'built'
174-
name: 'Building/fetching previous CI target: stdlib'
175-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
176-
--argstr job "stdlib"
177172
- if: steps.stepCheck.outputs.status == 'built'
178173
name: Building/fetching current CI target
179174
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
180175
--argstr job "coq-elpi"
181-
coq-elpi-no-stdlib:
182-
needs:
183-
- coq
184-
runs-on: ubuntu-latest
185-
steps:
186-
- name: Determine which commit to initially checkout
187-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
188-
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
189-
}}\" >> $GITHUB_ENV\nfi\n"
190-
- name: Git checkout
191-
uses: actions/checkout@v4
192-
with:
193-
fetch-depth: 0
194-
ref: ${{ env.target_commit }}
195-
- name: Determine which commit to test
196-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
197-
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
198-
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
199-
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
200-
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
201-
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
202-
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
203-
\ fi\nfi\n"
204-
- name: Git checkout
205-
uses: actions/checkout@v4
206-
with:
207-
fetch-depth: 0
208-
ref: ${{ env.tested_commit }}
209-
- name: Cachix install
210-
uses: cachix/install-nix-action@v30
211-
with:
212-
nix_path: nixpkgs=channel:nixpkgs-unstable
213-
- name: Cachix setup coq-elpi
214-
uses: cachix/cachix-action@v15
215-
with:
216-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
217-
extraPullNames: coq, coq-community, math-comp
218-
name: coq-elpi
219-
- id: stepGetDerivation
220-
name: Getting derivation for current job (coq-elpi-no-stdlib)
221-
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
222-
\"coq-master\" --argstr job \"coq-elpi-no-stdlib\" \\\n --dry-run 2> err
223-
> out || (touch fail; true)\n"
224-
- name: Error reporting
225-
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
226-
- name: Failure check
227-
run: if [ -e fail ]; then exit 1; else exit 0; fi;
228-
- id: stepCheck
229-
name: Checking presence of CI target for current job
230-
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
231-
- if: steps.stepCheck.outputs.status == 'built'
232-
name: 'Building/fetching previous CI target: coq'
233-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
234-
--argstr job "coq"
235-
- if: steps.stepCheck.outputs.status == 'built'
236-
name: Building/fetching current CI target
237-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
238-
--argstr job "coq-elpi-no-stdlib"
239176
coq-elpi-tests:
240177
needs:
241178
- coq

‎.github/workflows/nix-action-rocq-9.0.yml‎

Lines changed: 0 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -189,7 +189,6 @@ jobs:
189189
coq-elpi:
190190
needs:
191191
- coq
192-
- stdlib
193192
runs-on: ubuntu-latest
194193
steps:
195194
- name: Determine which commit to initially checkout
@@ -241,72 +240,10 @@ jobs:
241240
name: 'Building/fetching previous CI target: coq'
242241
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
243242
--argstr job "coq"
244-
- if: steps.stepCheck.outputs.status == 'built'
245-
name: 'Building/fetching previous CI target: stdlib'
246-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
247-
--argstr job "stdlib"
248243
- if: steps.stepCheck.outputs.status == 'built'
249244
name: Building/fetching current CI target
250245
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
251246
--argstr job "coq-elpi"
252-
coq-elpi-no-stdlib:
253-
needs:
254-
- coq
255-
runs-on: ubuntu-latest
256-
steps:
257-
- name: Determine which commit to initially checkout
258-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
259-
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
260-
}}\" >> $GITHUB_ENV\nfi\n"
261-
- name: Git checkout
262-
uses: actions/checkout@v4
263-
with:
264-
fetch-depth: 0
265-
ref: ${{ env.target_commit }}
266-
- name: Determine which commit to test
267-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
268-
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
269-
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
270-
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
271-
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
272-
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
273-
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
274-
\ fi\nfi\n"
275-
- name: Git checkout
276-
uses: actions/checkout@v4
277-
with:
278-
fetch-depth: 0
279-
ref: ${{ env.tested_commit }}
280-
- name: Cachix install
281-
uses: cachix/install-nix-action@v30
282-
with:
283-
nix_path: nixpkgs=channel:nixpkgs-unstable
284-
- name: Cachix setup coq-elpi
285-
uses: cachix/cachix-action@v15
286-
with:
287-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
288-
extraPullNames: coq, coq-community, math-comp
289-
name: coq-elpi
290-
- id: stepGetDerivation
291-
name: Getting derivation for current job (coq-elpi-no-stdlib)
292-
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
293-
\"rocq-9.0\" --argstr job \"coq-elpi-no-stdlib\" \\\n --dry-run 2> err >
294-
out || (touch fail; true)\n"
295-
- name: Error reporting
296-
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
297-
- name: Failure check
298-
run: if [ -e fail ]; then exit 1; else exit 0; fi;
299-
- id: stepCheck
300-
name: Checking presence of CI target for current job
301-
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
302-
- if: steps.stepCheck.outputs.status == 'built'
303-
name: 'Building/fetching previous CI target: coq'
304-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
305-
--argstr job "coq"
306-
- if: steps.stepCheck.outputs.status == 'built'
307-
name: Building/fetching current CI target
308-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
309-
--argstr job "coq-elpi-no-stdlib"
310247
coq-elpi-tests:
311248
needs:
312249
- coq

‎.gitignore‎

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -27,10 +27,10 @@ etc/__pycache__/
2727

2828
/.deps.elpi
2929

30-
src/coq_elpi_config.ml
31-
src/coq_elpi_vernacular_syntax.ml
32-
src/coq_elpi_arg_syntax.ml
33-
src/coq_elpi_builtins_HOAS.ml
30+
src/rocq_elpi_config.ml
31+
src/rocq_elpi_vernacular_syntax.ml
32+
src/rocq_elpi_arg_syntax.ml
33+
src/rocq_elpi_builtins_HOAS.ml
3434
doc/
3535

3636
Makefile.coq
@@ -45,16 +45,17 @@ META
4545

4646
*.cache
4747

48-
apps/coercion/src/coq_elpi_coercion_hook.ml
48+
apps/coercion/src/rocq_elpi_coercion_hook.ml
4949
.filestoinstall
50-
apps/tc/src/coq_elpi_tc_hook.ml
51-
apps/cs/src/coq_elpi_cs_hook.ml
50+
apps/tc/src/rocq_elpi_tc_hook.ml
51+
apps/cs/src/rocq_elpi_cs_hook.ml
5252

5353
*.timing
5454
_build
5555
tmp.out
56-
coq-elpi-tests.opam
57-
coq-elpi-tests.install
56+
rocq-elpi-tests.opam
57+
rocq-elpi-tests.install
58+
rocq-elpi.install
5859
coq-elpi.install
5960

60-
theories-stdlib/dune
61+
theories-stdlib/dune

‎.nix/config.nix‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ let master = [
1414
common-bundles = listToAttrs (forEach master (p:
1515
{ name = p; value.override.version = "master"; }))
1616
// {
17-
coq-elpi-no-stdlib.job = true;
1817
coq-elpi-tests.job = true;
1918
stdlib.job = true;
2019
coq-elpi-tests-stdlib.job = true;
@@ -35,7 +34,6 @@ let master = [
3534
"coq-8.20".coqPackages = common-bundles // {
3635
coq.override.version = "8.20";
3736
coq-elpi.override.elpi-version = "2.0.7";
38-
coq-elpi-no-stdlib.job = false;
3937
coq-elpi-tests-stdlib.job = false;
4038
};
4139

‎.nix/coq-overlays/coq-elpi-no-stdlib/default.nix‎

Lines changed: 0 additions & 11 deletions
This file was deleted.

‎.nix/coq-overlays/coq-elpi-tests-stdlib/default.nix‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,9 @@ coqPackages.lib.overrideCoqDerivation {
44

55
pname = "coq-elpi-tests-stdlib";
66

7+
propagatedBuildInputs = coq-elpi.propagatedBuildInputs
8+
++ [ coqPackages.stdlib ];
9+
710
buildPhase = ''
811
make test-stdlib
912
make examples-stdlib

‎.nix/coq-overlays/coq-elpi-tests/default.nix‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,6 @@ coqPackages.lib.overrideCoqDerivation {
44

55
pname = "coq-elpi-tests";
66

7-
propagatedBuildInputs =
8-
lib.filter (d: d?pname && d.pname != "stdlib")
9-
coq-elpi.propagatedBuildInputs;
10-
117
buildPhase = ''
128
make test-core
139
make examples

0 commit comments

Comments
 (0)