Skip to content

Commit 60964d3

Browse files
proux01proux01
committed
1 parent c6debec commit 60964d3

File tree

2 files changed

+2
-163
lines changed

2 files changed

+2
-163
lines changed

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

Lines changed: 0 additions & 163 deletions
Original file line numberDiff line numberDiff line change
@@ -234,80 +234,6 @@ jobs:
234234
name: Building/fetching current CI target
235235
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
236236
"coq-8.20" --argstr job "coq-elpi-tests-stdlib"
237-
coqeal:
238-
needs:
239-
- coq
240-
- mathcomp-algebra
241-
- multinomials
242-
- mathcomp-real-closed
243-
runs-on: ubuntu-latest
244-
steps:
245-
- name: Determine which commit to initially checkout
246-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
247-
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
248-
}}\" >> $GITHUB_ENV\nfi\n"
249-
- name: Git checkout
250-
uses: actions/checkout@v4
251-
with:
252-
fetch-depth: 0
253-
ref: ${{ env.target_commit }}
254-
- name: Determine which commit to test
255-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
256-
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
257-
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
258-
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
259-
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
260-
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
261-
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
262-
\ fi\nfi\n"
263-
- name: Git checkout
264-
uses: actions/checkout@v4
265-
with:
266-
fetch-depth: 0
267-
ref: ${{ env.tested_commit }}
268-
- name: Cachix install
269-
uses: cachix/install-nix-action@v31
270-
with:
271-
nix_path: nixpkgs=channel:nixpkgs-unstable
272-
- name: Cachix setup coq-elpi
273-
uses: cachix/cachix-action@v16
274-
with:
275-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
276-
extraPullNames: coq, coq-community, math-comp
277-
name: coq-elpi
278-
- id: stepGetDerivation
279-
name: Getting derivation for current job (coqeal)
280-
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
281-
\"coq-8.20\" --argstr job \"coqeal\" \\\n --dry-run 2> err > out || (touch
282-
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
283-
failed\"; exit 1; fi\n"
284-
- id: stepCheck
285-
name: Checking presence of CI target for current job
286-
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
287-
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
288-
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
289-
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
290-
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
291-
- if: steps.stepCheck.outputs.status != 'fetched'
292-
name: 'Building/fetching previous CI target: coq'
293-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
294-
"coq-8.20" --argstr job "coq"
295-
- if: steps.stepCheck.outputs.status != 'fetched'
296-
name: 'Building/fetching previous CI target: mathcomp-algebra'
297-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
298-
"coq-8.20" --argstr job "mathcomp-algebra"
299-
- if: steps.stepCheck.outputs.status != 'fetched'
300-
name: 'Building/fetching previous CI target: multinomials'
301-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
302-
"coq-8.20" --argstr job "multinomials"
303-
- if: steps.stepCheck.outputs.status != 'fetched'
304-
name: 'Building/fetching previous CI target: mathcomp-real-closed'
305-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
306-
"coq-8.20" --argstr job "mathcomp-real-closed"
307-
- if: steps.stepCheck.outputs.status != 'fetched'
308-
name: Building/fetching current CI target
309-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
310-
"coq-8.20" --argstr job "coqeal"
311237
corn:
312238
needs:
313239
- coq
@@ -1380,95 +1306,6 @@ jobs:
13801306
name: Building/fetching current CI target
13811307
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
13821308
"coq-8.20" --argstr job "mathcomp-order"
1383-
mathcomp-real-closed:
1384-
needs:
1385-
- coq
1386-
- mathcomp-ssreflect
1387-
- mathcomp-algebra
1388-
- mathcomp-field
1389-
- mathcomp-fingroup
1390-
- mathcomp-solvable
1391-
- mathcomp-bigenough
1392-
runs-on: ubuntu-latest
1393-
steps:
1394-
- name: Determine which commit to initially checkout
1395-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
1396-
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
1397-
}}\" >> $GITHUB_ENV\nfi\n"
1398-
- name: Git checkout
1399-
uses: actions/checkout@v4
1400-
with:
1401-
fetch-depth: 0
1402-
ref: ${{ env.target_commit }}
1403-
- name: Determine which commit to test
1404-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
1405-
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
1406-
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
1407-
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
1408-
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
1409-
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
1410-
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
1411-
\ fi\nfi\n"
1412-
- name: Git checkout
1413-
uses: actions/checkout@v4
1414-
with:
1415-
fetch-depth: 0
1416-
ref: ${{ env.tested_commit }}
1417-
- name: Cachix install
1418-
uses: cachix/install-nix-action@v31
1419-
with:
1420-
nix_path: nixpkgs=channel:nixpkgs-unstable
1421-
- name: Cachix setup coq-elpi
1422-
uses: cachix/cachix-action@v16
1423-
with:
1424-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
1425-
extraPullNames: coq, coq-community, math-comp
1426-
name: coq-elpi
1427-
- id: stepGetDerivation
1428-
name: Getting derivation for current job (mathcomp-real-closed)
1429-
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
1430-
\"coq-8.20\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run 2> err
1431-
> out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error:
1432-
getting derivation failed\"; exit 1; fi\n"
1433-
- id: stepCheck
1434-
name: Checking presence of CI target for current job
1435-
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
1436-
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
1437-
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
1438-
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
1439-
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
1440-
- if: steps.stepCheck.outputs.status != 'fetched'
1441-
name: 'Building/fetching previous CI target: coq'
1442-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1443-
"coq-8.20" --argstr job "coq"
1444-
- if: steps.stepCheck.outputs.status != 'fetched'
1445-
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
1446-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1447-
"coq-8.20" --argstr job "mathcomp-ssreflect"
1448-
- if: steps.stepCheck.outputs.status != 'fetched'
1449-
name: 'Building/fetching previous CI target: mathcomp-algebra'
1450-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1451-
"coq-8.20" --argstr job "mathcomp-algebra"
1452-
- if: steps.stepCheck.outputs.status != 'fetched'
1453-
name: 'Building/fetching previous CI target: mathcomp-field'
1454-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1455-
"coq-8.20" --argstr job "mathcomp-field"
1456-
- if: steps.stepCheck.outputs.status != 'fetched'
1457-
name: 'Building/fetching previous CI target: mathcomp-fingroup'
1458-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1459-
"coq-8.20" --argstr job "mathcomp-fingroup"
1460-
- if: steps.stepCheck.outputs.status != 'fetched'
1461-
name: 'Building/fetching previous CI target: mathcomp-solvable'
1462-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1463-
"coq-8.20" --argstr job "mathcomp-solvable"
1464-
- if: steps.stepCheck.outputs.status != 'fetched'
1465-
name: 'Building/fetching previous CI target: mathcomp-bigenough'
1466-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1467-
"coq-8.20" --argstr job "mathcomp-bigenough"
1468-
- if: steps.stepCheck.outputs.status != 'fetched'
1469-
name: Building/fetching current CI target
1470-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1471-
"coq-8.20" --argstr job "mathcomp-real-closed"
14721309
mathcomp-reals:
14731310
needs:
14741311
- coq

‎.nix/config.nix‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,8 @@ let master = [
6464
coq.override.version = "8.20";
6565
coq-elpi.override.elpi-version = "v3.1.0";
6666
odd-order.job = false; # no longer supported since https://github.com/math-comp/odd-order/pull/74
67+
mathcomp-real-closed.job = false; # real-closed dropped support for 8.20
68+
coqeal.job = false; # real-closed dropped support for 8.20
6769
};
6870

6971
"rocq-9.0" = { rocqPackages = rocq-common-bundles // {

0 commit comments

Comments
 (0)