Skip to content

Commit baafd50

Browse files
mkerjeanmkerjean
authored
Merge branch 'master' into linear_continuous
2 parents 9f17c34 + bd05c57 commit baafd50

108 files changed

Lines changed: 2365 additions & 2506 deletions

File tree

Some content is hidden

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

‎.github/workflows/deploy-docs-gh-pages.yml‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -28,10 +28,7 @@ jobs:
2828
default: https://github.com/ocaml/opam-repository.git
2929
3030
- name: Build Mathcomp Analysis
31-
run: opam install -y --deps-only . && opam exec -- make -j 4
32-
33-
- name: Install Rocqnavi
34-
run: opam install -y rocq-navi.0.3.1
31+
run: opam install -y --deps-only . --with-doc && opam exec -- make -j 4
3532

3633
- name: Generate Documents
3734
run: opam exec -- make html

‎.github/workflows/generate_docs.yml‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -35,10 +35,7 @@ jobs:
3535
default: https://github.com/ocaml/opam-repository.git
3636
3737
- name: Build Mathcomp Analysis
38-
run: opam install -y --deps-only . && opam exec -- make -j 4
39-
40-
- name: Install Rocqnavi
41-
run: opam install -y rocq-navi.0.3.1
38+
run: opam install -y --deps-only . --with-doc && opam exec -- make -j 4
4239

4340
- name: Generate Documents
4441
run: |

.github/workflows/nix-action-9.0-2.4.0.yml renamed to .github/workflows/nix-action-9.0-2.5.0.yml

Lines changed: 93 additions & 109 deletions
Large diffs are not rendered by default.

‎.github/workflows/nix-action-9.0.yml‎

