Skip to content

Commit dd94f77

Browse files
proux01proux01
authoredFeb 18, 2025··
Merge pull request #105 from proux01/ci-update
[CI] Update
·
2.1.0
2 parents ee402e2 + 6db39f0 commit dd94f77

File tree

8 files changed

+387
-154
lines changed

8 files changed

+387
-154
lines changed
 

‎.github/workflows/docker-action.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ jobs:
2020
- 'mathcomp/mathcomp:2.3.0-coq-8.20'
2121
- 'mathcomp/mathcomp:2.3.0-coq-dev'
2222
- 'mathcomp/mathcomp-dev:coq-8.20'
23-
- 'mathcomp/mathcomp-dev:coq-dev'
23+
- 'mathcomp/mathcomp-dev:rocq-prover-dev'
2424
fail-fast: false
2525
steps:
2626
- uses: actions/checkout@v4

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

+40-5
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,10 +169,6 @@ jobs:
170169
name: 'Building/fetching previous CI target: coq'
171170
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
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-8.20"
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-8.20"
@@ -260,6 +255,7 @@ jobs:
260255
needs:
261256
- coq
262257
- coq-elpi
258+
- stdlib
263259
runs-on: ubuntu-latest
264260
steps:
265261
- name: Determine which commit to initially checkout
@@ -315,6 +311,10 @@ jobs:
315311
name: 'Building/fetching previous CI target: coq-elpi'
316312
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
317313
--argstr job "coq-elpi"
314+
- if: steps.stepCheck.outputs.status == 'built'
315+
name: 'Building/fetching previous CI target: stdlib'
316+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
317+
--argstr job "stdlib"
318318
- if: steps.stepCheck.outputs.status == 'built'
319319
name: Building/fetching current CI target
320320
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -327,6 +327,7 @@ jobs:
327327
- mathcomp-algebra
328328
- mathcomp-field
329329
- hierarchy-builder
330+
- stdlib
330331
runs-on: ubuntu-latest
331332
steps:
332333
- name: Determine which commit to initially checkout
@@ -410,6 +411,10 @@ jobs:
410411
name: 'Building/fetching previous CI target: hierarchy-builder'
411412
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
412413
--argstr job "hierarchy-builder"
414+
- if: steps.stepCheck.outputs.status == 'built'
415+
name: 'Building/fetching previous CI target: stdlib'
416+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
417+
--argstr job "stdlib"
413418
- if: steps.stepCheck.outputs.status == 'built'
414419
name: Building/fetching current CI target
415420
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -420,6 +425,7 @@ jobs:
420425
- stdlib
421426
- mathcomp-ssreflect
422427
- hierarchy-builder
428+
- stdlib
423429
runs-on: ubuntu-latest
424430
steps:
425431
- name: Determine which commit to initially checkout
@@ -487,6 +493,10 @@ jobs:
487493
name: 'Building/fetching previous CI target: hierarchy-builder'
488494
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
489495
--argstr job "hierarchy-builder"
496+
- if: steps.stepCheck.outputs.status == 'built'
497+
name: 'Building/fetching previous CI target: stdlib'
498+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
499+
--argstr job "stdlib"
490500
- if: steps.stepCheck.outputs.status == 'built'
491501
name: Building/fetching current CI target
492502
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -722,6 +732,7 @@ jobs:
722732
- mathcomp-ssreflect
723733
- mathcomp-algebra
724734
- hierarchy-builder
735+
- stdlib
725736
runs-on: ubuntu-latest
726737
steps:
727738
- name: Determine which commit to initially checkout
@@ -797,6 +808,10 @@ jobs:
797808
name: 'Building/fetching previous CI target: hierarchy-builder'
798809
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
799810
--argstr job "hierarchy-builder"
811+
- if: steps.stepCheck.outputs.status == 'built'
812+
name: 'Building/fetching previous CI target: stdlib'
813+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
814+
--argstr job "stdlib"
800815
- if: steps.stepCheck.outputs.status == 'built'
801816
name: Building/fetching current CI target
802817
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -805,6 +820,7 @@ jobs:
805820
needs:
806821
- coq
807822
- mathcomp-ssreflect
823+
- stdlib
808824
runs-on: ubuntu-latest
809825
steps:
810826
- name: Determine which commit to initially checkout
@@ -860,6 +876,10 @@ jobs:
860876
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
861877
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
862878
--argstr job "mathcomp-ssreflect"
879+
- if: steps.stepCheck.outputs.status == 'built'
880+
name: 'Building/fetching previous CI target: stdlib'
881+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
882+
--argstr job "stdlib"
863883
- if: steps.stepCheck.outputs.status == 'built'
864884
name: Building/fetching current CI target
865885
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -871,6 +891,7 @@ jobs:
871891
- mathcomp-algebra
872892
- mathcomp-field
873893
- mathcomp-bigenough
894+
- stdlib
874895
runs-on: ubuntu-latest
875896
steps:
876897
- name: Determine which commit to initially checkout
@@ -946,6 +967,10 @@ jobs:
946967
name: 'Building/fetching previous CI target: mathcomp-bigenough'
947968
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
948969
--argstr job "mathcomp-bigenough"
970+
- if: steps.stepCheck.outputs.status == 'built'
971+
name: 'Building/fetching previous CI target: stdlib'
972+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
973+
--argstr job "stdlib"
949974
- if: steps.stepCheck.outputs.status == 'built'
950975
name: Building/fetching current CI target
951976
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -955,6 +980,7 @@ jobs:
955980
- coq
956981
- stdlib
957982
- hierarchy-builder
983+
- stdlib
958984
runs-on: ubuntu-latest
959985
steps:
960986
- name: Determine which commit to initially checkout
@@ -1014,6 +1040,10 @@ jobs:
10141040
name: 'Building/fetching previous CI target: hierarchy-builder'
10151041
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
10161042
--argstr job "hierarchy-builder"
1043+
- if: steps.stepCheck.outputs.status == 'built'
1044+
name: 'Building/fetching previous CI target: stdlib'
1045+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
1046+
--argstr job "stdlib"
10171047
- if: steps.stepCheck.outputs.status == 'built'
10181048
name: Building/fetching current CI target
10191049
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -1023,6 +1053,7 @@ jobs:
10231053
- coq
10241054
- mathcomp-algebra
10251055
- mathcomp-ssreflect
1056+
- stdlib
10261057
runs-on: ubuntu-latest
10271058
steps:
10281059
- name: Determine which commit to initially checkout
@@ -1086,6 +1117,10 @@ jobs:
10861117
name: 'Building/fetching previous CI target: mathcomp-fingroup'
10871118
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
10881119
--argstr job "mathcomp-fingroup"
1120+
- if: steps.stepCheck.outputs.status == 'built'
1121+
name: 'Building/fetching previous CI target: stdlib'
1122+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
1123+
--argstr job "stdlib"
10891124
- if: steps.stepCheck.outputs.status == 'built'
10901125
name: Building/fetching current CI target
10911126
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"

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

