Skip to content

Commit 662c232

Browse files
garesgares
authored
Merge pull request #771 from proux01/rocq
Enable compilation without the coq shim on Rocq 9.0
2 parents 8d3f28e + 27b5c88 commit 662c232

File tree

116 files changed

+923
-849
lines changed

Some content is hidden

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

116 files changed

+923
-849
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: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ jobs:
2323
uses: actions/checkout@v3
2424

2525
- name: setup ocaml
26-
uses: avsm/setup-ocaml@v3
26+
uses: ocaml/setup-ocaml@v3
2727
with:
2828
ocaml-compiler: 4.14.2
2929

@@ -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

‎.github/workflows/release.yml‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -41,16 +41,16 @@ jobs:
4141
- name: Create archive
4242
run: |
4343
VERSION="${GITHUB_REF_NAME_SLUG#v}"
44-
git archive -o coq-elpi-$VERSION.tar.gz --prefix=coq-elpi-$VERSION/ $GITHUB_SHA .
44+
git archive -o rocq-elpi-$VERSION.tar.gz --prefix=rocq-elpi-$VERSION/ $GITHUB_SHA .
4545
4646
- name: Release
4747
uses: softprops/action-gh-release@v1
4848
with:
49-
files: coq-elpi-*.tar.gz
49+
files: rocq-elpi-*.tar.gz
5050
fail_on_unmatched_files: true
5151
prerelease: true
5252
generate_release_notes: true
53-
name: Coq-Elpi ${{ github.ref }} for Coq XXX
53+
name: Rocq-Elpi ${{ github.ref }} for Rocq XXX
5454

5555
opam:
5656
runs-on: ubuntu-latest
@@ -63,11 +63,12 @@ jobs:
6363
fetch-tags: 'true'
6464

6565
- name: Use OCaml 4.14.x
66-
uses: avsm/setup-ocaml@v3
66+
uses: ocaml/setup-ocaml@v3
6767
with:
6868
ocaml-compiler: 4.14.x
6969
opam-local-packages: |
7070
!coq-elpi.opam
71+
!rocq-elpi.opam
7172
7273
- name: Write PAT
7374
env:
@@ -93,4 +94,4 @@ jobs:
9394
git tag
9495
TAG=`git tag --sort=-v:refname|head -1`
9596
echo selected tag: $TAG
96-
opam-publish --no-confirmation --tag=$TAG --packages-directory=${OPAM_SUITE:-released}/packages --repo=coq/opam --no-browser -v ${TAG##v} coq-elpi.opam https://github.com/LPCIC/coq-elpi/releases/download/$TAG/coq-elpi-${TAG##v}.tar.gz
97+
opam-publish --no-confirmation --tag=$TAG --packages-directory=${OPAM_SUITE:-released}/packages --repo=coq/opam --no-browser -v ${TAG##v} rocq-elpi.opam coq-elpi.opam https://github.com/LPCIC/coq-elpi/releases/download/$TAG/rocq-elpi-${TAG##v}.tar.gz

‎.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

0 commit comments

Comments
 (0)