Lines changed: 21 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ jobs:
6060
--argstr job "coq"
6161
mathcomp-analysis:
6262
needs:
63-
- coq
63+
- rocq-core
6464
- mathcomp-reals
6565
runs-on: ubuntu-latest
6666
steps:
@@ -111,9 +111,9 @@ jobs:
111111
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
112112
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
113113
- if: steps.stepCheck.outputs.status != 'fetched'
114-
name: 'Building/fetching previous CI target: coq'
114+
name: 'Building/fetching previous CI target: rocq-core'
115115
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
116-
--argstr job "coq"
116+
--argstr job "rocq-core"
117117
- if: steps.stepCheck.outputs.status != 'fetched'
118118
name: 'Building/fetching previous CI target: mathcomp-reals'
119119
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
@@ -126,17 +126,13 @@ jobs:
126126
name: 'Building/fetching previous CI target: mathcomp-bigenough'
127127
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
128128
--argstr job "mathcomp-bigenough"
129-
- if: steps.stepCheck.outputs.status != 'fetched'
130-
name: 'Building/fetching previous CI target: hierarchy-builder'
131-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
132-
--argstr job "hierarchy-builder"
133129
- if: steps.stepCheck.outputs.status != 'fetched'
134130
name: Building/fetching current CI target
135131
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
136132
--argstr job "mathcomp-analysis"
137133
mathcomp-analysis-single:
138134
needs:
139-
- coq
135+
- rocq-core
140136
runs-on: ubuntu-latest
141137
steps:
142138
- name: Determine which commit to initially checkout
@@ -186,13 +182,9 @@ jobs:
186182
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
187183
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
188184
- if: steps.stepCheck.outputs.status != 'fetched'
189-
name: 'Building/fetching previous CI target: coq'
190-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
191-
--argstr job "coq"
192-
- if: steps.stepCheck.outputs.status != 'fetched'
193-
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
185+
name: 'Building/fetching previous CI target: rocq-core'
194186
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
195-
--argstr job "mathcomp-ssreflect"
187+
--argstr job "rocq-core"
196188
- if: steps.stepCheck.outputs.status != 'fetched'
197189
name: 'Building/fetching previous CI target: mathcomp-algebra'
198190
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
@@ -217,17 +209,13 @@ jobs:
217209
name: 'Building/fetching previous CI target: stdlib'
218210
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
219211
--argstr job "stdlib"
220-
- if: steps.stepCheck.outputs.status != 'fetched'
221-
name: 'Building/fetching previous CI target: hierarchy-builder'
222-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
223-
--argstr job "hierarchy-builder"
224212
- if: steps.stepCheck.outputs.status != 'fetched'
225213
name: Building/fetching current CI target
226214
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
227215
--argstr job "mathcomp-analysis-single"
228216
mathcomp-analysis-stdlib:
229217
needs:
230-
- coq
218+
- rocq-core
231219
- mathcomp-analysis
232220
- mathcomp-reals-stdlib
233221
runs-on: ubuntu-latest
@@ -279,9 +267,9 @@ jobs:
279267
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
280268
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
281269
- if: steps.stepCheck.outputs.status != 'fetched'
282-
name: 'Building/fetching previous CI target: coq'
270+
name: 'Building/fetching previous CI target: rocq-core'
283271
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
284-
--argstr job "coq"
272+
--argstr job "rocq-core"
285273
- if: steps.stepCheck.outputs.status != 'fetched'
286274
name: 'Building/fetching previous CI target: mathcomp-analysis'
287275
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
@@ -294,17 +282,13 @@ jobs:
294282
name: 'Building/fetching previous CI target: stdlib'
295283
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
296284
--argstr job "stdlib"
297-
- if: steps.stepCheck.outputs.status != 'fetched'
298-
name: 'Building/fetching previous CI target: hierarchy-builder'
299-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
300-
--argstr job "hierarchy-builder"
301285
- if: steps.stepCheck.outputs.status != 'fetched'
302286
name: Building/fetching current CI target
303287
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
304288
--argstr job "mathcomp-analysis-stdlib"
305289
mathcomp-classical:
306290
needs:
307-
- coq
291+
- rocq-core
308292
runs-on: ubuntu-latest
309293
steps:
310294
- name: Determine which commit to initially checkout
@@ -354,13 +338,9 @@ jobs:
354338
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
355339
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
356340
- if: steps.stepCheck.outputs.status != 'fetched'
357-
name: 'Building/fetching previous CI target: coq'
358-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
359-
--argstr job "coq"
360-
- if: steps.stepCheck.outputs.status != 'fetched'
361-
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
341+
name: 'Building/fetching previous CI target: rocq-core'
362342
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
363-
--argstr job "mathcomp-ssreflect"
343+
--argstr job "rocq-core"
364344
- if: steps.stepCheck.outputs.status != 'fetched'
365345
name: 'Building/fetching previous CI target: mathcomp-algebra'
366346
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
@@ -369,17 +349,13 @@ jobs:
369349
name: 'Building/fetching previous CI target: mathcomp-finmap'
370350
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
371351
--argstr job "mathcomp-finmap"
372-
- if: steps.stepCheck.outputs.status != 'fetched'
373-
name: 'Building/fetching previous CI target: hierarchy-builder'
374-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
375-
--argstr job "hierarchy-builder"
376352
- if: steps.stepCheck.outputs.status != 'fetched'
377353
name: Building/fetching current CI target
378354
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
379355
--argstr job "mathcomp-classical"
380356
mathcomp-experimental-reals:
381357
needs:
382-
- coq
358+
- rocq-core
383359
- mathcomp-reals
384360
runs-on: ubuntu-latest
385361
steps:
@@ -430,9 +406,9 @@ jobs:
430406
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
431407
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
432408
- if: steps.stepCheck.outputs.status != 'fetched'
433-
name: 'Building/fetching previous CI target: coq'
409+
name: 'Building/fetching previous CI target: rocq-core'
434410
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
435-
--argstr job "coq"
411+
--argstr job "rocq-core"
436412
- if: steps.stepCheck.outputs.status != 'fetched'
437413
name: 'Building/fetching previous CI target: mathcomp-reals'
438414
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
@@ -441,10 +417,6 @@ jobs:
441417
name: 'Building/fetching previous CI target: mathcomp-bigenough'
442418
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
443419
--argstr job "mathcomp-bigenough"
444-
- if: steps.stepCheck.outputs.status != 'fetched'
445-
name: 'Building/fetching previous CI target: hierarchy-builder'
446-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
447-
--argstr job "hierarchy-builder"
448420
- if: steps.stepCheck.outputs.status != 'fetched'
449421
name: Building/fetching current CI target
450422
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
@@ -523,7 +495,7 @@ jobs:
523495
--argstr job "mathcomp-infotheo"
524496
mathcomp-reals:
525497
needs:
526-
- coq
498+
- rocq-core
527499
- mathcomp-classical
528500
runs-on: ubuntu-latest
529501
steps:
@@ -574,24 +546,20 @@ jobs:
574546
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
575547
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
576548
- if: steps.stepCheck.outputs.status != 'fetched'
577-
name: 'Building/fetching previous CI target: coq'
549+
name: 'Building/fetching previous CI target: rocq-core'
578550
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
579-
--argstr job "coq"
551+
--argstr job "rocq-core"
580552
- if: steps.stepCheck.outputs.status != 'fetched'
581553
name: 'Building/fetching previous CI target: mathcomp-classical'
582554
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
583555
--argstr job "mathcomp-classical"
584-
- if: steps.stepCheck.outputs.status != 'fetched'
585-
name: 'Building/fetching previous CI target: hierarchy-builder'
586-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
587-
--argstr job "hierarchy-builder"
588556
- if: steps.stepCheck.outputs.status != 'fetched'
589557
name: Building/fetching current CI target
590558
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
591559
--argstr job "mathcomp-reals"
592560
mathcomp-reals-stdlib:
593561
needs:
594-
- coq
562+
- rocq-core
595563
- mathcomp-reals
596564
runs-on: ubuntu-latest
597565
steps:
@@ -642,9 +610,9 @@ jobs:
642610
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
643611
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
644612
- if: steps.stepCheck.outputs.status != 'fetched'
645-
name: 'Building/fetching previous CI target: coq'
613+
name: 'Building/fetching previous CI target: rocq-core'
646614
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
647-
--argstr job "coq"
615+
--argstr job "rocq-core"
648616
- if: steps.stepCheck.outputs.status != 'fetched'
649617
name: 'Building/fetching previous CI target: mathcomp-reals'
650618
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
@@ -653,10 +621,6 @@ jobs:
653621
name: 'Building/fetching previous CI target: stdlib'
654622
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
655623
--argstr job "stdlib"
656-
- if: steps.stepCheck.outputs.status != 'fetched'
657-
name: 'Building/fetching previous CI target: hierarchy-builder'
658-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"
659-
--argstr job "hierarchy-builder"
660624
- if: steps.stepCheck.outputs.status != 'fetched'
661625
name: Building/fetching current CI target
662626
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0"

0 commit comments

Comments
 (0)