Skip to content

Commit 53a92eb

Browse files
proux01proux01
authored
Merge pull request #91 from proux01/no-ssreflect
Stop depending on all_ssreflect
2 parents 820f728 + ef063cb commit 53a92eb

9 files changed

Lines changed: 680 additions & 72 deletions

File tree

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

Lines changed: 341 additions & 16 deletions
Large diffs are not rendered by default.

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

Lines changed: 322 additions & 25 deletions
Large diffs are not rendered by default.

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

Lines changed: 11 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -239,6 +239,10 @@ jobs:
239239
name: 'Building/fetching previous CI target: coq'
240240
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
241241
"master" --argstr job "coq"
242+
- if: steps.stepCheck.outputs.status != 'fetched'
243+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
244+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
245+
"master" --argstr job "mathcomp-ssreflect"
242246
- if: steps.stepCheck.outputs.status != 'fetched'
243247
name: 'Building/fetching previous CI target: mathcomp-algebra'
244248
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -447,6 +451,10 @@ jobs:
447451
name: 'Building/fetching previous CI target: coq'
448452
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
449453
"master" --argstr job "coq"
454+
- if: steps.stepCheck.outputs.status != 'fetched'
455+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
456+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
457+
"master" --argstr job "mathcomp-ssreflect"
450458
- if: steps.stepCheck.outputs.status != 'fetched'
451459
name: 'Building/fetching previous CI target: mathcomp-field'
452460
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -752,7 +760,7 @@ jobs:
752760
"master" --argstr job "mathcomp-finmap"
753761
mathcomp-real-closed:
754762
needs:
755-
- coq
763+
- rocq-core
756764
- mathcomp-bigenough
757765
runs-on: ubuntu-latest
758766
steps:
@@ -803,29 +811,13 @@ jobs:
803811
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
804812
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
805813
- if: steps.stepCheck.outputs.status != 'fetched'
806-
name: 'Building/fetching previous CI target: coq'
807-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
808-
"master" --argstr job "coq"
809-
- if: steps.stepCheck.outputs.status != 'fetched'
810-
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
811-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
812-
"master" --argstr job "mathcomp-ssreflect"
813-
- if: steps.stepCheck.outputs.status != 'fetched'
814-
name: 'Building/fetching previous CI target: mathcomp-algebra'
814+
name: 'Building/fetching previous CI target: rocq-core'
815815
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
816-
"master" --argstr job "mathcomp-algebra"
816+
"master" --argstr job "rocq-core"
817817
- if: steps.stepCheck.outputs.status != 'fetched'
818818
name: 'Building/fetching previous CI target: mathcomp-field'
819819
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
820820
"master" --argstr job "mathcomp-field"
821-
- if: steps.stepCheck.outputs.status != 'fetched'
822-
name: 'Building/fetching previous CI target: mathcomp-fingroup'
823-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
824-
"master" --argstr job "mathcomp-fingroup"
825-
- if: steps.stepCheck.outputs.status != 'fetched'
826-
name: 'Building/fetching previous CI target: mathcomp-solvable'
827-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
828-
"master" --argstr job "mathcomp-solvable"
829821
- if: steps.stepCheck.outputs.status != 'fetched'
830822
name: 'Building/fetching previous CI target: mathcomp-bigenough'
831823
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle

‎.nix/config.nix‎

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,6 @@
99
## Will determine the default main-job of the bundles defined below
1010
attribute = "mathcomp-real-closed";
1111

12-
## Set this when the package has no rocqPackages version yet
13-
## (either in nixpkgs or in .nix/rocq-overlays)
14-
no-rocq-yet = true;
15-
1612
## If you want to select a different attribute (to build from the local sources as well)
1713
## when calling `nix-shell` and `nix-build` without the `--argstr job` argument
1814
# shell-attribute = "{{nix_name}}";
@@ -69,15 +65,13 @@
6965
coq.override.version = "9.0";
7066
coq-elpi.job = true;
7167
hierarchy-builder.job = true;
72-
mathcomp.override.version = "2.4.0";
7368
}; };
7469
"9.1" = { rocqPackages = {
7570
rocq-core.override.version = "9.1";
7671
}; coqPackages = revdeps-overrides // {
7772
coq.override.version = "9.1";
7873
coq-elpi.job = true;
7974
hierarchy-builder.job = true;
80-
mathcomp.override.version = "2.5.0";
8175
}; };
8276
"master" = {
8377
rocqPackages = master-overrides // {

‎.nix/coq-nix-toolbox.nix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"32b164eef0752f2e0d2b57feaba9933a1ec590fb"
1+
"44d8c6838d4e309671b551571f90652da37343f6"

‎default.nix‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@
44
bundle ? null, job ? null, inNixShell ? null, src ? ./.,
55
}@args:
66
let auto = fetchGit {
7-
url = "https://github.com/coq-community/coq-nix-toolbox.git";
8-
ref = "master";
7+
url = "https://github.com/proux01/coq-nix-toolbox.git";
8+
ref = "fix530989";
99
rev = import .nix/coq-nix-toolbox.nix;
1010
};
1111
in

‎theories/polyrcf.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
22
(* Distributed under the terms of CeCILL-B. *)
3-
From mathcomp Require Import all_ssreflect all_algebra polyorder.
3+
From mathcomp Require Import all_boot order all_algebra polyorder.
44
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
55

66
(****************************************************************************)

‎theories/qe_rcf_th.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
22
(* Distributed under the terms of CeCILL-B. *)
33
From Corelib Require Import Setoid.
4-
From mathcomp Require Import all_ssreflect all_algebra.
4+
From mathcomp Require Import all_boot order all_algebra.
55
From mathcomp Require Import polyorder polyrcf mxtens.
66
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
77

‎theories/realalg.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
22
(* Distributed under the terms of CeCILL-B. *)
33
From HB Require Import structures.
4-
From mathcomp Require Import all_ssreflect all_algebra all_field bigenough.
4+
From mathcomp Require Import all_boot order all_algebra all_field bigenough.
55
From mathcomp Require Import polyorder cauchyreals.
66
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
77

0 commit comments

Comments
 (0)