Skip to content

Commit 2f03016

Browse files
CohenCyrilgares
CohenCyril
and
gares
authored
Refactoring of the category theory example + removing plan B (#389)
* Refactoring of the category theory example + removing plan B Co-authored-by: Enrico Tassi <[email protected]>
1 parent 3b478ca commit 2f03016

File tree

14 files changed

+541
-995
lines changed

14 files changed

+541
-995
lines changed

‎.github/workflows/main.yml‎

Lines changed: 0 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -31,38 +31,6 @@ jobs:
3131
env:
3232
OPAMWITHTEST: 'true'
3333

34-
plan-B:
35-
runs-on: ubuntu-latest
36-
steps:
37-
- uses: actions/checkout@v2
38-
- uses: coq-community/docker-coq-action@v1
39-
with:
40-
opam_file: './coq-hierarchy-builder.opam'
41-
coq_version: '8.16'
42-
ocaml_version: '4.09-flambda'
43-
script: |
44-
mkdir /home/coq/workspace
45-
cp -ra . /home/coq/workspace
46-
cd /home/coq/workspace
47-
opam install ./coq-hierarchy-builder.opam
48-
sed -i.bak -e "s/-Q . HB//" -e "s|tests/factory_sort_tac.v||" _CoqProject.test-suite
49-
# This is what a user does to cut HB loose
50-
export COQ_ELPI_ATTRIBUTES="hb(log(raw))"
51-
make test-suite -j2
52-
wc -l `find . -name \*.v`
53-
coq.hb patch `find . -name \*.v`
54-
wc -l `find . -name \*.v`
55-
if git diff --quiet; then echo "No patch!"; exit 1; fi
56-
make clean
57-
opam remove coq-hierarchy-builder
58-
opam install ./coq-hierarchy-builder-shim.opam
59-
# Does it work?
60-
make test-suite -j2
61-
# We also test the reset facility works (we rebuild hb locally)
62-
make coq.hb
63-
./coq.hb reset `find . -name \*.v`
64-
mv _CoqProject.test-suite.bak _CoqProject.test-suite
65-
git diff --exit-code
6634

6735
release:
6836
runs-on: ubuntu-latest

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

Lines changed: 0 additions & 122 deletions
Original file line numberDiff line numberDiff line change
@@ -602,62 +602,6 @@ jobs:
602602
name: Building/fetching current CI target
603603
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
604604
--argstr job "hierarchy-builder"
605-
hierarchy-builder-shim:
606-
needs:
607-
- coq
608-
runs-on: ubuntu-latest
609-
steps:
610-
- name: Determine which commit to initially checkout
611-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
612-
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
613-
\ }}\" >> $GITHUB_ENV\nfi\n"
614-
- name: Git checkout
615-
uses: actions/checkout@v3
616-
with:
617-
fetch-depth: 0
618-
ref: ${{ env.target_commit }}
619-
- name: Determine which commit to test
620-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
621-
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
622-
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
623-
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
624-
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
625-
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
626-
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
627-
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
628-
- name: Git checkout
629-
uses: actions/checkout@v3
630-
with:
631-
fetch-depth: 0
632-
ref: ${{ env.tested_commit }}
633-
- name: Cachix install
634-
uses: cachix/install-nix-action@v20
635-
with:
636-
nix_path: nixpkgs=channel:nixpkgs-unstable
637-
- name: Cachix setup math-comp
638-
uses: cachix/cachix-action@v12
639-
with:
640-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
641-
extraPullNames: coq, coq-community
642-
name: math-comp
643-
- id: stepCheck
644-
name: Checking presence of CI target hierarchy-builder-shim
645-
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
646-
\ bundle \"coq-8.16\" --argstr job \"hierarchy-builder-shim\" \\\n --dry-run\
647-
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run\
648-
\ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
649-
- if: steps.stepCheck.outputs.status == 'built'
650-
name: 'Building/fetching previous CI target: coq'
651-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
652-
--argstr job "coq"
653-
- if: steps.stepCheck.outputs.status == 'built'
654-
name: 'Building/fetching previous CI target: coq-elpi'
655-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
656-
--argstr job "coq-elpi"
657-
- if: steps.stepCheck.outputs.status == 'built'
658-
name: Building/fetching current CI target
659-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
660-
--argstr job "hierarchy-builder-shim"
661605
interval:
662606
needs:
663607
- coq
@@ -1274,72 +1218,6 @@ jobs:
12741218
name: Building/fetching current CI target
12751219
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
12761220
--argstr job "mathcomp-single"
1277-
mathcomp-single-planB-src:
1278-
needs:
1279-
- coq
1280-
- hierarchy-builder
1281-
- hierarchy-builder
1282-
runs-on: ubuntu-latest
1283-
steps:
1284-
- name: Determine which commit to initially checkout
1285-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
1286-
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
1287-
\ }}\" >> $GITHUB_ENV\nfi\n"
1288-
- name: Git checkout
1289-
uses: actions/checkout@v3
1290-
with:
1291-
fetch-depth: 0
1292-
ref: ${{ env.target_commit }}
1293-
- name: Determine which commit to test
1294-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
1295-
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
1296-
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
1297-
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
1298-
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
1299-
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
1300-
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
1301-
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
1302-
- name: Git checkout
1303-
uses: actions/checkout@v3
1304-
with:
1305-
fetch-depth: 0
1306-
ref: ${{ env.tested_commit }}
1307-
- name: Cachix install
1308-
uses: cachix/install-nix-action@v20
1309-
with:
1310-
nix_path: nixpkgs=channel:nixpkgs-unstable
1311-
- name: Cachix setup math-comp
1312-
uses: cachix/cachix-action@v12
1313-
with:
1314-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
1315-
extraPullNames: coq, coq-community
1316-
name: math-comp
1317-
- id: stepCheck
1318-
name: Checking presence of CI target mathcomp-single-planB-src
1319-
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
1320-
\ bundle \"coq-8.16\" --argstr job \"mathcomp-single-planB-src\" \\\n --dry-run\
1321-
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run\
1322-
\ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
1323-
- if: steps.stepCheck.outputs.status == 'built'
1324-
name: 'Building/fetching previous CI target: coq'
1325-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
1326-
--argstr job "coq"
1327-
- if: steps.stepCheck.outputs.status == 'built'
1328-
name: 'Building/fetching previous CI target: hierarchy-builder'
1329-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
1330-
--argstr job "hierarchy-builder"
1331-
- if: steps.stepCheck.outputs.status == 'built'
1332-
name: 'Building/fetching previous CI target: coq-elpi'
1333-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
1334-
--argstr job "coq-elpi"
1335-
- if: steps.stepCheck.outputs.status == 'built'
1336-
name: 'Building/fetching previous CI target: hierarchy-builder'
1337-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
1338-
--argstr job "hierarchy-builder"
1339-
- if: steps.stepCheck.outputs.status == 'built'
1340-
name: Building/fetching current CI target
1341-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
1342-
--argstr job "mathcomp-single-planB-src"
13431221
mathcomp-solvable:
13441222
needs:
13451223
- coq

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

