From f6376df6201054dadc6805c48396da857e67a11a Mon Sep 17 00:00:00 2001 From: Ryan Lahfa Date: Tue, 27 Aug 2024 17:02:12 +0200 Subject: [PATCH] chore(docs/user): update to 4.11.0-rc2 Micro-guide for update: - Update the Lean flake. - Update all the sha256 hashes of every dependency if you have a compilation error, e.g. batteries changed, etc. The day where `inputs.lean.packages.${system}.deprecated` disappear, we will need to consider an alternative for the nixpkgs from lean, etc. Signed-off-by: Ryan Lahfa --- docs/user/flake.lock | 121 ++++--------------------------------------- docs/user/flake.nix | 18 +++---- 2 files changed, 18 insertions(+), 121 deletions(-) diff --git a/docs/user/flake.lock b/docs/user/flake.lock index 0eca7f7a9..cdc9b610c 100644 --- a/docs/user/flake.lock +++ b/docs/user/flake.lock @@ -17,22 +17,6 @@ "type": "github" } }, - "flake-compat": { - "flake": false, - "locked": { - "lastModified": 1673956053, - "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=", - "owner": "edolstra", - "repo": "flake-compat", - "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9", - "type": "github" - }, - "original": { - "owner": "edolstra", - "repo": "flake-compat", - "type": "github" - } - }, "flake-utils": { "inputs": { "systems": "systems" @@ -54,42 +38,24 @@ "lean": { "inputs": { "flake-utils": "flake-utils", - "lean4-mode": "lean4-mode", - "nix": "nix", - "nixpkgs": "nixpkgs_2", + "nixpkgs": "nixpkgs", "nixpkgs-old": "nixpkgs-old" }, "locked": { - "lastModified": 1722403448, - "narHash": "sha256-lNWr84aeVpI/p/oxkNAUlUMUROGGzHAkb2D9q8BzHeA=", + "lastModified": 1723429404, + "narHash": "sha256-Us3VccCsU1nsqMtAuG5hUYR95j7a8/dQqtBpQE4Cgb0=", "owner": "leanprover", "repo": "lean4", - "rev": "c375e19f6b656fcd594cdca3a38b8578634df8cd", + "rev": "0edf1bac392f7e2fe0266b28b51c498306363a84", "type": "github" }, "original": { "owner": "leanprover", - "ref": "v4.10.0", + "ref": "v4.11.0-rc2", "repo": "lean4", "type": "github" } }, - "lean4-mode": { - "flake": false, - "locked": { - "lastModified": 1709737301, - "narHash": "sha256-uT9JN2kLNKJK9c/S/WxLjiHmwijq49EgLb+gJUSDpz0=", - "owner": "leanprover", - "repo": "lean4-mode", - "rev": "f1f24c15134dee3754b82c9d9924866fe6bc6b9f", - "type": "github" - }, - "original": { - "owner": "leanprover", - "repo": "lean4-mode", - "type": "github" - } - }, "leanInk": { "flake": false, "locked": { @@ -106,22 +72,6 @@ "type": "github" } }, - "libgit2": { - "flake": false, - "locked": { - "lastModified": 1697646580, - "narHash": "sha256-oX4Z3S9WtJlwvj0uH9HlYcWv+x1hqp8mhXl7HsLu2f0=", - "owner": "libgit2", - "repo": "libgit2", - "rev": "45fd9ed7ae1a9b74b957ef4f337bc3c8b3df01b5", - "type": "github" - }, - "original": { - "owner": "libgit2", - "repo": "libgit2", - "type": "github" - } - }, "mdBook": { "flake": false, "locked": { @@ -138,39 +88,18 @@ "type": "github" } }, - "nix": { - "inputs": { - "flake-compat": "flake-compat", - "libgit2": "libgit2", - "nixpkgs": "nixpkgs", - "nixpkgs-regression": "nixpkgs-regression" - }, - "locked": { - "lastModified": 1711102798, - "narHash": "sha256-CXOIJr8byjolqG7eqCLa+Wfi7rah62VmLoqSXENaZnw=", - "owner": "NixOS", - "repo": "nix", - "rev": "a22328066416650471c3545b0b138669ea212ab4", - "type": "github" - }, - "original": { - "owner": "NixOS", - "repo": "nix", - "type": "github" - } - }, "nixpkgs": { "locked": { - "lastModified": 1709083642, - "narHash": "sha256-7kkJQd4rZ+vFrzWu8sTRtta5D1kBG0LSRYAfhtmMlSo=", + "lastModified": 1710889954, + "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "b550fe4b4776908ac2a861124307045f8e717c8e", + "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b", "type": "github" }, "original": { "owner": "NixOS", - "ref": "release-23.11", + "ref": "nixpkgs-unstable", "repo": "nixpkgs", "type": "github" } @@ -192,38 +121,6 @@ "type": "github" } }, - "nixpkgs-regression": { - "locked": { - "lastModified": 1643052045, - "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", - "type": "github" - }, - "original": { - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", - "type": "github" - } - }, - "nixpkgs_2": { - "locked": { - "lastModified": 1710889954, - "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b", - "type": "github" - }, - "original": { - "owner": "NixOS", - "ref": "nixpkgs-unstable", - "repo": "nixpkgs", - "type": "github" - } - }, "root": { "inputs": { "alectryon": "alectryon", diff --git a/docs/user/flake.nix b/docs/user/flake.nix index 4563f66bd..6499ef350 100644 --- a/docs/user/flake.nix +++ b/docs/user/flake.nix @@ -2,7 +2,7 @@ { description = "Aeneas documentation"; - inputs.lean.url = "github:leanprover/lean4/v4.10.0"; + inputs.lean.url = "github:leanprover/lean4/v4.11.0-rc2"; inputs.flake-utils.follows = "lean/flake-utils"; inputs.mdBook = { url = "github:leanprover/mdBook"; @@ -18,7 +18,7 @@ }; outputs = inputs@{ self, ... }: inputs.flake-utils.lib.eachDefaultSystem (system: - with inputs.lean.packages.${system}; with nixpkgs; + with inputs.lean.packages.${system}.deprecated; with nixpkgs; let doc-src = ./.; # lib.sourceByRegex ../. ["doc.*" "tests(/lean(/beginEndAsMacro.lean)?)?"]; leanLib = callPackage ./nix { }; @@ -87,7 +87,7 @@ aeneas-base = let - manifest = builtins.fromJSON (builtins.readFile ./lake-manifest.json); + manifest = builtins.fromJSON (builtins.readFile ../../backends/lean/lake-manifest.json); fetchFromLakeManifest = leanLib.fetchFromLakeManifest manifest; inherit (leanLib) addFakeFiles; @@ -95,14 +95,14 @@ name = "Batteries"; src = fetchFromLakeManifest { name = "batteries"; - hash = "sha256-JbOOKsUiYedNj3oiCNfwgkWyEIXsb1bAUm3uSEWsWPs="; + hash = "sha256-EGcjOcTu66rtAICAqgPKaR8kBlImoq4lUZfNZR9dHiY="; }; }; qq = buildLeanPackage { name = "Qq"; src = fetchFromLakeManifest { name = "Qq"; - hash = "sha256-//sZE32XzebePy81HEwNhIH8YW8iHgk+O8A0y/qNJrg="; + hash = "sha256-iFlAiq8Uxq+QD6ql4EMpRQENvIhKdioaleoEiDmMuDQ="; }; }; aesop = buildLeanPackage { @@ -110,7 +110,7 @@ deps = [ batteries ]; src = fetchFromLakeManifest { name = "aesop"; - hash = "sha256-LzooSD6NaSQyqKkBcxbSbjIZHrnDBx/lp/s4UdWeHpU="; + hash = "sha256-97xcl82SU9/EZ8L4vT7g/Ureoi11s3c4ZeFlaCd4Az4="; }; }; import-graph = buildLeanPackage { @@ -118,7 +118,7 @@ deps = [ batteries ]; src = fetchFromLakeManifest { name = "importGraph"; - hash = "sha256-3bWWnklUHuY/dA1Y3SK78SSDE+J8syEsMPJ67LnRI3M="; + hash = "sha256-u8tk5IWU/n47kmNAlxZCmurq7e08oCzANhsk9VJeCCM="; }; }; proof-widgets = buildLeanPackage { @@ -126,7 +126,7 @@ deps = [ batteries ]; src = fetchFromLakeManifest { name = "proofwidgets"; - hash = "sha256-6PzWhCNxxcuh0vEV0JhV0G30NVkYGEDup1j3KvG2VzA="; + hash = "sha256-jPvUi73NylxFiU5V0tjK92M0hJfHWZi5ULZldDwctYY="; }; overrideBuildModAttrs = addFakeFiles { @@ -150,7 +150,7 @@ name = "Mathlib"; src = fetchFromLakeManifest { name = "mathlib"; - hash = "sha256-gJYmaNDVus3vgUE3aNQfyMCcQJxw/lq5aYtLjs4OI7I="; + hash = "sha256-3FnWd0dUVhNyUPxLNNHA41RWF34fwmXulnRSIEmIQXM="; }; }; in