diff --git a/flake.lock b/flake.lock
index 09d4f3346e..b70aa050fe 100644
--- a/flake.lock
+++ b/flake.lock
@@ -1,5 +1,30 @@
 {
   "nodes": {
+    "dune": {
+      "inputs": {
+        "melange": "melange",
+        "nixpkgs": [
+          "nixpkgs"
+        ],
+        "nixpkgs-old": "nixpkgs-old",
+        "ocaml-overlays": "ocaml-overlays",
+        "oxcaml": "oxcaml",
+        "oxcaml-opam-repository": "oxcaml-opam-repository"
+      },
+      "locked": {
+        "lastModified": 1768085155,
+        "narHash": "sha256-kJud8gkBydJo9w4vsiO36NuAYtAamL3EUnaFPQyNkls=",
+        "owner": "ocaml",
+        "repo": "dune",
+        "rev": "f3e49cd3a22be721bfb85830ffd66ef62870b26c",
+        "type": "github"
+      },
+      "original": {
+        "owner": "ocaml",
+        "repo": "dune",
+        "type": "github"
+      }
+    },
     "flake-utils": {
       "inputs": {
         "systems": "systems"
@@ -18,13 +43,99 @@
         "type": "github"
       }
     },
+    "flake-utils_2": {
+      "inputs": {
+        "systems": "systems_2"
+      },
+      "locked": {
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "melange": {
+      "inputs": {
+        "melange-compiler-libs": "melange-compiler-libs",
+        "nixpkgs": [
+          "dune",
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1763880791,
+        "narHash": "sha256-aD3CrTlqEh/MPRjfbs3UgdjlX37zLSFZKQ5xOGuu2VI=",
+        "owner": "melange-re",
+        "repo": "melange",
+        "rev": "a63c2953970d3fd9e4eb0a0f8cd4ca1e400841ea",
+        "type": "github"
+      },
+      "original": {
+        "owner": "melange-re",
+        "ref": "v6-54",
+        "repo": "melange",
+        "type": "github"
+      }
+    },
+    "melange-compiler-libs": {
+      "inputs": {
+        "nixpkgs": [
+          "dune",
+          "melange",
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1760240634,
+        "narHash": "sha256-cmPZs92Vva6X06E8MreMVn6Yu5gqZtAYLJRweTEWwRY=",
+        "owner": "melange-re",
+        "repo": "melange-compiler-libs",
+        "rev": "b8d6659bfe3045938afa83f37b7c357c052d10c7",
+        "type": "github"
+      },
+      "original": {
+        "owner": "melange-re",
+        "ref": "5.4",
+        "repo": "melange-compiler-libs",
+        "type": "github"
+      }
+    },
+    "nix-github-actions": {
+      "inputs": {
+        "nixpkgs": [
+          "dune",
+          "oxcaml",
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1737420293,
+        "narHash": "sha256-F1G5ifvqTpJq7fdkT34e/Jy9VCyzd5XfJ9TO8fHhJWE=",
+        "owner": "nix-community",
+        "repo": "nix-github-actions",
+        "rev": "f4158fa080ef4503c8f4c820967d946c2af31ec9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-community",
+        "repo": "nix-github-actions",
+        "type": "github"
+      }
+    },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1758311079,
-        "narHash": "sha256-gzhpXuKF+oQShw8O2i60Zimk76xY43/OyFHoNDyrMos=",
+        "lastModified": 1768084859,
+        "narHash": "sha256-2/rfF9fO+6FcEOQB5vuRVRTCnb27ESJhjLT6HGf3AJg=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "12c6c1c3e263b957d19259104ed7218e9482b159",
+        "rev": "027202c37d51de884c6f5af4b6090532859907a7",
         "type": "github"
       },
       "original": {
@@ -34,9 +145,86 @@
         "type": "github"
       }
     },
-    "root": {
+    "nixpkgs-old": {
+      "locked": {
+        "lastModified": 1746662029,
+        "narHash": "sha256-2lFR2IQHaaUA5X2JMzQ3SGkj5IXFU/ztqpKD4I6vWCw=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "7f50d4b33363d3948543f6a02b90a2c66852a453",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "7f50d4b33363d3948543f6a02b90a2c66852a453",
+        "type": "github"
+      }
+    },
+    "ocaml-overlays": {
+      "inputs": {
+        "nixpkgs": [
+          "dune",
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1766954034,
+        "narHash": "sha256-uTqJvUxEsqUdKh5qDF7EBOFgDwV+SIiH2BU1fWI6yGU=",
+        "owner": "nix-ocaml",
+        "repo": "nix-overlays",
+        "rev": "50a9e2bf8de3ea924754d7e242dc055d22b34d44",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-ocaml",
+        "repo": "nix-overlays",
+        "type": "github"
+      }
+    },
+    "oxcaml": {
       "inputs": {
         "flake-utils": "flake-utils",
+        "nix-github-actions": "nix-github-actions",
+        "nixpkgs": [
+          "dune",
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1765548893,
+        "narHash": "sha256-fgn976ky1Qygbq3RoYq3uUe7E4LRHBJOrAP5+8/W7Zo=",
+        "owner": "oxcaml",
+        "repo": "oxcaml",
+        "rev": "71aae05ca41b54921bd24b8a74253943196ca1d9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "oxcaml",
+        "repo": "oxcaml",
+        "type": "github"
+      }
+    },
+    "oxcaml-opam-repository": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1764321512,
+        "narHash": "sha256-BjBv/2cHpLeOhK2zrmMHep4YCkc0cQmKbACdPZ9pxoo=",
+        "owner": "oxcaml",
+        "repo": "opam-repository",
+        "rev": "4359be11c299fae9aa74374f3f863f64c14e3bd0",
+        "type": "github"
+      },
+      "original": {
+        "owner": "oxcaml",
+        "repo": "opam-repository",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "dune": "dune",
+        "flake-utils": "flake-utils_2",
         "nixpkgs": "nixpkgs"
       }
     },
@@ -54,6 +242,21 @@
         "repo": "default",
         "type": "github"
       }
+    },
+    "systems_2": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
     }
   },
   "root": "root",
diff --git a/flake.nix b/flake.nix
index 4d33937357..f0e2ee04a0 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,45 +5,52 @@
     nixpkgs.url = "github:NixOS/nixpkgs/master";
 
     flake-utils.url = "github:numtide/flake-utils";
+
+    dune = {
+      url = "github:ocaml/dune";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
   };
 
-  outputs = { self, nixpkgs, flake-utils }:
+  outputs = { self, nixpkgs, flake-utils, dune }:
     flake-utils.lib.eachDefaultSystem (system:
       let
         pkgs = nixpkgs.legacyPackages.${system};
-        makeDevShell = { coq ? pkgs.coq }:
+        makeDevShell = { coq ? pkgs.coq, rocqPackages ? coq.passthru.rocqPackages or null }:
           let
             coqPackages = pkgs.mkCoqPackages coq // {
               __attrsFailEvaluation = true;
             };
+            ocamlPackages = coq.passthru.ocamlPackages or pkgs.ocamlPackages;
           in
           { extraPackages ? [ coqPackages.coq-lsp ] }:
           pkgs.mkShell {
             buildInputs =
-              [ pkgs.dune_3 pkgs.ocaml ] ++ extraPackages ++ [ coq ];
+              [
+                dune.packages.${system}.default
+                ocamlPackages.ocaml
+                ocamlPackages.findlib
+                pkgs.pkg-config
+              ] ++ extraPackages ++ [ coq ]
+              ++ pkgs.lib.optionals (rocqPackages != null) [ rocqPackages.rocq-core ];
           };
       in
       {
         packages.default = pkgs.coqPackages.mkCoqDerivation {
           pname = "hott";
-          version = "8.20";
+          version = "9.0";
           src = self;
           useDune = true;
         };
 
         devShells.default =
           makeDevShell
-            { coq = pkgs.coq_9_0; }
-            { };
-
-        devShells.coq_8_20 =
-          makeDevShell
-            { coq = pkgs.coq_8_20; }
+            { coq = pkgs.coq_9_1; }
             { };
 
-        devShells.coq_8_19 =
+        devShells.coq_9_0 =
           makeDevShell
-            { coq = pkgs.coq_8_19; }
+            { coq = pkgs.coq_9_0; }
             { };
 
         # To use, pass --impure to nix develop