Lines changed: 0 additions & 122 deletions
Original file line numberDiff line numberDiff line change
@@ -602,62 +602,6 @@ jobs:
602602
name: Building/fetching current CI target
603603
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17"
604604
--argstr job "hierarchy-builder"
605-
hierarchy-builder-shim:
606-
needs:
607-
- coq
608-
runs-on: ubuntu-latest
609-
steps:
610-
- name: Determine which commit to initially checkout
611-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
612-
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
613-
\ }}\" >> $GITHUB_ENV\nfi\n"
614-
- name: Git checkout
615-
uses: actions/checkout@v3
616-
with:
617-
fetch-depth: 0
618-
ref: ${{ env.target_commit }}
619-
- name: Determine which commit to test
620-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
621-
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
622-
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
623-
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
624-
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
625-
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
626-
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
627-
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
628-
- name: Git checkout
629-
uses: actions/checkout@v3
630-
with:
631-
fetch-depth: 0
632-
ref: ${{ env.tested_commit }}
633-
- name: Cachix install
634-
uses: cachix/install-nix-action@v20
635-
with:
636-
nix_path: nixpkgs=channel:nixpkgs-unstable
637-
- name: Cachix setup math-comp
638-
uses: cachix/cachix-action@v12
639-
with:
640-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
641-
extraPullNames: coq, coq-community
642-
name: math-comp
643-
- id: stepCheck
644-
name: Checking presence of CI target hierarchy-builder-shim
645-
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
646-
\ bundle \"coq-8.17\" --argstr job \"hierarchy-builder-shim\" \\\n --dry-run\
647-
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run\
648-
\ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
649-
- if: steps.stepCheck.outputs.status == 'built'
650-
name: 'Building/fetching previous CI target: coq'
651-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17"
652-
--argstr job "coq"
653-
- if: steps.stepCheck.outputs.status == 'built'
654-
name: 'Building/fetching previous CI target: coq-elpi'
655-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17"
656-
--argstr job "coq-elpi"
657-
- if: steps.stepCheck.outputs.status == 'built'
658-
name: Building/fetching current CI target
659-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17"
660-
--argstr job "hierarchy-builder-shim"
661605
interval:
662606
needs:
663607
- coq
@@ -1274,72 +1218,6 @@ jobs:
12741218
name: Building/fetching current CI target
12751219
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17"
12761220
--argstr job "mathcomp-single"
1277-
mathcomp-single-planB-src:
1278-
needs:
1279-
- coq
1280-
- hierarchy-builder
1281-
- hierarchy-builder
1282-
runs-on: ubuntu-latest
1283-
steps:
1284-
- name: Determine which commit to initially checkout
1285-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
1286-
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
1287-
\ }}\" >> $GITHUB_ENV\nfi\n"
1288-
- name: Git checkout
1289-
uses: actions/checkout@v3
1290-
with:
1291-
fetch-depth: 0
1292-
ref: ${{ env.target_commit }}
1293-
- name: Determine which commit to test
1294-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
1295-
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
1296-
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
1297-
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
1298-
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
1299-
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
1300-
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
1301-
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
1302-
- name: Git checkout
1303-
uses: actions/checkout@v3
1304-
with:
1305-
fetch-depth: 0
1306-
ref: ${{ env.tested_commit }}
1307-
- name: Cachix install
1308-
uses: cachix/install-nix-action@v20
1309-
with:
1310-
nix_path: nixpkgs=channel:nixpkgs-unstable
1311-
- name: Cachix setup math-comp
1312-
uses: cachix/cachix-action@v12
1313-
with:
1314-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
1315-
extraPullNames: coq, coq-community
1316-
name: math-comp
1317-
- id: stepCheck
1318-
name: Checking presence of CI target mathcomp-single-planB-src
1319-
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
1320-
\ bundle \"coq-8.17\" --argstr job \"mathcomp-single-planB-src\" \\\n --dry-run\
1321-
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run\
1322-
\ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
1323-
- if: steps.stepCheck.outputs.status == 'built'
1324-
name: 'Building/fetching previous CI target: coq'
1325-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17"
1326-
--argstr job "coq"
1327-
- if: steps.stepCheck.outputs.status == 'built'
1328-
name: 'Building/fetching previous CI target: hierarchy-builder'
1329-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17"
1330-
--argstr job "hierarchy-builder"
1331-
- if: steps.stepCheck.outputs.status == 'built'
1332-
name: 'Building/fetching previous CI target: coq-elpi'
1333-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17"
1334-
--argstr job "coq-elpi"
1335-
- if: steps.stepCheck.outputs.status == 'built'
1336-
name: 'Building/fetching previous CI target: hierarchy-builder'
1337-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17"
1338-
--argstr job "hierarchy-builder"
1339-
- if: steps.stepCheck.outputs.status == 'built'
1340-
name: Building/fetching current CI target
1341-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17"
1342-
--argstr job "mathcomp-single-planB-src"
13431221
mathcomp-solvable:
13441222
needs:
13451223
- coq

0 commit comments

Comments
 (0)