Skip to content

Commit 76de461

Browse files
proux01proux01
committed
[CI] Cleanup no longer useful overlays
1 parent f0f5c95 commit 76de461

File tree

5 files changed

+139
-113
lines changed

5 files changed

+139
-113
lines changed

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

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -314,6 +314,7 @@ jobs:
314314
- coq
315315
- mathcomp-classical
316316
- mathcomp-field
317+
- mathcomp-bigenough
317318
- hierarchy-builder
318319
runs-on: ubuntu-latest
319320
steps:
@@ -368,6 +369,10 @@ jobs:
368369
name: 'Building/fetching previous CI target: mathcomp-field'
369370
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
370371
--argstr job "mathcomp-field"
372+
- if: steps.stepCheck.outputs.status == 'built'
373+
name: 'Building/fetching previous CI target: mathcomp-bigenough'
374+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
375+
--argstr job "mathcomp-bigenough"
371376
- if: steps.stepCheck.outputs.status == 'built'
372377
name: 'Building/fetching previous CI target: hierarchy-builder'
373378
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
@@ -376,6 +381,63 @@ jobs:
376381
name: Building/fetching current CI target
377382
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
378383
--argstr job "mathcomp-analysis"
384+
mathcomp-bigenough:
385+
needs:
386+
- coq
387+
- mathcomp-ssreflect
388+
runs-on: ubuntu-latest
389+
steps:
390+
- name: Determine which commit to initially checkout
391+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
392+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
393+
\ }}\" >> $GITHUB_ENV\nfi\n"
394+
- name: Git checkout
395+
uses: actions/checkout@v3
396+
with:
397+
fetch-depth: 0
398+
ref: ${{ env.target_commit }}
399+
- name: Determine which commit to test
400+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
401+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
402+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
403+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
404+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
405+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
406+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
407+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
408+
- name: Git checkout
409+
uses: actions/checkout@v3
410+
with:
411+
fetch-depth: 0
412+
ref: ${{ env.tested_commit }}
413+
- name: Cachix install
414+
uses: cachix/install-nix-action@v27
415+
with:
416+
nix_path: nixpkgs=channel:nixpkgs-unstable
417+
- name: Cachix setup coq-elpi
418+
uses: cachix/cachix-action@v15
419+
with:
420+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
421+
extraPullNames: coq, coq-community, math-comp
422+
name: coq-elpi
423+
- id: stepCheck
424+
name: Checking presence of CI target mathcomp-bigenough
425+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
426+
\ bundle \"coq-master-min-elpi\" --argstr job \"mathcomp-bigenough\" \\\n\
427+
\ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run\
428+
\ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
429+
- if: steps.stepCheck.outputs.status == 'built'
430+
name: 'Building/fetching previous CI target: coq'
431+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
432+
--argstr job "coq"
433+
- if: steps.stepCheck.outputs.status == 'built'
434+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
435+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
436+
--argstr job "mathcomp-ssreflect"
437+
- if: steps.stepCheck.outputs.status == 'built'
438+
name: Building/fetching current CI target
439+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
440+
--argstr job "mathcomp-bigenough"
379441
mathcomp-character:
380442
needs:
381443
- coq

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

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -314,6 +314,7 @@ jobs:
314314
- coq
315315
- mathcomp-classical
316316
- mathcomp-field
317+
- mathcomp-bigenough
317318
- hierarchy-builder
318319
runs-on: ubuntu-latest
319320
steps:
@@ -368,6 +369,10 @@ jobs:
368369
name: 'Building/fetching previous CI target: mathcomp-field'
369370
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
370371
--argstr job "mathcomp-field"
372+
- if: steps.stepCheck.outputs.status == 'built'
373+
name: 'Building/fetching previous CI target: mathcomp-bigenough'
374+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
375+
--argstr job "mathcomp-bigenough"
371376
- if: steps.stepCheck.outputs.status == 'built'
372377
name: 'Building/fetching previous CI target: hierarchy-builder'
373378
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
@@ -376,6 +381,63 @@ jobs:
376381
name: Building/fetching current CI target
377382
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
378383
--argstr job "mathcomp-analysis"
384+
mathcomp-bigenough:
385+
needs:
386+
- coq
387+
- mathcomp-ssreflect
388+
runs-on: ubuntu-latest
389+
steps:
390+
- name: Determine which commit to initially checkout
391+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
392+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
393+
\ }}\" >> $GITHUB_ENV\nfi\n"
394+
- name: Git checkout
395+
uses: actions/checkout@v3
396+
with:
397+
fetch-depth: 0
398+
ref: ${{ env.target_commit }}
399+
- name: Determine which commit to test
400+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
401+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
402+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
403+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
404+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
405+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
406+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
407+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
408+
- name: Git checkout
409+
uses: actions/checkout@v3
410+
with:
411+
fetch-depth: 0
412+
ref: ${{ env.tested_commit }}
413+
- name: Cachix install
414+
uses: cachix/install-nix-action@v27
415+
with:
416+
nix_path: nixpkgs=channel:nixpkgs-unstable
417+
- name: Cachix setup coq-elpi
418+
uses: cachix/cachix-action@v15
419+
with:
420+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
421+
extraPullNames: coq, coq-community, math-comp
422+
name: coq-elpi
423+
- id: stepCheck
424+
name: Checking presence of CI target mathcomp-bigenough
425+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
426+
\ bundle \"coq-master\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\
427+
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\
428+
\ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
429+
- if: steps.stepCheck.outputs.status == 'built'
430+
name: 'Building/fetching previous CI target: coq'
431+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
432+
--argstr job "coq"
433+
- if: steps.stepCheck.outputs.status == 'built'
434+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
435+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
436+
--argstr job "mathcomp-ssreflect"
437+
- if: steps.stepCheck.outputs.status == 'built'
438+
name: Building/fetching current CI target
439+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
440+
--argstr job "mathcomp-bigenough"
379441
mathcomp-character:
380442
needs:
381443
- coq

‎.nix/config.nix‎

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
let common-bundles = {
22
hierarchy-builder.override.version = "master";
3-
hierarchy-builder-shim.job = false;
43
mathcomp.override.version = "master";
54
odd-order.override.version = "master";
65
mathcomp-analysis.override.version = "master";
76
mathcomp-finmap.override.version = "master";
87
mathcomp-classical.override.version = "master";
8+
mathcomp-bigenough.override.version = "master";
99

1010
mathcomp-single-planB-src.job = false;
1111
mathcomp-single-planB.job = false;
@@ -20,12 +20,22 @@ let common-bundles = {
2020
default-bundle = "coq-8.19";
2121
bundles = {
2222

23-
"coq-8.19".coqPackages = common-bundles // {
24-
coq.override.version = "8.19";
23+
"coq-8.19" = {
24+
coqPackages = common-bundles // {
25+
coq.override.version = "8.19";
26+
};
27+
ocamlPackages = {
28+
elpi.override.version = "v1.19.5";
29+
};
2530
};
2631

27-
"coq-master".coqPackages = common-bundles // {
28-
coq.override.version = "master";
32+
"coq-master" = {
33+
coqPackages = common-bundles // {
34+
coq.override.version = "master";
35+
};
36+
ocamlPackages = {
37+
elpi.override.version = "v1.19.5";
38+
};
2939
};
3040

3141
"coq-master-min-elpi" = {

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

Lines changed: 0 additions & 73 deletions
This file was deleted.

‎.nix/coq-overlays/hierarchy-builder/default.nix‎

Lines changed: 0 additions & 35 deletions
This file was deleted.

0 commit comments

Comments
 (0)