Use dune 3.7 and update the flake.lock

6 files changed, 73 insertions, 51 deletions

diff --git a/Makefile b/Makefile
index a05ba185..9df5f264 100644
--- a/Makefile
+++ b/Makefile
@@ -260,9 +260,9 @@ tleanp-%:
 	$(AENEAS_CMD)
 
 
-# Nix
+# Nix - TODO: add the lean tests
 .PHONY: nix
-nix: nix-aeneas-tests nix-aeneas-verify-fstar nix-aeneas-verify-coq nix-aeneas-verify-lean
+nix: nix-aeneas-tests nix-aeneas-verify-fstar nix-aeneas-verify-coq
 
 .PHONY: nix-aeneas-tests
 nix-aeneas-tests:
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index 7e585dd6..d0f57f32 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -42,7 +42,7 @@ val compute_abs_borrows_loans_maps :
     variant for instance) it calls the corresponding specialized function from
     {!InterpreterLoopsCore.PrimMatcher}.
  *)
-module MakeMatcher : functor (PM : PrimMatcher) -> Matcher
+module MakeMatcher : functor (_ : PrimMatcher) -> Matcher
 
 (** A matcher for joins (we use joins to compute loop fixed points).
 
@@ -58,7 +58,7 @@ module MakeMatcher : functor (PM : PrimMatcher) -> Matcher
     The join matcher is used to match the *concrete* values only. For this
     reason, we fail on the functions which match avalues.
  *)
