WIP

Author: proux01

.nix/config.nix

@@ -100,7 +100,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       "aac-tactics"
       "argosy"
       "async-test"
-      "atbr" # -> overlay
+      "atbr"
       "autosubst"
       "bbv"
       "bedrock2" # -> overlay
@@ -114,7 +114,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       # "compcert" # -> overlay
       "coqprime"
       "coquelicot"
-      "coqutil" # -> overlay
+      "coqutil"
       # "coq-elpi" # -> overlay
       # "coq-elpi-test" # -> overlay
       "coq-ext-lib"
@@ -149,7 +149,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       "mathcomp-finmap"
       "mathcomp-test"
       "mathcomp-zify"
-      "math-classes" # -> overlay
+      # "math-classes" # -> overlay
       "menhir"
       "neural-net-coq-interp"
       "odd-order"
@@ -163,10 +163,10 @@ with builtins; with (import <nixpkgs> {}).lib;
       "rewriter" # -> overlay
       "riscvcoq"
       "rupicola" # -> overlay
-      "sf" # -> overlay
+      "sf"
       "simple-io"
       # "smtcoq-trakt" # -> overlay
-      "stalmarck-tactic" # -> overlay
+      "stalmarck-tactic"
       "stdpp"
       "StructTact"
       "Verdi"
@@ -180,8 +180,8 @@ with builtins; with (import <nixpkgs> {}).lib;
       "waterproof"
     ];
     main = [
-      "equations" # -> overlay
-      "equations-test" # -> overlay
+      # "equations" # -> overlay
+      # "equations-test" # -> overlay
       "jasmin"
       "mathcomp-word"
       # "metacoq" # -> overlay
@@ -192,38 +192,32 @@ with builtins; with (import <nixpkgs> {}).lib;
       { name = p; value.override.version = "coq-master"; }))
     // listToAttrs (forEach main (p:
       { name = p; value.override.version = "main"; }))
-    // {
+    // { tlc.override.version = "master-for-coq-ci"; } // {
       stdlib-html.job = true;
       stdlib-refman-html.job = true;
       stdlib-subcomponents.job = true;
       stdlib-test.job = true;
-      # atbr.override.version = "split_stdlib";  # would be remove by moving BinNums.v back to Numbers
       # bedrock2.override.version = "proux01:split_stdlib";  # to test
       dpdgraph-test.override.version = "coq_19310";
       compcert.override.version = "proux01:split_stdlib";
       coq-elpi.override.version = "proux01:split_stdlib";
       coq-elpi-test.override.version = "proux01:split_stdlib";
       coq-tools.override.version = "proux01:split_stdlib";
-      # coqutil.override.version = "proux01:split_stdlib";  # to test
       # corn.override.version = "split_stdlib";  # to test (would probably require a dummy module for move of Qreals.v)
       cross-crypto.override.version = "proux01:split_stdlib";  # would require a dummy module for move of SetoidList?
       equations.override.version = "proux01:split_stdlib";
-      # equations-test.override.version = "proux01:split_stdlib";  # would be remove by moving BinNums.v back to Numbers
+      equations-test.override.version = "proux01:split_stdlib";
       # fiat-crypto.override.version = "proux01:split_stdlib";  # to test
       flocq.override.version = "split_stdlib";
       # kami.override.version = "proux01:split_stdlib";  # to test
-      # math-classes.override.version = "split_stdlib";  # to test (would probably require a dummy module for move of Qreals.v)
+      math-classes.override.version = "split_stdlib";
       metacoq.override.version = "proux01:split_stdlib";
       QuickChick.override.version = "proux01:split_stdlib";
       quickchick-test.override.version = "proux01:split_stdlib";
       # relation-algebra.override.version = "proux01:split_stdlib";  # to test after moving back BinNums.v but likely not
       # rewriter.override.version = "proux01:split_stdlib";  # to test
       # rupicola.override.version = "proux01:split_stdlib";  # would require "Require Coq.Numbers.DecimalString" to work again
-      # sf.override.version = "proux01:split_stdlib";  # to test (I would expect it to work again but might just be an ordering issue with extraction results)
       smtcoq-trakt.override.version = "proux01:split_stdlib-trakt";
-      # stalmarck-tactic.override.version = "split_stdlib";  # should no longer be needed after moving back BinNums.v
-      tlc.override.version = "master-for-coq-ci"; # -> overlay
-      # tlc.override.version = "proux01:split_stdlib";  # to test (I would expect it to work)
       vst.override.version = "proux01:split_stdlib";
 
       Cheerios.job = false;
@@ -237,7 +231,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       # aac-tactics.job = false;
       argosy.job = false;
       async-test.job = false;
-      # atbr.job = false;
+      atbr.job = false;
       autosubst.job = false;
       bbv.job = false;
       # bedrock2.job = false;
@@ -247,7 +241,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       ceres.job = false;
       coinduction.job = false;
       compcert.job = false;
-      coq-elpi.job = false;
+      # coq-elpi.job = false;
       coq-elpi-test.job = false;
       coq-ext-lib.job = false;
       coq-hammer.job = false;
@@ -262,12 +256,12 @@ with builtins; with (import <nixpkgs> {}).lib;
       deriving.job = false;
       dpdgraph-test.job = false;
       engine-bench.job = false;
-      # equations.job = false;
-      # equations-test.job = false;
+      equations.job = false;
+      equations-test.job = false;
       fiat-crypto.job = false;
       flocq.job = false;
       fourcolor.job = false;
-      hierarchy-builder.job = false;
+      # hierarchy-builder.job = false;
       hierarchy-builder-test.job = false;
       http.job = false;
       iris.job = false;
@@ -324,6 +318,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       # Free overlays (can be merged independently of the PR)
       # aac-tactics.override.version = "split_stdlib";
       # argosy.override.version = "proux01:split_stdlib";
+      # atbr.override.version = "split_stdlib";
       # autosubst.override.version = "split_stdlib";
       # bbv.override.version = "proux01:split_stdlib";
       # category-theory.override.version = "proux01:split_stdlib";
@@ -332,6 +327,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       # coq-hammer.override.version = "proux01:split_stdlib";
       # coq-hammer-tactics.override.version = "proux01:split_stdlib";
       # coq-performance-tests.override.version = "proux01:split_stdlib";
+      # coqutil.override.version = "proux01:split_stdlib";
       # engine-bench.override.version = "proux01:split_stdlib";
       # iris.override.version = "proux:split_stdlib";
       # ITree.override.version = "proux01:split_stdlib";
@@ -342,8 +338,10 @@ with builtins; with (import <nixpkgs> {}).lib;
       # paramcoq-test.override.version = "split_stdlib";
       # perennial.override.version = "proux01:split_stdlib";
       # riscvcoq.override.version = "proux01:split_stdlib";
+      # sf.override.version = "proux01:split_stdlib";
       # simple-io.override.version = "proux01:split_stdlib";
       # smtcoq.override.version = "proux01:split_stdlib";
+      # tlc.override.version = "proux01:split_stdlib";
       # waterproof.override.version = "proux01:split_stdlib";
     };
   in {