+91-7
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,10 +169,6 @@ 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"
@@ -260,6 +255,7 @@ jobs:
260255
needs:
261256
- coq
262257
- coq-elpi
258+
- stdlib
263259
runs-on: ubuntu-latest
264260
steps:
265261
- name: Determine which commit to initially checkout
@@ -315,6 +311,10 @@ jobs:
315311
name: 'Building/fetching previous CI target: coq-elpi'
316312
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
317313
--argstr job "coq-elpi"
314+
- if: steps.stepCheck.outputs.status == 'built'
315+
name: 'Building/fetching previous CI target: stdlib'
316+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
317+
--argstr job "stdlib"
318318
- if: steps.stepCheck.outputs.status == 'built'
319319
name: Building/fetching current CI target
320320
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
@@ -327,6 +327,7 @@ jobs:
327327
- mathcomp-algebra
328328
- mathcomp-field
329329
- hierarchy-builder
330+
- stdlib
330331
runs-on: ubuntu-latest
331332
steps:
332333
- name: Determine which commit to initially checkout
@@ -410,6 +411,10 @@ jobs:
410411
name: 'Building/fetching previous CI target: hierarchy-builder'
411412
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
412413
--argstr job "hierarchy-builder"
414+
- if: steps.stepCheck.outputs.status == 'built'
415+
name: 'Building/fetching previous CI target: stdlib'
416+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
417+
--argstr job "stdlib"
413418
- if: steps.stepCheck.outputs.status == 'built'
414419
name: Building/fetching current CI target
415420
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
@@ -420,6 +425,7 @@ jobs:
420425
- stdlib
421426
- mathcomp-ssreflect
422427
- hierarchy-builder
428+
- stdlib
423429
runs-on: ubuntu-latest
424430
steps:
425431
- name: Determine which commit to initially checkout
@@ -487,12 +493,20 @@ jobs:
487493
name: 'Building/fetching previous CI target: hierarchy-builder'
488494
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
489495
--argstr job "hierarchy-builder"
496+
- if: steps.stepCheck.outputs.status == 'built'
497+
name: 'Building/fetching previous CI target: stdlib'
498+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
499+
--argstr job "stdlib"
490500
- if: steps.stepCheck.outputs.status == 'built'
491501
name: Building/fetching current CI target
492502
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
493503
--argstr job "mathcomp-algebra"
494504
mathcomp-algebra-tactics:
495-
needs: []
505+
needs:
506+
- coq
507+
- mathcomp-algebra
508+
- coq-elpi
509+
- mathcomp-zify
496510
runs-on: ubuntu-latest
497511
steps:
498512
- name: Determine which commit to initially checkout
@@ -540,6 +554,22 @@ jobs:
540554
- id: stepCheck
541555
name: Checking presence of CI target for current job
542556
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
557+
- if: steps.stepCheck.outputs.status == 'built'
558+
name: 'Building/fetching previous CI target: coq'
559+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
560+
--argstr job "coq"
561+
- if: steps.stepCheck.outputs.status == 'built'
562+
name: 'Building/fetching previous CI target: mathcomp-algebra'
563+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
564+
--argstr job "mathcomp-algebra"
565+
- if: steps.stepCheck.outputs.status == 'built'
566+
name: 'Building/fetching previous CI target: coq-elpi'
567+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
568+
--argstr job "coq-elpi"
569+
- if: steps.stepCheck.outputs.status == 'built'
570+
name: 'Building/fetching previous CI target: mathcomp-zify'
571+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
572+
--argstr job "mathcomp-zify"
543573
- if: steps.stepCheck.outputs.status == 'built'
544574
name: Building/fetching current CI target
545575
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
@@ -551,6 +581,8 @@ jobs:
551581
- coqeal
552582
- mathcomp-real-closed
553583
- mathcomp-bigenough
584+
- mathcomp-zify
585+
- mathcomp-algebra-tactics
554586
runs-on: ubuntu-latest
555587
steps:
556588
- name: Determine which commit to initially checkout
@@ -618,6 +650,14 @@ jobs:
618650
name: 'Building/fetching previous CI target: mathcomp-bigenough'
619651
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
620652
--argstr job "mathcomp-bigenough"
653+
- if: steps.stepCheck.outputs.status == 'built'
654+
name: 'Building/fetching previous CI target: mathcomp-zify'
655+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
656+
--argstr job "mathcomp-zify"
657+
- if: steps.stepCheck.outputs.status == 'built'
658+
name: 'Building/fetching previous CI target: mathcomp-algebra-tactics'
659+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
660+
--argstr job "mathcomp-algebra-tactics"
621661
- if: steps.stepCheck.outputs.status == 'built'
622662
name: Building/fetching current CI target
623663
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
@@ -692,6 +732,7 @@ jobs:
692732
- mathcomp-ssreflect
693733
- mathcomp-algebra
694734
- hierarchy-builder
735+
- stdlib
695736
runs-on: ubuntu-latest
696737
steps:
697738
- name: Determine which commit to initially checkout
@@ -767,6 +808,10 @@ jobs:
767808
name: 'Building/fetching previous CI target: hierarchy-builder'
768809
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
769810
--argstr job "hierarchy-builder"
811+
- if: steps.stepCheck.outputs.status == 'built'
812+
name: 'Building/fetching previous CI target: stdlib'
813+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
814+
--argstr job "stdlib"
770815
- if: steps.stepCheck.outputs.status == 'built'
771816
name: Building/fetching current CI target
772817
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
@@ -775,6 +820,7 @@ jobs:
775820
needs:
776821
- coq
777822
- mathcomp-ssreflect
823+
- stdlib
778824
runs-on: ubuntu-latest
779825
steps:
780826
- name: Determine which commit to initially checkout
@@ -830,6 +876,10 @@ jobs:
830876
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
831877
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
832878
--argstr job "mathcomp-ssreflect"
879+
- if: steps.stepCheck.outputs.status == 'built'
880+
name: 'Building/fetching previous CI target: stdlib'
881+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
882+
--argstr job "stdlib"
833883
- if: steps.stepCheck.outputs.status == 'built'
834884
name: Building/fetching current CI target
835885
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
@@ -841,6 +891,7 @@ jobs:
841891
- mathcomp-algebra
842892
- mathcomp-field
843893
- mathcomp-bigenough
894+
- stdlib
844895
runs-on: ubuntu-latest
845896
steps:
846897
- name: Determine which commit to initially checkout
@@ -916,6 +967,10 @@ jobs:
916967
name: 'Building/fetching previous CI target: mathcomp-bigenough'
917968
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
918969
--argstr job "mathcomp-bigenough"
970+
- if: steps.stepCheck.outputs.status == 'built'
971+
name: 'Building/fetching previous CI target: stdlib'
972+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
973+
--argstr job "stdlib"
919974
- if: steps.stepCheck.outputs.status == 'built'
920975
name: Building/fetching current CI target
921976
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
@@ -925,6 +980,7 @@ jobs:
925980
- coq
926981
- stdlib
927982
- hierarchy-builder
983+
- stdlib
928984
runs-on: ubuntu-latest
929985
steps:
930986
- name: Determine which commit to initially checkout
@@ -984,12 +1040,20 @@ jobs:
9841040
name: 'Building/fetching previous CI target: hierarchy-builder'
9851041
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
9861042
--argstr job "hierarchy-builder"
1043+
- if: steps.stepCheck.outputs.status == 'built'
1044+
name: 'Building/fetching previous CI target: stdlib'
1045+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1046+
--argstr job "stdlib"
9871047
- if: steps.stepCheck.outputs.status == 'built'
9881048
name: Building/fetching current CI target
9891049
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
9901050
--argstr job "mathcomp-ssreflect"
9911051
mathcomp-zify:
992-
needs: []
1052+
needs:
1053+
- coq
1054+
- mathcomp-algebra
1055+
- mathcomp-ssreflect
1056+
- stdlib
9931057
runs-on: ubuntu-latest
9941058
steps:
9951059
- name: Determine which commit to initially checkout
@@ -1037,6 +1101,26 @@ jobs:
10371101
- id: stepCheck
10381102
name: Checking presence of CI target for current job
10391103
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
1104+
- if: steps.stepCheck.outputs.status == 'built'
1105+
name: 'Building/fetching previous CI target: coq'
1106+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1107+
--argstr job "coq"
1108+
- if: steps.stepCheck.outputs.status == 'built'
1109+
name: 'Building/fetching previous CI target: mathcomp-algebra'
1110+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1111+
--argstr job "mathcomp-algebra"
1112+
- if: steps.stepCheck.outputs.status == 'built'
1113+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
1114+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1115+
--argstr job "mathcomp-ssreflect"
1116+
- if: steps.stepCheck.outputs.status == 'built'
1117+
name: 'Building/fetching previous CI target: mathcomp-fingroup'
1118+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1119+
--argstr job "mathcomp-fingroup"
1120+
- if: steps.stepCheck.outputs.status == 'built'
1121+
name: 'Building/fetching previous CI target: stdlib'
1122+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1123+
--argstr job "stdlib"
10401124
- if: steps.stepCheck.outputs.status == 'built'
10411125
name: Building/fetching current CI target
10421126
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"

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

