Test moving back BinNums.v

Author: proux01

.nix/config.nix

@@ -100,10 +100,10 @@ with builtins; with (import <nixpkgs> {}).lib;
       "aac-tactics"
       "argosy"
       "async-test"
-      # "atbr" # -> overlay
+      "atbr" # -> overlay
       "autosubst"
       "bbv"
-      # "bedrock2" # -> overlay
+      "bedrock2" # -> overlay
       "bignums"
       "bignums-test"
       "category-theory"
@@ -114,20 +114,20 @@ with builtins; with (import <nixpkgs> {}).lib;
       # "compcert" # -> overlay
       "coqprime"
       "coquelicot"
-      # "coqutil" # -> overlay
+      "coqutil" # -> overlay
       # "coq-elpi" # -> overlay
       # "coq-elpi-test" # -> overlay
       "coq-ext-lib"
       "coq-hammer"
       "coq-hammer-tactics"
       "coq-performance-tests"
       # "coq-tools" # -> overlay
-      # "corn" # -> overlay
+      "corn" # -> overlay
       # "cross-crypto" # -> overlay
       "deriving"
       "engine-bench"
       # TODO fcsl_pcm -> wait for MC 2 port
-      # "fiat-crypto" # -> overlay
+      "fiat-crypto" # -> overlay
       # TODO fiat_parsers
       # TODO fiat_crypto_legacy
       # "flocq" # -> overlay
@@ -142,14 +142,14 @@ with builtins; with (import <nixpkgs> {}).lib;
       "ITree"
       "itree-io"
       "json"
-      # "kami" # -> overlay
+      "kami" # -> overlay
       "mathcomp"
       "mathcomp-analysis"
       "mathcomp-bigenough"
       "mathcomp-finmap"
       "mathcomp-test"
       "mathcomp-zify"
-      # "math-classes" # -> overlay
+      "math-classes" # -> overlay
       "menhir"
       "neural-net-coq-interp"
       "odd-order"
@@ -159,14 +159,14 @@ with builtins; with (import <nixpkgs> {}).lib;
       "perennial"
       # "QuickChick" # -> overlay
       # "quickchick-test" # -> overlay
-      # "relation-algebra" # -> overlay
-      # "rewriter" # -> overlay
+      "relation-algebra" # -> overlay
+      "rewriter" # -> overlay
       "riscvcoq"
-      # "rupicola" # -> overlay
-      # "sf" # -> overlay
+      "rupicola" # -> overlay
+      "sf" # -> overlay
       "simple-io"
       # "smtcoq-trakt" # -> overlay
-      # "stalmarck-tactic" # -> overlay
+      "stalmarck-tactic" # -> overlay
       "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
@@ -197,33 +197,33 @@ with builtins; with (import <nixpkgs> {}).lib;
       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
+      # 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)
+      # 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
-      fiat-crypto.override.version = "proux01:split_stdlib";  # to test
+      # equations-test.override.version = "proux01:split_stdlib";  # would be remove by moving BinNums.v back to Numbers
+      # 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)
+      # 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)
       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)
+      # 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)
+      # 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";
 
       # Free overlays (can be merged independently of the PR)