Skip to content

Commit f9c21c6

Browse files
garesgares
authored
Merge pull request #877 from proux01/ci-algebra-tactics
[CI] Add algebra-tactics
2 parents d527ac2 + 4a688cf commit f9c21c6

File tree

5 files changed

+629
-0
lines changed

5 files changed

+629
-0
lines changed

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

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -572,6 +572,85 @@ jobs:
572572
name: Building/fetching current CI target
573573
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
574574
"coq-8.20" --argstr job "mathcomp-algebra"
575+
mathcomp-algebra-tactics:
576+
needs:
577+
- coq
578+
- mathcomp-ssreflect
579+
- mathcomp-algebra
580+
- coq-elpi
581+
- mathcomp-zify
582+
runs-on: ubuntu-latest
583+
steps:
584+
- name: Determine which commit to initially checkout
585+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
586+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
587+
}}\" >> $GITHUB_ENV\nfi\n"
588+
- name: Git checkout
589+
uses: actions/checkout@v4
590+
with:
591+
fetch-depth: 0
592+
ref: ${{ env.target_commit }}
593+
- name: Determine which commit to test
594+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
595+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
596+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
597+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
598+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
599+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
600+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
601+
\ fi\nfi\n"
602+
- name: Git checkout
603+
uses: actions/checkout@v4
604+
with:
605+
fetch-depth: 0
606+
ref: ${{ env.tested_commit }}
607+
- name: Cachix install
608+
uses: cachix/install-nix-action@v31
609+
with:
610+
nix_path: nixpkgs=channel:nixpkgs-unstable
611+
- name: Cachix setup coq-elpi
612+
uses: cachix/cachix-action@v16
613+
with:
614+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
615+
extraPullNames: coq, coq-community, math-comp
616+
name: coq-elpi
617+
- id: stepGetDerivation
618+
name: Getting derivation for current job (mathcomp-algebra-tactics)
619+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
620+
\"coq-8.20\" --argstr job \"mathcomp-algebra-tactics\" \\\n --dry-run 2>
621+
err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"\
622+
Error: getting derivation failed\"; exit 1; fi\n"
623+
- id: stepCheck
624+
name: Checking presence of CI target for current job
625+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
626+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
627+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
628+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
629+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
630+
- if: steps.stepCheck.outputs.status != 'fetched'
631+
name: 'Building/fetching previous CI target: coq'
632+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
633+
"coq-8.20" --argstr job "coq"
634+
- if: steps.stepCheck.outputs.status != 'fetched'
635+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
636+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
637+
"coq-8.20" --argstr job "mathcomp-ssreflect"
638+
- if: steps.stepCheck.outputs.status != 'fetched'
639+
name: 'Building/fetching previous CI target: mathcomp-algebra'
640+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
641+
"coq-8.20" --argstr job "mathcomp-algebra"
642+
- if: steps.stepCheck.outputs.status != 'fetched'
643+
name: 'Building/fetching previous CI target: coq-elpi'
644+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
645+
"coq-8.20" --argstr job "coq-elpi"
646+
- if: steps.stepCheck.outputs.status != 'fetched'
647+
name: 'Building/fetching previous CI target: mathcomp-zify'
648+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
649+
"coq-8.20" --argstr job "mathcomp-zify"
650+
- if: steps.stepCheck.outputs.status != 'fetched'
651+
name: Building/fetching current CI target
652+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
653+
"coq-8.20" --argstr job "mathcomp-algebra-tactics"
575654
mathcomp-analysis:
576655
needs:
577656
- coq
@@ -1651,6 +1730,80 @@ jobs:
16511730
name: Building/fetching current CI target
16521731
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
16531732
"coq-8.20" --argstr job "mathcomp-ssreflect"
1733+
mathcomp-zify:
1734+
needs:
1735+
- coq
1736+
- mathcomp-boot
1737+
- mathcomp-algebra
1738+
- mathcomp-fingroup
1739+
runs-on: ubuntu-latest
1740+
steps:
1741+
- name: Determine which commit to initially checkout
1742+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
1743+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
1744+
}}\" >> $GITHUB_ENV\nfi\n"
1745+
- name: Git checkout
1746+
uses: actions/checkout@v4
1747+
with:
1748+
fetch-depth: 0
1749+
ref: ${{ env.target_commit }}
1750+
- name: Determine which commit to test
1751+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
1752+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
1753+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
1754+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
1755+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
1756+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
1757+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
1758+
\ fi\nfi\n"
1759+
- name: Git checkout
1760+
uses: actions/checkout@v4
1761+
with:
1762+
fetch-depth: 0
1763+
ref: ${{ env.tested_commit }}
1764+
- name: Cachix install
1765+
uses: cachix/install-nix-action@v31
1766+
with:
1767+
nix_path: nixpkgs=channel:nixpkgs-unstable
1768+
- name: Cachix setup coq-elpi
1769+
uses: cachix/cachix-action@v16
1770+
with:
1771+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
1772+
extraPullNames: coq, coq-community, math-comp
1773+
name: coq-elpi
1774+
- id: stepGetDerivation
1775+
name: Getting derivation for current job (mathcomp-zify)
1776+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
1777+
\"coq-8.20\" --argstr job \"mathcomp-zify\" \\\n --dry-run 2> err > out
1778+
|| (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting
1779+
derivation failed\"; exit 1; fi\n"
1780+
- id: stepCheck
1781+
name: Checking presence of CI target for current job
1782+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
1783+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
1784+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
1785+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
1786+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
1787+
- if: steps.stepCheck.outputs.status != 'fetched'
1788+
name: 'Building/fetching previous CI target: coq'
1789+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1790+
"coq-8.20" --argstr job "coq"
1791+
- if: steps.stepCheck.outputs.status != 'fetched'
1792+
name: 'Building/fetching previous CI target: mathcomp-boot'
1793+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1794+
"coq-8.20" --argstr job "mathcomp-boot"
1795+
- if: steps.stepCheck.outputs.status != 'fetched'
1796+
name: 'Building/fetching previous CI target: mathcomp-algebra'
1797+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1798+
"coq-8.20" --argstr job "mathcomp-algebra"
1799+
- if: steps.stepCheck.outputs.status != 'fetched'
1800+
name: 'Building/fetching previous CI target: mathcomp-fingroup'
1801+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1802+
"coq-8.20" --argstr job "mathcomp-fingroup"
1803+
- if: steps.stepCheck.outputs.status != 'fetched'
1804+
name: Building/fetching current CI target
1805+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1806+
"coq-8.20" --argstr job "mathcomp-zify"
16541807
multinomials:
16551808
needs:
16561809
- coq

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

Lines changed: 158 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -521,6 +521,85 @@ jobs:
521521
name: Building/fetching current CI target
522522
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
523523
"coq-master" --argstr job "mathcomp-algebra"
524+
mathcomp-algebra-tactics:
525+
needs:
526+
- coq
527+
- mathcomp-ssreflect
528+
- mathcomp-algebra
529+
- coq-elpi
530+
- mathcomp-zify
531+
runs-on: ubuntu-latest
532+
steps:
533+
- name: Determine which commit to initially checkout
534+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
535+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
536+
}}\" >> $GITHUB_ENV\nfi\n"
537+
- name: Git checkout
538+
uses: actions/checkout@v4
539+
with:
540+
fetch-depth: 0
541+
ref: ${{ env.target_commit }}
542+
- name: Determine which commit to test
543+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
544+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
545+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
546+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
547+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
548+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
549+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
550+
\ fi\nfi\n"
551+
- name: Git checkout
552+
uses: actions/checkout@v4
553+
with:
554+
fetch-depth: 0
555+
ref: ${{ env.tested_commit }}
556+
- name: Cachix install
557+
uses: cachix/install-nix-action@v31
558+
with:
559+
nix_path: nixpkgs=channel:nixpkgs-unstable
560+
- name: Cachix setup coq-elpi
561+
uses: cachix/cachix-action@v16
562+
with:
563+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
564+
extraPullNames: coq, coq-community, math-comp
565+
name: coq-elpi
566+
- id: stepGetDerivation
567+
name: Getting derivation for current job (mathcomp-algebra-tactics)
568+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
569+
\"coq-master\" --argstr job \"mathcomp-algebra-tactics\" \\\n --dry-run
570+
2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo
571+
\"Error: getting derivation failed\"; exit 1; fi\n"
572+
- id: stepCheck
573+
name: Checking presence of CI target for current job
574+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
575+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
576+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
577+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
578+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
579+
- if: steps.stepCheck.outputs.status != 'fetched'
580+
name: 'Building/fetching previous CI target: coq'
581+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
582+
"coq-master" --argstr job "coq"
583+
- if: steps.stepCheck.outputs.status != 'fetched'
584+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
585+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
586+
"coq-master" --argstr job "mathcomp-ssreflect"
587+
- if: steps.stepCheck.outputs.status != 'fetched'
588+
name: 'Building/fetching previous CI target: mathcomp-algebra'
589+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
590+
"coq-master" --argstr job "mathcomp-algebra"
591+
- if: steps.stepCheck.outputs.status != 'fetched'
592+
name: 'Building/fetching previous CI target: coq-elpi'
593+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
594+
"coq-master" --argstr job "coq-elpi"
595+
- if: steps.stepCheck.outputs.status != 'fetched'
596+
name: 'Building/fetching previous CI target: mathcomp-zify'
597+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
598+
"coq-master" --argstr job "mathcomp-zify"
599+
- if: steps.stepCheck.outputs.status != 'fetched'
600+
name: Building/fetching current CI target
601+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
602+
"coq-master" --argstr job "mathcomp-algebra-tactics"
524603
mathcomp-analysis:
525604
needs:
526605
- coq
@@ -1675,6 +1754,85 @@ jobs:
16751754
name: Building/fetching current CI target
16761755
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
16771756
"coq-master" --argstr job "mathcomp-ssreflect"
1757+
mathcomp-zify:
1758+
needs:
1759+
- coq
1760+
- mathcomp-boot
1761+
- mathcomp-algebra
1762+
- mathcomp-fingroup
1763+
- stdlib
1764+
runs-on: ubuntu-latest
1765+
steps:
1766+
- name: Determine which commit to initially checkout
1767+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
1768+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
1769+
}}\" >> $GITHUB_ENV\nfi\n"
1770+
- name: Git checkout
1771+
uses: actions/checkout@v4
1772+
with:
1773+
fetch-depth: 0
1774+
ref: ${{ env.target_commit }}
1775+
- name: Determine which commit to test
1776+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
1777+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
1778+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
1779+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
1780+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
1781+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
1782+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
1783+
\ fi\nfi\n"
1784+
- name: Git checkout
1785+
uses: actions/checkout@v4
1786+
with:
1787+
fetch-depth: 0
1788+
ref: ${{ env.tested_commit }}
1789+
- name: Cachix install
1790+
uses: cachix/install-nix-action@v31
1791+
with:
1792+
nix_path: nixpkgs=channel:nixpkgs-unstable
1793+
- name: Cachix setup coq-elpi
1794+
uses: cachix/cachix-action@v16
1795+
with:
1796+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
1797+
extraPullNames: coq, coq-community, math-comp
1798+
name: coq-elpi
1799+
- id: stepGetDerivation
1800+
name: Getting derivation for current job (mathcomp-zify)
1801+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
1802+
\"coq-master\" --argstr job \"mathcomp-zify\" \\\n --dry-run 2> err > out
1803+
|| (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting
1804+
derivation failed\"; exit 1; fi\n"
1805+
- id: stepCheck
1806+
name: Checking presence of CI target for current job
1807+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
1808+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
1809+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
1810+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
1811+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
1812+
- if: steps.stepCheck.outputs.status != 'fetched'
1813+
name: 'Building/fetching previous CI target: coq'
1814+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1815+
"coq-master" --argstr job "coq"
1816+
- if: steps.stepCheck.outputs.status != 'fetched'
1817+
name: 'Building/fetching previous CI target: mathcomp-boot'
1818+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1819+
"coq-master" --argstr job "mathcomp-boot"
1820+
- if: steps.stepCheck.outputs.status != 'fetched'
1821+
name: 'Building/fetching previous CI target: mathcomp-algebra'
1822+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1823+
"coq-master" --argstr job "mathcomp-algebra"
1824+
- if: steps.stepCheck.outputs.status != 'fetched'
1825+
name: 'Building/fetching previous CI target: mathcomp-fingroup'
1826+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1827+
"coq-master" --argstr job "mathcomp-fingroup"
1828+
- if: steps.stepCheck.outputs.status != 'fetched'
1829+
name: 'Building/fetching previous CI target: stdlib'
1830+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1831+
"coq-master" --argstr job "stdlib"
1832+
- if: steps.stepCheck.outputs.status != 'fetched'
1833+
name: Building/fetching current CI target
1834+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1835+
"coq-master" --argstr job "mathcomp-zify"
16781836
multinomials:
16791837
needs:
16801838
- coq

0 commit comments

Comments
 (0)