@@ -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
 
@@ -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
 ```
@@ -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+))? @@")
 
 
@@ -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
@@ -10,17 +10,17 @@
 import unittest
 
 sys.path.insert(0, str(Path(__file__).resolve().parents[1]))
-import upstream
+import check as checker
 
 
 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")
+        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,79 +94,79 @@ 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):
         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)
+                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)
                 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")
+        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)
 
 
@@ -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,
 
@@ -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
 
@@ -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);