Skip to content

Commit add2c2b

Browse files
garesgares
authored
Merge pull request #767 from proux01/split-stdlib
Remove Stdlib dependency
2 parents c95de28 + 7e98f1a commit add2c2b

File tree

129 files changed

+1325
-223
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

129 files changed

+1325
-223
lines changed

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

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -189,6 +189,7 @@ jobs:
189189
coq-elpi:
190190
needs:
191191
- coq
192+
- stdlib
192193
runs-on: ubuntu-latest
193194
steps:
194195
- name: Determine which commit to initially checkout
@@ -248,6 +249,64 @@ jobs:
248249
name: Building/fetching current CI target
249250
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
250251
--argstr job "coq-elpi"
252+
coq-elpi-tests:
253+
needs:
254+
- coq
255+
runs-on: ubuntu-latest
256+
steps:
257+
- name: Determine which commit to initially checkout
258+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
259+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
260+
}}\" >> $GITHUB_ENV\nfi\n"
261+
- name: Git checkout
262+
uses: actions/checkout@v4
263+
with:
264+
fetch-depth: 0
265+
ref: ${{ env.target_commit }}
266+
- name: Determine which commit to test
267+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
268+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
269+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
270+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
271+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
272+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
273+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
274+
\ fi\nfi\n"
275+
- name: Git checkout
276+
uses: actions/checkout@v4
277+
with:
278+
fetch-depth: 0
279+
ref: ${{ env.tested_commit }}
280+
- name: Cachix install
281+
uses: cachix/install-nix-action@v30
282+
with:
283+
nix_path: nixpkgs=channel:nixpkgs-unstable
284+
- name: Cachix setup coq-elpi
285+
uses: cachix/cachix-action@v15
286+
with:
287+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
288+
extraPullNames: coq, coq-community, math-comp
289+
name: coq-elpi
290+
- id: stepGetDerivation
291+
name: Getting derivation for current job (coq-elpi-tests)
292+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
293+
\"coq-8.20\" --argstr job \"coq-elpi-tests\" \\\n --dry-run 2> err > out
294+
|| (touch fail; true)\n"
295+
- name: Error reporting
296+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
297+
- name: Failure check
298+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
299+
- id: stepCheck
300+
name: Checking presence of CI target for current job
301+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
302+
- if: steps.stepCheck.outputs.status == 'built'
303+
name: 'Building/fetching previous CI target: coq'
304+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
305+
--argstr job "coq"
306+
- if: steps.stepCheck.outputs.status == 'built'
307+
name: Building/fetching current CI target
308+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
309+
--argstr job "coq-elpi-tests"
251310
coqeal:
252311
needs:
253312
- coq
@@ -535,6 +594,7 @@ jobs:
535594
mathcomp:
536595
needs:
537596
- coq
597+
- stdlib
538598
- mathcomp-ssreflect
539599
- mathcomp-fingroup
540600
- mathcomp-algebra
@@ -632,6 +692,7 @@ jobs:
632692
mathcomp-algebra:
633693
needs:
634694
- coq
695+
- stdlib
635696
- mathcomp-ssreflect
636697
- mathcomp-fingroup
637698
- hierarchy-builder
@@ -923,6 +984,7 @@ jobs:
923984
mathcomp-character:
924985
needs:
925986
- coq
987+
- stdlib
926988
- mathcomp-ssreflect
927989
- mathcomp-fingroup
928990
- mathcomp-algebra
@@ -1161,6 +1223,7 @@ jobs:
11611223
mathcomp-field:
11621224
needs:
11631225
- coq
1226+
- stdlib
11641227
- mathcomp-ssreflect
11651228
- mathcomp-fingroup
11661229
- mathcomp-algebra
@@ -1248,6 +1311,7 @@ jobs:
12481311
mathcomp-fingroup:
12491312
needs:
12501313
- coq
1314+
- stdlib
12511315
- mathcomp-ssreflect
12521316
- hierarchy-builder
12531317
runs-on: ubuntu-latest
@@ -1607,6 +1671,7 @@ jobs:
16071671
mathcomp-solvable:
16081672
needs:
16091673
- coq
1674+
- stdlib
16101675
- mathcomp-ssreflect
16111676
- mathcomp-fingroup
16121677
- mathcomp-algebra
@@ -1689,6 +1754,7 @@ jobs:
16891754
mathcomp-ssreflect:
16901755
needs:
16911756
- coq
1757+
- stdlib
16921758
- hierarchy-builder
16931759
runs-on: ubuntu-latest
16941760
steps:
@@ -1996,6 +2062,64 @@ jobs:
19962062
name: Building/fetching current CI target
19972063
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
19982064
--argstr job "relation-algebra"
2065+
stdlib:
2066+
needs:
2067+
- coq
2068+
runs-on: ubuntu-latest
2069+
steps:
2070+
- name: Determine which commit to initially checkout
2071+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
2072+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
2073+
}}\" >> $GITHUB_ENV\nfi\n"
2074+
- name: Git checkout
2075+
uses: actions/checkout@v4
2076+
with:
2077+
fetch-depth: 0
2078+
ref: ${{ env.target_commit }}
2079+
- name: Determine which commit to test
2080+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
2081+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
2082+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
2083+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
2084+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
2085+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
2086+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
2087+
\ fi\nfi\n"
2088+
- name: Git checkout
2089+
uses: actions/checkout@v4
2090+
with:
2091+
fetch-depth: 0
2092+
ref: ${{ env.tested_commit }}
2093+
- name: Cachix install
2094+
uses: cachix/install-nix-action@v30
2095+
with:
2096+
nix_path: nixpkgs=channel:nixpkgs-unstable
2097+
- name: Cachix setup coq-elpi
2098+
uses: cachix/cachix-action@v15
2099+
with:
2100+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
2101+
extraPullNames: coq, coq-community, math-comp
2102+
name: coq-elpi
2103+
- id: stepGetDerivation
2104+
name: Getting derivation for current job (stdlib)
2105+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
2106+
\"coq-8.20\" --argstr job \"stdlib\" \\\n --dry-run 2> err > out || (touch
2107+
fail; true)\n"
2108+
- name: Error reporting
2109+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
2110+
- name: Failure check
2111+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
2112+
- id: stepCheck
2113+
name: Checking presence of CI target for current job
2114+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
2115+
- if: steps.stepCheck.outputs.status == 'built'
2116+
name: 'Building/fetching previous CI target: coq'
2117+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
2118+
--argstr job "coq"
2119+
- if: steps.stepCheck.outputs.status == 'built'
2120+
name: Building/fetching current CI target
2121+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
2122+
--argstr job "stdlib"
19992123
name: Nix CI for bundle coq-8.20
20002124
on:
20012125
pull_request:

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

