Skip to content

Commit d0c3c40

Browse files
fajbproux01
fajb
authored and
proux01
committed
[zify] Define zify in terms of tify_* tactics
restructure components (isolate tify,zify)
1 parent 9fe34c3 commit d0c3c40

25 files changed

Lines changed: 772 additions & 534 deletions

File tree

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

Lines changed: 148 additions & 151 deletions
Large diffs are not rendered by default.

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

Lines changed: 135 additions & 138 deletions
Large diffs are not rendered by default.

‎.nix/config.nix‎

Lines changed: 26 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -285,22 +285,36 @@ with builtins; with (import <nixpkgs> {}).lib;
285285
# for a complete list of Coq packages available in Nix
286286
# * <github_login>:<branch> is such that this will use the branch <branch>
287287
# from https://github.com/<github_login>/<repository>
288+
bedrock2.override.version = "proux01:stdlib251";
289+
coq-elpi.override.version = "proux01:stdlib251";
290+
coqutil.override.version = "proux01:stdlib251";
291+
itauto.override.version = "proux01:stdlib251";
292+
equations.override.version = "proux01:stdlib251";
293+
equations-test.override.version = "proux01:stdlib251";
288294
smtcoq.override.version = "proux01:stdlib251";
289295
metarocq.override.version = "proux01:stdlib251";
290296
metarocq-test.override.version = "proux01:stdlib251";
297+
waterproof.override.version = "proux01:stdlib251";
291298
sf.job = false; # temporarily disactivated in Rocq CI
292299
trakt.job = false; # temporarily disactivated in Rocq CI
293300
smtcoq-trakt.job = false; # temporarily disactivated in Rocq CI
294301
};
295302
common-bundles = listToAttrs (forEach rocq-master (p:
296-
{ name = p; value.override.version = "master"; }));
303+
{ name = p; value.override.version = "master"; }))
304+
// {
305+
micromega-plugin.override.version = "tify";
306+
rocq-elpi.override.version = "proux01:stdlib251";
307+
rocq-elpi-test.override.version = "proux01:stdlib251";
308+
};
297309
in {
298310
"rocq-master" = { rocqPackages = common-bundles // {
299311
rocq-core.override.version = "master";
300312
stdlib-test.job = true;
301313
rocq-elpi.override.version = "master";
302-
rocq-elpi-test.override.version = "master";
314+
# rocq-elpi-test.override.version = "master";
315+
rocq-elpi-test.override.version = "proux01:stdlib251";
303316
hierarchy-builder.override.version = "master";
317+
# micromega-plugin.override.version = "master";
304318
micromega-plugin.override.version = "tify";
305319
micromega-plugin.job = false;
306320
mathcomp.override.version = "master";
@@ -357,7 +371,7 @@ with builtins; with (import <nixpkgs> {}).lib;
357371
dpdgraph-test.override.version = "7a0fba21287dd8889c55e6611f8ba219d012b81b";
358372
coq-hammer.override.version = "1d581299c2a85af175b53bd35370ea074af922ec";
359373
coq-hammer-tactics.override.version = "1d581299c2a85af175b53bd35370ea074af922ec";
360-
equations.override.version = "757662b9c875d7169a07b861d48e82157520ab1a";
374+
equations.job = false;
361375
equations-test.job = false;
362376
fiat-parsers.job = false; # broken
363377
metarocq.override.version = "e8f8078e756cc378b830eb5a8e4637df43d481af";
@@ -367,10 +381,13 @@ with builtins; with (import <nixpkgs> {}).lib;
367381
relation-algebra.override.version = "ba3db5783060d9e25d1db5e377fc9d71338a5160";
368382
rewriter.override.version = "dd37fb28ed7f01a3b7edc0675a86b95dd3eb1545";
369383
rocq-lean-import.override.version = "b8291b9dae4f5ed780112e95eea484e435199b46";
370-
smtcoq.override.version = "cff0a8cdb7c73b6c59965a749a4304f3c4ac01bf";
384+
# smtcoq.override.version = "cff0a8cdb7c73b6c59965a749a4304f3c4ac01bf";
385+
smtcoq.job = false;
386+
# smtcoq-trakt.override.version = "9392f7446a174b770110445c155a07b183cdca3d";
371387
stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512";
372388
unicoq.override.version = "d52374ca86e3885197f114555e742420fa9bbe94";
373-
waterproof.override.version = "99ad6ff78fa700c84ba0cb1d1bda27d8e0f11e1a";
389+
# waterproof.override.version = "99ad6ff78fa700c84ba0cb1d1bda27d8e0f11e1a";
390+
waterproof.job = false;
374391
compcert.job = false; # broken
375392
VST.job = false; # depends on compcert
376393
} // listToAttrs (forEach lighten-released (p:
@@ -391,7 +408,7 @@ with builtins; with (import <nixpkgs> {}).lib;
391408
dpdgraph-test.override.version = "7817def06d4e3abc2e54a2600cf6e29d63d58b8a";
392409
coq-hammer.override.version = "8649603dcbac5d92eaf1319a6b7cdfc65cdd804b";
393410
coq-hammer-tactics.override.version = "8649603dcbac5d92eaf1319a6b7cdfc65cdd804b";
394-
equations.override.version = "2137c8e7081f2d47ab903de0cc09fd6a05bfab01";
411+
equations.job = false;
395412
equations-test.job = false;
396413
fiat-parsers.job = false; # broken
397414
mtac2.override.version = "bcbefa79406fc113f878eb5f89758de241d81433";
@@ -400,10 +417,12 @@ with builtins; with (import <nixpkgs> {}).lib;
400417
rewriter.override.version = "9496defb8b236f442d11372f6e0b5e48aa38acfc";
401418
rocq-lean-import.override.version = "c3546102f242aaa1e9af921c78bdb1132522e444";
402419
# smtcoq.override.version = "5c6033c906249fcf98a48b4112f6996053124514";
420+
smtcoq.job = false;
403421
# smtcoq-trakt.override.version = "9392f7446a174b770110445c155a07b183cdca3d";
404422
stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512";
405423
unicoq.override.version = "28ec18aef35877829535316fc09825a25be8edf1";
406-
waterproof.override.version = "dd712eb0b7f5c205870dbd156736a684d40eeb9a";
424+
# waterproof.override.version = "dd712eb0b7f5c205870dbd156736a684d40eeb9a";
425+
waterproof.job = false;
407426
compcert.job = false; # broken
408427
VST.job = false; # depends on compcert
409428
mathcomp-algebra-tactics.job = false;

‎.nix/coq-overlays/itauto/default.nix‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
{
2+
lib,
3+
callPackage,
4+
mkCoqDerivation,
5+
coq,
6+
stdlib,
7+
dune,
8+
version ? null,
9+
}:
10+
11+
(mkCoqDerivation {
12+
pname = "itauto";
13+
owner = "fbesson";
14+
# domain = "gitlab.inria.fr";
15+
16+
release."8.20.0".sha256 = "sha256-LYKGbI3O6yw6CiTJNUGL11PT4q4o+gJK1kQgKQL0/Hk=";
17+
release."8.19.0".sha256 = "sha256-xKWCF4dYvvlJUVGCZcR2RLCG55vlGzu2GN30MeRvVD4=";
18+
release."8.18.0".sha256 = "sha256-4mDDnKTeYrf27uRMkydQxO7j2tfgTFXOREW474d40eo=";
19+
release."8.17.0".sha256 = "sha256-fgdnKchNT1Hyrq14gU8KWYnlSfg3qlsSw5A4+RoA26w=";
20+
release."8.16.0".sha256 = "sha256-4zAUYGlw/pBcLPv2GroIduIlvbfi1+Vy+TdY8KLCqO4=";
21+
release."8.15.0".sha256 = "sha256:10qpv4nx1p0wm9sas47yzsg9z22dhvizszfa21yff08a8fr0igya";
22+
release."8.14.0".sha256 = "sha256:1k6pqhv4dwpkwg81f2rlfg40wh070ks1gy9r0ravm2zhsbxqcfc9";
23+
release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A=";
24+
inherit version;
25+
defaultVersion =
26+
let
27+
case = case: out: { inherit case out; };
28+
in
29+
with lib.versions;
30+
lib.switch coq.coq-version [
31+
(case (isEq "8.20") "8.20.0")
32+
(case (isEq "8.19") "8.19.0")
33+
(case (isEq "8.18") "8.18.0")
34+
(case (isEq "8.17") "8.17.0")
35+
(case (isEq "8.16") "8.16.0")
36+
(case (isEq "8.15") "8.15.0")
37+
(case (isEq "8.14") "8.14.0")
38+
(case (isEq "8.13") "8.13+no")
39+
] null;
40+
41+
mlPlugin = true;
42+
nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
43+
enableParallelBuilding = false;
44+
45+
passthru.tests.suite = callPackage ./test.nix { };
46+
47+
propagatedBuildInputs = [ stdlib ];
48+
49+
meta = {
50+
description = "Reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support";
51+
maintainers = with lib.maintainers; [ siraben ];
52+
license = lib.licenses.gpl3Plus;
53+
};
54+
}).overrideAttrs
55+
(
56+
o:
57+
lib.optionalAttrs (o.version == "dev" || lib.versionAtLeast o.version "8.16") {
58+
propagatedBuildInputs = o.propagatedBuildInputs ++ [ coq.ocamlPackages.findlib ];
59+
}
60+
// lib.optionalAttrs (o.version == "dev" || lib.versionAtLeast o.version "8.18") {
61+
nativeBuildInputs = with coq.ocamlPackages; [
62+
ocaml
63+
findlib
64+
dune
65+
];
66+
}
67+
)

