bump

Author: RemyDegenne

lake-manifest.json

@@ -12,47 +12,47 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "828d43765f45eb050c06da3ce245f2c12d1306c0",
+   "rev": "9b5a133a39dc8213e71a71f14e2b7463d6d1ffd8",
    "name": "ChallengeGen",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.34.0",
+   "inputRev": "v4.35.0-rc2",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/RemyDegenne/meaning-graph",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fc2c3622756485f5b632ce22fa36117a3b206201",
+   "rev": "0b630e48856e8adce0ca4029fb3f54b0bcae9660",
    "name": "MeaningGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.34.0",
+   "inputRev": "v4.35.0-rc2",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/RemyDegenne/characterization",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "de3336285f154dc0fef95920b2b393b35e6fae1b",
+   "rev": "7be791ff6deefbce79834e445036966feb9c33e4",
    "name": "Characterization",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.34.0",
+   "inputRev": "v4.35.0-rc2",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cad4b633e75ea769b851f12f9ca3b4f0dfcc625f",
+   "rev": "9f8096e40b31715b1d8d5997f15a0bd832f7e37d",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.34.0",
+   "inputRev": "v4.35.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+   "rev": "2842b9871b04862f944c032e34052cb9448ccb71",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -62,7 +62,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a1a61c9678da010e958ed24cdfa6f635b85f172a",
+   "rev": "68a463c484e24708627b8761e8730e76b295d1e2",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -72,7 +72,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c",
+   "rev": "e50948299c4dc4a4c21b1c34b6a6a4fddc19f912",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -92,7 +92,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9b90b7f938d6169246325df002351014f49945ef",
+   "rev": "d047cb484b2f3598187450935dbcc84d078cb581",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -5,7 +5,7 @@ package Referee where
   version := v!"0.1.0"
   leanOptions := #[⟨`autoImplicit, false⟩]
 
-require verso from git "https://github.com/leanprover/verso" @ "v4.34.0"
+require verso from git "https://github.com/leanprover/verso" @ "v4.35.0-rc2"
 
 /-- The `@[specifies]` and `@[characterization]` attributes, in a *separate, dependency-free
 package* rather than a library of this one. A project that wants to annotate its specifications must
@@ -15,7 +15,7 @@ own, with its own checks.
 This tool depends on it for the other end of the same wire: reading the annotations back out of a
 target project needs the environment extension registered in *this* process, since imported
 extension entries are matched to registered extensions by name and silently dropped otherwise. -/
-require Characterization from git "https://github.com/RemyDegenne/characterization" @ "v4.34.0"
+require Characterization from git "https://github.com/RemyDegenne/characterization" @ "v4.35.0-rc2"
 
 /-- Declaration-dependency analysis, in a *separate, dependency-free package* rather than a library
 of this one, for the same reason as `Characterization`: it is useful on its own to any project that
@@ -25,7 +25,7 @@ this tool's build.
 That independence is why it is a repository of its own rather than a subdirectory here, and its own
 tests and proofs went with it. This tool is one such consumer — `Referee/Collect.lean` delegates
 every dependency computation to it — but it is not a privileged one. -/
-require MeaningGraph from git "https://github.com/RemyDegenne/meaning-graph" @ "v4.34.0"
+require MeaningGraph from git "https://github.com/RemyDegenne/meaning-graph" @ "v4.35.0-rc2"
 
 /-- Standalone-file extraction: one declaration turned into a file that compiles on its own, its
 dependencies inlined and its proofs `sorry`ed. A *separate, dependency-free package* for the same
@@ -39,7 +39,7 @@ something to say which declarations to extract and what each one's closure is.
 
 That independence is why it is a repository of its own rather than a subdirectory here, and its own
 checks went with it. -/
-require ChallengeGen from git "https://github.com/RemyDegenne/challenge-gen" @ "v4.34.0"
+require ChallengeGen from git "https://github.com/RemyDegenne/challenge-gen" @ "v4.35.0-rc2"
 
 /-- Junk-value analysis — where a definition rests on the value a total function returns outside the
 domain its name suggests — as a *separate, dependency-free package*, for the same reason as

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.34.0
+leanprover/lean4:v4.35.0-rc2