+75-6
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,10 +169,6 @@ jobs:
170169
name: 'Building/fetching previous CI target: coq'
171170
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
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 "rocq-9.0"
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 "rocq-9.0"
@@ -183,6 +178,7 @@ jobs:
183178
- coq
184179
- mathcomp-algebra
185180
- bignums
181+
- multinomials
186182
- mathcomp-real-closed
187183
runs-on: ubuntu-latest
188184
steps:
@@ -243,6 +239,10 @@ jobs:
243239
name: 'Building/fetching previous CI target: bignums'
244240
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
245241
--argstr job "bignums"
242+
- if: steps.stepCheck.outputs.status == 'built'
243+
name: 'Building/fetching previous CI target: multinomials'
244+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
245+
--argstr job "multinomials"
246246
- if: steps.stepCheck.outputs.status == 'built'
247247
name: 'Building/fetching previous CI target: mathcomp-real-closed'
248248
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
@@ -255,6 +255,7 @@ jobs:
255255
needs:
256256
- coq
257257
- coq-elpi
258+
- stdlib
258259
runs-on: ubuntu-latest
259260
steps:
260261
- name: Determine which commit to initially checkout
@@ -310,6 +311,10 @@ jobs:
310311
name: 'Building/fetching previous CI target: coq-elpi'
311312
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
312313
--argstr job "coq-elpi"
314+
- if: steps.stepCheck.outputs.status == 'built'
315+
name: 'Building/fetching previous CI target: stdlib'
316+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
317+
--argstr job "stdlib"
313318
- if: steps.stepCheck.outputs.status == 'built'
314319
name: Building/fetching current CI target
315320
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
@@ -322,6 +327,7 @@ jobs:
322327
- mathcomp-algebra
323328
- mathcomp-field
324329
- hierarchy-builder
330+
- stdlib
325331
runs-on: ubuntu-latest
326332
steps:
327333
- name: Determine which commit to initially checkout
@@ -405,6 +411,10 @@ jobs:
405411
name: 'Building/fetching previous CI target: hierarchy-builder'
406412
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
407413
--argstr job "hierarchy-builder"
414+
- if: steps.stepCheck.outputs.status == 'built'
415+
name: 'Building/fetching previous CI target: stdlib'
416+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
417+
--argstr job "stdlib"
408418
- if: steps.stepCheck.outputs.status == 'built'
409419
name: Building/fetching current CI target
410420
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
@@ -415,6 +425,7 @@ jobs:
415425
- stdlib
416426
- mathcomp-ssreflect
417427
- hierarchy-builder
428+
- stdlib
418429
runs-on: ubuntu-latest
419430
steps:
420431
- name: Determine which commit to initially checkout
@@ -482,6 +493,10 @@ jobs:
482493
name: 'Building/fetching previous CI target: hierarchy-builder'
483494
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
484495
--argstr job "hierarchy-builder"
496+
- if: steps.stepCheck.outputs.status == 'built'
497+
name: 'Building/fetching previous CI target: stdlib'
498+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
499+
--argstr job "stdlib"
485500
- if: steps.stepCheck.outputs.status == 'built'
486501
name: Building/fetching current CI target
487502
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
@@ -717,6 +732,7 @@ jobs:
717732
- mathcomp-ssreflect
718733
- mathcomp-algebra
719734
- hierarchy-builder
735+
- stdlib
720736
runs-on: ubuntu-latest
721737
steps:
722738
- name: Determine which commit to initially checkout
@@ -792,6 +808,10 @@ jobs:
792808
name: 'Building/fetching previous CI target: hierarchy-builder'
793809
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
794810
--argstr job "hierarchy-builder"
811+
- if: steps.stepCheck.outputs.status == 'built'
812+
name: 'Building/fetching previous CI target: stdlib'
813+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
814+
--argstr job "stdlib"
795815
- if: steps.stepCheck.outputs.status == 'built'
796816
name: Building/fetching current CI target
797817
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
@@ -800,6 +820,7 @@ jobs:
800820
needs:
801821
- coq
802822
- mathcomp-ssreflect
823+
- stdlib
803824
runs-on: ubuntu-latest
804825
steps:
805826
- name: Determine which commit to initially checkout
@@ -855,6 +876,10 @@ jobs:
855876
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
856877
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
857878
--argstr job "mathcomp-ssreflect"
879+
- if: steps.stepCheck.outputs.status == 'built'
880+
name: 'Building/fetching previous CI target: stdlib'
881+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
882+
--argstr job "stdlib"
858883
- if: steps.stepCheck.outputs.status == 'built'
859884
name: Building/fetching current CI target
860885
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
@@ -866,6 +891,7 @@ jobs:
866891
- mathcomp-algebra
867892
- mathcomp-field
868893
- mathcomp-bigenough
894+
- stdlib
869895
runs-on: ubuntu-latest
870896
steps:
871897
- name: Determine which commit to initially checkout
@@ -941,6 +967,10 @@ jobs:
941967
name: 'Building/fetching previous CI target: mathcomp-bigenough'
942968
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
943969
--argstr job "mathcomp-bigenough"
970+
- if: steps.stepCheck.outputs.status == 'built'
971+
name: 'Building/fetching previous CI target: stdlib'
972+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
973+
--argstr job "stdlib"
944974
- if: steps.stepCheck.outputs.status == 'built'
945975
name: Building/fetching current CI target
946976
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
@@ -950,6 +980,7 @@ jobs:
950980
- coq
951981
- stdlib
952982
- hierarchy-builder
983+
- stdlib
953984
runs-on: ubuntu-latest
954985
steps:
955986
- name: Determine which commit to initially checkout
@@ -1009,6 +1040,10 @@ jobs:
10091040
name: 'Building/fetching previous CI target: hierarchy-builder'
10101041
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
10111042
--argstr job "hierarchy-builder"
1043+
- if: steps.stepCheck.outputs.status == 'built'
1044+
name: 'Building/fetching previous CI target: stdlib'
1045+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
1046+
--argstr job "stdlib"
10121047
- if: steps.stepCheck.outputs.status == 'built'
10131048
name: Building/fetching current CI target
10141049
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
@@ -1018,6 +1053,7 @@ jobs:
10181053
- coq
10191054
- mathcomp-algebra
10201055
- mathcomp-ssreflect
1056+
- stdlib
10211057
runs-on: ubuntu-latest
10221058
steps:
10231059
- name: Determine which commit to initially checkout
@@ -1081,12 +1117,21 @@ jobs:
10811117
name: 'Building/fetching previous CI target: mathcomp-fingroup'
10821118
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
10831119
--argstr job "mathcomp-fingroup"
1120+
- if: steps.stepCheck.outputs.status == 'built'
1121+
name: 'Building/fetching previous CI target: stdlib'
1122+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
1123+
--argstr job "stdlib"
10841124
- if: steps.stepCheck.outputs.status == 'built'
10851125
name: Building/fetching current CI target
10861126
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
10871127
--argstr job "mathcomp-zify"
10881128
multinomials:
1089-
needs: []
1129+
needs:
1130+
- coq
1131+
- mathcomp-ssreflect
1132+
- mathcomp-algebra
1133+
- mathcomp-finmap
1134+
- mathcomp-bigenough
10901135
runs-on: ubuntu-latest
10911136
steps:
10921137
- name: Determine which commit to initially checkout
@@ -1134,6 +1179,30 @@ jobs:
11341179
- id: stepCheck
11351180
name: Checking presence of CI target for current job
11361181
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
1182+
- if: steps.stepCheck.outputs.status == 'built'
1183+
name: 'Building/fetching previous CI target: coq'
1184+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
1185+
--argstr job "coq"
1186+
- if: steps.stepCheck.outputs.status == 'built'
1187+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
1188+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
1189+
--argstr job "mathcomp-ssreflect"
1190+
- if: steps.stepCheck.outputs.status == 'built'
1191+
name: 'Building/fetching previous CI target: mathcomp-algebra'
1192+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
1193+
--argstr job "mathcomp-algebra"
1194+
- if: steps.stepCheck.outputs.status == 'built'
1195+
name: 'Building/fetching previous CI target: mathcomp-finmap'
1196+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
1197+
--argstr job "mathcomp-finmap"
1198+
- if: steps.stepCheck.outputs.status == 'built'
1199+
name: 'Building/fetching previous CI target: mathcomp-fingroup'
1200+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
1201+
--argstr job "mathcomp-fingroup"
1202+
- if: steps.stepCheck.outputs.status == 'built'
1203+
name: 'Building/fetching previous CI target: mathcomp-bigenough'
1204+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
1205+
--argstr job "mathcomp-bigenough"
11371206
- if: steps.stepCheck.outputs.status == 'built'
11381207
name: Building/fetching current CI target
11391208
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"

