Skip to content

Commit 3199032

Browse files
mattam82mattam82
authored
Merge pull request #138 from CertiRocq/port-metarocq-1.5.1
Port to metarocq 1.5.1
2 parents aff6fdf + 90288e2 commit 3199032

37 files changed

+690
-211
lines changed

‎.github/workflows/build.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ jobs:
1818
opam_file:
1919
- 'rocq-certirocq.opam'
2020
image:
21-
- 'mattam82/metacoq:metarocq-1.4.1-rocq-9.1'
21+
- 'mattam82/metacoq:metarocq-1.5.1-rocq-9.1'
2222
fail-fast: false # don't stop jobs if one fails
2323
steps:
2424
- uses: actions/checkout@v3

‎.github/workflows/nix-action-default.yml‎

Lines changed: 96 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ jobs:
22
CertiRocq:
33
needs:
44
- coq
5+
- metarocq
56
runs-on: ubuntu-latest
67
steps:
78
- name: Determine which commit to initially checkout
@@ -31,11 +32,12 @@ jobs:
3132
uses: cachix/install-nix-action@v31
3233
with:
3334
nix_path: nixpkgs=channel:nixpkgs-unstable
34-
- name: Cachix setup coq
35+
- name: Cachix setup metarocq
3536
uses: cachix/cachix-action@v16
3637
with:
37-
extraPullNames: coq-community, math-comp, metarocq
38-
name: coq
38+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
39+
extraPullNames: coq, coq-community, math-comp
40+
name: metarocq
3941
- id: stepGetDerivation
4042
name: Getting derivation for current job (CertiRocq)
4143
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
@@ -109,11 +111,12 @@ jobs:
109111
uses: cachix/install-nix-action@v31
110112
with:
111113
nix_path: nixpkgs=channel:nixpkgs-unstable
112-
- name: Cachix setup coq
114+
- name: Cachix setup metarocq
113115
uses: cachix/cachix-action@v16
114116
with:
115-
extraPullNames: coq-community, math-comp, metarocq
116-
name: coq
117+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
118+
extraPullNames: coq, coq-community, math-comp
119+
name: metarocq
117120
- id: stepGetDerivation
118121
name: Getting derivation for current job (coq)
119122
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
@@ -135,6 +138,89 @@ jobs:
135138
name: Building/fetching current CI target
136139
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
137140
"default" --argstr job "coq"
141+
metarocq:
142+
needs:
143+
- coq
144+
runs-on: ubuntu-latest
145+
steps:
146+
- name: Determine which commit to initially checkout
147+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
148+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
149+
}}\" >> $GITHUB_ENV\nfi\n"
150+
- name: Git checkout
151+
uses: actions/checkout@v6
152+
with:
153+
fetch-depth: 0
154+
ref: ${{ env.target_commit }}
155+
- name: Determine which commit to test
156+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
157+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
158+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
159+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
160+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
161+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
162+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
163+
\ fi\nfi\n"
164+
- name: Git checkout
165+
uses: actions/checkout@v6
166+
with:
167+
fetch-depth: 0
168+
ref: ${{ env.tested_commit }}
169+
- name: Cachix install
170+
uses: cachix/install-nix-action@v31
171+
with:
172+
nix_path: nixpkgs=channel:nixpkgs-unstable
173+
- name: Cachix setup metarocq
174+
uses: cachix/cachix-action@v16
175+
with:
176+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
177+
extraPullNames: coq, coq-community, math-comp
178+
name: metarocq
179+
- id: stepGetDerivation
180+
name: Getting derivation for current job (metarocq)
181+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
182+
\"default\" --argstr job \"metarocq\" \\\n --dry-run 2> err > out || (touch
183+
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
184+
failed\"; exit 1; fi\n"
185+
- id: stepCheck
186+
name: Checking presence of CI target for current job
187+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
188+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
189+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
190+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
191+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
192+
- if: steps.stepCheck.outputs.status != 'fetched'
193+
name: 'Building/fetching previous CI target: coq'
194+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
195+
"default" --argstr job "coq"
196+
- if: steps.stepCheck.outputs.status != 'fetched'
197+
name: 'Building/fetching previous CI target: equations'
198+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
199+
"default" --argstr job "equations"
200+
- if: steps.stepCheck.outputs.status != 'fetched'
201+
name: 'Building/fetching previous CI target: ExtLib'
202+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
203+
"default" --argstr job "ExtLib"
204+
- if: steps.stepCheck.outputs.status != 'fetched'
205+
name: 'Building/fetching previous CI target: metarocq-safechecker-plugin'
206+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
207+
"default" --argstr job "metarocq-safechecker-plugin"
208+
- if: steps.stepCheck.outputs.status != 'fetched'
209+
name: 'Building/fetching previous CI target: metarocq-erasure-plugin'
210+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
211+
"default" --argstr job "metarocq-erasure-plugin"
212+
- if: steps.stepCheck.outputs.status != 'fetched'
213+
name: 'Building/fetching previous CI target: metarocq-translations'
214+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
215+
"default" --argstr job "metarocq-translations"
216+
- if: steps.stepCheck.outputs.status != 'fetched'
217+
name: 'Building/fetching previous CI target: metarocq-quotation'
218+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
219+
"default" --argstr job "metarocq-quotation"
220+
- if: steps.stepCheck.outputs.status != 'fetched'
221+
name: Building/fetching current CI target
222+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
223+
"default" --argstr job "metarocq"
138224
rocq-core:
139225
needs: []
140226
runs-on: ubuntu-latest
@@ -166,11 +252,12 @@ jobs:
166252
uses: cachix/install-nix-action@v31
167253
with:
168254
nix_path: nixpkgs=channel:nixpkgs-unstable
169-
- name: Cachix setup coq
255+
- name: Cachix setup metarocq
170256
uses: cachix/cachix-action@v16
171257
with:
172-
extraPullNames: coq-community, math-comp, metarocq
173-
name: coq
258+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
259+
extraPullNames: coq, coq-community, math-comp
260+
name: metarocq
174261
- id: stepGetDerivation
175262
name: Getting derivation for current job (rocq-core)
176263
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle

‎.nix/config.nix‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,10 @@
2525
compcert.override.version = "3.17";
2626
wasmcert.job = false;
2727
wasmcert.override.version = "v2.2.0";
28-
metarocq.job = false;
29-
metarocq.override.version = "1.4.1-9.1";
28+
ExtLib.job = false;
29+
ExtLib.override.version = "0.13.0";
30+
metarocq.job = true;
31+
metarocq.override.version = "v1.5.1-9.1";
3032
}; rocqPackages = {
3133
rocq-core.override.version = "9.1";
3234
};
@@ -40,4 +42,7 @@
4042
cachix.math-comp = { };
4143
cachix.coq-community = { };
4244
cachix.metarocq = {};
45+
46+
cachix.metarocq.authToken = "CACHIX_AUTH_TOKEN";
47+
4348
}

‎.nix/coq-nix-toolbox.nix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"01dec2f674ed4aa3d7cc00c8fbfb826ea3291658"
1+
"7272a8cc11989ed3a62b3f14930485df28e1c777"

0 commit comments

Comments
 (0)