diff options
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.mli | 6 | ||||
| -rw-r--r-- | compiler/aeneas.opam | 2 | ||||
| -rw-r--r-- | compiler/dune-project | 2 | ||||
| -rw-r--r-- | flake.lock | 105 | ||||
| -rw-r--r-- | flake.nix | 5 |
6 files changed, 73 insertions, 51 deletions
@@ -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) @@ -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", @@ -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; [ |