Track Lean core changes for measurable monads and rdo

.github/upstream/Export.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 David Ledvinka. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Ledvinka
+-/
+import RandomDo.Monad.Notation
+import Lean.DeclarationRange
+import Lean.Data.Json
+
+/-!
+Run `lake env lean .github/upstream/Export.lean > .lake/upstream-current.json` after building the
+tracked modules. Source ranges come from the running toolchain's declaration metadata, including
+class fields and definition bodies. They are meaningful only at the accompanying Lean commit.
+-/
+
+open Lean RandomDo.Analogue
+
+run_cmd do
+  let env ← getEnv
+  let mut entries : Array Json := #[]
+  for (decl, _) in env.constants do
+    if let some sources := analogueAttr.getParam? env decl then
+      let some localIdx := env.getModuleIdxFor? decl
+        | throwError "No module for tracked declaration `{decl}`"
+      let localModule := env.header.moduleNames[localIdx.toNat]!
+      for source in sources do
+        let some idx := env.getModuleIdxFor? source
+          | throwError "No module for upstream declaration `{source}`"
+        let mod := env.header.moduleNames[idx.toNat]!
+        unless [`Init, `Lean, `Std].any (·.isPrefixOf mod) do
+          throwError "Analogue declaration `{source}` belongs to `{mod}`, not Lean core"
+        let some ranges ← findDeclarationRanges? source
+          | throwError "No source range for upstream declaration `{source}`"
+        let first := ranges.range.pos.line
+        let last := ranges.range.endPos.line - if ranges.range.endPos.column == 0 then 1 else 0
+        entries := entries.push <| Json.mkObj [
+          ("local", toJson decl.toString),
+          ("local_file", toJson (localModule.toString.replace "." "/" ++ ".lean")),
+          ("upstream", toJson source.toString),
+          ("path", toJson ("src/" ++ mod.toString.replace "." "/" ++ ".lean")),
+          ("start", toJson first), ("end", toJson last)]
+  let result := Json.mkObj [
+    ("schema", toJson (1 : Nat)), ("commit", toJson Lean.githash), ("entries", toJson entries)]
+  IO.println result.compress

.github/upstream/README.md

@@ -0,0 +1,89 @@
+# Lean core tracking
+
+This directory contains maintainer tooling run by GitHub Actions. The library provides only the
+`analogue` attribute and its annotations; checking, baseline updates, and issue reporting live here.
+All commands below run from the repository root.
+
+Use `@[analogue Core.declaration]` to link an adaptation to its Lean core counterpart:
+
+```lean
+@[analogue Bind]
+class MeasurableSpaceBind ...
+
+@[analogue Lean.Elab.Do.DoOps.default]
+def randOps ...
+```
+
+Multiple names use spaces: `@[analogue Pure Bind]`. Qualify names when necessary;
+`_root_.bind_congr`, for example, avoids resolving to the declaration being annotated.
+The attribute resolves and records names. It is defined in `RandomDo/Util/Analogue.lean` and has
+no dependency on this tooling. The exporter restricts this workflow's tracked origins to Lean core.
+
+## Checking for changes
+
+The initial scope is `RandomDo/Monad/MeasurableSpace.lean` and `RandomDo/Monad/Notation.lean`.
+To check the current toolchain against the recorded baselines:
+
+```sh
+lake build --wfail RandomDo.Monad.MeasurableSpace RandomDo.Monad.Notation
+lake env lean .github/upstream/Export.lean > .lake/upstream-current.json
+python3 .github/upstream/check.py check --metadata .lake/upstream-current.json
+```
+
+The build workflow runs this check on PRs. The exporter gets declaration locations from Lean;
+`.github/upstream/baseline.json` stores the source path, line range, and exact Lean commit for each
+mapping.
+The Python script uses Git to compare those upstream regions with the target revision. It
+requires Python 3.10+ and Git, with no Python packages. Later line insertions do not shift the
+baseline because its range always refers to its recorded commit.
+
+The weekly workflow compares against Lean's default development branch every Monday at 08:23 UTC.
+It maintains one issue listing affected declarations and linking to the full diff report.
+Unchanged relevant edits do not cause repeated updates. It closes the issue when differences
+are resolved; a failed check fails the workflow and leaves the issue alone. The schedule starts
+after merge to the default branch and can also be run manually.
+
+To run the same comparison locally:
+
+```sh
+python3 .github/upstream/check.py check --target HEAD --report .lake/upstream-report.md
+```
+
+Sources are fetched into `.lake/upstream-lean.git`; no future Lean code is built or executed.
+Use `--repo /path/to/lean4` before the subcommand to use a local Git repository without fetching.
+Exit codes are 0 for unchanged, 1 for changes, and 2 for errors. `--advisory` allows changes while
+still failing on errors; it is used by the weekly workflow.
+
+## Updating a baseline
+
+Review the upstream diff, adapt the local code as needed, and explain intentional differences
+in the PR. Then record just the declarations you reviewed:
+
+```sh
+python3 .github/upstream/check.py record --metadata .lake/upstream-current.json --only RDo.randOps
+```
+
+Commit the generated baseline change with the adaptation. Other declarations retain their
+baselines. For a rename, pass both old and new names to `--only`; for a removed annotation,
+pass its old name. `--all` explicitly records every mapping. Checks never advance baselines.
+To track another module, import it in `.github/upstream/Export.lean`, export, and record its mappings.
+
+## Scope
+
+The initial Lean v4.35.0 baseline starts monitoring the existing adaptations; it is not a
+correctness audit. Known differences include the omitted dead-syntax guard in the
+`mkPureApp` override in `RDo.randOps`, the loop adapters' missing `invariant` / `decreasing` syntax and
+verification hooks, and the measurable hierarchy's intentional omission of applicative classes.
+
+The checker reports edits within a declaration, including its body, and conservatively includes
+insertions and replacements at either boundary. Renames and file moves are reported at the old
+location. Changes to untracked helpers or surrounding sections can also affect behavior, so normal
+elaboration and behavior tests remain necessary.
+
+The checker, attribute, and issue tests run offline:
+
+```sh
+python3 -m unittest discover -s .github/upstream/tests -p 'test_check.py'
+lake env lean .github/upstream/tests/Analogue.lean
+node --test .github/upstream/tests/test_notify.cjs
+```

.github/upstream/baseline.json

@@ -0,0 +1,231 @@
+{
+  "schema": 1,
+  "repository": "https://github.com/leanprover/lean4",
+  "entries": [
+    {
+      "end": 41,
+      "local": "LawfulMeasurableSpaceFunctor",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Lawful/Basic.lean",
+      "start": 20,
+      "upstream": "LawfulFunctor",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 159,
+      "local": "LawfulMeasurableSpaceMonad",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Lawful/Basic.lean",
+      "start": 125,
+      "upstream": "LawfulMonad",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 3881,
+      "local": "MeasurableSpaceBind",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Prelude.lean",
+      "start": 3869,
+      "upstream": "Bind",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 180,
+      "local": "MeasurableSpaceBind.bind_congr",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Lawful/Basic.lean",
+      "start": 179,
+      "upstream": "bind_congr",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 388,
+      "local": "MeasurableSpaceForIn",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Core.lean",
+      "start": 366,
+      "upstream": "ForIn",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 416,
+      "local": "MeasurableSpaceForIn'",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Core.lean",
+      "start": 392,
+      "upstream": "ForIn'",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 3937,
+      "local": "MeasurableSpaceFunctor",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Prelude.lean",
+      "start": 3903,
+      "upstream": "Functor",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 186,
+      "local": "MeasurableSpaceFunctor.map_congr",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Lawful/Basic.lean",
+      "start": 185,
+      "upstream": "map_congr",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 4038,
+      "local": "MeasurableSpaceMonad",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Prelude.lean",
+      "start": 4020,
+      "upstream": "Monad",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 3899,
+      "local": "MeasurableSpacePure",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Prelude.lean",
+      "start": 3885,
+      "upstream": "Pure",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 409,
+      "local": "RDo.elabRDoFor",
+      "local_file": "RandomDo/Monad/Notation.lean",
+      "path": "src/Lean/Elab/BuiltinDo/For.lean",
+      "start": 274,
+      "upstream": "Lean.Elab.Do.elabDoFor",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 1104,
+      "local": "RDo.elabRand",
+      "local_file": "RandomDo/Monad/Notation.lean",
+      "path": "src/Lean/Elab/Do/Basic.lean",
+      "start": 1102,
+      "upstream": "Lean.Elab.Do.elabDo",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 87,
+      "local": "RDo.expandRDoFor",
+      "local_file": "RandomDo/Monad/Notation.lean",
+      "path": "src/Lean/Elab/BuiltinDo/For.lean",
+      "start": 24,
+      "upstream": "Lean.Elab.Do.expandDoFor",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 339,
+      "local": "RDo.randOps",
+      "local_file": "RandomDo/Monad/Notation.lean",
+      "path": "src/Lean/Elab/Do/Basic.lean",
+      "start": 309,
+      "upstream": "Lean.Elab.Do.DoOps.default",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 217,
+      "local": "RDo.rdoFor",
+      "local_file": "RandomDo/Monad/Notation.lean",
+      "path": "src/Lean/Parser/Do.lean",
+      "start": 208,
+      "upstream": "Lean.Parser.Term.doFor",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 186,
+      "local": "RDo.rdoForDecl",
+      "local_file": "RandomDo/Monad/Notation.lean",
+      "path": "src/Lean/Parser/Do.lean",
+      "start": 184,
+      "upstream": "Lean.Parser.Term.doForDecl",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 48,
+      "local": "id_mMap'",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Lawful/Basic.lean",
+      "start": 47,
+      "upstream": "id_map'",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 30,
+      "local": "instMeasurableSpaceForInOfForIn'",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Basic.lean",
+      "start": 16,
+      "upstream": "instForInOfForIn'",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 208,
+      "local": "mBind_mMap_left",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Lawful/Basic.lean",
+      "start": 205,
+      "upstream": "bind_map_left",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 167,
+      "local": "mBind_mPure",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Lawful/Basic.lean",
+      "start": 165,
+      "upstream": "bind_pure",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 183,
+      "local": "mBind_mPure_unit",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Lawful/Basic.lean",
+      "start": 182,
+      "upstream": "bind_pure_unit",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 174,
+      "local": "mMap_eq_mPure_mBind",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Lawful/Basic.lean",
+      "start": 169,
+      "upstream": "map_eq_pure_bind",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 203,
+      "local": "mMap_mBind",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Lawful/Basic.lean",
+      "start": 200,
+      "upstream": "map_bind",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 52,
+      "local": "mMap_mMap",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Lawful/Basic.lean",
+      "start": 50,
+      "upstream": "Functor.map_map",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    },
+    {
+      "end": 85,
+      "local": "mMap_mPure",
+      "local_file": "RandomDo/Monad/MeasurableSpace.lean",
+      "path": "src/Init/Control/Lawful/Basic.lean",
+      "start": 85,
+      "upstream": "LawfulApplicative.map_pure",
+      "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc"
+    }
+  ]
+}