Skip to content
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

Enable compilation without the coq shim on Rocq 9.0 #771

Merged
merged 3 commits into from
Feb 16, 2025
Merged

Enable compilation without the coq shim on Rocq 9.0 #771

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c3593bc
[CI] Update setup-ocaml action
proux01 Feb 11, 2025
f6df88c
Enable compilation without the coq shim on Rocq 9.0
proux01 Feb 7, 2025
27b5c88
Update release.yml
gares Feb 11, 2025
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: 1 addition & 1 deletion .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ jobs:
- uses: actions/checkout@v3
- uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-elpi.opam'
opam_file: 'rocq-elpi.opam'
custom_image: ${{ matrix.image }}
export: 'OPAMWITHTEST OPAMIGNORECONSTRAINTS OPAMVERBOSE' # space-separated list of variables
env:
Expand Down
8 changes: 5 additions & 3 deletions .github/workflows/doc.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ jobs:
uses: actions/checkout@v3

- name: setup ocaml
uses: avsm/setup-ocaml@v3
uses: ocaml/setup-ocaml@v3
with:
ocaml-compiler: 4.14.2

Expand All @@ -34,13 +34,15 @@ jobs:
opam repo add coq-dev https://coq.inria.fr/opam/core-dev
opam repo add extra-dev https://coq.inria.fr/opam/extra-dev
opam update
opam install coq-serapi.8.20.0+0.20.0 ./coq-elpi.opam coq-core.8.20.0
opam install coq-serapi.8.20.0+0.20.0 ./rocq-elpi.opam coq-core.8.20.0
sudo apt-get update
sudo apt-get install python3-pip -y
pip3 install git+https://github.com/cpitclaudel/alectryon.git@c8ab1ec

- name: build doc
run: opam exec -- make doc COQ_ELPI_ALREADY_INSTALLED=1
run: |
opam exec -- make dune-files
opam exec -- make doc COQ_ELPI_ALREADY_INSTALLED=1

- name: Save artifact
uses: actions/upload-artifact@v4
Expand Down
5 changes: 0 additions & 5 deletions .github/workflows/nix-action-coq-8.20.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -189,7 +189,6 @@ jobs:
coq-elpi:
needs:
- coq
- stdlib
runs-on: ubuntu-latest
steps:
- name: Determine which commit to initially checkout
Expand Down Expand Up @@ -241,10 +240,6 @@ jobs:
name: 'Building/fetching previous CI target: coq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
--argstr job "coq"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: stdlib'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
--argstr job "stdlib"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
Expand Down
63 changes: 0 additions & 63 deletions .github/workflows/nix-action-coq-master.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,7 +118,6 @@ jobs:
coq-elpi:
needs:
- coq
- stdlib
runs-on: ubuntu-latest
steps:
- name: Determine which commit to initially checkout
Expand Down Expand Up @@ -170,72 +169,10 @@ jobs:
name: 'Building/fetching previous CI target: coq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
--argstr job "coq"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: stdlib'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
--argstr job "stdlib"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
--argstr job "coq-elpi"
coq-elpi-no-stdlib:
needs:
- coq
runs-on: ubuntu-latest
steps:
- name: Determine which commit to initially checkout
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
}}\" >> $GITHUB_ENV\nfi\n"
- name: Git checkout
uses: actions/checkout@v4
with:
fetch-depth: 0
ref: ${{ env.target_commit }}
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
\ fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v4
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v30
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup coq-elpi
uses: cachix/cachix-action@v15
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community, math-comp
name: coq-elpi
- id: stepGetDerivation
name: Getting derivation for current job (coq-elpi-no-stdlib)
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
\"coq-master\" --argstr job \"coq-elpi-no-stdlib\" \\\n --dry-run 2> err
> out || (touch fail; true)\n"
- name: Error reporting
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
- name: Failure check
run: if [ -e fail ]; then exit 1; else exit 0; fi;
- id: stepCheck
name: Checking presence of CI target for current job
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: coq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
--argstr job "coq"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
--argstr job "coq-elpi-no-stdlib"
coq-elpi-tests:
needs:
- coq
Expand Down
63 changes: 0 additions & 63 deletions .github/workflows/nix-action-rocq-9.0.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -189,7 +189,6 @@ jobs:
coq-elpi:
needs:
- coq
- stdlib
runs-on: ubuntu-latest
steps:
- name: Determine which commit to initially checkout
Expand Down Expand Up @@ -241,72 +240,10 @@ jobs:
name: 'Building/fetching previous CI target: coq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
--argstr job "coq"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: stdlib'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
--argstr job "stdlib"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
--argstr job "coq-elpi"
coq-elpi-no-stdlib:
needs:
- coq
runs-on: ubuntu-latest
steps:
- name: Determine which commit to initially checkout
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
}}\" >> $GITHUB_ENV\nfi\n"
- name: Git checkout
uses: actions/checkout@v4
with:
fetch-depth: 0
ref: ${{ env.target_commit }}
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
\ fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v4
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v30
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup coq-elpi
uses: cachix/cachix-action@v15
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community, math-comp
name: coq-elpi
- id: stepGetDerivation
name: Getting derivation for current job (coq-elpi-no-stdlib)
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
\"rocq-9.0\" --argstr job \"coq-elpi-no-stdlib\" \\\n --dry-run 2> err >
out || (touch fail; true)\n"
- name: Error reporting
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
- name: Failure check
run: if [ -e fail ]; then exit 1; else exit 0; fi;
- id: stepCheck
name: Checking presence of CI target for current job
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: coq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
--argstr job "coq"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
--argstr job "coq-elpi-no-stdlib"
coq-elpi-tests:
needs:
- coq
Expand Down
11 changes: 6 additions & 5 deletions .github/workflows/release.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,16 +41,16 @@ jobs:
- name: Create archive
run: |
VERSION="${GITHUB_REF_NAME_SLUG#v}"
git archive -o coq-elpi-$VERSION.tar.gz --prefix=coq-elpi-$VERSION/ $GITHUB_SHA .
git archive -o rocq-elpi-$VERSION.tar.gz --prefix=rocq-elpi-$VERSION/ $GITHUB_SHA .

