diff --git a/.github/upstream/Export.lean b/.github/upstream/Export.lean new file mode 100644 index 0000000..92f838e --- /dev/null +++ b/.github/upstream/Export.lean @@ -0,0 +1,44 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +import RandomDo.Monad.Notation +import Lean.DeclarationRange +import Lean.Data.Json + +/-! +Run `lake env lean .github/upstream/Export.lean > .lake/upstream-current.json` after building the +tracked modules. Source ranges come from the running toolchain's declaration metadata, including +class fields and definition bodies. They are meaningful only at the accompanying Lean commit. +-/ + +open Lean RandomDo.Analogue + +run_cmd do + let env ← getEnv + let mut entries : Array Json := #[] + for (decl, _) in env.constants do + if let some sources := analogueAttr.getParam? env decl then + let some localIdx := env.getModuleIdxFor? decl + | throwError "No module for tracked declaration `{decl}`" + let localModule := env.header.moduleNames[localIdx.toNat]! + for source in sources do + let some idx := env.getModuleIdxFor? source + | throwError "No module for upstream declaration `{source}`" + let mod := env.header.moduleNames[idx.toNat]! + unless [`Init, `Lean, `Std].any (·.isPrefixOf mod) do + throwError "Analogue declaration `{source}` belongs to `{mod}`, not Lean core" + let some ranges ← findDeclarationRanges? source + | throwError "No source range for upstream declaration `{source}`" + let first := ranges.range.pos.line + let last := ranges.range.endPos.line - if ranges.range.endPos.column == 0 then 1 else 0 + entries := entries.push <| Json.mkObj [ + ("local", toJson decl.toString), + ("local_file", toJson (localModule.toString.replace "." "/" ++ ".lean")), + ("upstream", toJson source.toString), + ("path", toJson ("src/" ++ mod.toString.replace "." "/" ++ ".lean")), + ("start", toJson first), ("end", toJson last)] + let result := Json.mkObj [ + ("schema", toJson (1 : Nat)), ("commit", toJson Lean.githash), ("entries", toJson entries)] + IO.println result.compress diff --git a/.github/upstream/README.md b/.github/upstream/README.md new file mode 100644 index 0000000..908ae74 --- /dev/null +++ b/.github/upstream/README.md @@ -0,0 +1,89 @@ +# Lean core tracking + +This directory contains maintainer tooling run by GitHub Actions. The library provides only the +`analogue` attribute and its annotations; checking, baseline updates, and issue reporting live here. +All commands below run from the repository root. + +Use `@[analogue Core.declaration]` to link an adaptation to its Lean core counterpart: + +```lean +@[analogue Bind] +class MeasurableSpaceBind ... + +@[analogue Lean.Elab.Do.DoOps.default] +def randOps ... +``` + +Multiple names use spaces: `@[analogue Pure Bind]`. Qualify names when necessary; +`_root_.bind_congr`, for example, avoids resolving to the declaration being annotated. +The attribute resolves and records names. It is defined in `RandomDo/Util/Analogue.lean` and has +no dependency on this tooling. The exporter restricts this workflow's tracked origins to Lean core. + +## Checking for changes + +The initial scope is `RandomDo/Monad/MeasurableSpace.lean` and `RandomDo/Monad/Notation.lean`. +To check the current toolchain against the recorded baselines: + +```sh +lake build --wfail RandomDo.Monad.MeasurableSpace RandomDo.Monad.Notation +lake env lean .github/upstream/Export.lean > .lake/upstream-current.json +python3 .github/upstream/check.py check --metadata .lake/upstream-current.json +``` + +The build workflow runs this check on PRs. The exporter gets declaration locations from Lean; +`.github/upstream/baseline.json` stores the source path, line range, and exact Lean commit for each +mapping. +The Python script uses Git to compare those upstream regions with the target revision. It +requires Python 3.10+ and Git, with no Python packages. Later line insertions do not shift the +baseline because its range always refers to its recorded commit. + +The weekly workflow compares against Lean's default development branch every Monday at 08:23 UTC. +It maintains one issue listing affected declarations and linking to the full diff report. +Unchanged relevant edits do not cause repeated updates. It closes the issue when differences +are resolved; a failed check fails the workflow and leaves the issue alone. The schedule starts +after merge to the default branch and can also be run manually. + +To run the same comparison locally: + +```sh +python3 .github/upstream/check.py check --target HEAD --report .lake/upstream-report.md +``` + +Sources are fetched into `.lake/upstream-lean.git`; no future Lean code is built or executed. +Use `--repo /path/to/lean4` before the subcommand to use a local Git repository without fetching. +Exit codes are 0 for unchanged, 1 for changes, and 2 for errors. `--advisory` allows changes while +still failing on errors; it is used by the weekly workflow. + +## Updating a baseline + +Review the upstream diff, adapt the local code as needed, and explain intentional differences +in the PR. Then record just the declarations you reviewed: + +```sh +python3 .github/upstream/check.py record --metadata .lake/upstream-current.json --only RDo.randOps +``` + +Commit the generated baseline change with the adaptation. Other declarations retain their +baselines. For a rename, pass both old and new names to `--only`; for a removed annotation, +pass its old name. `--all` explicitly records every mapping. Checks never advance baselines. +To track another module, import it in `.github/upstream/Export.lean`, export, and record its mappings. + +## Scope + +The initial Lean v4.35.0 baseline starts monitoring the existing adaptations; it is not a +correctness audit. Known differences include the omitted dead-syntax guard in the +`mkPureApp` override in `RDo.randOps`, the loop adapters' missing `invariant` / `decreasing` syntax and +verification hooks, and the measurable hierarchy's intentional omission of applicative classes. + +The checker reports edits within a declaration, including its body, and conservatively includes +insertions and replacements at either boundary. Renames and file moves are reported at the old +location. Changes to untracked helpers or surrounding sections can also affect behavior, so normal +elaboration and behavior tests remain necessary. + +The checker, attribute, and issue tests run offline: + +```sh +python3 -m unittest discover -s .github/upstream/tests -p 'test_check.py' +lake env lean .github/upstream/tests/Analogue.lean +node --test .github/upstream/tests/test_notify.cjs +``` diff --git a/.github/upstream/baseline.json b/.github/upstream/baseline.json new file mode 100644 index 0000000..228a91b --- /dev/null +++ b/.github/upstream/baseline.json @@ -0,0 +1,231 @@ +{ + "schema": 1, + "repository": "https://github.com/leanprover/lean4", + "entries": [ + { + "end": 41, + "local": "LawfulMeasurableSpaceFunctor", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 20, + "upstream": "LawfulFunctor", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 159, + "local": "LawfulMeasurableSpaceMonad", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 125, + "upstream": "LawfulMonad", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 3881, + "local": "MeasurableSpaceBind", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Prelude.lean", + "start": 3869, + "upstream": "Bind", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 180, + "local": "MeasurableSpaceBind.bind_congr", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 179, + "upstream": "bind_congr", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 388, + "local": "MeasurableSpaceForIn", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Core.lean", + "start": 366, + "upstream": "ForIn", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 416, + "local": "MeasurableSpaceForIn'", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Core.lean", + "start": 392, + "upstream": "ForIn'", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 3937, + "local": "MeasurableSpaceFunctor", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Prelude.lean", + "start": 3903, + "upstream": "Functor", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 186, + "local": "MeasurableSpaceFunctor.map_congr", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 185, + "upstream": "map_congr", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 4038, + "local": "MeasurableSpaceMonad", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Prelude.lean", + "start": 4020, + "upstream": "Monad", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 3899, + "local": "MeasurableSpacePure", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Prelude.lean", + "start": 3885, + "upstream": "Pure", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 409, + "local": "RDo.elabRDoFor", + "local_file": "RandomDo/Monad/Notation.lean", + "path": "src/Lean/Elab/BuiltinDo/For.lean", + "start": 274, + "upstream": "Lean.Elab.Do.elabDoFor", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 1104, + "local": "RDo.elabRand", + "local_file": "RandomDo/Monad/Notation.lean", + "path": "src/Lean/Elab/Do/Basic.lean", + "start": 1102, + "upstream": "Lean.Elab.Do.elabDo", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 87, + "local": "RDo.expandRDoFor", + "local_file": "RandomDo/Monad/Notation.lean", + "path": "src/Lean/Elab/BuiltinDo/For.lean", + "start": 24, + "upstream": "Lean.Elab.Do.expandDoFor", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 339, + "local": "RDo.randOps", + "local_file": "RandomDo/Monad/Notation.lean", + "path": "src/Lean/Elab/Do/Basic.lean", + "start": 309, + "upstream": "Lean.Elab.Do.DoOps.default", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 217, + "local": "RDo.rdoFor", + "local_file": "RandomDo/Monad/Notation.lean", + "path": "src/Lean/Parser/Do.lean", + "start": 208, + "upstream": "Lean.Parser.Term.doFor", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 186, + "local": "RDo.rdoForDecl", + "local_file": "RandomDo/Monad/Notation.lean", + "path": "src/Lean/Parser/Do.lean", + "start": 184, + "upstream": "Lean.Parser.Term.doForDecl", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 48, + "local": "id_mMap'", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 47, + "upstream": "id_map'", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 30, + "local": "instMeasurableSpaceForInOfForIn'", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Basic.lean", + "start": 16, + "upstream": "instForInOfForIn'", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 208, + "local": "mBind_mMap_left", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 205, + "upstream": "bind_map_left", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 167, + "local": "mBind_mPure", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 165, + "upstream": "bind_pure", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 183, + "local": "mBind_mPure_unit", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 182, + "upstream": "bind_pure_unit", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 174, + "local": "mMap_eq_mPure_mBind", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 169, + "upstream": "map_eq_pure_bind", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 203, + "local": "mMap_mBind", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 200, + "upstream": "map_bind", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 52, + "local": "mMap_mMap", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 50, + "upstream": "Functor.map_map", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + }, + { + "end": 85, + "local": "mMap_mPure", + "local_file": "RandomDo/Monad/MeasurableSpace.lean", + "path": "src/Init/Control/Lawful/Basic.lean", + "start": 85, + "upstream": "LawfulApplicative.map_pure", + "commit": "eb6cafb7290e8bd5f2937522d8d804f58f02bafc" + } + ] +} diff --git a/.github/upstream/check.py b/.github/upstream/check.py new file mode 100644 index 0000000..841b28d --- /dev/null +++ b/.github/upstream/check.py @@ -0,0 +1,276 @@ +#!/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 functools import cache +from pathlib import Path, PurePosixPath + +ROOT = Path(__file__).resolve().parents[2] +REPOSITORY = "https://github.com/leanprover/lean4" +BASELINE = Path(__file__).with_name("baseline.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], + 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 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}") + + +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] = {} + + def resolve(self, ref: str) -> str: + 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. + 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] + + @cache + def read(self, commit: str, path: str) -> str: + return git(self.repo, "show", f"{commit}:{path}") + + @cache + def diff(self, before: str, after: str, path: str) -> str: + # 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(encoding="utf-8")) + 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 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}") + 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 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}") + + +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 + + +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"]) + 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) -> dict: + current = entries(metadata, baseline=False) + old = entries(baseline, baseline=True) if baseline is not None else {} + 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)}") + # 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: + validate_range(source, commit, entry) + result[key] = {**entry, "commit": commit} + 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 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}).", "", + "````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=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") + 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") + 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.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: + 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, 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", 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) + return 2 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/.github/upstream/notify.cjs b/.github/upstream/notify.cjs new file mode 100644 index 0000000..24260c4 --- /dev/null +++ b/.github/upstream/notify.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/.github/upstream/tests/Analogue.lean b/.github/upstream/tests/Analogue.lean new file mode 100644 index 0000000..0a74403 --- /dev/null +++ b/.github/upstream/tests/Analogue.lean @@ -0,0 +1,31 @@ +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 + +-- The attribute records relationships; the CI exporter enforces its Lean core scope. +@[analogue MeasurableSpaceMonad] +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/.github/upstream/tests/test_check.py b/.github/upstream/tests/test_check.py new file mode 100644 index 0000000..aa43b22 --- /dev/null +++ b/.github/upstream/tests/test_check.py @@ -0,0 +1,202 @@ +"""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 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) + 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 = ( + "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 = checker.record(None, self.metadata, self.source(), None) + + def source(self): + return checker.Source(self.repo) + + def commit(self): + 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 checker.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_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"]) + 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_nonexistent_source_is_an_error(self): + self.baseline["entries"][0]["path"] = "src/Missing.lean" + with self.assertRaises(checker.CheckError): + self.report(self.before) + + def test_missing_revision_is_an_error(self): + 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(checker.CheckError): + checker.check(baseline, self.source(), self.before) + baseline = copy.deepcopy(self.baseline) + baseline["entries"].append(baseline["entries"][0]) + with self.assertRaisesRegex(checker.CheckError, "Duplicate"): + checker.entries(baseline, baseline=True) + + def test_new_removed_and_moved_annotations_require_review(self): + 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(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(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(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 = checker.record(None, metadata, self.source(), None) + metadata["commit"] = self.change(self.original.replace("x + 1", "x + 2")) + 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 = 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 = 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 = 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): + 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"]) + + 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(checker.main(args), 1) + self.assertEqual(checker.main(args + ["--advisory"]), 0) + with contextlib.redirect_stderr(io.StringIO()): + self.assertEqual(checker.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_and_upstream_diff(self): + report = self.report(self.change(self.original.replace("x + 1", "x + 2"))) + text = checker.markdown(report) + for expected in ["Adapted.foo", "Example.foo", "- x + 1", "+ x + 2"]: + self.assertIn(expected, text) + + +if __name__ == "__main__": + unittest.main() diff --git a/.github/upstream/tests/test_notify.cjs b/.github/upstream/tests/test_notify.cjs new file mode 100644 index 0000000..1a7ab27 --- /dev/null +++ b/.github/upstream/tests/test_notify.cjs @@ -0,0 +1,71 @@ +const assert = require('node:assert/strict'); +const { test } = require('node:test'); +const updateIssue = require('../notify.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/.github/workflows/build.yml b/.github/workflows/build.yml index 550a3a1..3f1fe70 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -54,3 +54,22 @@ jobs: build-args: "--wfail" lint: true mk_all-check: true + + - name: Test upstream tracking + run: | + 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 .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 + 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..bb53757 --- /dev/null +++ b/.github/workflows/upstream-core.yml @@ -0,0 +1,41 @@ +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 .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('.lake/upstream-report.json', 'utf8')); + await require('./.github/upstream/notify.cjs')({ github, context }, report); diff --git a/RandomDo.lean b/RandomDo.lean index b2d4043..0f82f0f 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.Analogue diff --git a/RandomDo/Monad/MeasurableSpace.lean b/RandomDo/Monad/MeasurableSpace.lean index b593969..37ce9b6 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.Analogue /-! # 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. -/ +@[analogue 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. -/ +@[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 -/ @@ -74,6 +77,7 @@ The `>>=ₘ` operator is overloaded via instances of `MeasurableSpaceBind`. `MeasurableSpaceBind` is typically used via `MeasurableSpaceMonad`, which extends it. -/ +@[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. @@ -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 -/ +@[analogue 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 β] +@[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] +@[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] @@ -110,6 +117,7 @@ section Lawful open MeasurableSpaceFunctor /-- A `MeasurableSpaceFunctor` satisfies the measurable space functor laws. -/ +@[analogue 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 +@[analogue id_map', simp] +theorem id_mMap' (x : f α) : (fun a => a) <$>ₘ x = x := id_mMap x -@[simp] theorem mMap_mMap {g₀ : α → β} {g₁ : β → γ} (x : f α) +@[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 := (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. -/ +@[analogue 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 : α) : +@[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)] -@[simp] theorem mBind_mPure (x : m α) : x >>=ₘ mPure = x := by +@[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] +@[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] +@[analogue 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 α) +@[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] -@[simp] theorem mBind_mMap_left {f : α → β} (hf : Measurable f) (x : m α) +@[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 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. -/ +@[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 @@ -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. -/ +@[analogue 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] +@[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 2d2542b..0d21e32 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. -/ +@[analogue 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 +@[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 -/ +@[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 -/ -@[doElem_parser] def rdoFor := leading_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. -/ -@[macro rdoFor] def expandRDoFor : Macro := fun stx => do +@[analogue 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 +@[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 checkMutVarsForShadowing #[x] diff --git a/RandomDo/Util/Analogue.lean b/RandomDo/Util/Analogue.lean new file mode 100644 index 0000000..74e6bae --- /dev/null +++ b/RandomDo/Util/Analogue.lean @@ -0,0 +1,33 @@ +/- +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.Attributes + +/-! +# Analogous declarations + +`@[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 + +namespace RandomDo.Analogue + +open Lean + +/-- Record declarations that a local declaration adapts. -/ +syntax (name := analogue) "analogue " ident+ : attr + +/-- The declarations associated with each analogue. -/ +initialize analogueAttr : ParametricAttribute (Array Name) ← registerParametricAttribute { + name := `analogue + descr := "Record declarations that this declaration adapts." + getParam := fun _ stx => stx[1].getArgs.mapM resolveGlobalConstNoOverload +} + +end RandomDo.Analogue