Lines changed: 179 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -178,6 +178,185 @@ jobs:
178178
name: Building/fetching current CI target
179179
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
180180
--argstr job "coq-elpi"
181+
coq-elpi-no-stdlib:
182+
needs:
183+
- coq
184+
runs-on: ubuntu-latest
185+
steps:
186+
- name: Determine which commit to initially checkout
187+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
188+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
189+
}}\" >> $GITHUB_ENV\nfi\n"
190+
- name: Git checkout
191+
uses: actions/checkout@v4
192+
with:
193+
fetch-depth: 0
194+
ref: ${{ env.target_commit }}
195+
- name: Determine which commit to test
196+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
197+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
198+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
199+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
200+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
201+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
202+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
203+
\ fi\nfi\n"
204+
- name: Git checkout
205+
uses: actions/checkout@v4
206+
with:
207+
fetch-depth: 0
208+
ref: ${{ env.tested_commit }}
209+
- name: Cachix install
210+
uses: cachix/install-nix-action@v30
211+
with:
212+
nix_path: nixpkgs=channel:nixpkgs-unstable
213+
- name: Cachix setup coq-elpi
214+
uses: cachix/cachix-action@v15
215+
with:
216+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
217+
extraPullNames: coq, coq-community, math-comp
218+
name: coq-elpi
219+
- id: stepGetDerivation
220+
name: Getting derivation for current job (coq-elpi-no-stdlib)
221+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
222+
\"coq-master\" --argstr job \"coq-elpi-no-stdlib\" \\\n --dry-run 2> err
223+
> out || (touch fail; true)\n"
224+
- name: Error reporting
225+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
226+
- name: Failure check
227+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
228+
- id: stepCheck
229+
name: Checking presence of CI target for current job
230+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
231+
- if: steps.stepCheck.outputs.status == 'built'
232+
name: 'Building/fetching previous CI target: coq'
233+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
234+
--argstr job "coq"
235+
- if: steps.stepCheck.outputs.status == 'built'
236+
name: Building/fetching current CI target
237+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
238+
--argstr job "coq-elpi-no-stdlib"
239+
coq-elpi-tests:
240+
needs:
241+
- coq
242+
runs-on: ubuntu-latest
243+
steps:
244+
- name: Determine which commit to initially checkout
245+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
246+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
247+
}}\" >> $GITHUB_ENV\nfi\n"
248+
- name: Git checkout
249+
uses: actions/checkout@v4
250+
with:
251+
fetch-depth: 0
252+
ref: ${{ env.target_commit }}
253+
- name: Determine which commit to test
254+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
255+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
256+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
257+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
258+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
259+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
260+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
261+
\ fi\nfi\n"
262+
- name: Git checkout
263+
uses: actions/checkout@v4
264+
with:
265+
fetch-depth: 0
266+
ref: ${{ env.tested_commit }}
267+
- name: Cachix install
268+
uses: cachix/install-nix-action@v30
269+
with:
270+
nix_path: nixpkgs=channel:nixpkgs-unstable
271+
- name: Cachix setup coq-elpi
272+
uses: cachix/cachix-action@v15
273+
with:
274+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
275+
extraPullNames: coq, coq-community, math-comp
276+
name: coq-elpi
277+
- id: stepGetDerivation
278+
name: Getting derivation for current job (coq-elpi-tests)
279+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
280+
\"coq-master\" --argstr job \"coq-elpi-tests\" \\\n --dry-run 2> err > out
281+
|| (touch fail; true)\n"
282+
- name: Error reporting
283+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
284+
- name: Failure check
285+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
286+
- id: stepCheck
287+
name: Checking presence of CI target for current job
288+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
289+
- if: steps.stepCheck.outputs.status == 'built'
290+
name: 'Building/fetching previous CI target: coq'
291+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
292+
--argstr job "coq"
293+
- if: steps.stepCheck.outputs.status == 'built'
294+
name: Building/fetching current CI target
295+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
296+
--argstr job "coq-elpi-tests"
297+
coq-elpi-tests-stdlib:
298+
needs:
299+
- coq
300+
- stdlib
301+
runs-on: ubuntu-latest
302+
steps:
303+
- name: Determine which commit to initially checkout
304+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
305+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
306+
}}\" >> $GITHUB_ENV\nfi\n"
307+
- name: Git checkout
308+
uses: actions/checkout@v4
309+
with:
310+
fetch-depth: 0
311+
ref: ${{ env.target_commit }}
312+
- name: Determine which commit to test
313+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
314+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
315+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
316+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
317+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
318+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
319+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
320+
\ fi\nfi\n"
321+
- name: Git checkout
322+
uses: actions/checkout@v4
323+
with:
324+
fetch-depth: 0
325+
ref: ${{ env.tested_commit }}
326+
- name: Cachix install
327+
uses: cachix/install-nix-action@v30
328+
with:
329+
nix_path: nixpkgs=channel:nixpkgs-unstable
330+
- name: Cachix setup coq-elpi
331+
uses: cachix/cachix-action@v15
332+
with:
333+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
334+
extraPullNames: coq, coq-community, math-comp
335+
name: coq-elpi
336+
- id: stepGetDerivation
337+
name: Getting derivation for current job (coq-elpi-tests-stdlib)
338+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
339+
\"coq-master\" --argstr job \"coq-elpi-tests-stdlib\" \\\n --dry-run 2>
340+
err > out || (touch fail; true)\n"
341+
- name: Error reporting
342+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
343+
- name: Failure check
344+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
345+
- id: stepCheck
346+
name: Checking presence of CI target for current job
347+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
348+
- if: steps.stepCheck.outputs.status == 'built'
349+
name: 'Building/fetching previous CI target: coq'
350+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
351+
--argstr job "coq"
352+
- if: steps.stepCheck.outputs.status == 'built'
353+
name: 'Building/fetching previous CI target: stdlib'
354+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
355+
--argstr job "stdlib"
356+
- if: steps.stepCheck.outputs.status == 'built'
357+
name: Building/fetching current CI target
358+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
359+
--argstr job "coq-elpi-tests-stdlib"
181360
coqeal:
182361
needs:
183362
- coq

0 commit comments

Comments
 (0)