Skip to content

Commit 05925b1

Browse files
fajbproux01
fajb
authored and
proux01
committed
[zify] Define zify in terms of tify_* tactics
restructure components (isolate tify,zify)
1 parent 0a9bac7 commit 05925b1

23 files changed

Lines changed: 689 additions & 499 deletions

File tree

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

Lines changed: 62 additions & 128 deletions
Original file line numberDiff line numberDiff line change
@@ -1770,70 +1770,6 @@ jobs:
17701770
name: Building/fetching current CI target
17711771
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
17721772
"rocq-9.1" --argstr job "dpdgraph-test"
1773-
equations:
1774-
needs:
1775-
- coq
1776-
- stdlib
1777-
runs-on: ubuntu-latest
1778-
steps:
1779-
- name: Determine which commit to initially checkout
1780-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
1781-
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
1782-
}}\" >> $GITHUB_ENV\nfi\n"
1783-
- name: Git checkout
1784-
uses: actions/checkout@v6
1785-
with:
1786-
fetch-depth: 0
1787-
ref: ${{ env.target_commit }}
1788-
- name: Determine which commit to test
1789-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
1790-
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
1791-
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
1792-
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
1793-
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
1794-
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
1795-
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
1796-
\ fi\nfi\n"
1797-
- name: Git checkout
1798-
uses: actions/checkout@v6
1799-
with:
1800-
fetch-depth: 0
1801-
ref: ${{ env.tested_commit }}
1802-
- name: Cachix install
1803-
uses: cachix/install-nix-action@v31
1804-
with:
1805-
nix_path: nixpkgs=channel:nixpkgs-unstable
1806-
- name: Cachix setup coq
1807-
uses: cachix/cachix-action@v16
1808-
with:
1809-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
1810-
extraPullNames: coq-community, math-comp
1811-
name: coq
1812-
- id: stepGetDerivation
1813-
name: Getting derivation for current job (equations)
1814-
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
1815-
\"rocq-9.1\" --argstr job \"equations\" \\\n --dry-run 2> err > out || (touch
1816-
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
1817-
failed\"; exit 1; fi\n"
1818-
- id: stepCheck
1819-
name: Checking presence of CI target for current job
1820-
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
1821-
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
1822-
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
1823-
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
1824-
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
1825-
- if: steps.stepCheck.outputs.status != 'fetched'
1826-
name: 'Building/fetching previous CI target: coq'
1827-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1828-
"rocq-9.1" --argstr job "coq"
1829-
- if: steps.stepCheck.outputs.status != 'fetched'
1830-
name: 'Building/fetching previous CI target: stdlib'
1831-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1832-
"rocq-9.1" --argstr job "stdlib"
1833-
- if: steps.stepCheck.outputs.status != 'fetched'
1834-
name: Building/fetching current CI target
1835-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1836-
"rocq-9.1" --argstr job "equations"
18371773
fcsl-pcm:
18381774
needs:
18391775
- coq
@@ -2441,6 +2377,7 @@ jobs:
24412377
- mathcomp-order
24422378
- mathcomp-fingroup
24432379
- hierarchy-builder
2380+
- micromega-plugin
24442381
runs-on: ubuntu-latest
24452382
steps:
24462383
- name: Determine which commit to initially checkout
@@ -3586,6 +3523,65 @@ jobs:
35863523
name: Building/fetching current CI target
35873524
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
35883525
"rocq-9.1" --argstr job "mathcomp-zify"
3526+
micromega-plugin:
3527+
needs:
3528+
- rocq-core
3529+
runs-on: ubuntu-latest
3530+
steps:
3531+
- name: Determine which commit to initially checkout
3532+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
3533+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
3534+
}}\" >> $GITHUB_ENV\nfi\n"
3535+
- name: Git checkout
3536+
uses: actions/checkout@v6
3537+
with:
3538+
fetch-depth: 0
3539+
ref: ${{ env.target_commit }}
3540+
- name: Determine which commit to test
3541+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
3542+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
3543+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
3544+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
3545+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
3546+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
3547+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
3548+
\ fi\nfi\n"
3549+
- name: Git checkout
3550+
uses: actions/checkout@v6
3551+
with:
3552+
fetch-depth: 0
3553+
ref: ${{ env.tested_commit }}
3554+
- name: Cachix install
3555+
uses: cachix/install-nix-action@v31
3556+
with:
3557+
nix_path: nixpkgs=channel:nixpkgs-unstable
3558+
- name: Cachix setup coq
3559+
uses: cachix/cachix-action@v16
3560+
with:
3561+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
3562+
extraPullNames: coq-community, math-comp
3563+
name: coq
3564+
- id: stepGetDerivation
3565+
name: Getting derivation for current job (micromega-plugin)
3566+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
3567+
\"rocq-9.1\" --argstr job \"micromega-plugin\" \\\n --dry-run 2> err > out
3568+
|| (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting
3569+
derivation failed\"; exit 1; fi\n"
3570+
- id: stepCheck
3571+
name: Checking presence of CI target for current job
3572+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
3573+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
3574+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
3575+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
3576+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
3577+
- if: steps.stepCheck.outputs.status != 'fetched'
3578+
name: 'Building/fetching previous CI target: rocq-core'
3579+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3580+
"rocq-9.1" --argstr job "rocq-core"
3581+
- if: steps.stepCheck.outputs.status != 'fetched'
3582+
name: Building/fetching current CI target
3583+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3584+
"rocq-9.1" --argstr job "micromega-plugin"
35893585
mtac2:
35903586
needs:
35913587
- coq
@@ -4359,70 +4355,6 @@ jobs:
43594355
name: Building/fetching current CI target
43604356
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
43614357
"rocq-9.1" --argstr job "simple-io"
4362-
smtcoq:
4363-
needs:
4364-
- coq
4365-
- stdlib
4366-
runs-on: ubuntu-latest
4367-
steps:
4368-
- name: Determine which commit to initially checkout
4369-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
4370-
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
4371-
}}\" >> $GITHUB_ENV\nfi\n"
4372-
- name: Git checkout
4373-
uses: actions/checkout@v6
4374-
with:
4375-
fetch-depth: 0
4376-
ref: ${{ env.target_commit }}
4377-
- name: Determine which commit to test
4378-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
4379-
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
4380-
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
4381-
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
4382-
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
4383-
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
4384-
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
4385-
\ fi\nfi\n"
4386-
- name: Git checkout
4387-
uses: actions/checkout@v6
4388-
with:
4389-
fetch-depth: 0
4390-
ref: ${{ env.tested_commit }}
4391-
- name: Cachix install
4392-
uses: cachix/install-nix-action@v31
4393-
with:
4394-
nix_path: nixpkgs=channel:nixpkgs-unstable
4395-
- name: Cachix setup coq
4396-
uses: cachix/cachix-action@v16
4397-
with:
4398-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
4399-
extraPullNames: coq-community, math-comp
4400-
name: coq
4401-
- id: stepGetDerivation
4402-
name: Getting derivation for current job (smtcoq)
4403-
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
4404-
\"rocq-9.1\" --argstr job \"smtcoq\" \\\n --dry-run 2> err > out || (touch
4405-
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
4406-
failed\"; exit 1; fi\n"
4407-
- id: stepCheck
4408-
name: Checking presence of CI target for current job
4409-
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
4410-
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
4411-
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
4412-
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
4413-
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
4414-
- if: steps.stepCheck.outputs.status != 'fetched'
4415-
name: 'Building/fetching previous CI target: coq'
4416-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
4417-
"rocq-9.1" --argstr job "coq"
4418-
- if: steps.stepCheck.outputs.status != 'fetched'
4419-
name: 'Building/fetching previous CI target: stdlib'
4420-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
4421-
"rocq-9.1" --argstr job "stdlib"
4422-
- if: steps.stepCheck.outputs.status != 'fetched'
4423-
name: Building/fetching current CI target
4424-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
4425-
"rocq-9.1" --argstr job "smtcoq"
44264358
stalmarck:
44274359
needs:
44284360
- coq
@@ -4554,6 +4486,7 @@ jobs:
45544486
stdlib:
45554487
needs:
45564488
- rocq-core
4489+
- micromega-plugin
45574490
runs-on: ubuntu-latest
45584491
steps:
45594492
- name: Determine which commit to initially checkout
@@ -4618,6 +4551,7 @@ jobs:
46184551
needs:
46194552
- rocq-core
46204553
- stdlib
4554+
- micromega-plugin
46214555
runs-on: ubuntu-latest
46224556
steps:
46234557
- name: Determine which commit to initially checkout

0 commit comments

Comments
 (0)