From 611ec4c02c00d000df17c1d2b01765e96c7f3174 Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 21:49:33 +0000 Subject: [PATCH 1/4] Annotate measurable monad and rdo adaptations with Lean core origins --- RandomDo.lean | 1 + RandomDo/Monad/MeasurableSpace.lean | 33 ++++++++++++++++----- RandomDo/Monad/Notation.lean | 15 +++++++--- RandomDo/Util/Upstream.lean | 46 +++++++++++++++++++++++++++++ scripts/ExportUpstream.lean | 42 ++++++++++++++++++++++++++ scripts/tests/Upstream.lean | 34 +++++++++++++++++++++ 6 files changed, 160 insertions(+), 11 deletions(-) create mode 100644 RandomDo/Util/Upstream.lean create mode 100644 scripts/ExportUpstream.lean create mode 100644 scripts/tests/Upstream.lean diff --git a/RandomDo.lean b/RandomDo.lean index b2d4043..bde6e04 100644 --- a/RandomDo.lean +++ b/RandomDo.lean @@ -23,3 +23,4 @@ public import RandomDo.Tactic.IsMarkov.Deriving public import RandomDo.Tactic.IsMarkov.Elab public import RandomDo.Tactic.IsMarkov.ForInStep public import RandomDo.Tactic.IsMarkov.Lemmas +public import RandomDo.Util.Upstream diff --git a/RandomDo/Monad/MeasurableSpace.lean b/RandomDo/Monad/MeasurableSpace.lean index b593969..69d0546 100644 --- a/RandomDo/Monad/MeasurableSpace.lean +++ b/RandomDo/Monad/MeasurableSpace.lean @@ -7,6 +7,7 @@ module public import Mathlib.Control.Random public import Mathlib.MeasureTheory.Measure.GiryMonad +public meta import RandomDo.Util.Upstream /-! # Measurable Space Monad @@ -37,6 +38,7 @@ section MeasurableSpaceMonad /-- A functor on types with a `MeasurableSpace` instance. The `mMap` operator `<$>ₘ` is overloaded via instances of this class. This class does not require proofs of the `MeasurableSpaceFunctor` axioms. Proofs may be provided or required via the `LawfulMeasurableSpaceFunctor` class. -/ +@[upstream Functor] class MeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Type v) : Type (max (u+1) v) where /-- @@ -64,6 +66,7 @@ The `mPure` function is overloaded via `MeasurableSpacePure` instances. `MeasurableSpacePure` is typically accessed via `MeasurableSpaceMonad` instances, which extend it. -/ +@[upstream Pure] class MeasurableSpacePure (f : (α : Type u) → [MeasurableSpace α] → Type v) where /-- Given `a : α` where `α` has a `MeasurableSpace` instance, `mPure a : f α` represents an action that does nothing and returns a -/ @@ -74,6 +77,7 @@ The `>>=ₘ` operator is overloaded via instances of `MeasurableSpaceBind`. `MeasurableSpaceBind` is typically used via `MeasurableSpaceMonad`, which extends it. -/ +@[upstream Bind] class MeasurableSpaceBind (m : (α : Type u) → [MeasurableSpace α] → Type v) where /-- Sequences two computations, allowing the second to depend on the value computed by the first. @@ -87,6 +91,7 @@ class MeasurableSpaceBind (m : (α : Type u) → [MeasurableSpace α] → Type v /-- A monad on types with a `MeasurableSpace` instance. This abstraction allows the user to write code that depends on "random" side-effects -/ +@[upstream Monad] class MeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type v) : Type (max (u+1) v) extends MeasurableSpaceFunctor m, MeasurableSpacePure m, MeasurableSpaceBind m where @@ -95,10 +100,12 @@ class MeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type variable {m : (α : Type u) → [MeasurableSpace α] → Type v} {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] +@[upstream _root_.bind_congr] theorem MeasurableSpaceBind.bind_congr [MeasurableSpaceBind m] {x : m α} {f g : α → m β} (h : ∀ a, f a = g a) : x >>=ₘ f = x >>=ₘ g := by simp [funext h] +@[upstream _root_.map_congr] theorem MeasurableSpaceFunctor.map_congr [MeasurableSpaceFunctor m] {x : m α} {f g : α → β} (h : ∀ a, f a = g a) : (f <$>ₘ x : m β) = g <$>ₘ x := by simp [funext h] @@ -110,6 +117,7 @@ section Lawful open MeasurableSpaceFunctor /-- A `MeasurableSpaceFunctor` satisfies the measurable space functor laws. -/ +@[upstream LawfulFunctor] class LawfulMeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceFunctor f] [∀ α, [MeasurableSpace α] → MeasurableSpace (f α)] : Prop where @@ -135,9 +143,11 @@ variable {f : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpac [∀ α, [MeasurableSpace α] → MeasurableSpace (f α)] [LawfulMeasurableSpaceFunctor f] {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] -@[simp] theorem id_mMap' (x : f α) : (fun a => a) <$>ₘ x = x := id_mMap x +@[upstream id_map', simp] +theorem id_mMap' (x : f α) : (fun a => a) <$>ₘ x = x := id_mMap x -@[simp] theorem mMap_mMap {g₀ : α → β} {g₁ : β → γ} (x : f α) +@[upstream Functor.map_map, simp] +theorem mMap_mMap {g₀ : α → β} {g₁ : β → γ} (x : f α) (hg₀ : Measurable g₀) (hg₁ : Measurable g₁) : g₁ <$>ₘ g₀ <$>ₘ x = (fun a => g₁ (g₀ a)) <$>ₘ x := (comp_mMap x hg₀ hg₁).symm @@ -145,6 +155,7 @@ variable {f : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpac open MeasurableSpaceBind MeasurableSpacePure MeasurableSpaceFunctor /-- A `MeasurableSpaceMonad` satisfies the measurable space monad laws. -/ +@[upstream LawfulMonad] class LawfulMeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceMonad m] [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)] : Prop @@ -187,27 +198,33 @@ variable {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpac [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)] [LawfulMeasurableSpaceMonad m] {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] -@[simp] theorem mMap_mPure {f : α → β} (hf : Measurable f) (x : α) : +@[upstream LawfulApplicative.map_pure, simp] +theorem mMap_mPure {f : α → β} (hf : Measurable f) (x : α) : f <$>ₘ (mPure x : m α) = mPure (f x) := by rw [← mBind_mPure_comp hf, mPure_mBind _ (by fun_prop)] -@[simp] theorem mBind_mPure (x : m α) : x >>=ₘ mPure = x := by +@[upstream bind_pure, simp] +theorem mBind_mPure (x : m α) : x >>=ₘ mPure = x := by change x >>=ₘ (fun a => (mPure (id a))) = x rw [mBind_mPure_comp (by fun_prop), id_mMap] +@[upstream map_eq_pure_bind] theorem mMap_eq_mPure_mBind {f : α → β} (hf : Measurable f) (x : m α) : f <$>ₘ x = x >>=ₘ fun a => mPure (f a) := by rw [← mBind_mPure_comp hf x] +@[upstream bind_pure_unit] theorem mBind_mPure_unit {x : m PUnit} : (x >>=ₘ fun _ => mPure ⟨⟩) = x := by rw [mBind_mPure] -@[simp] theorem mMap_mBind {f : β → γ} (hf : Measurable f) (x : m α) +@[upstream map_bind, simp] +theorem mMap_mBind {f : β → γ} (hf : Measurable f) (x : m α) {g : α → m β} (hg : Measurable g) : f <$>ₘ (x >>=ₘ g) = x >>=ₘ fun a => f <$>ₘ g a := by rw [← mBind_mPure_comp hf, mBind_assoc _ hg (by fun_prop)] simp (disch := fun_prop) [mBind_mPure_comp] -@[simp] theorem mBind_mMap_left {f : α → β} (hf : Measurable f) (x : m α) +@[upstream bind_map_left, simp] +theorem mBind_mMap_left {f : α → β} (hf : Measurable f) (x : m α) {g : β → m γ} (hg : Measurable g) : ((f <$>ₘ x) >>=ₘ fun b => g b) = (x >>=ₘ fun a => g (f a)) := by rw [← mBind_mPure_comp hf] @@ -230,6 +247,7 @@ instance instMeasurableSpace {β : Type u} [mβ : MeasurableSpace β] : /-- Monadic iteration in `rdo`-blocks, using the `for x in xs` notation. -/ +@[upstream ForIn] class MeasurableSpaceForIn (ρ : Type uρ) (α : outParam (Type uα)) where /-- Monadically iterates over the contents of a collection `xs`, with a local state `b` and the @@ -241,6 +259,7 @@ class MeasurableSpaceForIn (ρ : Type uρ) (α : outParam (Type uα)) where /-- Monadic iteration in `rdo`-blocks with a membership proof, using the `for h : x in xs` notation. -/ +@[upstream ForIn'] class MeasurableSpaceForIn' (ρ : Type uρ) (α : outParam (Type uα)) (d : outParam (Membership α ρ)) where /-- @@ -251,7 +270,7 @@ class MeasurableSpaceForIn' (ρ : Type uρ) (α : outParam (Type uα)) forIn' {β : Type u} [MeasurableSpace β] (xs : ρ) (b : β) (f : (a : α) → a ∈ xs → β → m (ForInStep β)) : m β -@[simps] +@[upstream instForInOfForIn', simps] instance (priority := 500) instMeasurableSpaceForInOfForIn' {ρ : Type uρ} {α : Type uα} {d : Membership α ρ} [MeasurableSpaceForIn' m ρ α d] : MeasurableSpaceForIn m ρ α where diff --git a/RandomDo/Monad/Notation.lean b/RandomDo/Monad/Notation.lean index 2d2542b..a6f2f0f 100644 --- a/RandomDo/Monad/Notation.lean +++ b/RandomDo/Monad/Notation.lean @@ -6,6 +6,7 @@ Authors: David Ledvinka module public import RandomDo.Monad.MeasurableSpace +public meta import Lean.Elab.BuiltinDo.For public meta import Lean.Meta.ProdN /-! @@ -24,6 +25,7 @@ public meta section namespace RDo /-- Define `DoOp`s for `rdo` notation. -/ +@[upstream Lean.Elab.Do.DoOps.default] def randOps : DoOps := { DoOps.default with mkPureApp α e := do let ⟨m, u, v, _, _⟩ := (← read).monadInfo @@ -67,24 +69,28 @@ def randOps : DoOps := { DoOps.default with syntax (name := randKind) "rdo" doSeq : term /-- Define `rdo` notation elaborator. -/ -@[term_elab randKind] def elabRand : Term.TermElab := fun stx et? => do +@[upstream Lean.Elab.Do.elabDo, term_elab randKind] +def elabRand : Term.TermElab := fun stx et? => do let `(rdo $doSeq) := stx | throwUnsupportedSyntax elabDoWith randOps doSeq et? section LoopElab /-- parses `_ : _ in` for `rdo` for loops -/ +@[upstream Lean.Parser.Term.doForDecl] def rdoForDecl := leading_parser Lean.Parser.optional (atomic (Term.ident >> " : ")) >> termParser >> " in " >> withForbidden "rdo" termParser /-- parser for `rdo` for loops -/ -@[doElem_parser] def rdoFor := leading_parser +@[upstream Lean.Parser.Term.doFor, doElem_parser] +def rdoFor := leading_parser "for " >> sepBy1 rdoForDecl ", " >> "rdo " >> doSeq /-- Define expander for loops in `rdo` notation. Note this code mirrors core's implementation for `do` notation as much as possible. -/ -@[macro rdoFor] def expandRDoFor : Macro := fun stx => do +@[upstream Lean.Elab.Do.expandDoFor, macro rdoFor] +def expandRDoFor : Macro := fun stx => do match stx with | `(rdoFor| for $[$_ : ]? $_:ident in $_ rdo $_) => -- This is the target form of the expander, handled by `elabRDoFor` below. @@ -146,7 +152,8 @@ def rdoForDecl := leading_parser /-- Define loop elaborator for `rdo` notation. Note this code mirrors core's implementation for `do` notation as much as possible. -/ -@[doElem_elab rdoFor] def elabRDoFor : DoElab := fun stx dec => do +@[upstream Lean.Elab.Do.elabDoFor, doElem_elab rdoFor] +def elabRDoFor : DoElab := fun stx dec => do let `(rdoFor| for%$tk $[$h? : ]? $x:ident in $xs rdo $body) := stx | throwUnsupportedSyntax let dec ← dec.ensureUnitAt tk checkMutVarsForShadowing #[x] diff --git a/RandomDo/Util/Upstream.lean b/RandomDo/Util/Upstream.lean new file mode 100644 index 0000000..aa29dbf --- /dev/null +++ b/RandomDo/Util/Upstream.lean @@ -0,0 +1,46 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public meta import Lean.Elab.Command + +/-! +# Tracking adaptations of Lean core + +`@[upstream decl₁ decl₂]` records the Lean core declarations from which a declaration was adapted. +It checks that the names exist and stores them as metadata, without changing the declaration or +its docstring. `scripts/ExportUpstream.lean` exports this metadata for the upstream change checker. +See `docs/upstream-tracking.md` for the review and baseline update workflow. +-/ + +public meta section + +namespace RandomDo.Upstream + +open Lean + +/-- Mark a declaration as an adaptation of one or more declarations in Lean core. -/ +syntax (name := upstream) "upstream " ident+ : attr + +/-- The upstream declarations associated with each adapted declaration. -/ +initialize upstreamAttr : ParametricAttribute (Array Name) ← registerParametricAttribute { + name := `upstream + descr := "Record the Lean core declarations from which this declaration was adapted." + getParam := fun _ stx => do + let names ← stx[1].getArgs.mapM resolveGlobalConstNoOverload + for name in names do + let env ← getEnv + let some idx := env.getModuleIdxFor? name + | throwErrorAt stx "Upstream declaration `{name}` must be imported from Lean core" + let mod := env.header.moduleNames[idx.toNat]! + unless [`Init, `Lean, `Std].any (·.isPrefixOf mod) do + throwErrorAt stx "Upstream declaration `{name}` belongs to `{mod}`, not Lean core" + unless names.toList.eraseDups.length == names.size do + throwErrorAt stx "Duplicate upstream declarations" + return names +} + +end RandomDo.Upstream diff --git a/scripts/ExportUpstream.lean b/scripts/ExportUpstream.lean new file mode 100644 index 0000000..c1d66b1 --- /dev/null +++ b/scripts/ExportUpstream.lean @@ -0,0 +1,42 @@ +/- +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 scripts/ExportUpstream.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.Upstream + +run_cmd do + let env ← getEnv + let mut entries : Array Json := #[] + for (decl, _) in env.constants do + if let some sources := upstreamAttr.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]! + 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 diff --git a/scripts/tests/Upstream.lean b/scripts/tests/Upstream.lean new file mode 100644 index 0000000..221c597 --- /dev/null +++ b/scripts/tests/Upstream.lean @@ -0,0 +1,34 @@ +import RandomDo.Monad.Notation + +open Lean RandomDo.Upstream + +namespace UpstreamTests + +@[upstream Pure Bind] +def adapted : Nat := 0 + +run_cmd do + let env ← getEnv + unless upstreamAttr.getParam? env `UpstreamTests.adapted == some #[`Pure, `Bind] do + throwError "Multiple upstream references were not recorded" + unless upstreamAttr.getParam? env `RDo.randOps == some #[`Lean.Elab.Do.DoOps.default] do + throwError "Upstream metadata did not survive importing a compiled module" + +/-- error: Unknown constant `NoSuchCoreDeclaration` -/ +#guard_msgs in +@[upstream NoSuchCoreDeclaration] +def unknownOrigin : Nat := 0 + +/-- error: Duplicate upstream declarations -/ +#guard_msgs in +@[upstream Pure Pure] +def duplicateOrigin : Nat := 0 + +/-- +error: Upstream declaration `MeasurableSpaceMonad` belongs to `RandomDo.Monad.MeasurableSpace`, not Lean core +-/ +#guard_msgs in +@[upstream MeasurableSpaceMonad] +def nonCoreOrigin : Nat := 0 + +end UpstreamTests From 9005c791bcaba3fd1526a06d9741544c8fb891df Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 21:49:33 +0000 Subject: [PATCH 2/4] Check adapted core declarations in CI and report upstream changes weekly --- .github/workflows/build.yml | 18 ++ .github/workflows/upstream-core.yml | 73 +++++++ README.md | 5 +- docs/upstream-tracking.md | 109 ++++++++++ scripts/tests/test_upstream.py | 171 +++++++++++++++ scripts/upstream.py | 318 ++++++++++++++++++++++++++++ upstream.json | 281 ++++++++++++++++++++++++ 7 files changed, 974 insertions(+), 1 deletion(-) create mode 100644 .github/workflows/upstream-core.yml create mode 100644 docs/upstream-tracking.md create mode 100644 scripts/tests/test_upstream.py create mode 100644 scripts/upstream.py create mode 100644 upstream.json diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 550a3a1..0a9f9e1 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -54,3 +54,21 @@ jobs: build-args: "--wfail" lint: true mk_all-check: true + + - name: Test upstream tracking + run: | + python3 -m unittest discover -s scripts/tests -p 'test_upstream.py' + lake env lean scripts/tests/Upstream.lean + + - name: Check adapted definitions against the pinned Lean toolchain + run: | + lake env lean scripts/ExportUpstream.lean > .lake/upstream-current.json + python3 scripts/upstream.py check --metadata .lake/upstream-current.json \ + --report .lake/upstream-report.md + + - name: Show upstream changes + if: always() + run: | + if [ -f .lake/upstream-report.md ]; then + cat .lake/upstream-report.md >> "$GITHUB_STEP_SUMMARY" + fi diff --git a/.github/workflows/upstream-core.yml b/.github/workflows/upstream-core.yml new file mode 100644 index 0000000..19ff06f --- /dev/null +++ b/.github/workflows/upstream-core.yml @@ -0,0 +1,73 @@ +name: Watch Lean core adaptations + +on: + schedule: + - cron: '23 8 * * 1' + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: upstream-core-watch + cancel-in-progress: false + +jobs: + watch: + runs-on: ubuntu-latest + timeout-minutes: 15 + permissions: + contents: read + issues: write + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + # Even a manual run reports only the reviewed default-branch configuration. + ref: ${{ github.event.repository.default_branch }} + persist-credentials: false + + - name: Compare tracked definitions with Lean's development branch + run: | + python3 scripts/upstream.py check --target HEAD --advisory \ + --report upstream-report.md --json-report upstream-report.json + cat upstream-report.md >> "$GITHUB_STEP_SUMMARY" + + - name: Maintain one issue for changes needing review + uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8 + with: + script: | + const fs = require('fs'); + const report = JSON.parse(fs.readFileSync('upstream-report.json', 'utf8')); + const marker = ''; + const digest = ``; + const issues = await github.paginate(github.rest.issues.listForRepo, { + ...context.repo, state: 'all', creator: 'github-actions[bot]', per_page: 100, + }); + const issue = issues.find(i => !i.pull_request && i.body?.includes(marker)); + if (report.changes.length === 0) { + if (issue?.state === 'open') { + await github.rest.issues.update({ + ...context.repo, issue_number: issue.number, state: 'closed', + }); + } + return; + } + if (issue?.state === 'open' && issue.body?.includes(digest)) return; + const summary = fs.readFileSync('upstream-report.md', 'utf8'); + const run = `${context.serverUrl}/${context.repo.owner}/${context.repo.repo}/actions/runs/${context.runId}`; + // Leave room below GitHub's issue-body limit, also for non-ASCII source text. + let details = summary; + if (Buffer.byteLength(details, 'utf8') > 55000) { + details = Array.from(details).slice(0, 13000).join('') + + '\n\nReport truncated; see the workflow summary for the full diff.'; + } + const body = `${marker}\n${digest}\n${details}\n\n[Workflow report](${run})`; + if (issue) { + await github.rest.issues.update({ + ...context.repo, issue_number: issue.number, body, state: 'open', + }); + } else { + await github.rest.issues.create({ + ...context.repo, title: 'Lean core changes affecting adapted definitions', body, + }); + } diff --git a/README.md b/README.md index 5ba5618..b40c56d 100644 --- a/README.md +++ b/README.md @@ -1 +1,4 @@ -# Random-do notation \ No newline at end of file +# Random-do notation + +See [Tracking adaptations of Lean core](docs/upstream-tracking.md) for upstream annotations, +change reports, and the review workflow. diff --git a/docs/upstream-tracking.md b/docs/upstream-tracking.md new file mode 100644 index 0000000..80d671c --- /dev/null +++ b/docs/upstream-tracking.md @@ -0,0 +1,109 @@ +# Tracking adaptations of Lean core + +The initial scope is `RandomDo/Monad/MeasurableSpace.lean` and +`RandomDo/Monad/Notation.lean`. The annotations identify adaptations, not literal copies or +claims of semantic equivalence. They do not change the definitions or their docstrings. + +```lean +@[upstream Bind] +class MeasurableSpaceBind ... + +@[upstream Lean.Elab.Do.DoOps.default] +def randOps ... +``` + +Multiple origins use spaces: `@[upstream Pure Bind]`. Use fully qualified names when needed; +for example, `_root_.bind_congr` avoids resolving to the declaration being annotated. +The attribute rejects unknown names, duplicate origins, and declarations outside Lean core. +It is implemented in `RandomDo/Util/Upstream.lean`. To extend tracking to another module, +import that module in `scripts/ExportUpstream.lean` and record its annotated declarations. + +## Checking an upgrade + +Build the tracked modules, export their annotations, and compare against the running toolchain: + +```sh +lake build --wfail RandomDo.Monad.MeasurableSpace RandomDo.Monad.Notation +lake env lean scripts/ExportUpstream.lean > .lake/upstream-current.json +python3 scripts/upstream.py check --metadata .lake/upstream-current.json +``` + +The build workflow runs this check on PRs, along with the attribute and checker tests. +New or removed annotations require an explicit baseline update. An upstream name that disappears +will also fail to resolve when building against the new toolchain. + +`upstream.json` records, for each local/upstream pair, an immutable Lean commit, the upstream source +path and range, a hash of that source, and a review note. The exporter obtains ranges from Lean's +declaration metadata, including class fields, documentation, and definition bodies. A range is +used only with the exact commit at which it was recorded: later line insertions do not invalidate +it. The checker compares old upstream source with new upstream source, not with the intentionally +different RandomDo implementation. It needs Git and Python 3.10 or later, with no Python packages. + +## Reviewing and recording a change + +Read the report's upstream diff alongside the corresponding RandomDo declaration. Port relevant +changes or explain why they do not apply. Then record only the declarations reviewed in this PR: + +```sh +python3 scripts/upstream.py record --metadata .lake/upstream-current.json \ + --only RDo.randOps --note 'Ported the core change; measurable-space arguments remain explicit.' +``` + +Each selected declaration's origins receive the current toolchain commit and source range. +Other declarations keep their existing baselines. Commit the baseline update with the adaptation +or explanation, so reviewers can see both. `--all` explicitly records every exported annotation +and removes obsolete mappings; use it only when all affected entries have been reviewed. +For a local rename, `--all` also reconciles the old and new identities; unchanged upstream entries +still need accurate review notes. The checker never advances baselines automatically. + +The initial baseline is Lean v4.35.0. It records the existing adaptations as the starting point for +monitoring, not a completed correctness audit. In particular: + +- `RDo.randOps` supplies measurable-space arguments and currently omits core's dead-syntax guard + in `mkPureApp`. This is a known difference to investigate separately. +- The loop parsers, expander and elaborator retain the existing `rdo` adaptations; they do not + implement core's `invariant` / `decreasing` annotations or its verification-condition hooks. +- The class hierarchy and laws have measurable-space parameters and measurability hypotheses, + and omit the applicative layer. These differences are intentional. + +## Watching future core changes + +The `Watch Lean core adaptations` workflow checks upstream's default development branch each +Monday at 08:23 UTC and can also be run manually. Scheduled workflows become active once merged +to the repository's default branch. It reads upstream source only; it does not build or execute +future core code or change the project's toolchain. + +When a tracked region changes, the workflow opens or updates one GitHub issue with the affected +local declarations, review notes, source links, and upstream diffs. Unchanged relevant edits do +not cause repeated updates when unrelated commits land in core. The issue is closed when no +tracked differences remain. Fetch, metadata, and other check failures fail the workflow and do +not close an existing issue. The watcher has read-only contents access and permission to maintain its issue. +The PR checks add no token permissions to the existing build workflow. No baseline updates or code changes are made by the watcher. + +Run the same comparison locally: + +```sh +python3 scripts/upstream.py check --target HEAD --report .lake/upstream-report.md +``` + +Without `--repo`, the checker fetches from `leanprover/lean4` into `.lake/upstream-lean.git`. +Use `--repo /path/to/lean4` before `check` or `record` to use an existing Git repository without +fetching. Exit statuses are 0 for unchanged, 1 for changes needing review, and 2 for an incomplete +or invalid check. `--advisory` changes status 1 to 0; errors still fail. + +## Coverage and tests + +Moved or deleted files and renamed declarations are reported through changes at their recorded +locations. Insertions immediately at either boundary are conservatively flagged because they +can extend a declaration. Unrelated changes elsewhere in the same file are ignored. +This is source-change detection: changes to untracked helpers or surrounding module/section +context can also affect behavior. It does not prove that an adaptation remains correct. Keep the project's behavior and elaboration tests. + +```sh +python3 -m unittest discover -s scripts/tests -p 'test_upstream.py' +lake env lean scripts/tests/Upstream.lean +``` + +The Python tests construct local Git histories and require no network. They cover source/body +changes, boundary insertions, unrelated edits, moves/deletions, malformed or missing data, +partial review, exit statuses, baseline preservation, and notification deduplication. diff --git a/scripts/tests/test_upstream.py b/scripts/tests/test_upstream.py new file mode 100644 index 0000000..f43af36 --- /dev/null +++ b/scripts/tests/test_upstream.py @@ -0,0 +1,171 @@ +"""Exercise the checker against real, temporary Git histories; no network access.""" + +import contextlib +import copy +import io +import json +from pathlib import Path +import sys +import tempfile +import unittest + +sys.path.insert(0, str(Path(__file__).resolve().parents[1])) +import upstream + + +class UpstreamTest(unittest.TestCase): + def setUp(self): + self.temp = tempfile.TemporaryDirectory() + self.addCleanup(self.temp.cleanup) + self.repo = Path(self.temp.name) + upstream.git(self.repo, "init", "--quiet") + upstream.git(self.repo, "config", "user.email", "test@example.invalid") + upstream.git(self.repo, "config", "user.name", "Upstream tests") + self.path = self.repo / "src" / "Example.lean" + self.path.parent.mkdir() + self.original = ( + "namespace Example\n\n" + "def foo (x : Nat) : Nat :=\n" + " x + 1\n\n" + "def other : Nat := 10\n\n" + "end Example\n" + ) + self.path.write_text(self.original) + self.before = self.commit() + self.metadata = {"schema": 1, "commit": self.before, "entries": [{ + "local": "Adapted.foo", "local_file": "RandomDo/Example.lean", + "upstream": "Example.foo", "path": "src/Example.lean", "start": 3, "end": 4, + }]} + self.baseline = upstream.record(None, self.metadata, self.source(), None, "Adapted to m") + + def source(self): + return upstream.Source(self.repo) + + def commit(self): + upstream.git(self.repo, "add", ".") + upstream.git(self.repo, "commit", "--quiet", "--no-gpg-sign", "-m", "fixture") + return upstream.git(self.repo, "rev-parse", "HEAD").strip() + + def change(self, text): + self.path.write_text(text) + return self.commit() + + def report(self, target): + return upstream.check(self.baseline, self.source(), target) + + def test_unchanged_and_unrelated_edits(self): + self.assertEqual(self.report(self.before)["changes"], []) + target = self.change(self.original.replace("10", "20")) + self.assertEqual(self.report(target)["changes"], []) + + def test_unrelated_line_insertion_does_not_shift_the_baseline(self): + target = self.change("-- new module comment\n" + self.original) + self.assertEqual(self.report(target)["changes"], []) + + def test_statement_and_body_changes(self): + for old, new in [("x : Nat", "x : Int"), ("x + 1", "x + 2")]: + with self.subTest(new=new): + target = self.change(self.original.replace(old, new)) + report = self.report(target) + self.assertEqual(len(report["changes"]), 1) + self.assertIn(new, report["changes"][0]["diff"]) + + def test_insertions_at_both_boundaries_are_conservatively_reported(self): + for text in [self.original.replace("def foo", "@[inline]\ndef foo"), + self.original.replace(" x + 1\n", " x + 1\n + 2\n")]: + with self.subTest(text=text): + self.assertEqual(len(self.report(self.change(text))["changes"]), 1) + + def test_deleted_declaration_and_renamed_declaration(self): + target = self.change(self.original.replace("def foo (x : Nat) : Nat :=\n x + 1\n", "")) + self.assertTrue(self.report(target)["changes"]) + target = self.change(self.original.replace("def foo", "def renamed")) + self.assertTrue(self.report(target)["changes"]) + + def test_deleted_or_moved_file_is_reported(self): + self.path.rename(self.path.with_name("Moved.lean")) + self.assertTrue(self.report(self.commit())["changes"]) + + def test_corrupted_baseline_is_an_error(self): + self.baseline["entries"][0]["sha256"] = "0" * 64 + with self.assertRaisesRegex(upstream.CheckError, "hash mismatch"): + self.report(self.before) + + def test_missing_revision_is_an_error(self): + with self.assertRaises(upstream.CheckError): + self.report("no-such-revision") + + def test_source_range_and_identity_are_validated(self): + for key, value in [("start", 0), ("end", -1), ("path", "../outside.lean")]: + baseline = copy.deepcopy(self.baseline) + baseline["entries"][0][key] = value + with self.subTest(key=key), self.assertRaises(upstream.CheckError): + upstream.check(baseline, self.source(), self.before) + baseline = copy.deepcopy(self.baseline) + baseline["entries"].append(baseline["entries"][0]) + with self.assertRaisesRegex(upstream.CheckError, "Duplicate"): + upstream.entries(baseline, baseline=True) + + def test_new_removed_and_moved_annotations_require_review(self): + upstream.validate_mappings(self.baseline, self.metadata) + for key, value in [("local", "Adapted.new"), ("upstream", "Example.new"), + ("local_file", "RandomDo/New.lean")]: + metadata = copy.deepcopy(self.metadata) + metadata["entries"][0][key] = value + with self.subTest(key=key), self.assertRaises(upstream.CheckError): + upstream.validate_mappings(self.baseline, metadata) + + def test_range_must_match_exported_metadata_at_the_same_commit(self): + baseline = copy.deepcopy(self.baseline) + baseline["entries"][0]["start"] = 4 + with self.assertRaisesRegex(upstream.CheckError, "range disagrees"): + upstream.validate_mappings(baseline, self.metadata) + + def test_invalid_commit_types_are_check_errors(self): + for field in ("commit", "sha256"): + baseline = copy.deepcopy(self.baseline) + baseline["entries"][0][field] = None + with self.subTest(field=field), self.assertRaises(upstream.CheckError): + upstream.entries(baseline, baseline=True) + + def test_partial_review_preserves_other_baselines(self): + metadata = copy.deepcopy(self.metadata) + metadata["entries"].append({**metadata["entries"][0], "local": "Adapted.second"}) + baseline = upstream.record(None, metadata, self.source(), None, "Initial review") + metadata["commit"] = self.change(self.original.replace("x + 1", "x + 2")) + reviewed = upstream.record(baseline, metadata, self.source(), ["Adapted.foo"], "Ported fix") + by_name = {e["local"]: e for e in reviewed["entries"]} + self.assertEqual(by_name["Adapted.foo"]["commit"], metadata["commit"]) + self.assertEqual(by_name["Adapted.second"]["commit"], self.before) + report = upstream.check(reviewed, self.source(), metadata["commit"]) + self.assertEqual([c["local"] for c in report["changes"]], ["Adapted.second"]) + + def test_no_automatic_baseline_update_and_exit_codes(self): + lock = self.repo / "baseline.json" + lock.write_text(json.dumps(self.baseline)) + original = lock.read_bytes() + target = self.change(self.original.replace("x + 1", "x + 2")) + args = ["--baseline", str(lock), "--repo", str(self.repo), "check", "--target", target] + with contextlib.redirect_stdout(io.StringIO()): + self.assertEqual(upstream.main(args), 1) + self.assertEqual(upstream.main(args + ["--advisory"]), 0) + with contextlib.redirect_stderr(io.StringIO()): + self.assertEqual(upstream.main(args[:-1] + ["missing"] + ["--advisory"]), 2) + self.assertEqual(lock.read_bytes(), original) + + def test_notification_fingerprint_ignores_unrelated_commits(self): + changed = self.original.replace("x + 1", "x + 2") + first = self.report(self.change(changed)) + second = self.report(self.change("-- unrelated\n" + changed)) + self.assertNotEqual(first["target"], second["target"]) + self.assertEqual(first["fingerprint"], second["fingerprint"]) + + def test_report_includes_mapping_review_note_and_upstream_diff(self): + report = self.report(self.change(self.original.replace("x + 1", "x + 2"))) + text = upstream.markdown(report) + for expected in ["Adapted.foo", "Example.foo", "Adapted to m", "- x + 1", "+ x + 2"]: + self.assertIn(expected, text) + + +if __name__ == "__main__": + unittest.main() diff --git a/scripts/upstream.py b/scripts/upstream.py new file mode 100644 index 0000000..6051908 --- /dev/null +++ b/scripts/upstream.py @@ -0,0 +1,318 @@ +#!/usr/bin/env python3 +"""Track changes to annotated Lean core declarations. Python standard library only.""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import re +import subprocess +import sys +from dataclasses import dataclass +from pathlib import Path, PurePosixPath + +ROOT = Path(__file__).resolve().parents[1] +REPOSITORY = "https://github.com/leanprover/lean4" +LOCK = ROOT / "upstream.json" +SHA = re.compile(r"[0-9a-f]{40}\Z") +HUNK = re.compile(r"@@ -(\d+)(?:,(\d+))? \+(\d+)(?:,(\d+))? @@") + + +class CheckError(Exception): + """An incomplete check must fail, rather than report that nothing changed.""" + + +def git(repo: Path, *args: str) -> str: + result = subprocess.run( + ["git", "--no-pager", "-C", str(repo), *args], + text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False, + ) + if result.returncode: + raise CheckError(f"git {' '.join(args)} failed: {result.stderr.strip()}") + return result.stdout + + +def valid_ref(ref: str) -> str: + if not re.fullmatch(r"[A-Za-z0-9_][A-Za-z0-9_./-]*", ref) or ".." in ref: + raise CheckError(f"Invalid upstream revision: {ref!r}") + return ref + + +class Source: + def __init__(self, repo: Path | None): + self.fetch = repo is None + self.repo = repo or ROOT / ".lake" / "upstream-lean.git" + if self.fetch and not self.repo.exists(): + self.repo.mkdir(parents=True) + git(self.repo, "init", "--bare") + self.revisions: dict[str, str] = {} + self.files: dict[tuple[str, str], str] = {} + self.diffs: dict[tuple[str, str, str], str] = {} + + def resolve(self, ref: str) -> str: + valid_ref(ref) + if ref not in self.revisions: + if self.fetch: + # Fetch only data from the fixed upstream repository; never check out or execute it. + git(self.repo, "fetch", "--quiet", "--depth=1", "--no-tags", + REPOSITORY + ".git", ref) + commit = git(self.repo, "rev-parse", "FETCH_HEAD^{commit}").strip() + else: + commit = git(self.repo, "rev-parse", "--verify", ref + "^{commit}").strip() + if not SHA.fullmatch(commit): + raise CheckError(f"Not an upstream commit: {commit!r}") + self.revisions[ref] = commit + self.revisions[commit] = commit + return self.revisions[ref] + + def read(self, commit: str, path: str) -> str: + key = (commit, path) + if key not in self.files: + self.files[key] = git(self.repo, "show", f"{commit}:{path}") + return self.files[key] + + def diff(self, before: str, after: str, path: str) -> str: + key = (before, after, path) + if key not in self.diffs: + self.diffs[key] = git( + self.repo, "diff", "--no-ext-diff", "--no-textconv", "--no-renames", + "--unified=3", before, after, "--", path, + ) + return self.diffs[key] + + +def read_json(path: Path) -> dict: + value = json.loads(path.read_text()) + if not isinstance(value, dict) or value.get("schema") != 1: + raise CheckError(f"Unsupported metadata schema in {path}") + return value + + +def identity(entry: dict) -> tuple[str, str]: + return entry["local"], entry["upstream"] + + +def entries(document: dict, *, baseline: bool) -> dict[tuple[str, str], dict]: + records = document.get("entries") + if not isinstance(records, list) or not records: + raise CheckError("Expected a nonempty list of tracked declarations") + result = {} + for entry in records: + if not isinstance(entry, dict): + raise CheckError("Invalid tracked declaration") + for field in ("local", "upstream", "path", "local_file"): + if not isinstance(entry.get(field), str) or not entry[field].strip(): + raise CheckError(f"Missing {field} in tracked declaration") + for field in ("path", "local_file"): + path = PurePosixPath(entry[field]) + if path.is_absolute() or ".." in path.parts or not entry[field].endswith(".lean"): + raise CheckError(f"Invalid source path: {entry[field]}") + if not entry["path"].startswith("src/"): + raise CheckError(f"Not a Lean core source path: {entry['path']}") + start, end = entry.get("start"), entry.get("end") + if type(start) is not int or type(end) is not int or not 1 <= start <= end: + raise CheckError(f"Invalid source range for {entry['upstream']}") + if baseline: + if not isinstance(entry.get("commit"), str) or not SHA.fullmatch(entry["commit"]): + raise CheckError(f"Invalid baseline commit for {entry['upstream']}") + if not isinstance(entry.get("sha256"), str) or not re.fullmatch(r"[0-9a-f]{64}", entry["sha256"]): + raise CheckError(f"Missing source hash for {entry['upstream']}") + if not isinstance(entry.get("note"), str) or not entry["note"].strip(): + raise CheckError(f"Missing review note for {entry['local']}") + key = identity(entry) + if key in result: + raise CheckError(f"Duplicate upstream mapping: {key}") + result[key] = entry + if baseline and document.get("repository") != REPOSITORY: + raise CheckError("The baseline must refer to leanprover/lean4") + if not baseline and (not isinstance(document.get("commit"), str) + or not SHA.fullmatch(document["commit"])): + raise CheckError("The exporter must run with a Lean toolchain carrying a full commit hash") + return result + + +def validate_mappings(baseline: dict, metadata: dict) -> None: + old, current = entries(baseline, baseline=True), entries(metadata, baseline=False) + missing, removed = current.keys() - old.keys(), old.keys() - current.keys() + if missing or removed: + raise CheckError( + f"Annotations and baseline disagree. New mappings: {sorted(missing)}; " + f"removed mappings: {sorted(removed)}. Review and record the affected declarations." + ) + for key in old: + if old[key]["local_file"] != current[key]["local_file"]: + raise CheckError(f"{key[0]} moved locally; record its new location after review") + if old[key]["commit"] == metadata["commit"]: + if any(old[key][field] != current[key][field] for field in ("path", "start", "end")): + raise CheckError(f"Baseline range disagrees with Lean's metadata for {key[1]}") + + +def source_hash(source: Source, commit: str, entry: dict) -> str: + lines = source.read(commit, entry["path"]).splitlines(keepends=True) + if entry["end"] > len(lines): + raise CheckError(f"Source range exceeds {entry['path']} at {commit}") + text = "".join(lines[entry["start"] - 1:entry["end"]]) + return hashlib.sha256(text.encode()).hexdigest() + + +@dataclass +class Hunk: + old_start: int + lines: list[str] + + def edits(self, start: int, end: int) -> list[list[str]]: + """Return relevant edit blocks, excluding context and unrelated edits in the same hunk.""" + line = self.old_start + result, block, affected = [], [], False + for text in self.lines[1:]: + if text.startswith("+"): + # Include insertions at either boundary: these can extend a declaration. + affected |= start - 1 <= line - 1 <= end + block.append(text) + elif text.startswith("-"): + affected |= start <= line <= end + block.append(text) + line += 1 + elif text.startswith(" "): + if affected: + result.append(block) + block, affected = [], False + line += 1 + if affected: + result.append(block) + return result + + +def hunks(diff: str) -> list[Hunk]: + result: list[Hunk] = [] + for line in diff.splitlines(): + match = HUNK.match(line) + if match: + result.append(Hunk(int(match[1]), [line])) + elif result: + result[-1].lines.append(line) + return result + + +def check(baseline: dict, source: Source, target: str) -> dict: + tracked = entries(baseline, baseline=True) + target = source.resolve(target) + changes = [] + for key in sorted(tracked): + entry = tracked[key] + before = source.resolve(entry["commit"]) + if source_hash(source, before, entry) != entry["sha256"]: + raise CheckError(f"Baseline source hash mismatch for {entry['upstream']}") + relevant = [(h, h.edits(entry["start"], entry["end"])) + for h in hunks(source.diff(before, target, entry["path"]))] + relevant = [(h, edits) for h, edits in relevant if edits] + if relevant: + changes.append({**entry, "diff": "\n".join( + line for h, _ in relevant for line in h.lines), + "edits": [block for _, edits in relevant for block in edits]}) + # Unrelated upstream commits must not cause repeated issue updates. Hunk offsets may change + # when unrelated lines are inserted earlier in the file, so exclude them from the digest. + fingerprint = hashlib.sha256(json.dumps([ + [c["local"], c["local_file"], c["upstream"], c["path"], c["commit"], + c["start"], c["end"], c["note"], c["edits"]] + for c in changes + ], ensure_ascii=False, sort_keys=True).encode()).hexdigest() + return {"target": target, "checked": len(tracked), "changes": changes, + "fingerprint": fingerprint} + + +def record(baseline: dict | None, metadata: dict, source: Source, + selected: list[str] | None, note: str) -> dict: + current = entries(metadata, baseline=False) + old = entries(baseline, baseline=True) if baseline is not None else {} + if not note.strip(): + raise CheckError("A review note is required") + names = {key[0] for key in current} + chosen = set(selected) if selected else names + if not chosen <= names: + raise CheckError(f"Unknown tracked declarations: {sorted(chosen - names)}") + # --all also removes annotations that were deleted; --only preserves all other baselines. + result = {key: value for key, value in old.items() if selected and key[0] not in chosen} + commit = source.resolve(metadata["commit"]) + for key, entry in current.items(): + if key[0] in chosen: + result[key] = {**entry, "commit": commit, + "sha256": source_hash(source, commit, entry), "note": note} + return {"schema": 1, "repository": REPOSITORY, + "entries": [result[key] for key in sorted(result)]} + + +def markdown(report: dict) -> str: + lines = ["# Lean core changes affecting adapted definitions", "", + f"Checked {report['checked']} mappings against " + f"[{report['target'][:12]}]({REPOSITORY}/commit/{report['target']}).", ""] + if not report["changes"]: + lines.append("No changes intersect the tracked declarations since their recorded baselines.") + else: + lines += ["Review these upstream changes, then port them or explain why they do not apply. " + "Advance a declaration's baseline only after that review. " + "A moved or deleted source file is reported as a deletion.", ""] + for change in report["changes"]: + link = (f"{REPOSITORY}/blob/{change['commit']}/{change['path']}" + f"#L{change['start']}-L{change['end']}") + lines += [f"## `{change['local']}`", "", + f"Local file: `{change['local_file']}`. " + f"Upstream: [`{change['upstream']}`]({link}).", "", + f"Baseline note: {change['note']}", "", + f"[Full upstream comparison]({REPOSITORY}/compare/" + f"{change['commit']}...{report['target']})", "", "````diff", + change["diff"], "````", ""] + return "\n".join(lines) + "\n" + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--baseline", type=Path, default=LOCK) + parser.add_argument("--repo", type=Path, help="Use an existing Lean Git repository without fetching") + commands = parser.add_subparsers(dest="command", required=True) + check_parser = commands.add_parser("check", help="Report upstream changes; never update the baseline") + check_parser.add_argument("--metadata", type=Path, help="Exported annotations from the current build") + check_parser.add_argument("--target", help="Upstream revision (defaults to the exported Lean commit)") + check_parser.add_argument("--report", type=Path) + check_parser.add_argument("--json-report", type=Path) + check_parser.add_argument("--advisory", action="store_true", help="Exit successfully on drift, but not on errors") + record_parser = commands.add_parser("record", help="Record explicitly reviewed upstream baselines") + record_parser.add_argument("--metadata", type=Path, required=True) + choice = record_parser.add_mutually_exclusive_group(required=True) + choice.add_argument("--only", nargs="+", metavar="DECL") + choice.add_argument("--all", action="store_true") + record_parser.add_argument("--note", required=True) + args = parser.parse_args(argv) + try: + baseline = read_json(args.baseline) if args.baseline.exists() else None + metadata = read_json(args.metadata) if args.metadata else None + source = Source(args.repo) + if args.command == "record": + result = record(baseline, metadata, source, args.only, args.note) + args.baseline.write_text(json.dumps(result, ensure_ascii=False, indent=2) + "\n") + print(f"Recorded {len(result['entries'])} mappings in {args.baseline}") + return 0 + if baseline is None: + raise CheckError("No baseline; review the mappings and run the record command first") + if metadata: + validate_mappings(baseline, metadata) + target = args.target or (metadata["commit"] if metadata else None) + if target is None: + raise CheckError("check requires --metadata or --target") + report = check(baseline, source, target) + text = markdown(report) + if args.report: + args.report.write_text(text) + else: + print(text, end="") + if args.json_report: + args.json_report.write_text(json.dumps(report, ensure_ascii=False, indent=2) + "\n") + return 1 if report["changes"] and not args.advisory else 0 + except (CheckError, OSError, ValueError) as exc: + print(f"Upstream check failed: {exc}", file=sys.stderr) + return 2 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/upstream.json b/upstream.json new file mode 100644 index 0000000..976d024 --- /dev/null +++ b/upstream.json @@ -0,0 +1,281 @@ +{ + "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", + "sha256": "6cc2037bc873862c4b85679592862def80ffc25002449eb0f42b074911092b10", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "end": 159, + "local": "LawfulMeasurableSpaceMonad", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 125, + "upstream": "LawfulMonad", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", + "sha256": "e701a60ca37c38a4c6463db27120120bcddb9b7841e21c19fa9a05403e021896", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "end": 3881, + "local": "MeasurableSpaceBind", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Prelude.lean", + "start": 3869, + "upstream": "Bind", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", + "sha256": "210b68a6ae65efbf339df0cc96e8bbe74f8018ef5f2f4e3e1293f065f51cf487", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "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", + "sha256": "0ec2334c28a0e31bf8790a12ba2d2eae8a32c523280085089b5c2022a8e78026", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "end": 388, + "local": "MeasurableSpaceForIn", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Core.lean", + "start": 366, + "upstream": "ForIn", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", + "sha256": "45a34391c62bd3286fb6c60461f5a16d3147105004222240facdddc89d8801d0", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "end": 416, + "local": "MeasurableSpaceForIn'", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Core.lean", + "start": 392, + "upstream": "ForIn'", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", + "sha256": "63b45de3bbd497e26e4d9af17172e23eb8fa813cc493ca00a956003f6ae6b463", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "end": 3937, + "local": "MeasurableSpaceFunctor", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Prelude.lean", + "start": 3903, + "upstream": "Functor", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", + "sha256": "1be4516f598ce7e2dd50381f3f7fbb9d14bdc4f1f636bc94e83f5fa4a7eca667", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "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", + "sha256": "2fa31b1b51ecb17cb8f11d39b5cedeb2ab6bd89af909564f0676e37ced75f405", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "end": 4038, + "local": "MeasurableSpaceMonad", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Prelude.lean", + "start": 4020, + "upstream": "Monad", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", + "sha256": "6234016213a903ac9910fc72b4de104bcd4c9cb1ab33fc63f0ae52aa4f872c19", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "end": 3899, + "local": "MeasurableSpacePure", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Prelude.lean", + "start": 3885, + "upstream": "Pure", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", + "sha256": "997ff22ea7f4d2a759a49b9bfc8730eeeccf731ba5746ef87a63913243475799", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "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", + "sha256": "a76b98157e5aa89eaffa74a54eee1e0289b1f1a12011c2cc877bcfcc8cecf5ba", + "note": "Initial v4.35.0 baseline for the existing rdo loop adaptation. Core invariant/decreasing syntax and verification-condition hooks are not implemented; see docs/upstream-tracking.md." + }, + { + "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", + "sha256": "529ac011ffa6752eb1b845f722393177dbbf1a75d0d87e1c9ee0b6facfb15d5f", + "note": "Uses rdo syntax and passes randOps to the shared core elaborator." + }, + { + "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", + "sha256": "334393bb33da3c0ac44a58817fefa5980341f962d201223c0ee2a13d53a72956", + "note": "Initial v4.35.0 baseline for the existing rdo loop adaptation. Core invariant/decreasing syntax and verification-condition hooks are not implemented; see docs/upstream-tracking.md." + }, + { + "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", + "sha256": "912707da88c0d9bbbdb417857aa32923b6080d6f4eb92b08dd694302f6790afb", + "note": "Initial v4.35.0 baseline. Adds measurable-space arguments; the existing mkPureApp override omits the upstream dead-syntax guard, which remains a follow-up review item." + }, + { + "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", + "sha256": "38e65c348f80c6f644c1ac6a71a8e5647f1184e8d6e39447657463abe013ba1b", + "note": "Initial v4.35.0 baseline for the existing rdo loop adaptation. Core invariant/decreasing syntax and verification-condition hooks are not implemented; see docs/upstream-tracking.md." + }, + { + "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", + "sha256": "ee21206fa7575137d2438b36a9950a6838aeb63b2d187996e77385448ba2867d", + "note": "Initial v4.35.0 baseline for the existing rdo loop adaptation. Core invariant/decreasing syntax and verification-condition hooks are not implemented; see docs/upstream-tracking.md." + }, + { + "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", + "sha256": "a95c9957a4b53496da246b239ac5e3cf0674e31399b26dcaf431e5a22560de55", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "end": 30, + "local": "instMeasurableSpaceForInOfForIn'", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Basic.lean", + "start": 16, + "upstream": "instForInOfForIn'", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", + "sha256": "f3633bf63b71bb5167b596950cb20bf22fbbce08496990269ac08d8a8b7b9385", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "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", + "sha256": "9a6f4815d41cec24233f2b78492e54fc364adc1052daad6195c72e2937e523aa", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "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", + "sha256": "e9cf0d00e632a518d1c62d3aca72d4f586a7db23909d901a10e50bafb00eeb2f", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "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", + "sha256": "a3c9870f5e209316d44663a98e412b1ad6d6d325df90a5be1c00fa8f59969042", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "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", + "sha256": "ad6d8f6c43be7df2ec4dbf7d96b19e877fd693bf6afcad9d1539eb5d2705af46", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "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", + "sha256": "dd22185502a5bff4dcc033c76e846218c6b27835b54e08233ac3f6e76d596ea4", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "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", + "sha256": "50e2e660e52da2b9f147021b8f3bf3744f1244f861a649d689b5dec2e5353ff4", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + }, + { + "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", + "sha256": "0e46a1b086567226a38c7eb7d3deb3c387395caebb8a0838a164801743109a57", + "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + } + ] +} From e2e0d73c31454455f892a34ddd58ad5d2a8d7a77 Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 22:21:22 +0000 Subject: [PATCH 3/4] Rename analogue attribute and simplify core change tracking --- .github/workflows/build.yml | 3 +- .github/workflows/upstream-core.yml | 34 +--- README.md | 2 +- RandomDo.lean | 2 +- RandomDo/Monad/MeasurableSpace.lean | 40 ++--- RandomDo/Monad/Notation.lean | 12 +- .../Util/{Upstream.lean => Analogue.lean} | 20 +-- docs/upstream-tracking.md | 123 +++++-------- scripts/ExportUpstream.lean | 4 +- scripts/tests/Analogue.lean | 34 ++++ scripts/tests/Upstream.lean | 34 ---- scripts/tests/test_upstream.py | 61 +++++-- scripts/tests/test_upstream_issue.cjs | 71 ++++++++ scripts/upstream-issue.cjs | 31 ++++ scripts/upstream.py | 170 +++++++----------- upstream.json | 100 +++-------- 16 files changed, 363 insertions(+), 378 deletions(-) rename RandomDo/Util/{Upstream.lean => Analogue.lean} (73%) create mode 100644 scripts/tests/Analogue.lean delete mode 100644 scripts/tests/Upstream.lean create mode 100644 scripts/tests/test_upstream_issue.cjs create mode 100644 scripts/upstream-issue.cjs diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 0a9f9e1..6e4851d 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -58,7 +58,8 @@ jobs: - name: Test upstream tracking run: | python3 -m unittest discover -s scripts/tests -p 'test_upstream.py' - lake env lean scripts/tests/Upstream.lean + node --test scripts/tests/test_upstream_issue.cjs + lake env lean scripts/tests/Analogue.lean - name: Check adapted definitions against the pinned Lean toolchain run: | diff --git a/.github/workflows/upstream-core.yml b/.github/workflows/upstream-core.yml index 19ff06f..cd73066 100644 --- a/.github/workflows/upstream-core.yml +++ b/.github/workflows/upstream-core.yml @@ -38,36 +38,4 @@ jobs: script: | const fs = require('fs'); const report = JSON.parse(fs.readFileSync('upstream-report.json', 'utf8')); - const marker = ''; - const digest = ``; - const issues = await github.paginate(github.rest.issues.listForRepo, { - ...context.repo, state: 'all', creator: 'github-actions[bot]', per_page: 100, - }); - const issue = issues.find(i => !i.pull_request && i.body?.includes(marker)); - if (report.changes.length === 0) { - if (issue?.state === 'open') { - await github.rest.issues.update({ - ...context.repo, issue_number: issue.number, state: 'closed', - }); - } - return; - } - if (issue?.state === 'open' && issue.body?.includes(digest)) return; - const summary = fs.readFileSync('upstream-report.md', 'utf8'); - const run = `${context.serverUrl}/${context.repo.owner}/${context.repo.repo}/actions/runs/${context.runId}`; - // Leave room below GitHub's issue-body limit, also for non-ASCII source text. - let details = summary; - if (Buffer.byteLength(details, 'utf8') > 55000) { - details = Array.from(details).slice(0, 13000).join('') - + '\n\nReport truncated; see the workflow summary for the full diff.'; - } - const body = `${marker}\n${digest}\n${details}\n\n[Workflow report](${run})`; - if (issue) { - await github.rest.issues.update({ - ...context.repo, issue_number: issue.number, body, state: 'open', - }); - } else { - await github.rest.issues.create({ - ...context.repo, title: 'Lean core changes affecting adapted definitions', body, - }); - } + await require('./scripts/upstream-issue.cjs')({ github, context }, report); diff --git a/README.md b/README.md index b40c56d..e1d3acb 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ # Random-do notation -See [Tracking adaptations of Lean core](docs/upstream-tracking.md) for upstream annotations, +See [Tracking Lean core analogues](docs/upstream-tracking.md) for `analogue` annotations, change reports, and the review workflow. diff --git a/RandomDo.lean b/RandomDo.lean index bde6e04..0f82f0f 100644 --- a/RandomDo.lean +++ b/RandomDo.lean @@ -23,4 +23,4 @@ public import RandomDo.Tactic.IsMarkov.Deriving public import RandomDo.Tactic.IsMarkov.Elab public import RandomDo.Tactic.IsMarkov.ForInStep public import RandomDo.Tactic.IsMarkov.Lemmas -public import RandomDo.Util.Upstream +public import RandomDo.Util.Analogue diff --git a/RandomDo/Monad/MeasurableSpace.lean b/RandomDo/Monad/MeasurableSpace.lean index 69d0546..37ce9b6 100644 --- a/RandomDo/Monad/MeasurableSpace.lean +++ b/RandomDo/Monad/MeasurableSpace.lean @@ -7,7 +7,7 @@ module public import Mathlib.Control.Random public import Mathlib.MeasureTheory.Measure.GiryMonad -public meta import RandomDo.Util.Upstream +public meta import RandomDo.Util.Analogue /-! # Measurable Space Monad @@ -38,7 +38,7 @@ section MeasurableSpaceMonad /-- A functor on types with a `MeasurableSpace` instance. The `mMap` operator `<$>ₘ` is overloaded via instances of this class. This class does not require proofs of the `MeasurableSpaceFunctor` axioms. Proofs may be provided or required via the `LawfulMeasurableSpaceFunctor` class. -/ -@[upstream Functor] +@[analogue Functor] class MeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Type v) : Type (max (u+1) v) where /-- @@ -66,7 +66,7 @@ The `mPure` function is overloaded via `MeasurableSpacePure` instances. `MeasurableSpacePure` is typically accessed via `MeasurableSpaceMonad` instances, which extend it. -/ -@[upstream Pure] +@[analogue Pure] class MeasurableSpacePure (f : (α : Type u) → [MeasurableSpace α] → Type v) where /-- Given `a : α` where `α` has a `MeasurableSpace` instance, `mPure a : f α` represents an action that does nothing and returns a -/ @@ -77,7 +77,7 @@ The `>>=ₘ` operator is overloaded via instances of `MeasurableSpaceBind`. `MeasurableSpaceBind` is typically used via `MeasurableSpaceMonad`, which extends it. -/ -@[upstream Bind] +@[analogue Bind] class MeasurableSpaceBind (m : (α : Type u) → [MeasurableSpace α] → Type v) where /-- Sequences two computations, allowing the second to depend on the value computed by the first. @@ -91,7 +91,7 @@ class MeasurableSpaceBind (m : (α : Type u) → [MeasurableSpace α] → Type v /-- A monad on types with a `MeasurableSpace` instance. This abstraction allows the user to write code that depends on "random" side-effects -/ -@[upstream Monad] +@[analogue Monad] class MeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type v) : Type (max (u+1) v) extends MeasurableSpaceFunctor m, MeasurableSpacePure m, MeasurableSpaceBind m where @@ -100,12 +100,12 @@ class MeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type variable {m : (α : Type u) → [MeasurableSpace α] → Type v} {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] -@[upstream _root_.bind_congr] +@[analogue _root_.bind_congr] theorem MeasurableSpaceBind.bind_congr [MeasurableSpaceBind m] {x : m α} {f g : α → m β} (h : ∀ a, f a = g a) : x >>=ₘ f = x >>=ₘ g := by simp [funext h] -@[upstream _root_.map_congr] +@[analogue _root_.map_congr] theorem MeasurableSpaceFunctor.map_congr [MeasurableSpaceFunctor m] {x : m α} {f g : α → β} (h : ∀ a, f a = g a) : (f <$>ₘ x : m β) = g <$>ₘ x := by simp [funext h] @@ -117,7 +117,7 @@ section Lawful open MeasurableSpaceFunctor /-- A `MeasurableSpaceFunctor` satisfies the measurable space functor laws. -/ -@[upstream LawfulFunctor] +@[analogue LawfulFunctor] class LawfulMeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceFunctor f] [∀ α, [MeasurableSpace α] → MeasurableSpace (f α)] : Prop where @@ -143,10 +143,10 @@ variable {f : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpac [∀ α, [MeasurableSpace α] → MeasurableSpace (f α)] [LawfulMeasurableSpaceFunctor f] {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] -@[upstream id_map', simp] +@[analogue id_map', simp] theorem id_mMap' (x : f α) : (fun a => a) <$>ₘ x = x := id_mMap x -@[upstream Functor.map_map, simp] +@[analogue Functor.map_map, simp] theorem mMap_mMap {g₀ : α → β} {g₁ : β → γ} (x : f α) (hg₀ : Measurable g₀) (hg₁ : Measurable g₁) : g₁ <$>ₘ g₀ <$>ₘ x = (fun a => g₁ (g₀ a)) <$>ₘ x := @@ -155,7 +155,7 @@ theorem mMap_mMap {g₀ : α → β} {g₁ : β → γ} (x : f α) open MeasurableSpaceBind MeasurableSpacePure MeasurableSpaceFunctor /-- A `MeasurableSpaceMonad` satisfies the measurable space monad laws. -/ -@[upstream LawfulMonad] +@[analogue LawfulMonad] class LawfulMeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceMonad m] [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)] : Prop @@ -198,32 +198,32 @@ variable {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpac [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)] [LawfulMeasurableSpaceMonad m] {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] -@[upstream LawfulApplicative.map_pure, simp] +@[analogue LawfulApplicative.map_pure, simp] theorem mMap_mPure {f : α → β} (hf : Measurable f) (x : α) : f <$>ₘ (mPure x : m α) = mPure (f x) := by rw [← mBind_mPure_comp hf, mPure_mBind _ (by fun_prop)] -@[upstream bind_pure, simp] +@[analogue bind_pure, simp] theorem mBind_mPure (x : m α) : x >>=ₘ mPure = x := by change x >>=ₘ (fun a => (mPure (id a))) = x rw [mBind_mPure_comp (by fun_prop), id_mMap] -@[upstream map_eq_pure_bind] +@[analogue map_eq_pure_bind] theorem mMap_eq_mPure_mBind {f : α → β} (hf : Measurable f) (x : m α) : f <$>ₘ x = x >>=ₘ fun a => mPure (f a) := by rw [← mBind_mPure_comp hf x] -@[upstream bind_pure_unit] +@[analogue bind_pure_unit] theorem mBind_mPure_unit {x : m PUnit} : (x >>=ₘ fun _ => mPure ⟨⟩) = x := by rw [mBind_mPure] -@[upstream map_bind, simp] +@[analogue map_bind, simp] theorem mMap_mBind {f : β → γ} (hf : Measurable f) (x : m α) {g : α → m β} (hg : Measurable g) : f <$>ₘ (x >>=ₘ g) = x >>=ₘ fun a => f <$>ₘ g a := by rw [← mBind_mPure_comp hf, mBind_assoc _ hg (by fun_prop)] simp (disch := fun_prop) [mBind_mPure_comp] -@[upstream bind_map_left, simp] +@[analogue bind_map_left, simp] theorem mBind_mMap_left {f : α → β} (hf : Measurable f) (x : m α) {g : β → m γ} (hg : Measurable g) : ((f <$>ₘ x) >>=ₘ fun b => g b) = (x >>=ₘ fun a => g (f a)) := by @@ -247,7 +247,7 @@ instance instMeasurableSpace {β : Type u} [mβ : MeasurableSpace β] : /-- Monadic iteration in `rdo`-blocks, using the `for x in xs` notation. -/ -@[upstream ForIn] +@[analogue ForIn] class MeasurableSpaceForIn (ρ : Type uρ) (α : outParam (Type uα)) where /-- Monadically iterates over the contents of a collection `xs`, with a local state `b` and the @@ -259,7 +259,7 @@ class MeasurableSpaceForIn (ρ : Type uρ) (α : outParam (Type uα)) where /-- Monadic iteration in `rdo`-blocks with a membership proof, using the `for h : x in xs` notation. -/ -@[upstream ForIn'] +@[analogue ForIn'] class MeasurableSpaceForIn' (ρ : Type uρ) (α : outParam (Type uα)) (d : outParam (Membership α ρ)) where /-- @@ -270,7 +270,7 @@ class MeasurableSpaceForIn' (ρ : Type uρ) (α : outParam (Type uα)) forIn' {β : Type u} [MeasurableSpace β] (xs : ρ) (b : β) (f : (a : α) → a ∈ xs → β → m (ForInStep β)) : m β -@[upstream instForInOfForIn', simps] +@[analogue instForInOfForIn', simps] instance (priority := 500) instMeasurableSpaceForInOfForIn' {ρ : Type uρ} {α : Type uα} {d : Membership α ρ} [MeasurableSpaceForIn' m ρ α d] : MeasurableSpaceForIn m ρ α where diff --git a/RandomDo/Monad/Notation.lean b/RandomDo/Monad/Notation.lean index a6f2f0f..0d21e32 100644 --- a/RandomDo/Monad/Notation.lean +++ b/RandomDo/Monad/Notation.lean @@ -25,7 +25,7 @@ public meta section namespace RDo /-- Define `DoOp`s for `rdo` notation. -/ -@[upstream Lean.Elab.Do.DoOps.default] +@[analogue Lean.Elab.Do.DoOps.default] def randOps : DoOps := { DoOps.default with mkPureApp α e := do let ⟨m, u, v, _, _⟩ := (← read).monadInfo @@ -69,7 +69,7 @@ def randOps : DoOps := { DoOps.default with syntax (name := randKind) "rdo" doSeq : term /-- Define `rdo` notation elaborator. -/ -@[upstream Lean.Elab.Do.elabDo, term_elab randKind] +@[analogue Lean.Elab.Do.elabDo, term_elab randKind] def elabRand : Term.TermElab := fun stx et? => do let `(rdo $doSeq) := stx | throwUnsupportedSyntax elabDoWith randOps doSeq et? @@ -77,19 +77,19 @@ def elabRand : Term.TermElab := fun stx et? => do section LoopElab /-- parses `_ : _ in` for `rdo` for loops -/ -@[upstream Lean.Parser.Term.doForDecl] +@[analogue Lean.Parser.Term.doForDecl] def rdoForDecl := leading_parser Lean.Parser.optional (atomic (Term.ident >> " : ")) >> termParser >> " in " >> withForbidden "rdo" termParser /-- parser for `rdo` for loops -/ -@[upstream Lean.Parser.Term.doFor, doElem_parser] +@[analogue Lean.Parser.Term.doFor, doElem_parser] def rdoFor := leading_parser "for " >> sepBy1 rdoForDecl ", " >> "rdo " >> doSeq /-- Define expander for loops in `rdo` notation. Note this code mirrors core's implementation for `do` notation as much as possible. -/ -@[upstream Lean.Elab.Do.expandDoFor, macro rdoFor] +@[analogue Lean.Elab.Do.expandDoFor, macro rdoFor] def expandRDoFor : Macro := fun stx => do match stx with | `(rdoFor| for $[$_ : ]? $_:ident in $_ rdo $_) => @@ -152,7 +152,7 @@ def expandRDoFor : Macro := fun stx => do /-- Define loop elaborator for `rdo` notation. Note this code mirrors core's implementation for `do` notation as much as possible. -/ -@[upstream Lean.Elab.Do.elabDoFor, doElem_elab rdoFor] +@[analogue Lean.Elab.Do.elabDoFor, doElem_elab rdoFor] def elabRDoFor : DoElab := fun stx dec => do let `(rdoFor| for%$tk $[$h? : ]? $x:ident in $xs rdo $body) := stx | throwUnsupportedSyntax let dec ← dec.ensureUnitAt tk diff --git a/RandomDo/Util/Upstream.lean b/RandomDo/Util/Analogue.lean similarity index 73% rename from RandomDo/Util/Upstream.lean rename to RandomDo/Util/Analogue.lean index aa29dbf..e9ff98b 100644 --- a/RandomDo/Util/Upstream.lean +++ b/RandomDo/Util/Analogue.lean @@ -10,7 +10,7 @@ public meta import Lean.Elab.Command /-! # Tracking adaptations of Lean core -`@[upstream decl₁ decl₂]` records the Lean core declarations from which a declaration was adapted. +`@[analogue decl₁ decl₂]` records the Lean core declarations from which a declaration was adapted. It checks that the names exist and stores them as metadata, without changing the declaration or its docstring. `scripts/ExportUpstream.lean` exports this metadata for the upstream change checker. See `docs/upstream-tracking.md` for the review and baseline update workflow. @@ -18,29 +18,29 @@ See `docs/upstream-tracking.md` for the review and baseline update workflow. public meta section -namespace RandomDo.Upstream +namespace RandomDo.Analogue open Lean /-- Mark a declaration as an adaptation of one or more declarations in Lean core. -/ -syntax (name := upstream) "upstream " ident+ : attr +syntax (name := analogue) "analogue " ident+ : attr /-- The upstream declarations associated with each adapted declaration. -/ -initialize upstreamAttr : ParametricAttribute (Array Name) ← registerParametricAttribute { - name := `upstream +initialize analogueAttr : ParametricAttribute (Array Name) ← registerParametricAttribute { + name := `analogue descr := "Record the Lean core declarations from which this declaration was adapted." getParam := fun _ stx => do let names ← stx[1].getArgs.mapM resolveGlobalConstNoOverload + let env ← getEnv for name in names do - let env ← getEnv let some idx := env.getModuleIdxFor? name - | throwErrorAt stx "Upstream declaration `{name}` must be imported from Lean core" + | throwErrorAt stx "Analogue declaration `{name}` must be imported from Lean core" let mod := env.header.moduleNames[idx.toNat]! unless [`Init, `Lean, `Std].any (·.isPrefixOf mod) do - throwErrorAt stx "Upstream declaration `{name}` belongs to `{mod}`, not Lean core" + throwErrorAt stx "Analogue declaration `{name}` belongs to `{mod}`, not Lean core" unless names.toList.eraseDups.length == names.size do - throwErrorAt stx "Duplicate upstream declarations" + throwErrorAt stx "Duplicate analogue declarations" return names } -end RandomDo.Upstream +end RandomDo.Analogue diff --git a/docs/upstream-tracking.md b/docs/upstream-tracking.md index 80d671c..4547606 100644 --- a/docs/upstream-tracking.md +++ b/docs/upstream-tracking.md @@ -1,26 +1,24 @@ -# Tracking adaptations of Lean core +# Tracking Lean core analogues -The initial scope is `RandomDo/Monad/MeasurableSpace.lean` and -`RandomDo/Monad/Notation.lean`. The annotations identify adaptations, not literal copies or -claims of semantic equivalence. They do not change the definitions or their docstrings. +Use `@[analogue Core.declaration]` to link an adaptation to its Lean core counterpart: ```lean -@[upstream Bind] +@[analogue Bind] class MeasurableSpaceBind ... -@[upstream Lean.Elab.Do.DoOps.default] +@[analogue Lean.Elab.Do.DoOps.default] def randOps ... ``` -Multiple origins use spaces: `@[upstream Pure Bind]`. Use fully qualified names when needed; -for example, `_root_.bind_congr` avoids resolving to the declaration being annotated. -The attribute rejects unknown names, duplicate origins, and declarations outside Lean core. -It is implemented in `RandomDo/Util/Upstream.lean`. To extend tracking to another module, -import that module in `scripts/ExportUpstream.lean` and record its annotated declarations. +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 checks that each name exists in Lean core and records metadata without changing +any definition. It is defined in `RandomDo/Util/Analogue.lean`. -## Checking an upgrade +## Checking for changes -Build the tracked modules, export their annotations, and compare against the running toolchain: +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 @@ -28,82 +26,59 @@ lake env lean scripts/ExportUpstream.lean > .lake/upstream-current.json python3 scripts/upstream.py check --metadata .lake/upstream-current.json ``` -The build workflow runs this check on PRs, along with the attribute and checker tests. -New or removed annotations require an explicit baseline update. An upstream name that disappears -will also fail to resolve when building against the new toolchain. +The build workflow runs this check on PRs. The exporter gets declaration locations from Lean; +`upstream.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. -`upstream.json` records, for each local/upstream pair, an immutable Lean commit, the upstream source -path and range, a hash of that source, and a review note. The exporter obtains ranges from Lean's -declaration metadata, including class fields, documentation, and definition bodies. A range is -used only with the exact commit at which it was recorded: later line insertions do not invalidate -it. The checker compares old upstream source with new upstream source, not with the intentionally -different RandomDo implementation. It needs Git and Python 3.10 or later, with no Python packages. +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. -## Reviewing and recording a change - -Read the report's upstream diff alongside the corresponding RandomDo declaration. Port relevant -changes or explain why they do not apply. Then record only the declarations reviewed in this PR: +To run the same comparison locally: ```sh -python3 scripts/upstream.py record --metadata .lake/upstream-current.json \ - --only RDo.randOps --note 'Ported the core change; measurable-space arguments remain explicit.' +python3 scripts/upstream.py check --target HEAD --report .lake/upstream-report.md ``` -Each selected declaration's origins receive the current toolchain commit and source range. -Other declarations keep their existing baselines. Commit the baseline update with the adaptation -or explanation, so reviewers can see both. `--all` explicitly records every exported annotation -and removes obsolete mappings; use it only when all affected entries have been reviewed. -For a local rename, `--all` also reconciles the old and new identities; unchanged upstream entries -still need accurate review notes. The checker never advances baselines automatically. - -The initial baseline is Lean v4.35.0. It records the existing adaptations as the starting point for -monitoring, not a completed correctness audit. In particular: - -- `RDo.randOps` supplies measurable-space arguments and currently omits core's dead-syntax guard - in `mkPureApp`. This is a known difference to investigate separately. -- The loop parsers, expander and elaborator retain the existing `rdo` adaptations; they do not - implement core's `invariant` / `decreasing` annotations or its verification-condition hooks. -- The class hierarchy and laws have measurable-space parameters and measurability hypotheses, - and omit the applicative layer. These differences are intentional. - -## Watching future core changes +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. -The `Watch Lean core adaptations` workflow checks upstream's default development branch each -Monday at 08:23 UTC and can also be run manually. Scheduled workflows become active once merged -to the repository's default branch. It reads upstream source only; it does not build or execute -future core code or change the project's toolchain. +## Updating a baseline -When a tracked region changes, the workflow opens or updates one GitHub issue with the affected -local declarations, review notes, source links, and upstream diffs. Unchanged relevant edits do -not cause repeated updates when unrelated commits land in core. The issue is closed when no -tracked differences remain. Fetch, metadata, and other check failures fail the workflow and do -not close an existing issue. The watcher has read-only contents access and permission to maintain its issue. -The PR checks add no token permissions to the existing build workflow. No baseline updates or code changes are made by the watcher. - -Run the same comparison locally: +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 scripts/upstream.py check --target HEAD --report .lake/upstream-report.md +python3 scripts/upstream.py record --metadata .lake/upstream-current.json --only RDo.randOps ``` -Without `--repo`, the checker fetches from `leanprover/lean4` into `.lake/upstream-lean.git`. -Use `--repo /path/to/lean4` before `check` or `record` to use an existing Git repository without -fetching. Exit statuses are 0 for unchanged, 1 for changes needing review, and 2 for an incomplete -or invalid check. `--advisory` changes status 1 to 0; errors still fail. +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 `scripts/ExportUpstream.lean`, export, and record its mappings. + +## Scope -## Coverage and tests +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. -Moved or deleted files and renamed declarations are reported through changes at their recorded -locations. Insertions immediately at either boundary are conservatively flagged because they -can extend a declaration. Unrelated changes elsewhere in the same file are ignored. -This is source-change detection: changes to untracked helpers or surrounding module/section -context can also affect behavior. It does not prove that an adaptation remains correct. Keep the project's behavior and elaboration tests. +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 scripts/tests -p 'test_upstream.py' -lake env lean scripts/tests/Upstream.lean +lake env lean scripts/tests/Analogue.lean +node --test scripts/tests/test_upstream_issue.cjs ``` - -The Python tests construct local Git histories and require no network. They cover source/body -changes, boundary insertions, unrelated edits, moves/deletions, malformed or missing data, -partial review, exit statuses, baseline preservation, and notification deduplication. diff --git a/scripts/ExportUpstream.lean b/scripts/ExportUpstream.lean index c1d66b1..1603105 100644 --- a/scripts/ExportUpstream.lean +++ b/scripts/ExportUpstream.lean @@ -13,13 +13,13 @@ tracked modules. Source ranges come from the running toolchain's declaration met class fields and definition bodies. They are meaningful only at the accompanying Lean commit. -/ -open Lean RandomDo.Upstream +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 := upstreamAttr.getParam? env decl then + 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]! diff --git a/scripts/tests/Analogue.lean b/scripts/tests/Analogue.lean new file mode 100644 index 0000000..5dc67ce --- /dev/null +++ b/scripts/tests/Analogue.lean @@ -0,0 +1,34 @@ +import RandomDo.Monad.Notation + +open Lean RandomDo.Analogue + +namespace AnalogueTests + +@[analogue Pure Bind] +def adapted : Nat := 0 + +run_cmd do + let env ← getEnv + unless analogueAttr.getParam? env `AnalogueTests.adapted == some #[`Pure, `Bind] do + throwError "Multiple analogue references were not recorded" + unless analogueAttr.getParam? env `RDo.randOps == some #[`Lean.Elab.Do.DoOps.default] do + throwError "Analogue metadata did not survive importing a compiled module" + +/-- error: Unknown constant `NoSuchCoreDeclaration` -/ +#guard_msgs in +@[analogue NoSuchCoreDeclaration] +def unknownOrigin : Nat := 0 + +/-- error: Duplicate analogue declarations -/ +#guard_msgs in +@[analogue Pure Pure] +def duplicateOrigin : Nat := 0 + +/-- +error: Analogue declaration `MeasurableSpaceMonad` belongs to `RandomDo.Monad.MeasurableSpace`, not Lean core +-/ +#guard_msgs in +@[analogue MeasurableSpaceMonad] +def nonCoreOrigin : Nat := 0 + +end AnalogueTests diff --git a/scripts/tests/Upstream.lean b/scripts/tests/Upstream.lean deleted file mode 100644 index 221c597..0000000 --- a/scripts/tests/Upstream.lean +++ /dev/null @@ -1,34 +0,0 @@ -import RandomDo.Monad.Notation - -open Lean RandomDo.Upstream - -namespace UpstreamTests - -@[upstream Pure Bind] -def adapted : Nat := 0 - -run_cmd do - let env ← getEnv - unless upstreamAttr.getParam? env `UpstreamTests.adapted == some #[`Pure, `Bind] do - throwError "Multiple upstream references were not recorded" - unless upstreamAttr.getParam? env `RDo.randOps == some #[`Lean.Elab.Do.DoOps.default] do - throwError "Upstream metadata did not survive importing a compiled module" - -/-- error: Unknown constant `NoSuchCoreDeclaration` -/ -#guard_msgs in -@[upstream NoSuchCoreDeclaration] -def unknownOrigin : Nat := 0 - -/-- error: Duplicate upstream declarations -/ -#guard_msgs in -@[upstream Pure Pure] -def duplicateOrigin : Nat := 0 - -/-- -error: Upstream declaration `MeasurableSpaceMonad` belongs to `RandomDo.Monad.MeasurableSpace`, not Lean core --/ -#guard_msgs in -@[upstream MeasurableSpaceMonad] -def nonCoreOrigin : Nat := 0 - -end UpstreamTests diff --git a/scripts/tests/test_upstream.py b/scripts/tests/test_upstream.py index f43af36..0784637 100644 --- a/scripts/tests/test_upstream.py +++ b/scripts/tests/test_upstream.py @@ -36,7 +36,7 @@ def setUp(self): "local": "Adapted.foo", "local_file": "RandomDo/Example.lean", "upstream": "Example.foo", "path": "src/Example.lean", "start": 3, "end": 4, }]} - self.baseline = upstream.record(None, self.metadata, self.source(), None, "Adapted to m") + self.baseline = upstream.record(None, self.metadata, self.source(), None) def source(self): return upstream.Source(self.repo) @@ -76,6 +76,12 @@ def test_insertions_at_both_boundaries_are_conservatively_reported(self): with self.subTest(text=text): self.assertEqual(len(self.report(self.change(text))["changes"]), 1) + def test_replacing_neighboring_lines_can_extend_a_declaration(self): + for text in [self.original.replace("\n\ndef foo", "\n@[inline]\ndef foo"), + self.original.replace("x + 1\n\n", "x + 1\n + 2\n")]: + with self.subTest(text=text): + self.assertTrue(self.report(self.change(text))["changes"]) + def test_deleted_declaration_and_renamed_declaration(self): target = self.change(self.original.replace("def foo (x : Nat) : Nat :=\n x + 1\n", "")) self.assertTrue(self.report(target)["changes"]) @@ -86,9 +92,9 @@ def test_deleted_or_moved_file_is_reported(self): self.path.rename(self.path.with_name("Moved.lean")) self.assertTrue(self.report(self.commit())["changes"]) - def test_corrupted_baseline_is_an_error(self): - self.baseline["entries"][0]["sha256"] = "0" * 64 - with self.assertRaisesRegex(upstream.CheckError, "hash mismatch"): + def test_nonexistent_source_is_an_error(self): + self.baseline["entries"][0]["path"] = "src/Missing.lean" + with self.assertRaises(upstream.CheckError): self.report(self.before) def test_missing_revision_is_an_error(self): @@ -96,7 +102,7 @@ def test_missing_revision_is_an_error(self): self.report("no-such-revision") def test_source_range_and_identity_are_validated(self): - for key, value in [("start", 0), ("end", -1), ("path", "../outside.lean")]: + for key, value in [("start", 0), ("end", 1000), ("path", "../outside.lean")]: baseline = copy.deepcopy(self.baseline) baseline["entries"][0][key] = value with self.subTest(key=key), self.assertRaises(upstream.CheckError): @@ -121,25 +127,50 @@ def test_range_must_match_exported_metadata_at_the_same_commit(self): with self.assertRaisesRegex(upstream.CheckError, "range disagrees"): upstream.validate_mappings(baseline, self.metadata) - def test_invalid_commit_types_are_check_errors(self): - for field in ("commit", "sha256"): - baseline = copy.deepcopy(self.baseline) - baseline["entries"][0][field] = None - with self.subTest(field=field), self.assertRaises(upstream.CheckError): - upstream.entries(baseline, baseline=True) + def test_invalid_commit_is_a_check_error(self): + self.baseline["entries"][0]["commit"] = None + with self.assertRaises(upstream.CheckError): + upstream.entries(self.baseline, baseline=True) def test_partial_review_preserves_other_baselines(self): metadata = copy.deepcopy(self.metadata) metadata["entries"].append({**metadata["entries"][0], "local": "Adapted.second"}) - baseline = upstream.record(None, metadata, self.source(), None, "Initial review") + baseline = upstream.record(None, metadata, self.source(), None) metadata["commit"] = self.change(self.original.replace("x + 1", "x + 2")) - reviewed = upstream.record(baseline, metadata, self.source(), ["Adapted.foo"], "Ported fix") + reviewed = upstream.record(baseline, metadata, self.source(), ["Adapted.foo"]) by_name = {e["local"]: e for e in reviewed["entries"]} self.assertEqual(by_name["Adapted.foo"]["commit"], metadata["commit"]) self.assertEqual(by_name["Adapted.second"]["commit"], self.before) report = upstream.check(reviewed, self.source(), metadata["commit"]) self.assertEqual([c["local"] for c in report["changes"]], ["Adapted.second"]) + def test_removing_or_renaming_one_annotation_preserves_other_baselines(self): + for renamed in (False, True): + with self.subTest(renamed=renamed): + metadata = copy.deepcopy(self.metadata) + metadata["entries"].append({**metadata["entries"][0], "local": "Adapted.second"}) + baseline = upstream.record(None, metadata, self.source(), None) + metadata["commit"] = self.change(self.path.read_text() + "-- unrelated\n") + metadata["entries"].pop(0) + selected = ["Adapted.foo"] + if renamed: + metadata["entries"].append({**metadata["entries"][0], "local": "Adapted.new"}) + selected.append("Adapted.new") + recorded = upstream.record(baseline, metadata, self.source(), selected) + upstream.validate_mappings(recorded, metadata) + by_name = {e["local"]: e for e in recorded["entries"]} + self.assertNotIn("Adapted.foo", by_name) + self.assertEqual(by_name["Adapted.second"]["commit"], self.before) + if renamed: + self.assertEqual(by_name["Adapted.new"]["commit"], metadata["commit"]) + + def test_git_display_settings_cannot_hide_or_expand_changes(self): + upstream.git(self.repo, "config", "color.ui", "always") + upstream.git(self.repo, "config", "diff.interHunkContext", "100") + (self.repo / ".gitattributes").write_text("*.lean binary\n") + self.assertFalse(self.report(self.change(self.original.replace("10", "20")))["changes"]) + self.assertTrue(self.report(self.change(self.original.replace("x + 1", "x + 2")))["changes"]) + def test_no_automatic_baseline_update_and_exit_codes(self): lock = self.repo / "baseline.json" lock.write_text(json.dumps(self.baseline)) @@ -160,10 +191,10 @@ def test_notification_fingerprint_ignores_unrelated_commits(self): self.assertNotEqual(first["target"], second["target"]) self.assertEqual(first["fingerprint"], second["fingerprint"]) - def test_report_includes_mapping_review_note_and_upstream_diff(self): + def test_report_includes_mapping_and_upstream_diff(self): report = self.report(self.change(self.original.replace("x + 1", "x + 2"))) text = upstream.markdown(report) - for expected in ["Adapted.foo", "Example.foo", "Adapted to m", "- x + 1", "+ x + 2"]: + for expected in ["Adapted.foo", "Example.foo", "- x + 1", "+ x + 2"]: self.assertIn(expected, text) diff --git a/scripts/tests/test_upstream_issue.cjs b/scripts/tests/test_upstream_issue.cjs new file mode 100644 index 0000000..f5d7ddc --- /dev/null +++ b/scripts/tests/test_upstream_issue.cjs @@ -0,0 +1,71 @@ +const assert = require('node:assert/strict'); +const { test } = require('node:test'); +const updateIssue = require('../upstream-issue.cjs'); + +const context = { + repo: { owner: 'example', repo: 'RandomDo' }, serverUrl: 'https://github.com', runId: 42, +}; +const report = { + fingerprint: 'abc', + changes: [{ local: 'RDo.randOps', upstream: 'Lean.Elab.Do.DoOps.default', + commit: 'deadbeef', path: 'src/Lean/Elab/Do/Basic.lean', start: 10, end: 20 }], +}; +const marker = ''; +const issue = { number: 7, state: 'open', body: marker }; + +async function run(issues, current = report) { + const calls = []; + const github = { + paginate: async () => issues, + rest: { issues: { + listForRepo: {}, + create: async args => calls.push({ operation: 'create', ...args }), + update: async args => calls.push({ operation: 'update', ...args }), + } }, + }; + await updateIssue({ github, context }, current); + return calls; +} + +test('creates one issue containing mappings and a link to the complete report', async () => { + const [call] = await run([]); + assert.equal(call.operation, 'create'); + assert.equal(call.owner, context.repo.owner); + assert.equal(call.repo, context.repo.repo); + assert.match(call.body, /RDo\.randOps/); + assert.match(call.body, /blob\/deadbeef\/src\/Lean\/Elab\/Do\/Basic\.lean#L10-L20/); + assert.match(call.body, /https:\/\/github.com\/example\/RandomDo\/actions\/runs\/42/); +}); + +test('updates an existing tracker and ignores other issues and pull requests', async () => { + const calls = await run([{ number: 1, body: 'Unrelated issue' }, + { number: 2, body: marker, pull_request: {} }, issue]); + assert.equal(calls.length, 1); + assert.equal(calls[0].operation, 'update'); + assert.equal(calls[0].issue_number, 7); +}); + +test('does not update an issue when the relevant edits are unchanged', async () => { + const [created] = await run([]); + assert.deepEqual(await run([{ ...issue, body: created.body }]), []); +}); + +test('closes the tracker when no differences remain', async () => { + const calls = await run([issue], { ...report, changes: [] }); + assert.deepEqual(calls, [{ operation: 'update', ...context.repo, issue_number: 7, state: 'closed' }]); + assert.deepEqual(await run([], { ...report, changes: [] }), []); + assert.deepEqual(await run([{ ...issue, state: 'closed' }], { ...report, changes: [] }), []); +}); + +test('reopens the same issue when differences remain', async () => { + const [created] = await run([]); + const [call] = await run([{ ...issue, state: 'closed', body: created.body }]); + assert.equal(call.operation, 'update'); + assert.equal(call.issue_number, 7); + assert.equal(call.state, 'open'); +}); + +test('propagates API failures', async () => { + const github = { rest: { issues: {} }, paginate: async () => { throw new Error('API unavailable'); } }; + await assert.rejects(updateIssue({ github, context }, report), /API unavailable/); +}); diff --git a/scripts/upstream-issue.cjs b/scripts/upstream-issue.cjs new file mode 100644 index 0000000..24260c4 --- /dev/null +++ b/scripts/upstream-issue.cjs @@ -0,0 +1,31 @@ +// Keep GitHub issue handling separate from the source checker so both work offline in tests. +module.exports = async function updateIssue({ github, context }, report) { + const marker = ''; + const digest = ``; + const issues = await github.paginate(github.rest.issues.listForRepo, { + ...context.repo, state: 'all', creator: 'github-actions[bot]', per_page: 100, + }); + const issue = issues.find(i => !i.pull_request && i.body?.includes(marker)); + if (report.changes.length === 0) { + if (issue?.state === 'open') { + await github.rest.issues.update({ ...context.repo, issue_number: issue.number, state: 'closed' }); + } + return; + } + if (issue?.state === 'open' && issue.body?.includes(digest)) return; + + const run = `${context.serverUrl}/${context.repo.owner}/${context.repo.repo}/actions/runs/${context.runId}`; + const mappings = report.changes.map(c => + `- \`${c.local}\` → [\`${c.upstream}\`](https://github.com/leanprover/lean4/blob/${c.commit}/${c.path}#L${c.start}-L${c.end})`); + const body = [marker, digest, + 'Lean core has changed in these tracked declarations since their recorded baselines:', '', + ...mappings, '', `[Review the upstream diffs](${run}), then update the affected adaptations and baselines.`, + ].join('\n'); + if (issue) { + await github.rest.issues.update({ ...context.repo, issue_number: issue.number, body, state: 'open' }); + } else { + await github.rest.issues.create({ + ...context.repo, title: 'Lean core changes affecting adapted definitions', body, + }); + } +}; diff --git a/scripts/upstream.py b/scripts/upstream.py index 6051908..70a8b14 100644 --- a/scripts/upstream.py +++ b/scripts/upstream.py @@ -9,12 +9,12 @@ import re import subprocess import sys -from dataclasses import dataclass +from functools import cache from pathlib import Path, PurePosixPath ROOT = Path(__file__).resolve().parents[1] REPOSITORY = "https://github.com/leanprover/lean4" -LOCK = ROOT / "upstream.json" +BASELINE = ROOT / "upstream.json" SHA = re.compile(r"[0-9a-f]{40}\Z") HUNK = re.compile(r"@@ -(\d+)(?:,(\d+))? \+(\d+)(?:,(\d+))? @@") @@ -26,17 +26,16 @@ class CheckError(Exception): def git(repo: Path, *args: str) -> str: result = subprocess.run( ["git", "--no-pager", "-C", str(repo), *args], - text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False, + encoding="utf-8", stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False, ) if result.returncode: raise CheckError(f"git {' '.join(args)} failed: {result.stderr.strip()}") return result.stdout -def valid_ref(ref: str) -> str: +def validate_ref(ref: str) -> None: if not re.fullmatch(r"[A-Za-z0-9_][A-Za-z0-9_./-]*", ref) or ".." in ref: raise CheckError(f"Invalid upstream revision: {ref!r}") - return ref class Source: @@ -47,11 +46,9 @@ def __init__(self, repo: Path | None): self.repo.mkdir(parents=True) git(self.repo, "init", "--bare") self.revisions: dict[str, str] = {} - self.files: dict[tuple[str, str], str] = {} - self.diffs: dict[tuple[str, str, str], str] = {} def resolve(self, ref: str) -> str: - valid_ref(ref) + validate_ref(ref) if ref not in self.revisions: if self.fetch: # Fetch only data from the fixed upstream repository; never check out or execute it. @@ -66,24 +63,21 @@ def resolve(self, ref: str) -> str: self.revisions[commit] = commit return self.revisions[ref] + @cache def read(self, commit: str, path: str) -> str: - key = (commit, path) - if key not in self.files: - self.files[key] = git(self.repo, "show", f"{commit}:{path}") - return self.files[key] + return git(self.repo, "show", f"{commit}:{path}") + @cache def diff(self, before: str, after: str, path: str) -> str: - key = (before, after, path) - if key not in self.diffs: - self.diffs[key] = git( - self.repo, "diff", "--no-ext-diff", "--no-textconv", "--no-renames", - "--unified=3", before, after, "--", path, - ) - return self.diffs[key] + # Zero context makes each hunk one contiguous edit. Ignore local display settings and + # attributes that could otherwise color the patch, merge hunks, or hide text as binary. + return git(self.repo, "diff", "--no-color", "--text", "--no-ext-diff", "--no-textconv", + "--no-renames", "--unified=0", "--inter-hunk-context=0", + "--diff-algorithm=myers", "--no-indent-heuristic", before, after, "--", path) def read_json(path: Path) -> dict: - value = json.loads(path.read_text()) + value = json.loads(path.read_text(encoding="utf-8")) if not isinstance(value, dict) or value.get("schema") != 1: raise CheckError(f"Unsupported metadata schema in {path}") return value @@ -113,13 +107,8 @@ def entries(document: dict, *, baseline: bool) -> dict[tuple[str, str], dict]: start, end = entry.get("start"), entry.get("end") if type(start) is not int or type(end) is not int or not 1 <= start <= end: raise CheckError(f"Invalid source range for {entry['upstream']}") - if baseline: - if not isinstance(entry.get("commit"), str) or not SHA.fullmatch(entry["commit"]): - raise CheckError(f"Invalid baseline commit for {entry['upstream']}") - if not isinstance(entry.get("sha256"), str) or not re.fullmatch(r"[0-9a-f]{64}", entry["sha256"]): - raise CheckError(f"Missing source hash for {entry['upstream']}") - if not isinstance(entry.get("note"), str) or not entry["note"].strip(): - raise CheckError(f"Missing review note for {entry['local']}") + if baseline and (not isinstance(entry.get("commit"), str) or not SHA.fullmatch(entry["commit"])): + raise CheckError(f"Invalid baseline commit for {entry['upstream']}") key = identity(entry) if key in result: raise CheckError(f"Duplicate upstream mapping: {key}") @@ -148,50 +137,31 @@ def validate_mappings(baseline: dict, metadata: dict) -> None: raise CheckError(f"Baseline range disagrees with Lean's metadata for {key[1]}") -def source_hash(source: Source, commit: str, entry: dict) -> str: - lines = source.read(commit, entry["path"]).splitlines(keepends=True) - if entry["end"] > len(lines): +def validate_range(source: Source, commit: str, entry: dict) -> None: + if entry["end"] > len(source.read(commit, entry["path"]).splitlines()): raise CheckError(f"Source range exceeds {entry['path']} at {commit}") - text = "".join(lines[entry["start"] - 1:entry["end"]]) - return hashlib.sha256(text.encode()).hexdigest() - - -@dataclass -class Hunk: - old_start: int - lines: list[str] - - def edits(self, start: int, end: int) -> list[list[str]]: - """Return relevant edit blocks, excluding context and unrelated edits in the same hunk.""" - line = self.old_start - result, block, affected = [], [], False - for text in self.lines[1:]: - if text.startswith("+"): - # Include insertions at either boundary: these can extend a declaration. - affected |= start - 1 <= line - 1 <= end - block.append(text) - elif text.startswith("-"): - affected |= start <= line <= end - block.append(text) - line += 1 - elif text.startswith(" "): - if affected: - result.append(block) - block, affected = [], False - line += 1 - if affected: - result.append(block) - return result - - -def hunks(diff: str) -> list[Hunk]: - result: list[Hunk] = [] - for line in diff.splitlines(): - match = HUNK.match(line) - if match: - result.append(Hunk(int(match[1]), [line])) - elif result: - result[-1].lines.append(line) + + +def changed_hunks(diff: str, start: int, end: int) -> list[str]: + """Select zero-context hunks touching the inclusive baseline range.""" + result = [] + for hunk in re.split(r"(?m)^(?=@@ -)", diff)[1:]: + match = HUNK.match(hunk) + if match is None: + raise CheckError("Invalid Git diff hunk") + first = int(match[1]) + count = int(match[2]) if match[2] is not None else 1 + # A pure insertion is anchored after `first`. Include both boundaries because a new + # attribute or trailing clause can extend the declaration beyond its old source range. + if count == 0: + touches = start - 1 <= first <= end + else: + # Replacing a neighboring line can also add an attribute or trailing clause. + added = int(match[4]) if match[4] is not None else 1 + margin = 1 if added else 0 + touches = first <= end + margin and first + count > start - margin + if touches: + result.append(hunk.rstrip("\n")) return result @@ -202,43 +172,33 @@ def check(baseline: dict, source: Source, target: str) -> dict: for key in sorted(tracked): entry = tracked[key] before = source.resolve(entry["commit"]) - if source_hash(source, before, entry) != entry["sha256"]: - raise CheckError(f"Baseline source hash mismatch for {entry['upstream']}") - relevant = [(h, h.edits(entry["start"], entry["end"])) - for h in hunks(source.diff(before, target, entry["path"]))] - relevant = [(h, edits) for h, edits in relevant if edits] - if relevant: - changes.append({**entry, "diff": "\n".join( - line for h, _ in relevant for line in h.lines), - "edits": [block for _, edits in relevant for block in edits]}) - # Unrelated upstream commits must not cause repeated issue updates. Hunk offsets may change - # when unrelated lines are inserted earlier in the file, so exclude them from the digest. - fingerprint = hashlib.sha256(json.dumps([ - [c["local"], c["local_file"], c["upstream"], c["path"], c["commit"], - c["start"], c["end"], c["note"], c["edits"]] - for c in changes - ], ensure_ascii=False, sort_keys=True).encode()).hexdigest() + validate_range(source, before, entry) + hunks = changed_hunks(source.diff(before, target, entry["path"]), entry["start"], entry["end"]) + if hunks: + changes.append({**entry, "diff": "\n".join(hunks)}) + # Exclude hunk headings: unrelated insertions can shift the target's line numbers. + edits = [{**c, "diff": "\n".join(line for line in c["diff"].splitlines() + if not line.startswith("@@ "))} for c in changes] + fingerprint = hashlib.sha256(json.dumps(edits, sort_keys=True).encode()).hexdigest() return {"target": target, "checked": len(tracked), "changes": changes, "fingerprint": fingerprint} def record(baseline: dict | None, metadata: dict, source: Source, - selected: list[str] | None, note: str) -> dict: + selected: list[str] | None) -> dict: current = entries(metadata, baseline=False) old = entries(baseline, baseline=True) if baseline is not None else {} - if not note.strip(): - raise CheckError("A review note is required") - names = {key[0] for key in current} + names = {key[0] for key in old.keys() | current.keys()} chosen = set(selected) if selected else names if not chosen <= names: raise CheckError(f"Unknown tracked declarations: {sorted(chosen - names)}") - # --all also removes annotations that were deleted; --only preserves all other baselines. + # Include old names so --only can remove or rename an annotation without advancing others. result = {key: value for key, value in old.items() if selected and key[0] not in chosen} commit = source.resolve(metadata["commit"]) for key, entry in current.items(): if key[0] in chosen: - result[key] = {**entry, "commit": commit, - "sha256": source_hash(source, commit, entry), "note": note} + validate_range(source, commit, entry) + result[key] = {**entry, "commit": commit} return {"schema": 1, "repository": REPOSITORY, "entries": [result[key] for key in sorted(result)]} @@ -250,25 +210,21 @@ def markdown(report: dict) -> str: if not report["changes"]: lines.append("No changes intersect the tracked declarations since their recorded baselines.") else: - lines += ["Review these upstream changes, then port them or explain why they do not apply. " - "Advance a declaration's baseline only after that review. " - "A moved or deleted source file is reported as a deletion.", ""] + lines += ["Review these changes before advancing the affected baselines.", ""] for change in report["changes"]: link = (f"{REPOSITORY}/blob/{change['commit']}/{change['path']}" f"#L{change['start']}-L{change['end']}") lines += [f"## `{change['local']}`", "", f"Local file: `{change['local_file']}`. " f"Upstream: [`{change['upstream']}`]({link}).", "", - f"Baseline note: {change['note']}", "", - f"[Full upstream comparison]({REPOSITORY}/compare/" - f"{change['commit']}...{report['target']})", "", "````diff", + "````diff", change["diff"], "````", ""] return "\n".join(lines) + "\n" def main(argv: list[str] | None = None) -> int: parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("--baseline", type=Path, default=LOCK) + parser.add_argument("--baseline", type=Path, default=BASELINE) parser.add_argument("--repo", type=Path, help="Use an existing Lean Git repository without fetching") commands = parser.add_subparsers(dest="command", required=True) check_parser = commands.add_parser("check", help="Report upstream changes; never update the baseline") @@ -276,21 +232,22 @@ def main(argv: list[str] | None = None) -> int: check_parser.add_argument("--target", help="Upstream revision (defaults to the exported Lean commit)") check_parser.add_argument("--report", type=Path) check_parser.add_argument("--json-report", type=Path) - check_parser.add_argument("--advisory", action="store_true", help="Exit successfully on drift, but not on errors") + check_parser.add_argument("--advisory", action="store_true", + help="Exit successfully on drift, but not on errors") record_parser = commands.add_parser("record", help="Record explicitly reviewed upstream baselines") record_parser.add_argument("--metadata", type=Path, required=True) choice = record_parser.add_mutually_exclusive_group(required=True) choice.add_argument("--only", nargs="+", metavar="DECL") choice.add_argument("--all", action="store_true") - record_parser.add_argument("--note", required=True) args = parser.parse_args(argv) try: baseline = read_json(args.baseline) if args.baseline.exists() else None metadata = read_json(args.metadata) if args.metadata else None source = Source(args.repo) if args.command == "record": - result = record(baseline, metadata, source, args.only, args.note) - args.baseline.write_text(json.dumps(result, ensure_ascii=False, indent=2) + "\n") + result = record(baseline, metadata, source, args.only) + args.baseline.write_text( + json.dumps(result, ensure_ascii=False, indent=2) + "\n", encoding="utf-8") print(f"Recorded {len(result['entries'])} mappings in {args.baseline}") return 0 if baseline is None: @@ -303,11 +260,12 @@ def main(argv: list[str] | None = None) -> int: report = check(baseline, source, target) text = markdown(report) if args.report: - args.report.write_text(text) + args.report.write_text(text, encoding="utf-8") else: print(text, end="") if args.json_report: - args.json_report.write_text(json.dumps(report, ensure_ascii=False, indent=2) + "\n") + args.json_report.write_text( + json.dumps(report, ensure_ascii=False, indent=2) + "\n", encoding="utf-8") return 1 if report["changes"] and not args.advisory else 0 except (CheckError, OSError, ValueError) as exc: print(f"Upstream check failed: {exc}", file=sys.stderr) diff --git a/upstream.json b/upstream.json index 976d024..228a91b 100644 --- a/upstream.json +++ b/upstream.json @@ -9,9 +9,7 @@ "path": "src/Init/Control/Lawful/Basic.lean", "start": 20, "upstream": "LawfulFunctor", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "6cc2037bc873862c4b85679592862def80ffc25002449eb0f42b074911092b10", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 159, @@ -20,9 +18,7 @@ "path": "src/Init/Control/Lawful/Basic.lean", "start": 125, "upstream": "LawfulMonad", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "e701a60ca37c38a4c6463db27120120bcddb9b7841e21c19fa9a05403e021896", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 3881, @@ -31,9 +27,7 @@ "path": "src/Init/Prelude.lean", "start": 3869, "upstream": "Bind", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "210b68a6ae65efbf339df0cc96e8bbe74f8018ef5f2f4e3e1293f065f51cf487", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 180, @@ -42,9 +36,7 @@ "path": "src/Init/Control/Lawful/Basic.lean", "start": 179, "upstream": "bind_congr", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "0ec2334c28a0e31bf8790a12ba2d2eae8a32c523280085089b5c2022a8e78026", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 388, @@ -53,9 +45,7 @@ "path": "src/Init/Core.lean", "start": 366, "upstream": "ForIn", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "45a34391c62bd3286fb6c60461f5a16d3147105004222240facdddc89d8801d0", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 416, @@ -64,9 +54,7 @@ "path": "src/Init/Core.lean", "start": 392, "upstream": "ForIn'", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "63b45de3bbd497e26e4d9af17172e23eb8fa813cc493ca00a956003f6ae6b463", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 3937, @@ -75,9 +63,7 @@ "path": "src/Init/Prelude.lean", "start": 3903, "upstream": "Functor", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "1be4516f598ce7e2dd50381f3f7fbb9d14bdc4f1f636bc94e83f5fa4a7eca667", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 186, @@ -86,9 +72,7 @@ "path": "src/Init/Control/Lawful/Basic.lean", "start": 185, "upstream": "map_congr", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "2fa31b1b51ecb17cb8f11d39b5cedeb2ab6bd89af909564f0676e37ced75f405", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 4038, @@ -97,9 +81,7 @@ "path": "src/Init/Prelude.lean", "start": 4020, "upstream": "Monad", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "6234016213a903ac9910fc72b4de104bcd4c9cb1ab33fc63f0ae52aa4f872c19", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 3899, @@ -108,9 +90,7 @@ "path": "src/Init/Prelude.lean", "start": 3885, "upstream": "Pure", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "997ff22ea7f4d2a759a49b9bfc8730eeeccf731ba5746ef87a63913243475799", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 409, @@ -119,9 +99,7 @@ "path": "src/Lean/Elab/BuiltinDo/For.lean", "start": 274, "upstream": "Lean.Elab.Do.elabDoFor", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "a76b98157e5aa89eaffa74a54eee1e0289b1f1a12011c2cc877bcfcc8cecf5ba", - "note": "Initial v4.35.0 baseline for the existing rdo loop adaptation. Core invariant/decreasing syntax and verification-condition hooks are not implemented; see docs/upstream-tracking.md." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 1104, @@ -130,9 +108,7 @@ "path": "src/Lean/Elab/Do/Basic.lean", "start": 1102, "upstream": "Lean.Elab.Do.elabDo", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "529ac011ffa6752eb1b845f722393177dbbf1a75d0d87e1c9ee0b6facfb15d5f", - "note": "Uses rdo syntax and passes randOps to the shared core elaborator." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 87, @@ -141,9 +117,7 @@ "path": "src/Lean/Elab/BuiltinDo/For.lean", "start": 24, "upstream": "Lean.Elab.Do.expandDoFor", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "334393bb33da3c0ac44a58817fefa5980341f962d201223c0ee2a13d53a72956", - "note": "Initial v4.35.0 baseline for the existing rdo loop adaptation. Core invariant/decreasing syntax and verification-condition hooks are not implemented; see docs/upstream-tracking.md." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 339, @@ -152,9 +126,7 @@ "path": "src/Lean/Elab/Do/Basic.lean", "start": 309, "upstream": "Lean.Elab.Do.DoOps.default", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "912707da88c0d9bbbdb417857aa32923b6080d6f4eb92b08dd694302f6790afb", - "note": "Initial v4.35.0 baseline. Adds measurable-space arguments; the existing mkPureApp override omits the upstream dead-syntax guard, which remains a follow-up review item." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 217, @@ -163,9 +135,7 @@ "path": "src/Lean/Parser/Do.lean", "start": 208, "upstream": "Lean.Parser.Term.doFor", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "38e65c348f80c6f644c1ac6a71a8e5647f1184e8d6e39447657463abe013ba1b", - "note": "Initial v4.35.0 baseline for the existing rdo loop adaptation. Core invariant/decreasing syntax and verification-condition hooks are not implemented; see docs/upstream-tracking.md." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 186, @@ -174,9 +144,7 @@ "path": "src/Lean/Parser/Do.lean", "start": 184, "upstream": "Lean.Parser.Term.doForDecl", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "ee21206fa7575137d2438b36a9950a6838aeb63b2d187996e77385448ba2867d", - "note": "Initial v4.35.0 baseline for the existing rdo loop adaptation. Core invariant/decreasing syntax and verification-condition hooks are not implemented; see docs/upstream-tracking.md." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 48, @@ -185,9 +153,7 @@ "path": "src/Init/Control/Lawful/Basic.lean", "start": 47, "upstream": "id_map'", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "a95c9957a4b53496da246b239ac5e3cf0674e31399b26dcaf431e5a22560de55", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 30, @@ -196,9 +162,7 @@ "path": "src/Init/Control/Basic.lean", "start": 16, "upstream": "instForInOfForIn'", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "f3633bf63b71bb5167b596950cb20bf22fbbce08496990269ac08d8a8b7b9385", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 208, @@ -207,9 +171,7 @@ "path": "src/Init/Control/Lawful/Basic.lean", "start": 205, "upstream": "bind_map_left", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "9a6f4815d41cec24233f2b78492e54fc364adc1052daad6195c72e2937e523aa", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 167, @@ -218,9 +180,7 @@ "path": "src/Init/Control/Lawful/Basic.lean", "start": 165, "upstream": "bind_pure", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "e9cf0d00e632a518d1c62d3aca72d4f586a7db23909d901a10e50bafb00eeb2f", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 183, @@ -229,9 +189,7 @@ "path": "src/Init/Control/Lawful/Basic.lean", "start": 182, "upstream": "bind_pure_unit", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "a3c9870f5e209316d44663a98e412b1ad6d6d325df90a5be1c00fa8f59969042", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 174, @@ -240,9 +198,7 @@ "path": "src/Init/Control/Lawful/Basic.lean", "start": 169, "upstream": "map_eq_pure_bind", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "ad6d8f6c43be7df2ec4dbf7d96b19e877fd693bf6afcad9d1539eb5d2705af46", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 203, @@ -251,9 +207,7 @@ "path": "src/Init/Control/Lawful/Basic.lean", "start": 200, "upstream": "map_bind", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "dd22185502a5bff4dcc033c76e846218c6b27835b54e08233ac3f6e76d596ea4", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 52, @@ -262,9 +216,7 @@ "path": "src/Init/Control/Lawful/Basic.lean", "start": 50, "upstream": "Functor.map_map", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "50e2e660e52da2b9f147021b8f3bf3744f1244f861a649d689b5dec2e5353ff4", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" }, { "end": 85, @@ -273,9 +225,7 @@ "path": "src/Init/Control/Lawful/Basic.lean", "start": 85, "upstream": "LawfulApplicative.map_pure", - "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc", - "sha256": "0e46a1b086567226a38c7eb7d3deb3c387395caebb8a0838a164801743109a57", - "note": "Adapted to measurable-space parameters and measurable maps; the hierarchy intentionally omits the applicative layer." + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" } ] } From 18ba424b1d21d850c845d4aa31c2f59e4b0fc2da Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 22:36:05 +0000 Subject: [PATCH 4/4] Isolate upstream maintenance tooling under .github --- .../upstream/Export.lean | 4 +- .../upstream/README.md | 35 ++++++---- .../upstream/baseline.json | 0 .../upstream.py => .github/upstream/check.py | 4 +- .../upstream/notify.cjs | 0 .../upstream}/tests/Analogue.lean | 17 ++--- .../upstream/tests/test_check.py | 70 +++++++++---------- .../upstream/tests/test_notify.cjs | 2 +- .github/workflows/build.yml | 10 +-- .github/workflows/upstream-core.yml | 10 +-- README.md | 5 +- RandomDo/Util/Analogue.lean | 29 +++----- 12 files changed, 87 insertions(+), 99 deletions(-) rename scripts/ExportUpstream.lean => .github/upstream/Export.lean (87%) rename docs/upstream-tracking.md => .github/upstream/README.md (68%) rename upstream.json => .github/upstream/baseline.json (100%) rename scripts/upstream.py => .github/upstream/check.py (99%) rename scripts/upstream-issue.cjs => .github/upstream/notify.cjs (100%) rename {scripts => .github/upstream}/tests/Analogue.lean (67%) rename scripts/tests/test_upstream.py => .github/upstream/tests/test_check.py (76%) rename scripts/tests/test_upstream_issue.cjs => .github/upstream/tests/test_notify.cjs (98%) diff --git a/scripts/ExportUpstream.lean b/.github/upstream/Export.lean similarity index 87% rename from scripts/ExportUpstream.lean rename to .github/upstream/Export.lean index 1603105..92f838e 100644 --- a/scripts/ExportUpstream.lean +++ b/.github/upstream/Export.lean @@ -8,7 +8,7 @@ import Lean.DeclarationRange import Lean.Data.Json /-! -Run `lake env lean scripts/ExportUpstream.lean > .lake/upstream-current.json` after building the +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. -/ @@ -27,6 +27,8 @@ run_cmd 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 diff --git a/docs/upstream-tracking.md b/.github/upstream/README.md similarity index 68% rename from docs/upstream-tracking.md rename to .github/upstream/README.md index 4547606..908ae74 100644 --- a/docs/upstream-tracking.md +++ b/.github/upstream/README.md @@ -1,4 +1,8 @@ -# Tracking Lean core analogues +# 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: @@ -12,8 +16,8 @@ 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 checks that each name exists in Lean core and records metadata without changing -any definition. It is defined in `RandomDo/Util/Analogue.lean`. +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 @@ -22,12 +26,13 @@ To check the current toolchain against the recorded baselines: ```sh lake build --wfail RandomDo.Monad.MeasurableSpace RandomDo.Monad.Notation -lake env lean scripts/ExportUpstream.lean > .lake/upstream-current.json -python3 scripts/upstream.py check --metadata .lake/upstream-current.json +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; -`upstream.json` stores the source path, line range, and exact Lean commit for each mapping. +`.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. @@ -41,7 +46,7 @@ after merge to the default branch and can also be run manually. To run the same comparison locally: ```sh -python3 scripts/upstream.py check --target HEAD --report .lake/upstream-report.md +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. @@ -55,13 +60,13 @@ Review the upstream diff, adapt the local code as needed, and explain intentiona in the PR. Then record just the declarations you reviewed: ```sh -python3 scripts/upstream.py record --metadata .lake/upstream-current.json --only RDo.randOps +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 `scripts/ExportUpstream.lean`, export, and record its mappings. +To track another module, import it in `.github/upstream/Export.lean`, export, and record its mappings. ## Scope @@ -71,14 +76,14 @@ correctness audit. Known differences include the omitted dead-syntax guard in th 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. +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 scripts/tests -p 'test_upstream.py' -lake env lean scripts/tests/Analogue.lean -node --test scripts/tests/test_upstream_issue.cjs +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 ``` diff --git a/upstream.json b/.github/upstream/baseline.json similarity index 100% rename from upstream.json rename to .github/upstream/baseline.json diff --git a/scripts/upstream.py b/.github/upstream/check.py similarity index 99% rename from scripts/upstream.py rename to .github/upstream/check.py index 70a8b14..841b28d 100644 --- a/scripts/upstream.py +++ b/.github/upstream/check.py @@ -12,9 +12,9 @@ from functools import cache from pathlib import Path, PurePosixPath -ROOT = Path(__file__).resolve().parents[1] +ROOT = Path(__file__).resolve().parents[2] REPOSITORY = "https://github.com/leanprover/lean4" -BASELINE = ROOT / "upstream.json" +BASELINE = Path(__file__).with_name("baseline.json") SHA = re.compile(r"[0-9a-f]{40}\Z") HUNK = re.compile(r"@@ -(\d+)(?:,(\d+))? \+(\d+)(?:,(\d+))? @@") diff --git a/scripts/upstream-issue.cjs b/.github/upstream/notify.cjs similarity index 100% rename from scripts/upstream-issue.cjs rename to .github/upstream/notify.cjs diff --git a/scripts/tests/Analogue.lean b/.github/upstream/tests/Analogue.lean similarity index 67% rename from scripts/tests/Analogue.lean rename to .github/upstream/tests/Analogue.lean index 5dc67ce..0a74403 100644 --- a/scripts/tests/Analogue.lean +++ b/.github/upstream/tests/Analogue.lean @@ -19,16 +19,13 @@ run_cmd do @[analogue NoSuchCoreDeclaration] def unknownOrigin : Nat := 0 -/-- error: Duplicate analogue declarations -/ -#guard_msgs in -@[analogue Pure Pure] -def duplicateOrigin : Nat := 0 - -/-- -error: Analogue declaration `MeasurableSpaceMonad` belongs to `RandomDo.Monad.MeasurableSpace`, not Lean core --/ -#guard_msgs in +-- The attribute records relationships; the CI exporter enforces its Lean core scope. @[analogue MeasurableSpaceMonad] -def nonCoreOrigin : Nat := 0 +def localOrigin : Nat := 0 + +run_cmd do + let env ← getEnv + unless analogueAttr.getParam? env `AnalogueTests.localOrigin == some #[`MeasurableSpaceMonad] do + throwError "Analogue metadata should allow declarations outside Lean core" end AnalogueTests diff --git a/scripts/tests/test_upstream.py b/.github/upstream/tests/test_check.py similarity index 76% rename from scripts/tests/test_upstream.py rename to .github/upstream/tests/test_check.py index 0784637..aa43b22 100644 --- a/scripts/tests/test_upstream.py +++ b/.github/upstream/tests/test_check.py @@ -10,7 +10,7 @@ import unittest sys.path.insert(0, str(Path(__file__).resolve().parents[1])) -import upstream +import check as checker class UpstreamTest(unittest.TestCase): @@ -18,9 +18,9 @@ def setUp(self): self.temp = tempfile.TemporaryDirectory() self.addCleanup(self.temp.cleanup) self.repo = Path(self.temp.name) - upstream.git(self.repo, "init", "--quiet") - upstream.git(self.repo, "config", "user.email", "test@example.invalid") - upstream.git(self.repo, "config", "user.name", "Upstream tests") + checker.git(self.repo, "init", "--quiet") + checker.git(self.repo, "config", "user.email", "test@example.invalid") + checker.git(self.repo, "config", "user.name", "Upstream tests") self.path = self.repo / "src" / "Example.lean" self.path.parent.mkdir() self.original = ( @@ -36,22 +36,22 @@ def setUp(self): "local": "Adapted.foo", "local_file": "RandomDo/Example.lean", "upstream": "Example.foo", "path": "src/Example.lean", "start": 3, "end": 4, }]} - self.baseline = upstream.record(None, self.metadata, self.source(), None) + self.baseline = checker.record(None, self.metadata, self.source(), None) def source(self): - return upstream.Source(self.repo) + return checker.Source(self.repo) def commit(self): - upstream.git(self.repo, "add", ".") - upstream.git(self.repo, "commit", "--quiet", "--no-gpg-sign", "-m", "fixture") - return upstream.git(self.repo, "rev-parse", "HEAD").strip() + checker.git(self.repo, "add", ".") + checker.git(self.repo, "commit", "--quiet", "--no-gpg-sign", "-m", "fixture") + return checker.git(self.repo, "rev-parse", "HEAD").strip() def change(self, text): self.path.write_text(text) return self.commit() def report(self, target): - return upstream.check(self.baseline, self.source(), target) + return checker.check(self.baseline, self.source(), target) def test_unchanged_and_unrelated_edits(self): self.assertEqual(self.report(self.before)["changes"], []) @@ -94,54 +94,54 @@ def test_deleted_or_moved_file_is_reported(self): def test_nonexistent_source_is_an_error(self): self.baseline["entries"][0]["path"] = "src/Missing.lean" - with self.assertRaises(upstream.CheckError): + with self.assertRaises(checker.CheckError): self.report(self.before) def test_missing_revision_is_an_error(self): - with self.assertRaises(upstream.CheckError): + with self.assertRaises(checker.CheckError): self.report("no-such-revision") def test_source_range_and_identity_are_validated(self): for key, value in [("start", 0), ("end", 1000), ("path", "../outside.lean")]: baseline = copy.deepcopy(self.baseline) baseline["entries"][0][key] = value - with self.subTest(key=key), self.assertRaises(upstream.CheckError): - upstream.check(baseline, self.source(), self.before) + with self.subTest(key=key), self.assertRaises(checker.CheckError): + checker.check(baseline, self.source(), self.before) baseline = copy.deepcopy(self.baseline) baseline["entries"].append(baseline["entries"][0]) - with self.assertRaisesRegex(upstream.CheckError, "Duplicate"): - upstream.entries(baseline, baseline=True) + with self.assertRaisesRegex(checker.CheckError, "Duplicate"): + checker.entries(baseline, baseline=True) def test_new_removed_and_moved_annotations_require_review(self): - upstream.validate_mappings(self.baseline, self.metadata) + checker.validate_mappings(self.baseline, self.metadata) for key, value in [("local", "Adapted.new"), ("upstream", "Example.new"), ("local_file", "RandomDo/New.lean")]: metadata = copy.deepcopy(self.metadata) metadata["entries"][0][key] = value - with self.subTest(key=key), self.assertRaises(upstream.CheckError): - upstream.validate_mappings(self.baseline, metadata) + with self.subTest(key=key), self.assertRaises(checker.CheckError): + checker.validate_mappings(self.baseline, metadata) def test_range_must_match_exported_metadata_at_the_same_commit(self): baseline = copy.deepcopy(self.baseline) baseline["entries"][0]["start"] = 4 - with self.assertRaisesRegex(upstream.CheckError, "range disagrees"): - upstream.validate_mappings(baseline, self.metadata) + with self.assertRaisesRegex(checker.CheckError, "range disagrees"): + checker.validate_mappings(baseline, self.metadata) def test_invalid_commit_is_a_check_error(self): self.baseline["entries"][0]["commit"] = None - with self.assertRaises(upstream.CheckError): - upstream.entries(self.baseline, baseline=True) + with self.assertRaises(checker.CheckError): + checker.entries(self.baseline, baseline=True) def test_partial_review_preserves_other_baselines(self): metadata = copy.deepcopy(self.metadata) metadata["entries"].append({**metadata["entries"][0], "local": "Adapted.second"}) - baseline = upstream.record(None, metadata, self.source(), None) + baseline = checker.record(None, metadata, self.source(), None) metadata["commit"] = self.change(self.original.replace("x + 1", "x + 2")) - reviewed = upstream.record(baseline, metadata, self.source(), ["Adapted.foo"]) + reviewed = checker.record(baseline, metadata, self.source(), ["Adapted.foo"]) by_name = {e["local"]: e for e in reviewed["entries"]} self.assertEqual(by_name["Adapted.foo"]["commit"], metadata["commit"]) self.assertEqual(by_name["Adapted.second"]["commit"], self.before) - report = upstream.check(reviewed, self.source(), metadata["commit"]) + report = checker.check(reviewed, self.source(), metadata["commit"]) self.assertEqual([c["local"] for c in report["changes"]], ["Adapted.second"]) def test_removing_or_renaming_one_annotation_preserves_other_baselines(self): @@ -149,15 +149,15 @@ def test_removing_or_renaming_one_annotation_preserves_other_baselines(self): with self.subTest(renamed=renamed): metadata = copy.deepcopy(self.metadata) metadata["entries"].append({**metadata["entries"][0], "local": "Adapted.second"}) - baseline = upstream.record(None, metadata, self.source(), None) + baseline = checker.record(None, metadata, self.source(), None) metadata["commit"] = self.change(self.path.read_text() + "-- unrelated\n") metadata["entries"].pop(0) selected = ["Adapted.foo"] if renamed: metadata["entries"].append({**metadata["entries"][0], "local": "Adapted.new"}) selected.append("Adapted.new") - recorded = upstream.record(baseline, metadata, self.source(), selected) - upstream.validate_mappings(recorded, metadata) + recorded = checker.record(baseline, metadata, self.source(), selected) + checker.validate_mappings(recorded, metadata) by_name = {e["local"]: e for e in recorded["entries"]} self.assertNotIn("Adapted.foo", by_name) self.assertEqual(by_name["Adapted.second"]["commit"], self.before) @@ -165,8 +165,8 @@ def test_removing_or_renaming_one_annotation_preserves_other_baselines(self): self.assertEqual(by_name["Adapted.new"]["commit"], metadata["commit"]) def test_git_display_settings_cannot_hide_or_expand_changes(self): - upstream.git(self.repo, "config", "color.ui", "always") - upstream.git(self.repo, "config", "diff.interHunkContext", "100") + checker.git(self.repo, "config", "color.ui", "always") + checker.git(self.repo, "config", "diff.interHunkContext", "100") (self.repo / ".gitattributes").write_text("*.lean binary\n") self.assertFalse(self.report(self.change(self.original.replace("10", "20")))["changes"]) self.assertTrue(self.report(self.change(self.original.replace("x + 1", "x + 2")))["changes"]) @@ -178,10 +178,10 @@ def test_no_automatic_baseline_update_and_exit_codes(self): target = self.change(self.original.replace("x + 1", "x + 2")) args = ["--baseline", str(lock), "--repo", str(self.repo), "check", "--target", target] with contextlib.redirect_stdout(io.StringIO()): - self.assertEqual(upstream.main(args), 1) - self.assertEqual(upstream.main(args + ["--advisory"]), 0) + self.assertEqual(checker.main(args), 1) + self.assertEqual(checker.main(args + ["--advisory"]), 0) with contextlib.redirect_stderr(io.StringIO()): - self.assertEqual(upstream.main(args[:-1] + ["missing"] + ["--advisory"]), 2) + self.assertEqual(checker.main(args[:-1] + ["missing"] + ["--advisory"]), 2) self.assertEqual(lock.read_bytes(), original) def test_notification_fingerprint_ignores_unrelated_commits(self): @@ -193,7 +193,7 @@ def test_notification_fingerprint_ignores_unrelated_commits(self): def test_report_includes_mapping_and_upstream_diff(self): report = self.report(self.change(self.original.replace("x + 1", "x + 2"))) - text = upstream.markdown(report) + text = checker.markdown(report) for expected in ["Adapted.foo", "Example.foo", "- x + 1", "+ x + 2"]: self.assertIn(expected, text) diff --git a/scripts/tests/test_upstream_issue.cjs b/.github/upstream/tests/test_notify.cjs similarity index 98% rename from scripts/tests/test_upstream_issue.cjs rename to .github/upstream/tests/test_notify.cjs index f5d7ddc..1a7ab27 100644 --- a/scripts/tests/test_upstream_issue.cjs +++ b/.github/upstream/tests/test_notify.cjs @@ -1,6 +1,6 @@ const assert = require('node:assert/strict'); const { test } = require('node:test'); -const updateIssue = require('../upstream-issue.cjs'); +const updateIssue = require('../notify.cjs'); const context = { repo: { owner: 'example', repo: 'RandomDo' }, serverUrl: 'https://github.com', runId: 42, diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 6e4851d..3f1fe70 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -57,14 +57,14 @@ jobs: - name: Test upstream tracking run: | - python3 -m unittest discover -s scripts/tests -p 'test_upstream.py' - node --test scripts/tests/test_upstream_issue.cjs - lake env lean scripts/tests/Analogue.lean + python3 -m unittest discover -s .github/upstream/tests -p 'test_check.py' + node --test .github/upstream/tests/test_notify.cjs + lake env lean .github/upstream/tests/Analogue.lean - name: Check adapted definitions against the pinned Lean toolchain run: | - lake env lean scripts/ExportUpstream.lean > .lake/upstream-current.json - python3 scripts/upstream.py check --metadata .lake/upstream-current.json \ + lake env lean .github/upstream/Export.lean > .lake/upstream-current.json + python3 .github/upstream/check.py check --metadata .lake/upstream-current.json \ --report .lake/upstream-report.md - name: Show upstream changes diff --git a/.github/workflows/upstream-core.yml b/.github/workflows/upstream-core.yml index cd73066..bb53757 100644 --- a/.github/workflows/upstream-core.yml +++ b/.github/workflows/upstream-core.yml @@ -28,14 +28,14 @@ jobs: - name: Compare tracked definitions with Lean's development branch run: | - python3 scripts/upstream.py check --target HEAD --advisory \ - --report upstream-report.md --json-report upstream-report.json - cat upstream-report.md >> "$GITHUB_STEP_SUMMARY" + python3 .github/upstream/check.py check --target HEAD --advisory \ + --report .lake/upstream-report.md --json-report .lake/upstream-report.json + cat .lake/upstream-report.md >> "$GITHUB_STEP_SUMMARY" - name: Maintain one issue for changes needing review uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8 with: script: | const fs = require('fs'); - const report = JSON.parse(fs.readFileSync('upstream-report.json', 'utf8')); - await require('./scripts/upstream-issue.cjs')({ github, context }, report); + const report = JSON.parse(fs.readFileSync('.lake/upstream-report.json', 'utf8')); + await require('./.github/upstream/notify.cjs')({ github, context }, report); diff --git a/README.md b/README.md index e1d3acb..5ba5618 100644 --- a/README.md +++ b/README.md @@ -1,4 +1 @@ -# Random-do notation - -See [Tracking Lean core analogues](docs/upstream-tracking.md) for `analogue` annotations, -change reports, and the review workflow. +# Random-do notation \ No newline at end of file diff --git a/RandomDo/Util/Analogue.lean b/RandomDo/Util/Analogue.lean index e9ff98b..74e6bae 100644 --- a/RandomDo/Util/Analogue.lean +++ b/RandomDo/Util/Analogue.lean @@ -5,15 +5,13 @@ Authors: David Ledvinka -/ module -public meta import Lean.Elab.Command +public meta import Lean.Attributes /-! -# Tracking adaptations of Lean core +# Analogous declarations -`@[analogue decl₁ decl₂]` records the Lean core declarations from which a declaration was adapted. -It checks that the names exist and stores them as metadata, without changing the declaration or -its docstring. `scripts/ExportUpstream.lean` exports this metadata for the upstream change checker. -See `docs/upstream-tracking.md` for the review and baseline update workflow. +`@[analogue f g]` records declarations that a local declaration adapts. +The names are resolved when the attribute is applied and stored as metadata. -/ public meta section @@ -22,25 +20,14 @@ namespace RandomDo.Analogue open Lean -/-- Mark a declaration as an adaptation of one or more declarations in Lean core. -/ +/-- Record declarations that a local declaration adapts. -/ syntax (name := analogue) "analogue " ident+ : attr -/-- The upstream declarations associated with each adapted declaration. -/ +/-- The declarations associated with each analogue. -/ initialize analogueAttr : ParametricAttribute (Array Name) ← registerParametricAttribute { name := `analogue - descr := "Record the Lean core declarations from which this declaration was adapted." - getParam := fun _ stx => do - let names ← stx[1].getArgs.mapM resolveGlobalConstNoOverload - let env ← getEnv - for name in names do - let some idx := env.getModuleIdxFor? name - | throwErrorAt stx "Analogue declaration `{name}` must be imported from Lean core" - let mod := env.header.moduleNames[idx.toNat]! - unless [`Init, `Lean, `Std].any (·.isPrefixOf mod) do - throwErrorAt stx "Analogue declaration `{name}` belongs to `{mod}`, not Lean core" - unless names.toList.eraseDups.length == names.size do - throwErrorAt stx "Duplicate analogue declarations" - return names + descr := "Record declarations that this declaration adapts." + getParam := fun _ stx => stx[1].getArgs.mapM resolveGlobalConstNoOverload } end RandomDo.Analogue