Bump Lean version

PatrickMassot · Jul 19, 2024 · 2ca20b1 · 2ca20b1
1 parent dd9bf4b
commit 2ca20b1
Show file tree

Hide file tree

Showing 4 changed files with 20 additions and 9 deletions.
diff --git a/Verbose/English/Help.lean b/Verbose/English/Help.lean
@@ -424,6 +424,8 @@ configureAnonymousGoalSplittingLemmas Iff.intro Iff.intro' And.intro And.intro'
 
 configureHelpProviders DefaultHypHelp DefaultGoalHelp
 
+set_option linter.unusedTactic false
+
 /--
 info: Help
 • By h applied to n₀ using hn₀ we get (hyp : P n₀)

diff --git a/Verbose/French/Help.lean b/Verbose/French/Help.lean
@@ -424,6 +424,8 @@ configureAnonymousGoalSplittingLemmas Iff.intro Iff.intro' And.intro And.intro'
 
 configureHelpProviders DefaultHypHelp DefaultGoalHelp
 
+set_option linter.unusedTactic false
+
 /--
 info: Aide
 • Par h appliqué à n₀ en utilisant hn₀ on obtient (hyp : P n₀)

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,10 +1,11 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
+   "scope": "leanprover-community",
+   "rev": "f27beb10b53350d6c1257ba3a8899df369135cc3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,6 +14,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
+   "scope": "leanprover-community",
    "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
+   "scope": "leanprover-community",
+   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
+   "scope": "leanprover-community",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +64,8 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "9cff34c8c3bb7759115f12715b45301544dd0093",
+   "scope": "",
+   "rev": "23c87df3dc33f21c40279c894022a37b71ffa918",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc3
+leanprover/lean4:v4.10.0-rc2
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.9.0-rc3
		leanprover/lean4:v4.10.0-rc2