‎.nix/coq-overlays/itauto/test.nix‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
{
2+
stdenv,
3+
lib,
4+
coq,
5+
itauto,
6+
}:
7+
8+
let
9+
excluded = lib.optionals (lib.versions.isEq "8.16" itauto.version) [
10+
"arith.v"
11+
"refl_bool.v"
12+
];
13+
in
14+
15+
stdenv.mkDerivation {
16+
pname = "coq${coq.coq-version}-itauto-test";
17+
inherit (itauto) src version;
18+
19+
nativeCheckInputs = [
20+
coq
21+
itauto
22+
];
23+
24+
dontConfigure = true;
25+
dontBuild = true;
26+
doCheck = true;
27+
28+
checkPhase = ''
29+
cd test-suite
30+
for m in *.v
31+
do
32+
echo -n ${lib.concatStringsSep " " excluded} | grep --silent $m && continue
33+
echo $m && coqc $m
34+
done
35+
'';
36+
37+
installPhase = "touch $out";
38+
}

‎.nix/rocq-overlays/stdlib-refman-html/default.nix‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,12 @@ rocqPackages.lib.overrideRocqDerivation {
1515

1616
useDune = true;
1717

18-
buildPhase = ''
18+
configurePhase = ''
19+
export COQPATH=''${ROCQPATH}
1920
patchShebangs dev/with-rocq-wrap.sh
21+
'';
22+
23+
buildPhase = ''
2024
dev/with-rocq-wrap.sh dune build --root . --no-buffer @refman-html ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
2125
'';
2226

‎rocq-stdlib.opam‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ dev-repo: "git+https://github.com/coq/stdlib.git"
2626
depends: [
2727
"rocq-runtime"
2828
"rocq-core" {>= "9.1"}
29+
"micromega-plugin" {= "dev"}
2930
]
3031
build: [
3132
[make "-j" jobs]

‎subcomponents/lia.v‎

Lines changed: 1 addition & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,3 @@
11
From subcomponents Require ring.
2+
From subcomponents Require tify.
23
From Stdlib Require micromega.Lia.
3-
From Stdlib Require micromega.SatDivMod.
4-
From Stdlib Require micromega.Zify.
5-
From Stdlib Require micromega.ZifyBool.
6-
From Stdlib Require micromega.ZifyClasses.
7-
From Stdlib Require micromega.ZifyComparison.
8-
From Stdlib Require micromega.ZifyInst.
9-
From Stdlib Require micromega.ZifyN.
10-
From Stdlib Require micromega.ZifyNat.
11-
From Stdlib Require micromega.ZifyPow.

‎subcomponents/tify.v‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
From subcomponents Require integers.
2+
From subcomponents Require ring.
3+
From Stdlib Require micromega.Tify.
4+
From Stdlib Require micromega.Zify.
5+
From Stdlib Require micromega.SatDivMod.
6+
From Stdlib Require micromega.ZifyBool.
7+
From Stdlib Require micromega.ZifyClasses.
8+
From Stdlib Require micromega.ZifyComparison.
9+
From Stdlib Require micromega.ZifyInst.
10+
From Stdlib Require micromega.ZifyN.
11+
From Stdlib Require micromega.ZifyNat.
12+
From Stdlib Require micromega.ZifyPow.

‎test-suite/micromega/bug_18158.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ Goal forall x y ,
8585
-> Z.le (Z.shiftr y 8) 255
8686
-> Z.le (Z.shiftr x 24) 255.
8787
intros.
88-
Zify.zify_saturate.
88+
Tify.tify_saturate.
8989
(* [mp_lia zchecker] used to raise a [Stack overflow] error. It is supposed to fail normally. *)
9090
assert_fails (mp_lia zchecker).
9191
Abort.

0 commit comments

Comments
 (0)