Skip to content

Commit 237c005

Browse files
committed
1 parent 433824e commit 237c005

8 files changed

Lines changed: 454 additions & 624 deletions

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

Lines changed: 60 additions & 103 deletions
Large diffs are not rendered by default.

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

Lines changed: 60 additions & 103 deletions
Large diffs are not rendered by default.

‎.github/workflows/nix-action-rocq-9.2.yml‎

Lines changed: 121 additions & 103 deletions
Large diffs are not rendered by default.

‎.github/workflows/nix-action-rocq-9.3.yml‎

Lines changed: 121 additions & 103 deletions
Large diffs are not rendered by default.

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

Lines changed: 55 additions & 168 deletions
Large diffs are not rendered by default.

‎.nix/config.nix‎

Lines changed: 34 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -34,13 +34,6 @@ with builtins; with (import <nixpkgs> {}).lib;
3434

3535
bundles = let
3636
master = [
37-
"mathcomp-analysis"
38-
"mathcomp-bigenough"
39-
"mathcomp-classical"
40-
"mathcomp-finmap"
41-
"mathcomp-real-closed"
42-
];
43-
coq-master = master ++ [
4437
"coq-bits"
4538
"coqeal"
4639
"coquelicot"
@@ -52,8 +45,13 @@ with builtins; with (import <nixpkgs> {}).lib;
5245
"interval"
5346
"mathcomp-abel"
5447
"mathcomp-algebra-tactics"
48+
"mathcomp-analysis"
5549
"mathcomp-apery"
50+
"mathcomp-bigenough"
51+
"mathcomp-classical"
52+
"mathcomp-finmap"
5653
"mathcomp-infotheo"
54+
"mathcomp-real-closed"
5755
"mathcomp-word"
5856
"mathcomp-zify"
5957
"multinomials"
@@ -72,37 +70,36 @@ with builtins; with (import <nixpkgs> {}).lib;
7270
mathcomp-doc.job = true;
7371
mathcomp.job = false;
7472
stdlib.job = true;
73+
jasmin.override.version = "main";
74+
ssprove.override.version = "main";
75+
CertiRocq.job = false;
76+
ConCert.job = false;
77+
libvalidsdp.job = false;
78+
relation-algebra.job = false;
79+
validsdp.job = false;
80+
wasmcert.job = false;
81+
# To add an overlay applying to all bundles,
82+
# add below a line like
83+
#<package>.override.version = "<github_login>:<branch>";
84+
# where
85+
# * <package> will typically be one of the strings above (without the quotes)
86+
# or look at https://github.com/NixOS/nixpkgs/tree/master/pkgs/development/coq-modules
87+
# for a complete list of Coq packages available in Nix
88+
# * <github_login>:<branch> is such that this will use the branch <branch>
89+
# from https://github.com/<github_login>/<repository>
7590
};
76-
coq-common-bundles = listToAttrs (forEach coq-master (p:
77-
{ name = p; value.override.version = "master"; }))
78-
// { jasmin.override.version = "main";
79-
ssprove.override.version = "pi8027:deprecation_mc2.4";
80-
# To add an overlay applying to all bundles,
81-
# add below a line like
82-
#<package>.override.version = "<github_login>:<branch>";
83-
# where
84-
# * <package> will typically be one of the strings above (without the quotes)
85-
# or look at https://github.com/NixOS/nixpkgs/tree/master/pkgs/development/coq-modules
86-
# for a complete list of Coq packages available in Nix
87-
# * <github_login>:<branch> is such that this will use the branch <branch>
88-
# from https://github.com/<github_login>/<repository>
89-
};
9091
in {
9192
"rocq-master" = { rocqPackages = common-bundles // {
9293
rocq-core.override.version = "master";
93-
stdlib.override.version = "master";
94-
bignums.override.version = "master";
94+
coq.override.version = "master";
9595
rocq-elpi.override.version = "master";
9696
hierarchy-builder.override.version = "master";
9797
micromega-plugin.override.version = "master";
98-
mathcomp.job = false;
99-
rocqnavi.override.version = "master";
100-
}; coqPackages = coq-common-bundles // {
101-
coq.override.version = "master";
10298
stdlib.override.version = "master";
10399
bignums.override.version = "master";
104-
coq-elpi.override.version = "master";
105-
hierarchy-builder.override.version = "master";
100+
mathcomp.job = false;
101+
rocqnavi.override.version = "master";
102+
autosubst.job = false;
106103
interval.job = false;
107104
coquelicot.job = false;
108105
ssprove.job = false;
@@ -114,11 +111,10 @@ with builtins; with (import <nixpkgs> {}).lib;
114111
}; };
115112
"rocq-9.3" = { rocqPackages = common-bundles // {
116113
rocq-core.override.version = "9.3";
117-
micromega-plugin.override.version = "master";
118-
micromega-plugin.job = false;
119-
}; coqPackages = coq-common-bundles // {
120114
coq.override.version = "9.3";
121115
coq-elpi.job = true;
116+
micromega-plugin.override.version = "master";
117+
micromega-plugin.job = false;
122118
hierarchy-builder.job = true;
123119
interval.job = false;
124120
jasmin.job = false; # waiting for InteractionTrees
@@ -127,11 +123,10 @@ with builtins; with (import <nixpkgs> {}).lib;
127123
}; };
128124
"rocq-9.2" = { rocqPackages = common-bundles // {
129125
rocq-core.override.version = "9.2";
130-
micromega-plugin.override.version = "master";
131-
micromega-plugin.job = false;
132-
}; coqPackages = coq-common-bundles // {
133126
coq.override.version = "9.2";
134127
coq-elpi.job = true;
128+
micromega-plugin.override.version = "master";
129+
micromega-plugin.job = false;
135130
hierarchy-builder.job = true;
136131
interval.job = false;
137132
jasmin.job = false; # waiting for InteractionTrees
@@ -142,21 +137,19 @@ with builtins; with (import <nixpkgs> {}).lib;
142137
}; };
143138
"rocq-9.1" = { rocqPackages = common-bundles // {
144139
rocq-core.override.version = "9.1";
145-
micromega-plugin.override.version = "master";
146-
micromega-plugin.job = false;
147-
}; coqPackages = coq-common-bundles // {
148140
coq.override.version = "9.1";
149141
coq-elpi.job = true;
142+
micromega-plugin.override.version = "master";
143+
micromega-plugin.job = false;
150144
hierarchy-builder.job = true;
151145
ConCert.job = false;
152146
}; };
153147
"rocq-9.0" = { rocqPackages = common-bundles // {
154148
rocq-core.override.version = "9.0";
155-
micromega-plugin.override.version = "master";
156-
micromega-plugin.job = false;
157-
}; coqPackages = coq-common-bundles // {
158149
coq.override.version = "9.0";
159150
coq-elpi.job = true;
151+
micromega-plugin.override.version = "master";
152+
micromega-plugin.job = false;
160153
hierarchy-builder.job = true;
161154
odd-order.job = false; # odd-order dropped support for 9.0
162155
}; };

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"39f7d7aa1abe2eb6df5539d4c3c5982d01c63ae0"
1+
"2aed22b9e8069cbb66e8597941e11d825ce337bc"

‎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/rocq-community/coq-nix-toolbox.git";
8-
ref = "master";
7+
url = "https://github.com/proux01/coq-nix-toolbox.git";
8+
ref = "test-merge-derivations";
99
# putting a ref here is strongly advised
1010
rev = import .nix/coq-nix-toolbox.nix;
1111
};

0 commit comments

Comments
 (0)