Skip to content

Commit 9005c79

Browse files
author
David Ledvinka
committed
Check adapted core declarations in CI and report upstream changes weekly
1 parent 611ec4c commit 9005c79

7 files changed

Lines changed: 974 additions & 1 deletion

File tree

‎.github/workflows/build.yml‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,3 +54,21 @@ jobs:
5454
build-args: "--wfail"
5555
lint: true
5656
mk_all-check: true
57+
58+
- name: Test upstream tracking
59+
run: |
60+
python3 -m unittest discover -s scripts/tests -p 'test_upstream.py'
61+
lake env lean scripts/tests/Upstream.lean
62+
63+
- name: Check adapted definitions against the pinned Lean toolchain
64+
run: |
65+
lake env lean scripts/ExportUpstream.lean > .lake/upstream-current.json
66+
python3 scripts/upstream.py check --metadata .lake/upstream-current.json \
67+
--report .lake/upstream-report.md
68+
69+
- name: Show upstream changes
70+
if: always()
71+
run: |
72+
if [ -f .lake/upstream-report.md ]; then
73+
cat .lake/upstream-report.md >> "$GITHUB_STEP_SUMMARY"
74+
fi

‎.github/workflows/upstream-core.yml‎

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
name: Watch Lean core adaptations
2+
3+
on:
4+
schedule:
5+
- cron: '23 8 * * 1'
6+
workflow_dispatch:
7+
8+
permissions:
9+
contents: read
10+
11+
concurrency:
12+
group: upstream-core-watch
13+
cancel-in-progress: false
14+
15+
jobs:
16+
watch:
17+
runs-on: ubuntu-latest
18+
timeout-minutes: 15
19+
permissions:
20+
contents: read
21+
issues: write
22+
steps:
23+
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
24+
with:
25+
# Even a manual run reports only the reviewed default-branch configuration.
26+
ref: ${{ github.event.repository.default_branch }}
27+
persist-credentials: false
28+
29+
- name: Compare tracked definitions with Lean's development branch
30+
run: |
31+
python3 scripts/upstream.py check --target HEAD --advisory \
32+
--report upstream-report.md --json-report upstream-report.json
33+
cat upstream-report.md >> "$GITHUB_STEP_SUMMARY"
34+
35+
- name: Maintain one issue for changes needing review
36+
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
37+
with:
38+
script: |
39+
const fs = require('fs');
40+
const report = JSON.parse(fs.readFileSync('upstream-report.json', 'utf8'));
41+
const marker = '<!-- randomdo-upstream-core-watch -->';
42+
const digest = `<!-- upstream-fingerprint:${report.fingerprint} -->`;
43+
const issues = await github.paginate(github.rest.issues.listForRepo, {
44+
...context.repo, state: 'all', creator: 'github-actions[bot]', per_page: 100,
45+
});
46+
const issue = issues.find(i => !i.pull_request && i.body?.includes(marker));
47+
if (report.changes.length === 0) {
48+
if (issue?.state === 'open') {
49+
await github.rest.issues.update({
50+
...context.repo, issue_number: issue.number, state: 'closed',
51+
});
52+
}
53+
return;
54+
}
55+
if (issue?.state === 'open' && issue.body?.includes(digest)) return;
56+
const summary = fs.readFileSync('upstream-report.md', 'utf8');
57+
const run = `${context.serverUrl}/${context.repo.owner}/${context.repo.repo}/actions/runs/${context.runId}`;
58+
// Leave room below GitHub's issue-body limit, also for non-ASCII source text.
59+
let details = summary;
60+
if (Buffer.byteLength(details, 'utf8') > 55000) {
61+
details = Array.from(details).slice(0, 13000).join('')
62+
+ '\n\nReport truncated; see the workflow summary for the full diff.';
63+
}
64+
const body = `${marker}\n${digest}\n${details}\n\n[Workflow report](${run})`;
65+
if (issue) {
66+
await github.rest.issues.update({
67+
...context.repo, issue_number: issue.number, body, state: 'open',
68+
});
69+
} else {
70+
await github.rest.issues.create({
71+
...context.repo, title: 'Lean core changes affecting adapted definitions', body,
72+
});
73+
}

