@@ -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: |
 
@@ -38,36 +38,4 @@ jobs:
           script: |
             const fs = require('fs');
             const report = JSON.parse(fs.readFileSync('upstream-report.json', 'utf8'));
-            const marker = '<!-- randomdo-upstream-core-watch -->';
-            const digest = `<!-- upstream-fingerprint:${report.fingerprint} -->`;
-            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);
@@ -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.
@@ -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
@@ -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
 
@@ -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,27 +69,27 @@ 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?
 
 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
 
@@ -10,37 +10,37 @@ 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.
 -/
 
 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