- name: Release
uses: softprops/action-gh-release@v1
with:
files: coq-elpi-*.tar.gz
files: rocq-elpi-*.tar.gz
fail_on_unmatched_files: true
prerelease: true
generate_release_notes: true
name: Coq-Elpi ${{ github.ref }} for Coq XXX
name: Rocq-Elpi ${{ github.ref }} for Rocq XXX

opam:
runs-on: ubuntu-latest
Expand All @@ -63,11 +63,12 @@ jobs:
fetch-tags: 'true'

- name: Use OCaml 4.14.x
uses: avsm/setup-ocaml@v3
uses: ocaml/setup-ocaml@v3
with:
ocaml-compiler: 4.14.x
opam-local-packages: |
!coq-elpi.opam
!rocq-elpi.opam

- name: Write PAT
env:
Expand All @@ -93,4 +94,4 @@ jobs:
git tag
TAG=`git tag --sort=-v:refname|head -1`
echo selected tag: $TAG
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
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
21 changes: 11 additions & 10 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,10 +27,10 @@ etc/__pycache__/

/.deps.elpi

src/coq_elpi_config.ml
src/coq_elpi_vernacular_syntax.ml
src/coq_elpi_arg_syntax.ml
src/coq_elpi_builtins_HOAS.ml
src/rocq_elpi_config.ml
src/rocq_elpi_vernacular_syntax.ml
src/rocq_elpi_arg_syntax.ml
src/rocq_elpi_builtins_HOAS.ml
doc/

Makefile.coq
Expand All @@ -45,16 +45,17 @@ META

*.cache

apps/coercion/src/coq_elpi_coercion_hook.ml
apps/coercion/src/rocq_elpi_coercion_hook.ml
.filestoinstall
apps/tc/src/coq_elpi_tc_hook.ml
apps/cs/src/coq_elpi_cs_hook.ml
apps/tc/src/rocq_elpi_tc_hook.ml
apps/cs/src/rocq_elpi_cs_hook.ml

*.timing
_build
tmp.out
coq-elpi-tests.opam
coq-elpi-tests.install
rocq-elpi-tests.opam
rocq-elpi-tests.install
rocq-elpi.install
coq-elpi.install

theories-stdlib/dune
theories-stdlib/dune
2 changes: 0 additions & 2 deletions .nix/config.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,6 @@ let master = [
common-bundles = listToAttrs (forEach master (p:
{ name = p; value.override.version = "master"; }))
// {
coq-elpi-no-stdlib.job = true;
coq-elpi-tests.job = true;
stdlib.job = true;
coq-elpi-tests-stdlib.job = true;
Expand All @@ -35,7 +34,6 @@ let master = [
"coq-8.20".coqPackages = common-bundles // {
coq.override.version = "8.20";
coq-elpi.override.elpi-version = "2.0.7";
coq-elpi-no-stdlib.job = false;
coq-elpi-tests-stdlib.job = false;
};

Expand Down
11 changes: 0 additions & 11 deletions .nix/coq-overlays/coq-elpi-no-stdlib/default.nix
View file
Open in desktop

This file was deleted.

3 changes: 3 additions & 0 deletions .nix/coq-overlays/coq-elpi-tests-stdlib/default.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,9 @@ coqPackages.lib.overrideCoqDerivation {

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

propagatedBuildInputs = coq-elpi.propagatedBuildInputs
++ [ coqPackages.stdlib ];

buildPhase = ''
make test-stdlib
make examples-stdlib
Expand Down
4 changes: 0 additions & 4 deletions .nix/coq-overlays/coq-elpi-tests/default.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,6 @@ coqPackages.lib.overrideCoqDerivation {

pname = "coq-elpi-tests";

propagatedBuildInputs =
lib.filter (d: d?pname && d.pname != "stdlib")
coq-elpi.propagatedBuildInputs;

buildPhase = ''
make test-core
make examples
Expand Down
Loading
Loading