Rocq 9.1

Author: 4ever2

.github/workflows/nix-action-default.yml

@@ -31,16 +31,17 @@ with (import <nixpkgs> {}).lib;
   ## /!\ Remove this field as soon as the package is available on nixpkgs.
   ## /!\ Manual overlays in `.nix/rocq-overlays` or `.nix/coq-overlays`
   ##     should be preferred then.
-  buildInputs = [ "equations" "metarocq" ];
-  nativeBuildInputs = [ "equations" ];
-    
+  #buildInputs = [ "equations" "metarocq" ];
+  #nativeBuildInputs = [ "equations" ];
+
   ## Indicate the relative location of your _CoqProject
   ## If not specified, it defaults to "_CoqProject"
   # coqproject = "_CoqProject";
 
   ## select an entry to build in the following `bundles` set
   ## defaults to "default"
   default-bundle = "default";
+  no-rocq-yet = true;
 
   ## write one `bundles.name` attribute set per
   ## alternative configuration
@@ -49,14 +50,13 @@ with (import <nixpkgs> {}).lib;
   bundles.default = {
     ## You can override Rocq and other Rocq rocqPackages
     ## through the following attribute
-    rocqPackages.rocq-core.override.version = "9.0";
-    rocqPackages.coq-core.override.version = "9.0";
+    rocqPackages.rocq-core.override.version = "9.1";
     ## You can override Coq and other Coq coqPackages
     ## through the following attribute
-    coqPackages.coq.override.version = "9.0";
-    coqPackages.equations.override.version = "1.3.1-9.0";
-    
-    coqPackages.metarocq.override.version = "1.4-9.0";
+    coqPackages.coq.override.version = "9.1";
+    coqPackages.equations.override.version = "v1.3.1-9.1";
+
+    coqPackages.metarocq.override.version = "v1.4.1-9.1";
     coqPackages.ceres.override.version = "0.4.1";
 
     ## In some cases, light overrides are not available/enough
@@ -104,17 +104,17 @@ with (import <nixpkgs> {}).lib;
   cachix.coq = {};
   cachix.math-comp = {};
   cachix.coq-community = {};
-  
+
   ## If you have write access to one of these caches you can
   ## provide the auth token or signing key through a secret
   ## variable on GitHub. Then, you should give the variable
   ## name here. For instance, coq-community projects can use
   ## the following line instead of the one above:
   cachix.metarocq.authToken = "CACHIX_AUTH_TOKEN";
-  
+
   ## Or if you have a signing key for a given Cachix cache:
   # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY"
-  
+
   ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY
   ## are the names of secret variables. They are set in
   ## GitHub's web interface.

.nix/config.nix

@@ -1 +1 @@
-"36b6af97e5de62782c4cc0dfdda3a40e64d668ad"
+"0aea8a65129226303ab48e6119a1f8eeae3b15f1"

.nix/coq-nix-toolbox.nix

@@ -16,15 +16,15 @@ install: [
   [make "-j%{jobs}%" "install"]
 ]
 depends: [
-  "rocq-core" { >= "9.0" }
+  "rocq-core" { >= "9.1" }
   "rocq-stdlib" { >= "9.0" }
   "coq-ceres" { >= "0.4.1"}
-  "rocq-metarocq-erasure-plugin" { = "1.4+9.0" }
+  "rocq-metarocq-erasure-plugin" { >= "1.4" & < "1.4.2" }
   "malfunction" { >= "0.7" }
 ]
 tags: [
   "keyword:extraction"
   "category:Miscellaneous/Rocq Extensions"
   "date:2025-04-23"
   "logpath:VerifiedExtraction"
-]
+]