From 37005203b07136fb33c3489b169113058159a959 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Mon, 13 Jan 2025 17:44:31 +0100
Subject: [PATCH 1/2] Update charon

---
 flake.lock | 26 +++++++-------------------
 1 file changed, 7 insertions(+), 19 deletions(-)

diff --git a/flake.lock b/flake.lock
index ee60ea5..1699e46 100644
--- a/flake.lock
+++ b/flake.lock
@@ -66,7 +66,6 @@
         "crane": [
           "crane"
         ],
-        "flake-compat": "flake-compat",
         "flake-utils": [
           "flake-utils"
         ],
@@ -74,16 +73,20 @@
           "eurydice",
           "nixpkgs"
         ],
+        "nixpkgs-ocaml": [
+          "charon",
+          "nixpkgs"
+        ],
         "rust-overlay": [
           "rust-overlay"
         ]
       },
       "locked": {
-        "lastModified": 1736369122,
-        "narHash": "sha256-LKddoHMQKNJBzeY4c3zQUy+bNCgjlBdKfs7TghpQodI=",
+        "lastModified": 1736782668,
+        "narHash": "sha256-s2bUC/GDEjawaQCh/GE955uehSi/ACdT+1z2CMqIRow=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "df3b7fd4c1277827c92b4a2cb84347f1f54d92a6",
+        "rev": "1c628d8a9704ee3ab0b9289c73b84848c508d26d",
         "type": "github"
       },
       "original": {
@@ -138,21 +141,6 @@
         "type": "github"
       }
     },
-    "flake-compat": {
-      "locked": {
-        "lastModified": 1717312683,
-        "narHash": "sha256-FrlieJH50AuvagamEvWMIE6D2OAnERuDboFDYAED/dE=",
-        "owner": "nix-community",
-        "repo": "flake-compat",
-        "rev": "38fd3954cf65ce6faf3d0d45cd26059e059f07ea",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nix-community",
-        "repo": "flake-compat",
-        "type": "github"
-      }
-    },
     "flake-utils": {
       "inputs": {
         "systems": "systems"

From a7f283c30d1c5a1dcd7527dda929039ca29c3206 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Mon, 13 Jan 2025 17:44:35 +0100
Subject: [PATCH 2/2] Use different nixpkgs for rust and ocaml toolchains

---
 flake.lock | 31 +++++++++----------------------
 flake.nix  | 14 ++++++--------
 2 files changed, 15 insertions(+), 30 deletions(-)

diff --git a/flake.lock b/flake.lock
index 1699e46..3ac18a4 100644
--- a/flake.lock
+++ b/flake.lock
@@ -14,8 +14,7 @@
           "fstar"
         ],
         "nixpkgs": [
-          "eurydice",
-          "nixpkgs"
+          "nixpkgs-ocaml"
         ]
       },
       "locked": {
@@ -70,12 +69,10 @@
           "flake-utils"
         ],
         "nixpkgs": [
-          "eurydice",
           "nixpkgs"
         ],
         "nixpkgs-ocaml": [
-          "charon",
-          "nixpkgs"
+          "nixpkgs-ocaml"
         ],
         "rust-overlay": [
           "rust-overlay"
@@ -125,7 +122,9 @@
           "karamel",
           "nixpkgs"
         ],
-        "recent_nixpkgs": "recent_nixpkgs"
+        "recent_nixpkgs": [
+          "nixpkgs"
+        ]
       },
       "locked": {
         "lastModified": 1736548395,
@@ -328,22 +327,6 @@
         "type": "github"
       }
     },
-    "recent_nixpkgs": {
-      "locked": {
-        "lastModified": 1735563628,
-        "narHash": "sha256-OnSAY7XDSx7CtDoqNh8jwVwh4xNL/2HaJxGjryLWzX8=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "b134951a4c9f3c995fd7be05f3243f8ecd65d798",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixos-24.05",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
     "root": {
       "inputs": {
         "aeneas": "aeneas",
@@ -367,6 +350,10 @@
         ],
         "libcrux": "libcrux",
         "nixpkgs": "nixpkgs_2",
+        "nixpkgs-ocaml": [
+          "eurydice",
+          "nixpkgs"
+        ],
         "rust-overlay": "rust-overlay"
       }
     },
diff --git a/flake.nix b/flake.nix
index 8222be0..07750b3 100644
--- a/flake.nix
+++ b/flake.nix
@@ -2,7 +2,8 @@
   # The inputs we care about are: hax, charon, eurydice, libcrux, bertie. We
   # take good care to avoid duplicated inputs to save on evaluation time.
   inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs";
+    nixpkgs.url = "github:nixos/nixpkgs"; # Recent nixpkgs for rust-overlay
+    nixpkgs-ocaml.follows = "eurydice/nixpkgs"; # eurydice nixpkgs for ocaml compat
     flake-utils.follows = "fstar/flake-utils";
     crane.url = "github:ipetkov/crane/da87d1af7e4e09fd0271432340a5cadf3eb96005";
     karamel.follows = "eurydice/karamel";
@@ -13,24 +14,21 @@
     };
     charon = {
       url = "github:aeneasverif/charon";
-      inputs.nixpkgs.follows = "eurydice/nixpkgs";
+      inputs.nixpkgs.follows = "nixpkgs";
+      inputs.nixpkgs-ocaml.follows = "nixpkgs-ocaml";
       inputs.flake-utils.follows = "flake-utils";
       inputs.rust-overlay.follows = "rust-overlay";
       inputs.crane.follows = "crane";
     };
     aeneas = {
       url = "github:aeneasverif/aeneas";
-      inputs.nixpkgs.follows = "eurydice/nixpkgs";
+      inputs.nixpkgs.follows = "nixpkgs-ocaml";
       inputs.charon.follows = "charon";
       inputs.fstar.follows = "fstar";
     };
     eurydice = {
       url = "github:aeneasverif/eurydice";
-      # If we override this, we would need to override karamel's nixpkgs too to
-      # get compatible ocaml versions, but flakes don't support nested
-      # overrides. We also can't use eurydice's nixpkgs everywhere because it
-      # does not contain `mold-wrapped` which is required by libcrux.
-      # inputs.nixpkgs.follows = "nixpkgs";
+      inputs.recent_nixpkgs.follows = "nixpkgs";
       inputs.flake-utils.follows = "flake-utils";
       inputs.charon.follows = "charon";
     };