‎.nix/config.nix

+15-10
Original file line numberDiff line numberDiff line change
@@ -112,8 +112,16 @@
112112
# from https://github.com/<github_login>/<repository>
113113
};
114114
in {
115-
"coq-master".coqPackages = common-bundles // {
115+
"coq-master" = { rocqPackages = {
116+
rocq-core.override.version = "master";
117+
stdlib.override.version = "master";
118+
bignums.override.version = "master";
119+
rocq-elpi.override.version = "master";
120+
rocq-elpi.override.elpi-version = "2.0.7";
121+
}; coqPackages = common-bundles // {
116122
coq.override.version = "master";
123+
stdlib.override.version = "master";
124+
bignums.override.version = "master";
117125
coq-elpi.override.version = "master";
118126
coq-elpi.override.elpi-version = "2.0.7";
119127
hierarchy-builder.override.version = "master";
@@ -122,24 +130,21 @@
122130
mathcomp-bigenough.override.version = "master";
123131
multinomials.override.version = "master";
124132
mathcomp-real-closed.override.version = "master";
125-
stdlib.override.version = "master";
126-
bignums.override.version = "master";
127133
mathcomp-zify.override.version = "master";
128134
mathcomp-algebra-tactics.override.version = "master";
129-
};
135+
}; };
130136
"rocq-9.0".coqPackages = common-bundles // {
131137
coq.override.version = "9.0";
132-
coq-elpi.override.version = "master";
133-
coq-elpi.override.elpi-version = "2.0.7";
134-
hierarchy-builder.override.version = "master";
138+
coq-elpi.job = true;
139+
hierarchy-builder.job = true;
135140
mathcomp.override.version = "2.3.0";
136-
multinomials.override.version = "2.3.0"; # needs a release
141+
multinomials.override.version = "2.3.0";
137142
};
138143
"coq-8.20".coqPackages = common-bundles // {
139144
coq.override.version = "8.20";
140-
coq-elpi.override.version = "master";
145+
coq-elpi.override.version = "2.5.0";
141146
coq-elpi.override.elpi-version = "2.0.7";
142-
hierarchy-builder.override.version = "master";
147+
hierarchy-builder.override.version = "1.8.1";
143148
mathcomp.override.version = "2.3.0";
144149
};
145150
};