‎README.md‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,4 @@
1-
# Random-do notation
1+
# Random-do notation
2+
3+
See [Tracking adaptations of Lean core](docs/upstream-tracking.md) for upstream annotations,
4+
change reports, and the review workflow.

‎docs/upstream-tracking.md‎

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
# Tracking adaptations of Lean core
2+
3+
The initial scope is `RandomDo/Monad/MeasurableSpace.lean` and
4+
`RandomDo/Monad/Notation.lean`. The annotations identify adaptations, not literal copies or
5+
claims of semantic equivalence. They do not change the definitions or their docstrings.
6+
7+
```lean
8+
@[upstream Bind]
9+
class MeasurableSpaceBind ...
10+
11+
@[upstream Lean.Elab.Do.DoOps.default]
12+
def randOps ...
13+
```
14+
15+
Multiple origins use spaces: `@[upstream Pure Bind]`. Use fully qualified names when needed;
16+
for example, `_root_.bind_congr` avoids resolving to the declaration being annotated.
17+
The attribute rejects unknown names, duplicate origins, and declarations outside Lean core.
18+
It is implemented in `RandomDo/Util/Upstream.lean`. To extend tracking to another module,
19+
import that module in `scripts/ExportUpstream.lean` and record its annotated declarations.
20+
21+
## Checking an upgrade
22+
23+
Build the tracked modules, export their annotations, and compare against the running toolchain:
24+
25+
```sh
26+
lake build --wfail RandomDo.Monad.MeasurableSpace RandomDo.Monad.Notation
27+
lake env lean scripts/ExportUpstream.lean > .lake/upstream-current.json
28+
python3 scripts/upstream.py check --metadata .lake/upstream-current.json
29+
```
30+
31+
The build workflow runs this check on PRs, along with the attribute and checker tests.
32+
New or removed annotations require an explicit baseline update. An upstream name that disappears
33+
will also fail to resolve when building against the new toolchain.
34+
35+
`upstream.json` records, for each local/upstream pair, an immutable Lean commit, the upstream source
36+
path and range, a hash of that source, and a review note. The exporter obtains ranges from Lean's
37+
declaration metadata, including class fields, documentation, and definition bodies. A range is
38+
used only with the exact commit at which it was recorded: later line insertions do not invalidate
39+
it. The checker compares old upstream source with new upstream source, not with the intentionally
40+
different RandomDo implementation. It needs Git and Python 3.10 or later, with no Python packages.
41+
42+
## Reviewing and recording a change
43+
44+
Read the report's upstream diff alongside the corresponding RandomDo declaration. Port relevant
45+
changes or explain why they do not apply. Then record only the declarations reviewed in this PR:
46+
47+
```sh
48+
python3 scripts/upstream.py record --metadata .lake/upstream-current.json \
49+
--only RDo.randOps --note 'Ported the core change; measurable-space arguments remain explicit.'
50+
```
51+
52+
Each selected declaration's origins receive the current toolchain commit and source range.
53+
Other declarations keep their existing baselines. Commit the baseline update with the adaptation
54+
or explanation, so reviewers can see both. `--all` explicitly records every exported annotation
55+
and removes obsolete mappings; use it only when all affected entries have been reviewed.
56+
For a local rename, `--all` also reconciles the old and new identities; unchanged upstream entries
57+
still need accurate review notes. The checker never advances baselines automatically.
58+
59+
The initial baseline is Lean v4.35.0. It records the existing adaptations as the starting point for
60+
monitoring, not a completed correctness audit. In particular:
61+
62+
- `RDo.randOps` supplies measurable-space arguments and currently omits core's dead-syntax guard
63+
in `mkPureApp`. This is a known difference to investigate separately.
64+
- The loop parsers, expander and elaborator retain the existing `rdo` adaptations; they do not
65+
implement core's `invariant` / `decreasing` annotations or its verification-condition hooks.
66+
- The class hierarchy and laws have measurable-space parameters and measurability hypotheses,
67+
and omit the applicative layer. These differences are intentional.
68+
69+
## Watching future core changes
70+
71+
The `Watch Lean core adaptations` workflow checks upstream's default development branch each
72+
Monday at 08:23 UTC and can also be run manually. Scheduled workflows become active once merged
73+
to the repository's default branch. It reads upstream source only; it does not build or execute
74+
future core code or change the project's toolchain.
75+
76+
When a tracked region changes, the workflow opens or updates one GitHub issue with the affected
77+
local declarations, review notes, source links, and upstream diffs. Unchanged relevant edits do
78+
not cause repeated updates when unrelated commits land in core. The issue is closed when no
79+
tracked differences remain. Fetch, metadata, and other check failures fail the workflow and do
80+
not close an existing issue. The watcher has read-only contents access and permission to maintain its issue.
81+
The PR checks add no token permissions to the existing build workflow. No baseline updates or code changes are made by the watcher.
82+
83+
Run the same comparison locally:
84+
85+
```sh
86+
python3 scripts/upstream.py check --target HEAD --report .lake/upstream-report.md
87+
```
88+
89+
Without `--repo`, the checker fetches from `leanprover/lean4` into `.lake/upstream-lean.git`.
90+
Use `--repo /path/to/lean4` before `check` or `record` to use an existing Git repository without
91+
fetching. Exit statuses are 0 for unchanged, 1 for changes needing review, and 2 for an incomplete
92+
or invalid check. `--advisory` changes status 1 to 0; errors still fail.
93+
94+
## Coverage and tests
95+
96+
Moved or deleted files and renamed declarations are reported through changes at their recorded
97+
locations. Insertions immediately at either boundary are conservatively flagged because they
98+
can extend a declaration. Unrelated changes elsewhere in the same file are ignored.
99+
This is source-change detection: changes to untracked helpers or surrounding module/section
100+
context can also affect behavior. It does not prove that an adaptation remains correct. Keep the project's behavior and elaboration tests.
101+
102+
```sh
103+
python3 -m unittest discover -s scripts/tests -p 'test_upstream.py'
104+
lake env lean scripts/tests/Upstream.lean
105+
```
106+
107+
The Python tests construct local Git histories and require no network. They cover source/body
108+
changes, boundary insertions, unrelated edits, moves/deletions, malformed or missing data,
109+
partial review, exit statuses, baseline preservation, and notification deduplication.

