Merge pull request #536 from Seasawher/auto-update-branch

Lean/Mathlib update

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `337d737caea8838b2303b3cd16fb35e75acedd84`
+Mathlib version: `35f7a9bdabaf259310b5434c0e67f4b7b704b96d`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `337d737caea8838b2303b3cd16fb35e75acedd84`
+Mathlib version: `35f7a9bdabaf259310b5434c0e67f4b7b704b96d`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `337d737caea8838b2303b3cd16fb35e75acedd84`
+Mathlib version: `35f7a9bdabaf259310b5434c0e67f4b7b704b96d`
 
 ## Elab.async
 type: `Bool`
@@ -74,7 +74,7 @@ type: `Bool`
 
 default: `false`
 
-(aesop) collect statistics about Aesop invocations. Use #aesop_stats to display the collected statistics.
+(aesop) Collect statistics about Aesop invocations. Use #aesop_stats to display the collected statistics.
 
 ## aesop.dev.dynamicStructuring
 type: `Bool`
@@ -111,6 +111,13 @@ default: `false`
 
 (aesop) Print smaller error messages. Used for testing.
 
+## aesop.stats.file
+type: `String`
+
+default: `""`
+
+(aesop) Write statistics about Aesop invocations to the given file in JSONL format. Each invocation adds one JSON record to the file.
+
 ## aesop.warn.applyIff
 type: `Bool`
 
@@ -904,6 +911,13 @@ default: `false`
 
 enable the ppRoundtrip linter
 
+## linter.privateModule
+type: `Bool`
+
+default: `false`
+
+Enable the `privateModule` linter, which lints against nonempty modules that have only private declarations.
+
 ## linter.pythonStyle
 type: `Bool`
 
@@ -2136,7 +2150,7 @@ Number of results requested from statesearch (default 6)
 ## statesearch.revision
 type: `String`
 
-default: `"v4.26.0-rc1"`
+default: `"v4.26.0-rc2"`
 
 Revision of LeanStateSearch to use
 

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `337d737caea8838b2303b3cd16fb35e75acedd84`
+Mathlib version: `35f7a9bdabaf259310b5434c0e67f4b7b704b96d`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "337d737caea8838b2303b3cd16fb35e75acedd84",
+   "rev": "35f7a9bdabaf259310b5434c0e67f4b7b704b96d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ec4a54b5308c1f46b4b52a9c62fb67d193aa0972",
+   "rev": "74835c84b38e4070b8240a063c6417c767e551ae",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7ff87023a8e1b358d2d01c1bc56b040a60609577",
+   "rev": "6e3bb4bf31f731ab28891fe229eb347ec7d5dad3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "894c511d39bf442636bcba085245a1cf2bbdf665",
+   "rev": "2aaad968dd10a168b644b6a5afd4b92496af4710",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.81",
+   "inputRev": "v0.0.82",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c00943d5ff28c6dc623dbc24f8d659a9d3a3d29a",
+   "rev": "ea86e311a31a4dfa2abf3d7c0664b8c28499369e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1be06a278c3c249edafb722bfb278622024929d8",
+   "rev": "a31845b5557fd5e47d52b9e2977a1b0eff3c38c3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c278d4e94fe43bc38da4966795dc0c72538e68ab",
+   "rev": "30cfb2255996f3e6217a77fd940fde1f3e12ccc2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "00fad25fa9bedece1f1f988ab9c180dfe3d535b3",
+   "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0-rc1",
+   "inputRev": "v4.26.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "«mathlib4-help»",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.26.0-rc1
+leanprover/lean4:v4.26.0-rc2