‎.nix/coq-nix-toolbox.nix

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"ee1cc6946f9f33dd281f74cd5c5273786f0e0850"
1+
"249b84ba5526b5b8c49f236923d595c8505717f2"

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

+164
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
{
2+
lib,
3+
mkCoqDerivation,
4+
which,
5+
coq,
6+
rocqPackages,
7+
stdlib,
8+
version ? null,
9+
elpi-version ? null,
10+
}:
11+
12+
let
13+
default-elpi-version = if elpi-version != null then elpi-version else (
14+
lib.switch coq.coq-version [
15+
{ case = "8.11"; out = "1.11.4"; }
16+
{ case = "8.12"; out = "1.12.0"; }
17+
{ case = "8.13"; out = "1.13.7"; }
18+
{ case = "8.14"; out = "1.13.7"; }
19+
{ case = "8.15"; out = "1.15.0"; }
20+
{ case = "8.16"; out = "1.17.0"; }
21+
{ case = "8.17"; out = "1.17.0"; }
22+
{ case = "8.18"; out = "1.18.1"; }
23+
{ case = "8.19"; out = "1.18.1"; }
24+
{ case = "8.20"; out = "1.19.2"; }
25+
{ case = "9.0"; out = "2.0.7"; }
26+
] { }
27+
);
28+
elpi = coq.ocamlPackages.elpi.override { version = default-elpi-version; };
29+
propagatedBuildInputs_wo_elpi = [
30+
coq.ocamlPackages.findlib
31+
];
32+
derivation = mkCoqDerivation {
33+
pname = "elpi";
34+
repo = "coq-elpi";
35+
owner = "LPCIC";
36+
inherit version;
37+
defaultVersion = lib.switch coq.coq-version [
38+
{ case = "9.0"; out = "2.5.0"; }
39+
{ case = "8.20"; out = "2.2.0"; }
40+
{ case = "8.19"; out = "2.0.1"; }
41+
{ case = "8.18"; out = "2.0.0"; }
42+
{ case = "8.17"; out = "1.18.0"; }
43+
{ case = "8.16"; out = "1.15.6"; }
44+
{ case = "8.15"; out = "1.14.0"; }
45+
{ case = "8.14"; out = "1.11.2"; }
46+
{ case = "8.13"; out = "1.11.1"; }
47+
{ case = "8.12"; out = "1.8.3_8.12"; }
48+
{ case = "8.11"; out = "1.6.3_8.11"; }
49+
] null;
50+
release."2.5.0".sha256 = "sha256-Z5xjO83X/ZoTQlWnVupGXPH3HuJefr57Kv128I0dltg=";
51+
release."2.4.0".sha256 = "sha256-W2+vVGExLLux8e0nSZESSoMVvrLxhL6dmXkb+JuKiqc=";
52+
release."2.2.0".sha256 = "sha256-rADEoqTXM7/TyYkUKsmCFfj6fjpWdnZEOK++5oLfC/I=";
53+
release."2.0.1".sha256 = "sha256-cuoPsEJ+JRLVc9Golt2rJj4P7lKltTrrmQijjoViooc=";
54+
release."2.0.0".sha256 = "sha256-A/cH324M21k3SZ7+YWXtaYEbu6dZQq3K0cb1RMKjbsM=";
55+
release."1.19.0".sha256 = "sha256-kGoo61nJxeG/BqV+iQaV3iinwPStND+7+fYMxFkiKrQ=";
56+
release."1.18.0".sha256 = "sha256-2fCOlhqi4YkiL5n8SYHuc3pLH+DArf9zuMH7IhpBc2Y=";
57+
release."1.17.0".sha256 = "sha256-J8GatRKFU0ekNCG3V5dBI+FXypeHcLgC5QJYGYzFiEM=";
58+
release."1.15.6".sha256 = "sha256-qc0q01tW8NVm83801HHOBHe/7H1/F2WGDbKO6nCXfno=";
59+
release."1.15.1".sha256 = "sha256-NT2RlcIsFB9AvBhMxil4ZZIgx+KusMqDflj2HgQxsZg=";
60+
release."1.14.0".sha256 = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp";
61+
release."1.13.0".sha256 = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n";
62+
release."1.12.1".sha256 = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY=";
63+
release."1.11.2".sha256 = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4";
64+
release."1.11.1".sha256 = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc";
65+
release."1.10.1".sha256 = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk";
66+
release."1.9.7".sha256 = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1";
67+
release."1.9.5".sha256 = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6";
68+
release."1.9.4".sha256 = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq";
69+
release."1.9.3".sha256 = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z";
70+
release."1.9.2".sha256 = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07";
71+
release."1.8.3_8.12".sha256 = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557";
72+
release."1.8.3_8.12".version = "1.8.3";
73+
release."1.8.2_8.12".sha256 = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y";
74+
release."1.8.2_8.12".version = "1.8.2";
75+
release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r";
76+
release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1";
77+
release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8";
78+
release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp";
79+
release."1.6.3_8.11".version = "1.6.3";
80+
release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn";
81+
release."1.6.2_8.11".version = "1.6.2";
82+
release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53";
83+
release."1.6.1_8.11".version = "1.6.1";
84+
release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq";
85+
release."1.6.0_8.11".version = "1.6.0";
86+
release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
87+
releaseRev = v: "v${v}";
88+
89+
buildFlags = [ "OCAMLWARN=" ];
90+
91+
mlPlugin = true;
92+
useDuneifVersion = v: lib.versions.isGe "2.2.0" v || v == "dev";
93+
94+
propagatedBuildInputs = propagatedBuildInputs_wo_elpi ++ [ elpi ];
95+
96+
preConfigure = ''
97+
make elpi/dune || true
98+
'';
99+
100+
meta = {
101+
description = "Coq plugin embedding ELPI";
102+
maintainers = [ lib.maintainers.cohencyril ];
103+
license = lib.licenses.lgpl21Plus;
104+
};
105+
};
106+
patched-derivation1 = derivation.overrideAttrs
107+
(
108+
o:
109+
lib.optionalAttrs (o ? elpi-version)
110+
{
111+
propagatedBuildInputs = propagatedBuildInputs_wo_elpi ++ [
112+
(coq.ocamlPackages.elpi.override { version = o.elpi-version; })
113+
];
114+
}
115+
);
116+
patched-derivation2 = patched-derivation1.overrideAttrs
117+
(
118+
o:
119+
lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.2.0" o.version))
120+
{
121+
propagatedBuildInputs = o.propagatedBuildInputs ++ [ coq.ocamlPackages.ppx_optcomp ];
122+
}
123+
);
124+
patched-derivation3 = patched-derivation2.overrideAttrs
125+
(
126+
o:
127+
lib.optionalAttrs (o.version != null && o.version == "2.4.0")
128+
{
129+
propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
130+
}
131+
);
132+
patched-derivation4 = patched-derivation3.overrideAttrs
133+
(
134+
o:
135+
# this is just a wrapper for rocPackages.rocq-elpi for Rocq >= 9.0
136+
if coq.version != null && (coq.version == "dev"
137+
|| lib.versions.isGe "9.0" coq.version) then {
138+
configurePhase = ''
139+
echo no configuration
140+
'';
141+
buildPhase = ''
142+
echo building nothing
143+
'';
144+
installPhase = ''
145+
echo installing nothing
146+
'';
147+
propagatedBuildInputs = o.propagatedBuildInputs
148+
++ [ rocqPackages.rocq-elpi ];
149+
} else lib.optionalAttrs (o.version != null && (o.version == "dev"
150+
|| lib.versions.isGe "2.5.0" o.version)) {
151+
configurePhase = ''
152+
make dune-files || true
153+
'';
154+
buildPhase = ''
155+
dune build -p rocq-elpi @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
156+
'';
157+
installPhase = ''
158+
dune install --root . rocq-elpi --prefix=$out --libdir $OCAMLFIND_DESTDIR
159+
mkdir $out/lib/coq/
160+
mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version}
161+
'';
162+
}
163+
);
164+
in patched-derivation4

‎.nix/coq-overlays/coqeal/default.nix

-124
This file was deleted.

0 commit comments

Comments
 (0)
Please sign in to comment.