-module MakeJoinMatcher : functor (S : MatchJoinState) -> PrimMatcher
+module MakeJoinMatcher : functor (_ : MatchJoinState) -> PrimMatcher
 
 (** An auxiliary matcher that we use for two purposes:
     - to check if two contexts are equivalent modulo id substitution (i.e.,
@@ -67,7 +67,7 @@ module MakeJoinMatcher : functor (S : MatchJoinState) -> PrimMatcher
       target context to the values and borrows in a source context (see
       {!match_ctx_with_target}).
  *)
-module MakeCheckEquivMatcher : functor (S : MatchCheckEquivState) ->
+module MakeCheckEquivMatcher : functor (_ : MatchCheckEquivState) ->
   CheckEquivMatcher
 
 (** Compute whether two contexts are equivalent modulo an identifier substitution.
diff --git a/compiler/aeneas.opam b/compiler/aeneas.opam
index 571b2d33..c92e8a1c 100644
--- a/compiler/aeneas.opam
+++ b/compiler/aeneas.opam
@@ -9,7 +9,7 @@ license: "Apache-2.0"
 homepage: "https://github.com/AeneasVerif/aeneas"
 bug-reports: "https://github.com/AeneasVerif/aeneas/issues"
 depends: [
-  "dune" {>= "2.8"}
+  "dune" {>= "3.7"}
   "odoc" {with-doc}
 ]
 build: [
diff --git a/compiler/dune-project b/compiler/dune-project
index 650eeec0..9910e549 100644
--- a/compiler/dune-project
+++ b/compiler/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.8)
+(lang dune 3.7)
 
 (name aeneas)
 
diff --git a/flake.lock b/flake.lock
index 4112d86f..46a19dfb 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,11 +8,11 @@
         "rust-overlay": "rust-overlay_2"
       },
       "locked": {
-        "lastModified": 1679487286,
-        "narHash": "sha256-CSg7RD174YC2Vf/qPb3aRcabFaT9vYDm1HnJrlWhyAE=",
+        "lastModified": 1683659996,
+        "narHash": "sha256-fgUHjKclaxwHr2fmQEblEwa3AG01oti2mtgc/IvnzQY=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "0f33a841710dfabf2557e7cfb30c820027ca56d1",
+        "rev": "1216ba9de82030adcf75ed894bca60624b8229a5",
         "type": "github"
       },
       "original": {
@@ -35,11 +35,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1673056065,
-        "narHash": "sha256-a68tMDTDqdAauxq377ALl4Uwm6oh9MeoY2WbTYRWZoo=",
+        "lastModified": 1683505101,
+        "narHash": "sha256-VBU64Jfu2V4sUR5+tuQS9erBRAe/QEYUxdVMcJGMZZs=",
         "owner": "ipetkov",
         "repo": "crane",
-        "rev": "0144134311767fcee80213321f079a8ffa0b9cc1",
+        "rev": "7b5bd9e5acb2bb0cfba2d65f34d8568a894cdb6c",
         "type": "github"
       },
       "original": {
@@ -51,11 +51,11 @@
     "flake-compat": {
       "flake": false,
       "locked": {
-        "lastModified": 1668681692,
-        "narHash": "sha256-Ht91NGdewz8IQLtWZ9LCeNXMSXHUss+9COoqu6JLmXU=",
+        "lastModified": 1673956053,
+        "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=",
         "owner": "edolstra",
         "repo": "flake-compat",
-        "rev": "009399224d5e398d03b22badca40a37ac85412a1",
+        "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9",
         "type": "github"
       },
       "original": {
@@ -65,12 +65,15 @@
       }
     },
     "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
       "locked": {
-        "lastModified": 1667395993,
-        "narHash": "sha256-nuEHfE/LcWyuSWnS8t12N1wc105Qtau+/OdUAjtQ0rA=",
+        "lastModified": 1681202837,
+        "narHash": "sha256-H+Rh19JDwRtpVPAWp64F+rlEtxUWBAQW28eAi3SRSzg=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "5aed5285a952e0b949eb3ba02c12fa4fcfef535f",
+        "rev": "cfacdce06f30d2b68473a46042957675eebb3401",
         "type": "github"
       },
       "original": {
@@ -95,14 +98,14 @@
     },
     "flake-utils_3": {
       "inputs": {
-        "systems": "systems"
+        "systems": "systems_2"
       },
       "locked": {
-        "lastModified": 1681202837,
-        "narHash": "sha256-H+Rh19JDwRtpVPAWp64F+rlEtxUWBAQW28eAi3SRSzg=",
+        "lastModified": 1685518550,
+        "narHash": "sha256-o2d0KcvaXzTrPRIo0kOLV0/QXHhDQ5DTi+OxcjO8xqY=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "cfacdce06f30d2b68473a46042957675eebb3401",
+        "rev": "a1720a10a6cfe8234c0e93907ffe81be440f4cef",
         "type": "github"
       },
       "original": {
@@ -147,11 +150,11 @@
         "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1683501815,
-        "narHash": "sha256-+DX6VE4CmO5+n+Vp+BJi0qLWh8BJZk5i3SqKUjhRMBg=",
+        "lastModified": 1683934850,
+        "narHash": "sha256-qGN5BdNNsM4TFzYTajIdj5Cm84X5WlP41gB9VLIhSxc=",
         "owner": "fstarlang",
         "repo": "fstar",
-        "rev": "3f1c7aecb2f24ec907cdcb1c480f2aa67b087063",
+        "rev": "2c89426093d3a883d08ce9a60ac4539f6f1df1aa",
         "type": "github"
       },
       "original": {
@@ -180,11 +183,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1683481401,
-        "narHash": "sha256-NEFEEjDDew6Q8p4zExOX2FBXcqoZrz1yVZFWIH0kFyA=",
+        "lastModified": 1683838937,
+        "narHash": "sha256-GCtSeDEISmp1+m4J8WNosa8zzqxyVPw7e5z/oBgn3lg=",
         "owner": "hacl-star",
         "repo": "hacl-star",
-        "rev": "f55deda4d9ce1f06c71d23180911163a75c85c85",
+        "rev": "3e283efd721ceff6fc11eef4c4908662287a6ff9",
         "type": "github"
       },
       "original": {
@@ -210,11 +213,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1683508931,
-        "narHash": "sha256-EbwwSDubjm12tyWcxhjwWsmgzuI1M5pVdO+9k+hPXZ0=",
+        "lastModified": 1683940878,
+        "narHash": "sha256-XxhR8jI5oF/gce3MCgmzcSkNGzeZXJeP1gfgWfo9p8A=",
         "owner": "hacl-star",
         "repo": "hacl-nix",
-        "rev": "4f427b15b3c0766938b0ba387a0716991a18e692",
+        "rev": "a4e4322d2e51b1f8050dd292609e8afbf56d1235",
         "type": "github"
       },
       "original": {
@@ -259,15 +262,16 @@
         "nixpkgs": "nixpkgs_5"
       },
       "locked": {
-        "lastModified": 1681865920,
-        "narHash": "sha256-jaZ2QpZxG4OGeJW8T5WFw+eAt09GDbk0sStc7WCoxsg=",
+        "lastModified": 1681922867,
+        "narHash": "sha256-pW9jfrL8HGTdrrfD/rU/b148648enJRt3nvCx+vbuDc=",
         "owner": "leanprover",
         "repo": "lake",
-        "rev": "257fc59a6464f5732a4f49e7dda0fc37475819fb",
+        "rev": "6544bc7e102eaaaed6d727ef61d78fc194deaf4c",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
+        "ref": "lean4-master",
         "repo": "lake",
         "type": "github"
       }
@@ -280,11 +284,11 @@
         "nixpkgs": "nixpkgs_4"
       },
       "locked": {
-        "lastModified": 1683577548,
-        "narHash": "sha256-kujPgXEoXUsUt7MIwIaOjNLSIkHpqx7o8kT01nRIpYM=",
+        "lastModified": 1685538626,
+        "narHash": "sha256-R4sJ/w2sBSJmF1p4SHuqh00QXf+Bjxvujdex0s4QHXM=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "ad4b822734adfd7800194eb574b31fe540923302",
+        "rev": "28538fc74889ea2dedbc30e236ce26492e5823ca",
         "type": "github"
       },
       "original": {
@@ -333,11 +337,11 @@
         "nixpkgs": "nixpkgs_7"
       },
       "locked": {
-        "lastModified": 1683577548,
-        "narHash": "sha256-kujPgXEoXUsUt7MIwIaOjNLSIkHpqx7o8kT01nRIpYM=",
+        "lastModified": 1685538626,
+        "narHash": "sha256-R4sJ/w2sBSJmF1p4SHuqh00QXf+Bjxvujdex0s4QHXM=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "ad4b822734adfd7800194eb574b31fe540923302",
+        "rev": "28538fc74889ea2dedbc30e236ce26492e5823ca",
         "type": "github"
       },
       "original": {
@@ -420,11 +424,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1673134516,
-        "narHash": "sha256-mAZQKqkNQbBmJnmUU0blOfkKlgMSSVyPHdeWeuKad8U=",
+        "lastModified": 1683408522,
+        "narHash": "sha256-9kcPh6Uxo17a3kK3XCHhcWiV1Yu1kYj22RHiymUhMkU=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "f6f44561884c3470e2b783683d5dbac42dfc833b",
+        "rev": "897876e4c484f1e8f92009fd11b7d988a121a4e7",
         "type": "github"
       },
       "original": {
@@ -590,11 +594,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1672712534,
-        "narHash": "sha256-8S0DdMPcbITnlOu0uA81mTo3hgX84wK8S9wS34HEFY4=",
+        "lastModified": 1683080331,
+        "narHash": "sha256-nGDvJ1DAxZIwdn6ww8IFwzoHb2rqBP4wv/65Wt5vflk=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "69fb7bf0a8c40e6c4c197fa1816773774c8ac59f",
+        "rev": "d59c3fa0cba8336e115b376c2d9e91053aa59e56",
         "type": "github"
       },
       "original": {
@@ -615,11 +619,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1673231106,
-        "narHash": "sha256-Tbw4N/TL+nHmxF8RBoOJbl/6DRRzado/9/ttPEzkGr8=",
+        "lastModified": 1683598806,
+        "narHash": "sha256-L0tcBTcF6QzFFvWbXO2TXlBszAvxvm3zblYe0iUF/Yk=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "3488cec01351c2f1086b02a3a61808be7a25103e",
+        "rev": "0cef0c3ed57980dc9a8b916e6b596d7f2f6d34f1",
         "type": "github"
       },
       "original": {
@@ -642,6 +646,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 8ebbca73..cb88c340 100644
--- a/flake.nix
+++ b/flake.nix
@@ -9,7 +9,9 @@
     nixpkgs.follows = "charon/nixpkgs";
     hacl-nix.url = "github:hacl-star/hacl-nix";
     lean.url = "github:leanprover/lean4";
-    lake.url = "github:leanprover/lake";
+    #lake.url = "github:leanprover/lake";
+    lake.url = "github:leanprover/lake/lean4-master";
+    #lake.flake = false;
   };
 
   # Remark: keep the list of outputs in sync with the list of inputs above
@@ -52,6 +54,7 @@
         aeneas = ocamlPackages.buildDunePackage {
           pname = "aeneas";
           version = "0.1.0";
+          duneVersion = "3";
           src = ./compiler;
           buildInputs = [ easy_logging ocamlgraph unionFind charon.packages.${system}.charon-ml ]
             ++ (with ocamlPackages; [