Skip to content

Commit a1fa355

Browse files
4ever24ever2
authored
[8.20] Bump MetaCoq version (#260)
2 parents 606294e + 9c5a251 commit a1fa355

File tree

5 files changed

+38
-55
lines changed

5 files changed

+38
-55
lines changed

‎.github/coq-concert.opam.locked‎

Lines changed: 7 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -12,26 +12,19 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
1212
depends: [
1313
"coq" {= "8.20.0"}
1414
"coq-bignums" {= "9.0.0+coq8.20"}
15-
"coq-metacoq-common" {= "1.3.2+8.20"}
16-
"coq-metacoq-erasure" {= "1.3.2+8.20"}
17-
"coq-metacoq-pcuic" {= "1.3.2+8.20"}
18-
"coq-metacoq-safechecker" {= "1.3.2+8.20"}
19-
"coq-metacoq-template" {= "1.3.2+8.20"}
20-
"coq-metacoq-template-pcuic" {= "1.3.2+8.20"}
21-
"coq-metacoq-utils" {= "1.3.2+8.20"}
15+
"coq-metacoq-common" {= "1.3.4+8.20"}
16+
"coq-metacoq-erasure" {= "1.3.4+8.20"}
17+
"coq-metacoq-pcuic" {= "1.3.4+8.20"}
18+
"coq-metacoq-safechecker" {= "1.3.4+8.20"}
19+
"coq-metacoq-template" {= "1.3.4+8.20"}
20+
"coq-metacoq-template-pcuic" {= "1.3.4+8.20"}
21+
"coq-metacoq-utils" {= "1.3.4+8.20"}
2222
"coq-rust-extraction" {= "dev"}
2323
"coq-elm-extraction" {= "0.1.0"}
2424
"coq-quickchick" {= "2.0.4"}
2525
"coq-stdpp" {= "1.11.0"}
2626
]
2727
pin-depends: [
28-
["coq-metacoq-utils.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
29-
["coq-metacoq-common.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
30-
["coq-metacoq-template.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
31-
["coq-metacoq-template-pcuic.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
32-
["coq-metacoq-pcuic.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
33-
["coq-metacoq-safechecker.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
34-
["coq-metacoq-erasure.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
3528
["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#c5d9cbae417213fe25b42f08678f28507cc6b99e"]
3629
]
3730
build: [

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

Lines changed: 21 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -45,15 +45,15 @@ jobs:
4545
- id: stepGetDerivation
4646
name: Getting derivation for current job (ConCert)
4747
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
48-
\"8.20\" --argstr job \"ConCert\" \\\n --dry-run &> out || (touch
48+
\"8.20\" --argstr job \"ConCert\" \\\n --dry-run 2> err > out || (touch
4949
fail; true)\n"
5050
- name: Error reporting
51-
run: "echo \"out=\"; cat out\n"
51+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
5252
- name: Failure check
5353
run: if [ -e fail ]; then exit 1; else exit 0; fi;
5454
- id: stepCheck
5555
name: Checking presence of CI target for current job
56-
run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
56+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
5757
- if: steps.stepCheck.outputs.status == 'built'
5858
name: 'Building/fetching previous CI target: coq'
5959
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -128,15 +128,15 @@ jobs:
128128
- id: stepGetDerivation
129129
name: Getting derivation for current job (ElmExtraction)
130130
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
131-
\"8.20\" --argstr job \"ElmExtraction\" \\\n --dry-run &> out || (touch
131+
\"8.20\" --argstr job \"ElmExtraction\" \\\n --dry-run 2> err > out || (touch
132132
fail; true)\n"
133133
- name: Error reporting
134-
run: "echo \"out=\"; cat out\n"
134+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
135135
- name: Failure check
136136
run: if [ -e fail ]; then exit 1; else exit 0; fi;
137137
- id: stepCheck
138138
name: Checking presence of CI target for current job
139-
run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
139+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
140140
- if: steps.stepCheck.outputs.status == 'built'
141141
name: 'Building/fetching previous CI target: coq'
142142
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -190,15 +190,15 @@ jobs:
190190
- id: stepGetDerivation
191191
name: Getting derivation for current job (QuickChick)
192192
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
193-
\"8.20\" --argstr job \"QuickChick\" \\\n --dry-run &> out || (touch
193+
\"8.20\" --argstr job \"QuickChick\" \\\n --dry-run 2> err > out || (touch
194194
fail; true)\n"
195195
- name: Error reporting
196-
run: "echo \"out=\"; cat out\n"
196+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
197197
- name: Failure check
198198
run: if [ -e fail ]; then exit 1; else exit 0; fi;
199199
- id: stepCheck
200200
name: Checking presence of CI target for current job
201-
run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
201+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
202202
- if: steps.stepCheck.outputs.status == 'built'
203203
name: 'Building/fetching previous CI target: coq'
204204
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -261,15 +261,15 @@ jobs:
261261
- id: stepGetDerivation
262262
name: Getting derivation for current job (RustExtraction)
263263
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
264-
\"8.20\" --argstr job \"RustExtraction\" \\\n --dry-run &> out ||
264+
\"8.20\" --argstr job \"RustExtraction\" \\\n --dry-run 2> err > out ||
265265
(touch fail; true)\n"
266266
- name: Error reporting
267-
run: "echo \"out=\"; cat out\n"
267+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
268268
- name: Failure check
269269
run: if [ -e fail ]; then exit 1; else exit 0; fi;
270270
- id: stepCheck
271271
name: Checking presence of CI target for current job
272-
run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
272+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
273273
- if: steps.stepCheck.outputs.status == 'built'
274274
name: 'Building/fetching previous CI target: coq'
275275
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -322,15 +322,15 @@ jobs:
322322
- id: stepGetDerivation
323323
name: Getting derivation for current job (coq)
324324
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
325-
\"8.20\" --argstr job \"coq\" \\\n --dry-run &> out || (touch fail;
325+
\"8.20\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail;
326326
true)\n"
327327
- name: Error reporting
328-
run: "echo \"out=\"; cat out\n"
328+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
329329
- name: Failure check
330330
run: if [ -e fail ]; then exit 1; else exit 0; fi;
331331
- id: stepCheck
332332
name: Checking presence of CI target for current job
333-
run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
333+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
334334
- if: steps.stepCheck.outputs.status == 'built'
335335
name: Building/fetching current CI target
336336
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -376,15 +376,15 @@ jobs:
376376
- id: stepGetDerivation
377377
name: Getting derivation for current job (metacoq)
378378
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
379-
\"8.20\" --argstr job \"metacoq\" \\\n --dry-run &> out || (touch
379+
\"8.20\" --argstr job \"metacoq\" \\\n --dry-run 2> err > out || (touch
380380
fail; true)\n"
381381
- name: Error reporting
382-
run: "echo \"out=\"; cat out\n"
382+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
383383
- name: Failure check
384384
run: if [ -e fail ]; then exit 1; else exit 0; fi;
385385
- id: stepCheck
386386
name: Checking presence of CI target for current job
387-
run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
387+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
388388
- if: steps.stepCheck.outputs.status == 'built'
389389
name: 'Building/fetching previous CI target: coq'
390390
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -454,15 +454,15 @@ jobs:
454454
- id: stepGetDerivation
455455
name: Getting derivation for current job (stdpp)
456456
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
457-
\"8.20\" --argstr job \"stdpp\" \\\n --dry-run &> out || (touch fail;
457+
\"8.20\" --argstr job \"stdpp\" \\\n --dry-run 2> err > out || (touch fail;
458458
true)\n"
459459
- name: Error reporting
460-
run: "echo \"out=\"; cat out\n"
460+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
461461
- name: Failure check
462462
run: if [ -e fail ]; then exit 1; else exit 0; fi;
463463
- id: stepCheck
464464
name: Checking presence of CI target for current job
465-
run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
465+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
466466
- if: steps.stepCheck.outputs.status == 'built'
467467
name: 'Building/fetching previous CI target: coq'
468468
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -497,6 +497,3 @@ on:
497497
push:
498498
branches:
499499
- master
500-
concurrency:
501-
group: "${{ github.workflow }}-${{ github.event.pull_request.number || github.head_ref || github.ref }}"
502-
cancel-in-progress: true

‎.nix/config.nix‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,10 @@
1010

1111
bundles."8.20" = {
1212
coqPackages.coq.override.version = "8.20";
13-
coqPackages.metacoq.override.version = "coq-8.20";
13+
coqPackages.metacoq.override.version = "1.3.4-8.20";
1414
coqPackages.stdpp.override.version = "1.11.0";
1515
coqPackages.QuickChick.override.version = "2.0.4";
16-
coqPackages.RustExtraction.override.version = "coq-8.20";
16+
coqPackages.RustExtraction.override.version = "c5d9cbae417213fe25b42f08678f28507cc6b99e";
1717
coqPackages.ElmExtraction.override.version = "0.1.0";
1818
};
1919

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"78d95509824be9e3339c1c0ee19f9c085f32b23e"
1+
"a1f630a232a3e2c739df99d0a947bf7465d2f8bb"

‎coq-concert.opam‎

Lines changed: 7 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -17,26 +17,19 @@ depends: [
1717
"coq" {>= "8.20" & < "8.21~"}
1818
"coq-bignums" {>= "8"}
1919
"coq-quickchick" {>= "2.0.4"}
20-
"coq-metacoq-utils" {>= "1.3.1" & < "1.4~"}
21-
"coq-metacoq-common" {>= "1.3.1" & < "1.4~"}
22-
"coq-metacoq-template" {>= "1.3.1" & < "1.4~"}
23-
"coq-metacoq-template-pcuic" {>= "1.3.1" & < "1.4~"}
24-
"coq-metacoq-pcuic" {>= "1.3.1" & < "1.4~"}
25-
"coq-metacoq-safechecker" {>= "1.3.1" & < "1.4~"}
26-
"coq-metacoq-erasure" {>= "1.3.1" & < "1.4~"}
20+
"coq-metacoq-utils" {>= "1.3.4" & < "1.4~"}
21+
"coq-metacoq-common" {>= "1.3.4" & < "1.4~"}
22+
"coq-metacoq-template" {>= "1.3.4" & < "1.4~"}
23+
"coq-metacoq-template-pcuic" {>= "1.3.4" & < "1.4~"}
24+
"coq-metacoq-pcuic" {>= "1.3.4" & < "1.4~"}
25+
"coq-metacoq-safechecker" {>= "1.3.4" & < "1.4~"}
26+
"coq-metacoq-erasure" {>= "1.3.4" & < "1.4~"}
2727
"coq-rust-extraction" {= "dev"}
2828
"coq-elm-extraction" {= "0.1.0"}
2929
"coq-stdpp" {>= "1.10.0" & < "1.12~"}
3030
]
3131

3232
pin-depends: [
33-
["coq-metacoq-utils.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
34-
["coq-metacoq-common.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
35-
["coq-metacoq-template.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
36-
["coq-metacoq-template-pcuic.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
37-
["coq-metacoq-pcuic.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
38-
["coq-metacoq-safechecker.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
39-
["coq-metacoq-erasure.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
4033
["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#c5d9cbae417213fe25b42f08678f28507cc6b99e"]
4134
]
4235

0 commit comments

Comments
 (0)