‎scripts/tests/test_upstream.py‎

Lines changed: 171 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,171 @@
1+
"""Exercise the checker against real, temporary Git histories; no network access."""
2+
3+
import contextlib
4+
import copy
5+
import io
6+
import json
7+
from pathlib import Path
8+
import sys
9+
import tempfile
10+
import unittest
11+
12+
sys.path.insert(0, str(Path(__file__).resolve().parents[1]))
13+
import upstream
14+
15+
16+
class UpstreamTest(unittest.TestCase):
17+
def setUp(self):
18+
self.temp = tempfile.TemporaryDirectory()
19+
self.addCleanup(self.temp.cleanup)
20+
self.repo = Path(self.temp.name)
21+
upstream.git(self.repo, "init", "--quiet")
22+
upstream.git(self.repo, "config", "user.email", "test@example.invalid")
23+
upstream.git(self.repo, "config", "user.name", "Upstream tests")
24+
self.path = self.repo / "src" / "Example.lean"
25+
self.path.parent.mkdir()
26+
self.original = (
27+
"namespace Example\n\n"
28+
"def foo (x : Nat) : Nat :=\n"
29+
" x + 1\n\n"
30+
"def other : Nat := 10\n\n"
31+
"end Example\n"
32+
)
33+
self.path.write_text(self.original)
34+
self.before = self.commit()
35+
self.metadata = {"schema": 1, "commit": self.before, "entries": [{
36+
"local": "Adapted.foo", "local_file": "RandomDo/Example.lean",
37+
"upstream": "Example.foo", "path": "src/Example.lean", "start": 3, "end": 4,
38+
}]}
39+
self.baseline = upstream.record(None, self.metadata, self.source(), None, "Adapted to m")
40+
41+
def source(self):
42+
return upstream.Source(self.repo)
43+
44+
def commit(self):
45+
upstream.git(self.repo, "add", ".")
46+
upstream.git(self.repo, "commit", "--quiet", "--no-gpg-sign", "-m", "fixture")
47+
return upstream.git(self.repo, "rev-parse", "HEAD").strip()
48+
49+
def change(self, text):
50+
self.path.write_text(text)
51+
return self.commit()
52+
53+
def report(self, target):
54+
return upstream.check(self.baseline, self.source(), target)
55+
56+
def test_unchanged_and_unrelated_edits(self):
57+
self.assertEqual(self.report(self.before)["changes"], [])
58+
target = self.change(self.original.replace("10", "20"))
59+
self.assertEqual(self.report(target)["changes"], [])
60+
61+
def test_unrelated_line_insertion_does_not_shift_the_baseline(self):
62+
target = self.change("-- new module comment\n" + self.original)
63+
self.assertEqual(self.report(target)["changes"], [])
64+
65+
def test_statement_and_body_changes(self):
66+
for old, new in [("x : Nat", "x : Int"), ("x + 1", "x + 2")]:
67+
with self.subTest(new=new):
68+
target = self.change(self.original.replace(old, new))
69+
report = self.report(target)
70+
self.assertEqual(len(report["changes"]), 1)
71+
self.assertIn(new, report["changes"][0]["diff"])
72+
73+
def test_insertions_at_both_boundaries_are_conservatively_reported(self):
74+
for text in [self.original.replace("def foo", "@[inline]\ndef foo"),
75+
self.original.replace(" x + 1\n", " x + 1\n + 2\n")]:
76+
with self.subTest(text=text):
77+
self.assertEqual(len(self.report(self.change(text))["changes"]), 1)
78+
79+
def test_deleted_declaration_and_renamed_declaration(self):
80+
target = self.change(self.original.replace("def foo (x : Nat) : Nat :=\n x + 1\n", ""))
81+
self.assertTrue(self.report(target)["changes"])
82+
target = self.change(self.original.replace("def foo", "def renamed"))
83+
self.assertTrue(self.report(target)["changes"])
84+
85+
def test_deleted_or_moved_file_is_reported(self):
86+
self.path.rename(self.path.with_name("Moved.lean"))
87+
self.assertTrue(self.report(self.commit())["changes"])
88+
89+
def test_corrupted_baseline_is_an_error(self):
90+
self.baseline["entries"][0]["sha256"] = "0" * 64
91+
with self.assertRaisesRegex(upstream.CheckError, "hash mismatch"):
92+
self.report(self.before)
93+
94+
def test_missing_revision_is_an_error(self):
95+
with self.assertRaises(upstream.CheckError):
96+
self.report("no-such-revision")
97+
98+
def test_source_range_and_identity_are_validated(self):
99+
for key, value in [("start", 0), ("end", -1), ("path", "../outside.lean")]:
100+
baseline = copy.deepcopy(self.baseline)
101+
baseline["entries"][0][key] = value
102+
with self.subTest(key=key), self.assertRaises(upstream.CheckError):
103+
upstream.check(baseline, self.source(), self.before)
104+
baseline = copy.deepcopy(self.baseline)
105+
baseline["entries"].append(baseline["entries"][0])
106+
with self.assertRaisesRegex(upstream.CheckError, "Duplicate"):
107+
upstream.entries(baseline, baseline=True)
108+
109+
def test_new_removed_and_moved_annotations_require_review(self):
110+
upstream.validate_mappings(self.baseline, self.metadata)
111+
for key, value in [("local", "Adapted.new"), ("upstream", "Example.new"),
112+
("local_file", "RandomDo/New.lean")]:
113+
metadata = copy.deepcopy(self.metadata)
114+
metadata["entries"][0][key] = value
115+
with self.subTest(key=key), self.assertRaises(upstream.CheckError):
116+
upstream.validate_mappings(self.baseline, metadata)
117+
118+
def test_range_must_match_exported_metadata_at_the_same_commit(self):
119+
baseline = copy.deepcopy(self.baseline)
120+
baseline["entries"][0]["start"] = 4
121+
with self.assertRaisesRegex(upstream.CheckError, "range disagrees"):
122+
upstream.validate_mappings(baseline, self.metadata)
123+
124+
def test_invalid_commit_types_are_check_errors(self):
125+
for field in ("commit", "sha256"):
126+
baseline = copy.deepcopy(self.baseline)
127+
baseline["entries"][0][field] = None
128+
with self.subTest(field=field), self.assertRaises(upstream.CheckError):
129+
upstream.entries(baseline, baseline=True)
130+
131+
def test_partial_review_preserves_other_baselines(self):
132+
metadata = copy.deepcopy(self.metadata)
133+
metadata["entries"].append({**metadata["entries"][0], "local": "Adapted.second"})
134+
baseline = upstream.record(None, metadata, self.source(), None, "Initial review")
135+
metadata["commit"] = self.change(self.original.replace("x + 1", "x + 2"))
136+
reviewed = upstream.record(baseline, metadata, self.source(), ["Adapted.foo"], "Ported fix")
137+
by_name = {e["local"]: e for e in reviewed["entries"]}
138+
self.assertEqual(by_name["Adapted.foo"]["commit"], metadata["commit"])
139+
self.assertEqual(by_name["Adapted.second"]["commit"], self.before)
140+
report = upstream.check(reviewed, self.source(), metadata["commit"])
141+
self.assertEqual([c["local"] for c in report["changes"]], ["Adapted.second"])
142+
143+
def test_no_automatic_baseline_update_and_exit_codes(self):
144+
lock = self.repo / "baseline.json"
145+
lock.write_text(json.dumps(self.baseline))
146+
original = lock.read_bytes()
147+
target = self.change(self.original.replace("x + 1", "x + 2"))
148+
args = ["--baseline", str(lock), "--repo", str(self.repo), "check", "--target", target]
149+
with contextlib.redirect_stdout(io.StringIO()):
150+
self.assertEqual(upstream.main(args), 1)
151+
self.assertEqual(upstream.main(args + ["--advisory"]), 0)
152+
with contextlib.redirect_stderr(io.StringIO()):
153+
self.assertEqual(upstream.main(args[:-1] + ["missing"] + ["--advisory"]), 2)
154+
self.assertEqual(lock.read_bytes(), original)
155+
156+
def test_notification_fingerprint_ignores_unrelated_commits(self):
157+
changed = self.original.replace("x + 1", "x + 2")
158+
first = self.report(self.change(changed))
159+
second = self.report(self.change("-- unrelated\n" + changed))
160+
self.assertNotEqual(first["target"], second["target"])
161+
self.assertEqual(first["fingerprint"], second["fingerprint"])
162+
163+
def test_report_includes_mapping_review_note_and_upstream_diff(self):
164+
report = self.report(self.change(self.original.replace("x + 1", "x + 2")))
165+
text = upstream.markdown(report)
166+
for expected in ["Adapted.foo", "Example.foo", "Adapted to m", "- x + 1", "+ x + 2"]:
167+
self.assertIn(expected, text)
168+
169+
170+
if __name__ == "__main__":
171+
unittest.main()

0 commit comments

Comments
 (0)