Use dune build in opam/nix packages

.github/dependabot.yml

@@ -6,4 +6,4 @@ updates:
       interval: "weekly"
       day: "monday"
     labels:
-      - "dependencies"
+      - "part: dependencies"

.gitignore

@@ -65,3 +65,6 @@ Makefile.rocq.conf
 docs/
 # Dune
 _build/
+
+# Nix
+result

.nix/config.nix

@@ -12,7 +12,7 @@
       coq.override.version = "9.0";
       mathcomp.job = false;
       mathcomp.override.version = "2.3.0";
-      mathcomp-analysis.override.version = "1.8.0";
+      mathcomp-analysis.override.version = "1.12.0";
     }; rocqPackages = {
       rocq-core.override.version = "9.0";
     };

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"3e11db1b014f5f6bedf9322eed22ef325c868f9b"
+"af97ff6bc64b9ca3c6101bf4c6ad6cdb50236d73"

.nix/coq-overlays/ssprove/default.nix

@@ -15,6 +15,7 @@
 mkCoqDerivation {
   pname = "ssprove";
   owner = "SSProve";
+  opam-name = "rocq-ssprove";
 
   inherit version;
   defaultVersion =
@@ -57,6 +58,8 @@ mkCoqDerivation {
   release."0.2.0".sha256 = "sha256-GDkWH0LUsW165vAUoYC5of9ndr0MbfBtmrPhsJVXi3o=";
   release."0.1.0".sha256 = "sha256-Yj+k+mBsudi3d6bRVlZLyM4UqQnzAX5tHvxtKoIuNTE=";
 
+  useDune = true;
+
   propagatedBuildInputs = [
     equations
     mathcomp-boot

.nix/nixpkgs.nix

@@ -1,4 +1,4 @@
 fetchTarball {
-    url = "https://github.com/NixOS/nixpkgs/archive/082f768988f85a3c4bef2afc7add7821c61a0787.tar.gz";
-    sha256 = "0d6641rsisygspzaw4xh95z6b3mhrr8nlkzndsz8ab2rshd7na7g";
+    url = "https://github.com/NixOS/nixpkgs/archive/2cce2415f39a7845cf97c823e7135f44f4eff809.tar.gz";
+    sha256 = "0i4k6mmf4v8h550f7nr0pjvzrmaan331bkyqg9h21df4axc1r0di";
   }

flake.nix

@@ -7,22 +7,24 @@
     let
       ssprovePkg = { lib, mkCoqDerivation, coq
                   , equations, extructures, deriving
-                  , mathcomp-analysis, mathcomp-ssreflect
+                  , mathcomp-analysis, mathcomp-boot
                   , mathcomp-experimental-reals
                   , mathcomp-word}:
         mkCoqDerivation {
           pname = "ssprove";
           owner = "SSProve";
-          version = "0.2.0";
+          opam-name = "rocq-ssprove";
+          version = "0.3.1";
           src = ./.;
+          useDune = true;
           propagatedBuildInputs = [
             equations
+            mathcomp-boot
             mathcomp-analysis
             mathcomp-experimental-reals
-            mathcomp-ssreflect
-            mathcomp-word
-            deriving
             extructures
+            deriving
+            mathcomp-word
           ];
           meta = {
             description = "A foundational framework for modular cryptographic proofs in Rocq ";

rocq-ssprove.opam

@@ -10,6 +10,7 @@ dev-repo: "git+https://github.com/SSProve/ssprove.git"
 doc: "https://SSProve.github.io/ssprove/index.html"
 license: "MIT"
 depends: [
+  "dune" {>= "3.21"}
   "rocq-core" {>= "9.0" & < "9.2~"}
   "rocq-stdlib" {>= "9.0" & < "9.2~"}
   "rocq-equations" {(>= "1.3.1+9.0")}
@@ -21,10 +22,18 @@ depends: [
   "coq-deriving" {(>= "0.2.1" & < "dev")}
 ]
 build: [
-  [make "-j%{jobs}%"]
-]
-install: [
-  [make "install"]
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
 ]
 tags: [
   "keyword:cryptography"

theories/dune

@@ -18,6 +18,17 @@
       Stdlib
       Equations
       mathcomp
+      mathcomp.algebra
+      mathcomp.word
+      mathcomp.classical
+      mathcomp.reals
+      mathcomp.experimental_reals
+      mathcomp.fingroup
+      mathcomp.finmap
+      mathcomp.solvable
+      mathcomp.bigenough
+      mathcomp.ssreflect
+      mathcomp.order
       HB
       elpi
       elpi_elpi