From cfcf26753fe7edee1824c9c69fa00113f64301b9 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 23 Apr 2026 17:26:15 -0700 Subject: [PATCH 01/22] First cut --- Tools/PurityCheck.lean | 167 +++++++++++++++++++++++++++++++++++++++++ lakefile.toml | 4 + 2 files changed, 171 insertions(+) create mode 100644 Tools/PurityCheck.lean diff --git a/Tools/PurityCheck.lean b/Tools/PurityCheck.lean new file mode 100644 index 0000000000..344ae4451c --- /dev/null +++ b/Tools/PurityCheck.lean @@ -0,0 +1,167 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Lean.Parser +import Lean.Parser.Command +import Lean.Parser.Module +import Lean.Elab.Import + +/-! # Module Purity Checker + +Determines whether elaborating a Lean module could potentially perform I/O. + +Uses a conservative allowlist approach: commands whose elaboration is known to +be pure are on the allowlist; everything else is treated as potentially impure. + +## Usage + + lake exe purityCheck [--impure-only] [file2.lean ...] + +Prints each file with its purity status. With `--impure-only`, only prints +files that might perform I/O (useful for cache invalidation). +-/ + +open Lean Parser + +/-- Commands whose elaboration is known to be pure (no I/O side effects). -/ +private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ + -- Top-level declarations (elaborate types/terms but don't execute them) + ``Command.declaration, + ``Command.«deriving», + + -- Structural / scoping + ``Command.«section», + ``Command.«namespace», + ``Command.«end», + ``Command.«variable», + ``Command.«universe», + ``Command.«open», + ``Command.«export», + ``Command.«import», + ``Command.«mutual», + ``Command.«in», + ``Command.«include», + ``Command.«omit», + ``Command.withWeakNamespace, + ``Command.withExporting, + + -- Options and attributes (pure metadata) + ``Command.«set_option», + ``Command.«attribute», + + -- Inspection commands (pure — only print/check, no execution) + ``Command.check, + ``Command.check_failure, + ``Command.print, + ``Command.printSig, + ``Command.printAxioms, + ``Command.printEqns, + ``Command.printTacTags, + ``Command.«where», + ``Command.version, + ``Command.synth, + + -- Assertions about the environment (pure checks) + ``Command.assertNotExists, + ``Command.assertNotImported, + ``Command.checkAssertions, + + -- Documentation + ``Command.moduleDoc, + ``Command.addDocString, + + -- Misc pure commands + ``Command.«register_tactic_tag», + ``Command.«tactic_extension», + ``Command.«recommended_spelling», + ``Command.genInjectiveTheorems, + ``Command.registerErrorExplanationStx, + ``Command.«init_quot», + ``Command.exit, + ``Command.eoi +] + +/-- Command kind prefixes known to be pure (syntax/notation/macro definitions). -/ +private def pureCommandPrefixes : Array Name := #[ + `Lean.Parser.Command.syntax, + `Lean.Parser.Command.syntaxCat, + `Lean.Parser.Command.notation, + `Lean.Parser.Command.macro, + `Lean.Parser.Command.macro_rules, + `Lean.Parser.Command.elab, + `Lean.Parser.Command.elab_rules, + `Lean.Parser.Command.«scoped», + `Lean.Parser.Command.«local», + `Lean.Parser.Command.simproc, + `Lean.Parser.Command.builtin_simproc, + `Lean.Parser.Command.dsimproc, + `Lean.Parser.Command.builtin_dsimproc, + `Lean.Parser.Command.register_simp_attr, + `Lean.Parser.Command.register_option, + `Lean.Parser.Command.register_builtin_option, + `Lean.Parser.Command.register_label_attr, + `Lean.Parser.Command.«infix», + `Lean.Parser.Command.«infixl», + `Lean.Parser.Command.«infixr», + `Lean.Parser.Command.«prefix», + `Lean.Parser.Command.«postfix», + `Lean.Parser.Command.declare_syntax_cat, + `Lean.Parser.Command.declare_config_elab, + `Lean.Parser.Command.declare_command_config_elab, + `Lean.Parser.Command.declare_config_getter, + `Lean.Parser.Command.declare_simp_like_tactic, + `Lean.Parser.Command.declare_tagged_region +] + +/-- Check if a command syntax node kind is known to be pure. -/ +private def isPureCommand (kind : SyntaxNodeKind) : Bool := + pureCommandKinds.contains kind || + pureCommandPrefixes.any (fun pfx => pfx.isPrefixOf kind) || + kind == nullKind + +/-- Parse a .lean file and check all top-level commands for purity. +Returns the list of impure command kind names (empty = pure module). -/ +def checkFilePurity (contents : String) (fileName : String := "") : + IO (List (SyntaxNodeKind × String.Pos.Raw)) := do + let inputCtx := mkInputContext contents fileName + let (header, parserState, msgs) ← parseHeader inputCtx + let (env, _msgs) ← Elab.processHeader header {} msgs inputCtx + let pmctx : ParserModuleContext := { env, options := {} } + let mut reasons : List (SyntaxNodeKind × String.Pos.Raw) := [] + let mut mps := parserState + let mut messages := MessageLog.empty + let mut done := false + while !done do + let (cmd, mps', msgs') := parseCommand inputCtx pmctx mps messages + mps := mps' + messages := msgs' + if isTerminalCommand cmd then + done := true + else + let kind := cmd.getKind + if !isPureCommand kind then + reasons := (kind, cmd.getPos?.getD 0) :: reasons + return reasons.reverse + +def main (args : List String) : IO UInt32 := do + let impureOnly := args.contains "--impure-only" + let files := args.filter (fun a => !a.startsWith "--") + if files.isEmpty then + IO.eprintln "Usage: purityCheck [--impure-only] [file2.lean ...]" + return 1 + let mut exitCode : UInt32 := 0 + for file in files do + let contents ← IO.FS.readFile file + let reasons ← checkFilePurity contents file + if reasons.isEmpty then + unless impureOnly do + IO.println s!"PURE: {file}" + else + IO.println s!"IMPURE: {file}" + for (kind, pos) in reasons do + IO.println s!" - {kind} at byte {pos}" + exitCode := 1 + return exitCode diff --git a/lakefile.toml b/lakefile.toml index 3010e6ef3a..ec3229a9fb 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -40,3 +40,7 @@ root = "Scripts.ImportStats" [[lean_exe]] name = "DiffTestCore" + +[[lean_exe]] +name = "purityCheck" +root = "Tools.PurityCheck" From 42a6d5a8ae3bce72a24d692b186e049d1d4b831b Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 24 Apr 2026 08:37:14 -0700 Subject: [PATCH 02/22] Script --- Tools/PurityCheck.lean | 64 ++++++++++++++++++++++++++---- Tools/invalidate_impure_cache.sh | 67 ++++++++++++++++++++++++++++++++ 2 files changed, 124 insertions(+), 7 deletions(-) create mode 100755 Tools/invalidate_impure_cache.sh diff --git a/Tools/PurityCheck.lean b/Tools/PurityCheck.lean index 344ae4451c..2cc94eedae 100644 --- a/Tools/PurityCheck.lean +++ b/Tools/PurityCheck.lean @@ -87,6 +87,7 @@ private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ /-- Command kind prefixes known to be pure (syntax/notation/macro definitions). -/ private def pureCommandPrefixes : Array Name := #[ `Lean.Parser.Command.syntax, + `Lean.Parser.Command.syntaxAbbrev, `Lean.Parser.Command.syntaxCat, `Lean.Parser.Command.notation, `Lean.Parser.Command.macro, @@ -113,7 +114,10 @@ private def pureCommandPrefixes : Array Name := #[ `Lean.Parser.Command.declare_command_config_elab, `Lean.Parser.Command.declare_config_getter, `Lean.Parser.Command.declare_simp_like_tactic, - `Lean.Parser.Command.declare_tagged_region + `Lean.Parser.Command.declare_tagged_region, + `Lean.Parser.Command.mixfix, + `Lean.Parser.Command.grindPattern, + `Lean.Parser.Command.binderPredicate ] /-- Check if a command syntax node kind is known to be pure. -/ @@ -146,22 +150,68 @@ def checkFilePurity (contents : String) (fileName : String := "") : reasons := (kind, cmd.getPos?.getD 0) :: reasons return reasons.reverse +/-- Recursively collect all .lean files under a directory. -/ +partial def collectLeanFiles (path : System.FilePath) : IO (Array System.FilePath) := do + let mut result := #[] + if ← path.isDir then + for entry in ← path.readDir do + let sub ← collectLeanFiles entry.path + result := result ++ sub + else if path.extension == some "lean" then + result := result.push path + return result + +/-- Resolve arguments: expand directories into .lean files. -/ +def resolveInputs (inputs : List String) : IO (Array System.FilePath) := do + let mut files := #[] + for input in inputs do + let path : System.FilePath := input + if ← path.isDir then + files := files ++ (← collectLeanFiles path) + else + files := files.push path + return files + def main (args : List String) : IO UInt32 := do let impureOnly := args.contains "--impure-only" - let files := args.filter (fun a => !a.startsWith "--") - if files.isEmpty then - IO.eprintln "Usage: purityCheck [--impure-only] [file2.lean ...]" + -- Parse --output + let rec findOutput : List String → Option String + | "--output" :: v :: _ => some v + | _ :: rest => findOutput rest + | [] => none + let outputFile := findOutput args + -- Collect non-flag arguments as inputs + let mut inputs : List String := [] + let mut skipNext := false + for arg in args do + if skipNext then + skipNext := false + else if arg == "--output" then + skipNext := true + else if !arg.startsWith "--" then + inputs := arg :: inputs + let inputPaths := inputs.reverse + if inputPaths.isEmpty then + IO.eprintln "Usage: purityCheck [--impure-only] [--output ] [path ...]" + IO.eprintln " can be a .lean file or a directory (recursively scanned)" return 1 + let files ← resolveInputs inputPaths let mut exitCode : UInt32 := 0 - for file in files do + let mut outputLines : Array String := #[] + for file in files.toList.mergeSort (·.toString < ·.toString) do let contents ← IO.FS.readFile file - let reasons ← checkFilePurity contents file + let reasons ← checkFilePurity contents file.toString if reasons.isEmpty then unless impureOnly do IO.println s!"PURE: {file}" else - IO.println s!"IMPURE: {file}" + let line := s!"IMPURE: {file}" + IO.println line + outputLines := outputLines.push file.toString for (kind, pos) in reasons do IO.println s!" - {kind} at byte {pos}" exitCode := 1 + if let some outPath := outputFile then + IO.FS.writeFile outPath (outputLines.toList.map (· ++ "\n") |>.foldl (· ++ ·) "") + IO.eprintln s!"Wrote {outputLines.size} impure files to {outPath}" return exitCode diff --git a/Tools/invalidate_impure_cache.sh b/Tools/invalidate_impure_cache.sh new file mode 100755 index 0000000000..eca4285028 --- /dev/null +++ b/Tools/invalidate_impure_cache.sh @@ -0,0 +1,67 @@ +#!/bin/bash + +# Usage: ./invalidate_impure_cache.sh [--dry-run] +# +# Runs the purityCheck tool on all .lean files in Strata/ and StrataTest/, +# then deletes cached build artifacts for any module whose elaboration +# might perform I/O. +# +# Options: +# --dry-run Show what would be deleted without actually deleting + +set -euo pipefail + +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" +PROJECT_ROOT="$(cd "$SCRIPT_DIR/.." && pwd)" +LAKE_BUILD="$PROJECT_ROOT/.lake/build" + +dry_run=0 +if [ "${1:-}" = "--dry-run" ]; then + dry_run=1 +fi + +# Ensure purityCheck is built +echo "Building purityCheck..." +(cd "$PROJECT_ROOT" && lake build purityCheck > /dev/null 2>&1) + +# Run purity check +echo "Scanning for impure modules..." +LEAN_PATH="$LAKE_BUILD/lib/lean:$PROJECT_ROOT/.lake/packages/plausible/.lake/build/lib/lean" +impure_files=$(cd "$PROJECT_ROOT" && LEAN_PATH="$LEAN_PATH" \ + .lake/build/bin/purityCheck --impure-only \ + Strata/ StrataTest/ StrataMain.lean 2>/dev/null \ + | grep "^IMPURE:" | sed 's/^IMPURE: *//' || true) + +if [ -z "$impure_files" ]; then + echo "All modules are pure — nothing to invalidate." + exit 0 +fi + +count=0 +deleted=0 + +while IFS= read -r lean_file; do + # Strata//Foo/Bar.lean → Strata/Foo/Bar (strip .lean, normalize //) + stem=$(echo "$lean_file" | sed 's/\.lean$//' | sed 's|//|/|g') + + for dir in "$LAKE_BUILD/lib/lean" "$LAKE_BUILD/ir"; do + # Find all artifacts matching this stem + for artifact in "$dir/$stem".*; do + [ -e "$artifact" ] || continue + if [ $dry_run -eq 1 ]; then + echo " would delete: $artifact" + else + rm -f "$artifact" + fi + deleted=$((deleted + 1)) + done + done + count=$((count + 1)) +done <<< "$impure_files" + +if [ $dry_run -eq 1 ]; then + echo "" + echo "Dry run: $count impure modules, $deleted artifacts would be deleted." +else + echo "Invalidated $count impure modules ($deleted artifacts deleted)." +fi From 166b1027e481f36e282cf81cc0f828966469264e Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sat, 25 Apr 2026 07:46:28 -0700 Subject: [PATCH 03/22] lake exe instead --- Scripts/Skim.lean | 92 ++++++++++++++++++++++++++++++++++++++ Tools/PurityCheck.lean | 2 +- Tools/PurityCheckMain.lean | 2 + lakefile.toml | 10 ++++- 4 files changed, 104 insertions(+), 2 deletions(-) create mode 100644 Scripts/Skim.lean create mode 100644 Tools/PurityCheckMain.lean diff --git a/Scripts/Skim.lean b/Scripts/Skim.lean new file mode 100644 index 0000000000..ae0d747c71 --- /dev/null +++ b/Scripts/Skim.lean @@ -0,0 +1,92 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Tools.PurityCheck + +/-! # Lake Cache Skimmer + +Deletes cached `.lake/build/` artifacts for all modules whose elaboration +might perform I/O, so that `lake build` re-elaborates them from scratch. + +## Usage + + lake exe skim [--dry-run] +-/ + +namespace Skim + +/-- Recursively collect all `.lean` files under a directory. -/ +partial def findLeanFiles (root : System.FilePath) : IO (Array System.FilePath) := do + let mut result := #[] + if ← root.isDir then + for entry in ← root.readDir do + result := result ++ (← findLeanFiles entry.path) + else if root.extension == some "lean" then + result := result.push root + return result + +/-- Given a `.lean` source path, delete all matching build artifacts. -/ +def deleteArtifacts (lakeBuild : System.FilePath) (leanFile : System.FilePath) + (dryRun : Bool) : IO Nat := do + -- Strata//Foo/Bar.lean → Strata/Foo/Bar + let raw := leanFile.toString.replace "//" "/" + let stem := (if raw.endsWith ".lean" then raw.dropEnd 5 else raw).toString + let mut deleted := 0 + for dir in #["lib/lean", "ir"] do + let base := (lakeBuild / dir / stem).toString + let parent : System.FilePath := (lakeBuild / dir / stem).parent.getD "." + if ← parent.isDir then + for entry in ← parent.readDir do + let entryStr := entry.path.toString + if entryStr.startsWith (base ++ ".") then + if dryRun then + IO.println s!" would delete: {entry.path}" + else + IO.FS.removeFile entry.path + deleted := deleted + 1 + return deleted + +end Skim + +def main (args : List String) : IO UInt32 := do + let dryRun := args.contains "--dry-run" + + let cwd ← IO.currentDir + let lakeBuild := cwd / ".lake" / "build" + + unless ← (cwd / "lakefile.toml").pathExists do + IO.eprintln "Error: must be run from the project root (where lakefile.toml is)" + return 1 + + unless ← lakeBuild.isDir do + IO.eprintln "No .lake/build/ directory found — nothing to skim." + return 0 + + IO.println "Scanning for impure modules..." + let mut allFiles := #[] + for dir in #["Strata", "StrataTest"] do + let path : System.FilePath := dir + if ← path.isDir then + allFiles := allFiles ++ (← Skim.findLeanFiles path) + let mainFile : System.FilePath := "StrataMain.lean" + if ← mainFile.pathExists then + allFiles := allFiles.push mainFile + + let mut impureCount := 0 + let mut totalDeleted := 0 + for file in allFiles do + let contents ← IO.FS.readFile file + let reasons ← checkFilePurity contents file.toString + unless reasons.isEmpty do + impureCount := impureCount + 1 + let deleted ← Skim.deleteArtifacts lakeBuild file dryRun + totalDeleted := totalDeleted + deleted + + if dryRun then + IO.println s!"\nDry run: {impureCount} impure modules, {totalDeleted} artifacts would be deleted." + else + IO.println s!"Skimmed {impureCount} impure modules ({totalDeleted} artifacts deleted)." + return 0 diff --git a/Tools/PurityCheck.lean b/Tools/PurityCheck.lean index 2cc94eedae..01d95680c4 100644 --- a/Tools/PurityCheck.lean +++ b/Tools/PurityCheck.lean @@ -172,7 +172,7 @@ def resolveInputs (inputs : List String) : IO (Array System.FilePath) := do files := files.push path return files -def main (args : List String) : IO UInt32 := do +def purityCheckMain (args : List String) : IO UInt32 := do let impureOnly := args.contains "--impure-only" -- Parse --output let rec findOutput : List String → Option String diff --git a/Tools/PurityCheckMain.lean b/Tools/PurityCheckMain.lean new file mode 100644 index 0000000000..5c241a700f --- /dev/null +++ b/Tools/PurityCheckMain.lean @@ -0,0 +1,2 @@ +import Tools.PurityCheck +def main := purityCheckMain diff --git a/lakefile.toml b/lakefile.toml index ec3229a9fb..0103313eaf 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -43,4 +43,12 @@ name = "DiffTestCore" [[lean_exe]] name = "purityCheck" -root = "Tools.PurityCheck" +root = "Tools.PurityCheckMain" + +[[lean_lib]] +name = "Tools" +globs = ["Tools.+"] + +[[lean_exe]] +name = "skim" +root = "Scripts.Skim" From 9e9990ba4d421ba53ef5fa6fc3a7640f64afc430 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sat, 25 Apr 2026 07:47:47 -0700 Subject: [PATCH 04/22] remove old version --- Tools/invalidate_impure_cache.sh | 67 -------------------------------- 1 file changed, 67 deletions(-) delete mode 100755 Tools/invalidate_impure_cache.sh diff --git a/Tools/invalidate_impure_cache.sh b/Tools/invalidate_impure_cache.sh deleted file mode 100755 index eca4285028..0000000000 --- a/Tools/invalidate_impure_cache.sh +++ /dev/null @@ -1,67 +0,0 @@ -#!/bin/bash - -# Usage: ./invalidate_impure_cache.sh [--dry-run] -# -# Runs the purityCheck tool on all .lean files in Strata/ and StrataTest/, -# then deletes cached build artifacts for any module whose elaboration -# might perform I/O. -# -# Options: -# --dry-run Show what would be deleted without actually deleting - -set -euo pipefail - -SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" -PROJECT_ROOT="$(cd "$SCRIPT_DIR/.." && pwd)" -LAKE_BUILD="$PROJECT_ROOT/.lake/build" - -dry_run=0 -if [ "${1:-}" = "--dry-run" ]; then - dry_run=1 -fi - -# Ensure purityCheck is built -echo "Building purityCheck..." -(cd "$PROJECT_ROOT" && lake build purityCheck > /dev/null 2>&1) - -# Run purity check -echo "Scanning for impure modules..." -LEAN_PATH="$LAKE_BUILD/lib/lean:$PROJECT_ROOT/.lake/packages/plausible/.lake/build/lib/lean" -impure_files=$(cd "$PROJECT_ROOT" && LEAN_PATH="$LEAN_PATH" \ - .lake/build/bin/purityCheck --impure-only \ - Strata/ StrataTest/ StrataMain.lean 2>/dev/null \ - | grep "^IMPURE:" | sed 's/^IMPURE: *//' || true) - -if [ -z "$impure_files" ]; then - echo "All modules are pure — nothing to invalidate." - exit 0 -fi - -count=0 -deleted=0 - -while IFS= read -r lean_file; do - # Strata//Foo/Bar.lean → Strata/Foo/Bar (strip .lean, normalize //) - stem=$(echo "$lean_file" | sed 's/\.lean$//' | sed 's|//|/|g') - - for dir in "$LAKE_BUILD/lib/lean" "$LAKE_BUILD/ir"; do - # Find all artifacts matching this stem - for artifact in "$dir/$stem".*; do - [ -e "$artifact" ] || continue - if [ $dry_run -eq 1 ]; then - echo " would delete: $artifact" - else - rm -f "$artifact" - fi - deleted=$((deleted + 1)) - done - done - count=$((count + 1)) -done <<< "$impure_files" - -if [ $dry_run -eq 1 ]; then - echo "" - echo "Dry run: $count impure modules, $deleted artifacts would be deleted." -else - echo "Invalidated $count impure modules ($deleted artifacts deleted)." -fi From 6a702e36a8bdbbbbdb766f4a8f4267b859f8e52f Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sat, 25 Apr 2026 08:04:29 -0700 Subject: [PATCH 05/22] line numbers --- Tools/PurityCheck.lean | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/Tools/PurityCheck.lean b/Tools/PurityCheck.lean index 01d95680c4..79fbbbb6ac 100644 --- a/Tools/PurityCheck.lean +++ b/Tools/PurityCheck.lean @@ -126,15 +126,21 @@ private def isPureCommand (kind : SyntaxNodeKind) : Bool := pureCommandPrefixes.any (fun pfx => pfx.isPrefixOf kind) || kind == nullKind +/-- An impure command found during purity checking. -/ +structure ImpureCommand where + kind : SyntaxNodeKind + line : Nat + col : Nat + /-- Parse a .lean file and check all top-level commands for purity. -Returns the list of impure command kind names (empty = pure module). -/ +Returns the list of impure commands found (empty = pure module). -/ def checkFilePurity (contents : String) (fileName : String := "") : - IO (List (SyntaxNodeKind × String.Pos.Raw)) := do + IO (List ImpureCommand) := do let inputCtx := mkInputContext contents fileName let (header, parserState, msgs) ← parseHeader inputCtx let (env, _msgs) ← Elab.processHeader header {} msgs inputCtx let pmctx : ParserModuleContext := { env, options := {} } - let mut reasons : List (SyntaxNodeKind × String.Pos.Raw) := [] + let mut reasons : List ImpureCommand := [] let mut mps := parserState let mut messages := MessageLog.empty let mut done := false @@ -147,7 +153,8 @@ def checkFilePurity (contents : String) (fileName : String := "") : else let kind := cmd.getKind if !isPureCommand kind then - reasons := (kind, cmd.getPos?.getD 0) :: reasons + let pos := inputCtx.fileMap.toPosition (cmd.getPos?.getD 0) + reasons := { kind, line := pos.line, col := pos.column } :: reasons return reasons.reverse /-- Recursively collect all .lean files under a directory. -/ @@ -208,8 +215,8 @@ def purityCheckMain (args : List String) : IO UInt32 := do let line := s!"IMPURE: {file}" IO.println line outputLines := outputLines.push file.toString - for (kind, pos) in reasons do - IO.println s!" - {kind} at byte {pos}" + for r in reasons do + IO.println s!" - {r.kind} at {r.line}:{r.col}" exitCode := 1 if let some outPath := outputFile then IO.FS.writeFile outPath (outputLines.toList.map (· ++ "\n") |>.foldl (· ++ ·) "") From e681e29c00e00057cd3372c038cdf8bac58a390c Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sat, 25 Apr 2026 11:15:44 -0700 Subject: [PATCH 06/22] Switch to textual scanning --- Tools/PurityCheck.lean | 195 ++++++++++++----------------------------- 1 file changed, 54 insertions(+), 141 deletions(-) diff --git a/Tools/PurityCheck.lean b/Tools/PurityCheck.lean index 79fbbbb6ac..ce8b5511f2 100644 --- a/Tools/PurityCheck.lean +++ b/Tools/PurityCheck.lean @@ -4,166 +4,82 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Lean.Parser -import Lean.Parser.Command -import Lean.Parser.Module -import Lean.Elab.Import - /-! # Module Purity Checker Determines whether elaborating a Lean module could potentially perform I/O. -Uses a conservative allowlist approach: commands whose elaboration is known to -be pure are on the allowlist; everything else is treated as potentially impure. +Uses text scanning for known impure command patterns. This is sound because +Lean's impure-during-elaboration commands are a closed set — there are only +a handful of ways to trigger IO during elaboration, and they all have +distinctive textual signatures. ## Usage - lake exe purityCheck [--impure-only] [file2.lean ...] + lake exe purityCheck [--impure-only] [--output ] [path ...] Prints each file with its purity status. With `--impure-only`, only prints files that might perform I/O (useful for cache invalidation). -/ -open Lean Parser - -/-- Commands whose elaboration is known to be pure (no I/O side effects). -/ -private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ - -- Top-level declarations (elaborate types/terms but don't execute them) - ``Command.declaration, - ``Command.«deriving», - - -- Structural / scoping - ``Command.«section», - ``Command.«namespace», - ``Command.«end», - ``Command.«variable», - ``Command.«universe», - ``Command.«open», - ``Command.«export», - ``Command.«import», - ``Command.«mutual», - ``Command.«in», - ``Command.«include», - ``Command.«omit», - ``Command.withWeakNamespace, - ``Command.withExporting, - - -- Options and attributes (pure metadata) - ``Command.«set_option», - ``Command.«attribute», - - -- Inspection commands (pure — only print/check, no execution) - ``Command.check, - ``Command.check_failure, - ``Command.print, - ``Command.printSig, - ``Command.printAxioms, - ``Command.printEqns, - ``Command.printTacTags, - ``Command.«where», - ``Command.version, - ``Command.synth, - - -- Assertions about the environment (pure checks) - ``Command.assertNotExists, - ``Command.assertNotImported, - ``Command.checkAssertions, - - -- Documentation - ``Command.moduleDoc, - ``Command.addDocString, - - -- Misc pure commands - ``Command.«register_tactic_tag», - ``Command.«tactic_extension», - ``Command.«recommended_spelling», - ``Command.genInjectiveTheorems, - ``Command.registerErrorExplanationStx, - ``Command.«init_quot», - ``Command.exit, - ``Command.eoi -] - -/-- Command kind prefixes known to be pure (syntax/notation/macro definitions). -/ -private def pureCommandPrefixes : Array Name := #[ - `Lean.Parser.Command.syntax, - `Lean.Parser.Command.syntaxAbbrev, - `Lean.Parser.Command.syntaxCat, - `Lean.Parser.Command.notation, - `Lean.Parser.Command.macro, - `Lean.Parser.Command.macro_rules, - `Lean.Parser.Command.elab, - `Lean.Parser.Command.elab_rules, - `Lean.Parser.Command.«scoped», - `Lean.Parser.Command.«local», - `Lean.Parser.Command.simproc, - `Lean.Parser.Command.builtin_simproc, - `Lean.Parser.Command.dsimproc, - `Lean.Parser.Command.builtin_dsimproc, - `Lean.Parser.Command.register_simp_attr, - `Lean.Parser.Command.register_option, - `Lean.Parser.Command.register_builtin_option, - `Lean.Parser.Command.register_label_attr, - `Lean.Parser.Command.«infix», - `Lean.Parser.Command.«infixl», - `Lean.Parser.Command.«infixr», - `Lean.Parser.Command.«prefix», - `Lean.Parser.Command.«postfix», - `Lean.Parser.Command.declare_syntax_cat, - `Lean.Parser.Command.declare_config_elab, - `Lean.Parser.Command.declare_command_config_elab, - `Lean.Parser.Command.declare_config_getter, - `Lean.Parser.Command.declare_simp_like_tactic, - `Lean.Parser.Command.declare_tagged_region, - `Lean.Parser.Command.mixfix, - `Lean.Parser.Command.grindPattern, - `Lean.Parser.Command.binderPredicate -] - -/-- Check if a command syntax node kind is known to be pure. -/ -private def isPureCommand (kind : SyntaxNodeKind) : Bool := - pureCommandKinds.contains kind || - pureCommandPrefixes.any (fun pfx => pfx.isPrefixOf kind) || - kind == nullKind - /-- An impure command found during purity checking. -/ structure ImpureCommand where - kind : SyntaxNodeKind + kind : String line : Nat col : Nat -/-- Parse a .lean file and check all top-level commands for purity. -Returns the list of impure commands found (empty = pure module). -/ -def checkFilePurity (contents : String) (fileName : String := "") : +/-- Text patterns that indicate impure commands. Each pattern is matched +against the start of a trimmed line. The patterns cover all known ways +to perform IO during Lean module elaboration: + +- `#eval` / `#eval!` — executes arbitrary code +- `initialize` / `builtin_initialize` — runs code at module load time +- `#guard_msgs` — executes code and checks output +- `#guard` — executes a boolean check at elaboration time + +Custom elaborators defined via `initialize` in *other* modules could +perform IO, but those are caught by the `initialize` pattern in the +module that defines them. -/ +private def impurePatterns : Array (String × String) := #[ + ("#eval!", "eval!"), + ("#eval ", "eval"), + ("#eval\n", "eval"), + ("#guard_msgs", "guard_msgs"), + ("#guard ", "guard"), + ("builtin_initialize", "builtin_initialize"), + ("initialize ", "initialize"), + ("initialize\n", "initialize"), + ("public initialize", "initialize"), + ("private initialize", "initialize"), + ("protected initialize", "initialize") +] + +/-- Scan file text for impure command patterns. -/ +def textScanForImpurity (contents : String) : List ImpureCommand := + go (contents.splitOn "\n") 1 +where + go : List String → Nat → List ImpureCommand + | [], _ => [] + | line :: rest, lineNum => + let trimmed := line.trimAsciiStart.toString + match impurePatterns.findSome? fun (pat, kind) => + if trimmed.startsWith pat then + some { kind, line := lineNum, col := line.length - trimmed.length : ImpureCommand } + else none + with + | some cmd => cmd :: go rest (lineNum + 1) + | none => go rest (lineNum + 1) + +/-- Check a file for purity. Returns impure commands found (empty = pure). -/ +def checkFilePurity (contents : String) (_fileName : String := "") : IO (List ImpureCommand) := do - let inputCtx := mkInputContext contents fileName - let (header, parserState, msgs) ← parseHeader inputCtx - let (env, _msgs) ← Elab.processHeader header {} msgs inputCtx - let pmctx : ParserModuleContext := { env, options := {} } - let mut reasons : List ImpureCommand := [] - let mut mps := parserState - let mut messages := MessageLog.empty - let mut done := false - while !done do - let (cmd, mps', msgs') := parseCommand inputCtx pmctx mps messages - mps := mps' - messages := msgs' - if isTerminalCommand cmd then - done := true - else - let kind := cmd.getKind - if !isPureCommand kind then - let pos := inputCtx.fileMap.toPosition (cmd.getPos?.getD 0) - reasons := { kind, line := pos.line, col := pos.column } :: reasons - return reasons.reverse + return textScanForImpurity contents -/-- Recursively collect all .lean files under a directory. -/ +/-- Recursively collect all `.lean` files under a directory. -/ partial def collectLeanFiles (path : System.FilePath) : IO (Array System.FilePath) := do let mut result := #[] if ← path.isDir then for entry in ← path.readDir do - let sub ← collectLeanFiles entry.path - result := result ++ sub + result := result ++ (← collectLeanFiles entry.path) else if path.extension == some "lean" then result := result.push path return result @@ -181,13 +97,11 @@ def resolveInputs (inputs : List String) : IO (Array System.FilePath) := do def purityCheckMain (args : List String) : IO UInt32 := do let impureOnly := args.contains "--impure-only" - -- Parse --output let rec findOutput : List String → Option String | "--output" :: v :: _ => some v | _ :: rest => findOutput rest | [] => none let outputFile := findOutput args - -- Collect non-flag arguments as inputs let mut inputs : List String := [] let mut skipNext := false for arg in args do @@ -212,8 +126,7 @@ def purityCheckMain (args : List String) : IO UInt32 := do unless impureOnly do IO.println s!"PURE: {file}" else - let line := s!"IMPURE: {file}" - IO.println line + IO.println s!"IMPURE: {file}" outputLines := outputLines.push file.toString for r in reasons do IO.println s!" - {r.kind} at {r.line}:{r.col}" From 5e9a02c09e6c5ffc4bb6bf6270c59328474844b4 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sat, 25 Apr 2026 17:30:27 -0700 Subject: [PATCH 07/22] Revert "Switch to textual scanning" This reverts commit e681e29c00e00057cd3372c038cdf8bac58a390c. --- Tools/PurityCheck.lean | 195 +++++++++++++++++++++++++++++------------ 1 file changed, 141 insertions(+), 54 deletions(-) diff --git a/Tools/PurityCheck.lean b/Tools/PurityCheck.lean index ce8b5511f2..79fbbbb6ac 100644 --- a/Tools/PurityCheck.lean +++ b/Tools/PurityCheck.lean @@ -4,82 +4,166 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +import Lean.Parser +import Lean.Parser.Command +import Lean.Parser.Module +import Lean.Elab.Import + /-! # Module Purity Checker Determines whether elaborating a Lean module could potentially perform I/O. -Uses text scanning for known impure command patterns. This is sound because -Lean's impure-during-elaboration commands are a closed set — there are only -a handful of ways to trigger IO during elaboration, and they all have -distinctive textual signatures. +Uses a conservative allowlist approach: commands whose elaboration is known to +be pure are on the allowlist; everything else is treated as potentially impure. ## Usage - lake exe purityCheck [--impure-only] [--output ] [path ...] + lake exe purityCheck [--impure-only] [file2.lean ...] Prints each file with its purity status. With `--impure-only`, only prints files that might perform I/O (useful for cache invalidation). -/ +open Lean Parser + +/-- Commands whose elaboration is known to be pure (no I/O side effects). -/ +private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ + -- Top-level declarations (elaborate types/terms but don't execute them) + ``Command.declaration, + ``Command.«deriving», + + -- Structural / scoping + ``Command.«section», + ``Command.«namespace», + ``Command.«end», + ``Command.«variable», + ``Command.«universe», + ``Command.«open», + ``Command.«export», + ``Command.«import», + ``Command.«mutual», + ``Command.«in», + ``Command.«include», + ``Command.«omit», + ``Command.withWeakNamespace, + ``Command.withExporting, + + -- Options and attributes (pure metadata) + ``Command.«set_option», + ``Command.«attribute», + + -- Inspection commands (pure — only print/check, no execution) + ``Command.check, + ``Command.check_failure, + ``Command.print, + ``Command.printSig, + ``Command.printAxioms, + ``Command.printEqns, + ``Command.printTacTags, + ``Command.«where», + ``Command.version, + ``Command.synth, + + -- Assertions about the environment (pure checks) + ``Command.assertNotExists, + ``Command.assertNotImported, + ``Command.checkAssertions, + + -- Documentation + ``Command.moduleDoc, + ``Command.addDocString, + + -- Misc pure commands + ``Command.«register_tactic_tag», + ``Command.«tactic_extension», + ``Command.«recommended_spelling», + ``Command.genInjectiveTheorems, + ``Command.registerErrorExplanationStx, + ``Command.«init_quot», + ``Command.exit, + ``Command.eoi +] + +/-- Command kind prefixes known to be pure (syntax/notation/macro definitions). -/ +private def pureCommandPrefixes : Array Name := #[ + `Lean.Parser.Command.syntax, + `Lean.Parser.Command.syntaxAbbrev, + `Lean.Parser.Command.syntaxCat, + `Lean.Parser.Command.notation, + `Lean.Parser.Command.macro, + `Lean.Parser.Command.macro_rules, + `Lean.Parser.Command.elab, + `Lean.Parser.Command.elab_rules, + `Lean.Parser.Command.«scoped», + `Lean.Parser.Command.«local», + `Lean.Parser.Command.simproc, + `Lean.Parser.Command.builtin_simproc, + `Lean.Parser.Command.dsimproc, + `Lean.Parser.Command.builtin_dsimproc, + `Lean.Parser.Command.register_simp_attr, + `Lean.Parser.Command.register_option, + `Lean.Parser.Command.register_builtin_option, + `Lean.Parser.Command.register_label_attr, + `Lean.Parser.Command.«infix», + `Lean.Parser.Command.«infixl», + `Lean.Parser.Command.«infixr», + `Lean.Parser.Command.«prefix», + `Lean.Parser.Command.«postfix», + `Lean.Parser.Command.declare_syntax_cat, + `Lean.Parser.Command.declare_config_elab, + `Lean.Parser.Command.declare_command_config_elab, + `Lean.Parser.Command.declare_config_getter, + `Lean.Parser.Command.declare_simp_like_tactic, + `Lean.Parser.Command.declare_tagged_region, + `Lean.Parser.Command.mixfix, + `Lean.Parser.Command.grindPattern, + `Lean.Parser.Command.binderPredicate +] + +/-- Check if a command syntax node kind is known to be pure. -/ +private def isPureCommand (kind : SyntaxNodeKind) : Bool := + pureCommandKinds.contains kind || + pureCommandPrefixes.any (fun pfx => pfx.isPrefixOf kind) || + kind == nullKind + /-- An impure command found during purity checking. -/ structure ImpureCommand where - kind : String + kind : SyntaxNodeKind line : Nat col : Nat -/-- Text patterns that indicate impure commands. Each pattern is matched -against the start of a trimmed line. The patterns cover all known ways -to perform IO during Lean module elaboration: - -- `#eval` / `#eval!` — executes arbitrary code -- `initialize` / `builtin_initialize` — runs code at module load time -- `#guard_msgs` — executes code and checks output -- `#guard` — executes a boolean check at elaboration time - -Custom elaborators defined via `initialize` in *other* modules could -perform IO, but those are caught by the `initialize` pattern in the -module that defines them. -/ -private def impurePatterns : Array (String × String) := #[ - ("#eval!", "eval!"), - ("#eval ", "eval"), - ("#eval\n", "eval"), - ("#guard_msgs", "guard_msgs"), - ("#guard ", "guard"), - ("builtin_initialize", "builtin_initialize"), - ("initialize ", "initialize"), - ("initialize\n", "initialize"), - ("public initialize", "initialize"), - ("private initialize", "initialize"), - ("protected initialize", "initialize") -] - -/-- Scan file text for impure command patterns. -/ -def textScanForImpurity (contents : String) : List ImpureCommand := - go (contents.splitOn "\n") 1 -where - go : List String → Nat → List ImpureCommand - | [], _ => [] - | line :: rest, lineNum => - let trimmed := line.trimAsciiStart.toString - match impurePatterns.findSome? fun (pat, kind) => - if trimmed.startsWith pat then - some { kind, line := lineNum, col := line.length - trimmed.length : ImpureCommand } - else none - with - | some cmd => cmd :: go rest (lineNum + 1) - | none => go rest (lineNum + 1) - -/-- Check a file for purity. Returns impure commands found (empty = pure). -/ -def checkFilePurity (contents : String) (_fileName : String := "") : +/-- Parse a .lean file and check all top-level commands for purity. +Returns the list of impure commands found (empty = pure module). -/ +def checkFilePurity (contents : String) (fileName : String := "") : IO (List ImpureCommand) := do - return textScanForImpurity contents + let inputCtx := mkInputContext contents fileName + let (header, parserState, msgs) ← parseHeader inputCtx + let (env, _msgs) ← Elab.processHeader header {} msgs inputCtx + let pmctx : ParserModuleContext := { env, options := {} } + let mut reasons : List ImpureCommand := [] + let mut mps := parserState + let mut messages := MessageLog.empty + let mut done := false + while !done do + let (cmd, mps', msgs') := parseCommand inputCtx pmctx mps messages + mps := mps' + messages := msgs' + if isTerminalCommand cmd then + done := true + else + let kind := cmd.getKind + if !isPureCommand kind then + let pos := inputCtx.fileMap.toPosition (cmd.getPos?.getD 0) + reasons := { kind, line := pos.line, col := pos.column } :: reasons + return reasons.reverse -/-- Recursively collect all `.lean` files under a directory. -/ +/-- Recursively collect all .lean files under a directory. -/ partial def collectLeanFiles (path : System.FilePath) : IO (Array System.FilePath) := do let mut result := #[] if ← path.isDir then for entry in ← path.readDir do - result := result ++ (← collectLeanFiles entry.path) + let sub ← collectLeanFiles entry.path + result := result ++ sub else if path.extension == some "lean" then result := result.push path return result @@ -97,11 +181,13 @@ def resolveInputs (inputs : List String) : IO (Array System.FilePath) := do def purityCheckMain (args : List String) : IO UInt32 := do let impureOnly := args.contains "--impure-only" + -- Parse --output let rec findOutput : List String → Option String | "--output" :: v :: _ => some v | _ :: rest => findOutput rest | [] => none let outputFile := findOutput args + -- Collect non-flag arguments as inputs let mut inputs : List String := [] let mut skipNext := false for arg in args do @@ -126,7 +212,8 @@ def purityCheckMain (args : List String) : IO UInt32 := do unless impureOnly do IO.println s!"PURE: {file}" else - IO.println s!"IMPURE: {file}" + let line := s!"IMPURE: {file}" + IO.println line outputLines := outputLines.push file.toString for r in reasons do IO.println s!" - {r.kind} at {r.line}:{r.col}" From ff5990a4647d83535912f778dce9a30a92880362 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sat, 25 Apr 2026 18:17:37 -0700 Subject: [PATCH 08/22] Inspect .olean files --- Scripts/Skim.lean | 97 +++++++++++++++++++++++++++++++++--------- Tools/PurityCheck.lean | 4 ++ 2 files changed, 80 insertions(+), 21 deletions(-) diff --git a/Scripts/Skim.lean b/Scripts/Skim.lean index ae0d747c71..9bd57d591a 100644 --- a/Scripts/Skim.lean +++ b/Scripts/Skim.lean @@ -4,21 +4,34 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Tools.PurityCheck +import Lean +import Lean.Compiler.InitAttr -/-! # Lake Cache Skimmer +/-! # Lake Build + Skim -Deletes cached `.lake/build/` artifacts for all modules whose elaboration -might perform I/O, so that `lake build` re-elaborates them from scratch. +Runs `lake build`, then identifies modules whose elaboration may have performed +IO and deletes their build artifacts so the next build re-elaborates them. ## Usage - lake exe skim [--dry-run] + lake exe skim [--dry-run] [-- ...] + +## Detection strategy + +Two complementary checks: + +1. **`.olean` inspection**: Load each module's environment and check for `[init]` + attributed declarations. This precisely detects `initialize`/`builtin_initialize`. + +2. **Text scan**: Grep source files for `#eval`, `#guard_msgs`, `#guard`, `run_cmd`, + `run_elab`, `run_meta`. These execute code during elaboration but don't leave + `[init]` markers in the environment. -/ +open Lean + namespace Skim -/-- Recursively collect all `.lean` files under a directory. -/ partial def findLeanFiles (root : System.FilePath) : IO (Array System.FilePath) := do let mut result := #[] if ← root.isDir then @@ -28,10 +41,36 @@ partial def findLeanFiles (root : System.FilePath) : IO (Array System.FilePath) result := result.push root return result -/-- Given a `.lean` source path, delete all matching build artifacts. -/ +/-- Convert `Strata/DL/Lambda/LExpr.lean` → `Strata.DL.Lambda.LExpr` -/ +def sourceToModule (path : System.FilePath) : Name := + let s := path.toString.replace "//" "/" + let s := if s.endsWith ".lean" then (s.dropEnd 5).toString else s + s.splitOn "/" |>.foldl (· ++ Name.mkSimple ·) .anonymous + +/-- Text patterns for commands that execute code but don't leave `[init]` markers. -/ +private def evalPatterns : Array String := #[ + "#eval!", "#eval ", "#eval\n", + "#guard_msgs", "#guard ", + "run_cmd", "run_elab", "run_meta" +] + +def hasEvalText (contents : String) : Bool := + contents.splitOn "\n" |>.any fun line => + let trimmed := line.trimAsciiStart.toString + evalPatterns.any (trimmed.startsWith ·) + +/-- Check if a module has `[init]` declarations by loading its `.olean`. -/ +def hasInitDecls (modName : Name) : IO Bool := do + let env ← importModules #[{ module := modName }] {} + let header := env.header + let modIdx := header.moduleNames.size - 1 + if h : modIdx < header.moduleData.size then + let modData := header.moduleData[modIdx] + return modData.constNames.any (hasInitAttr env) + return false + def deleteArtifacts (lakeBuild : System.FilePath) (leanFile : System.FilePath) (dryRun : Bool) : IO Nat := do - -- Strata//Foo/Bar.lean → Strata/Foo/Bar let raw := leanFile.toString.replace "//" "/" let stem := (if raw.endsWith ".lean" then raw.dropEnd 5 else raw).toString let mut deleted := 0 @@ -40,8 +79,7 @@ def deleteArtifacts (lakeBuild : System.FilePath) (leanFile : System.FilePath) let parent : System.FilePath := (lakeBuild / dir / stem).parent.getD "." if ← parent.isDir then for entry in ← parent.readDir do - let entryStr := entry.path.toString - if entryStr.startsWith (base ++ ".") then + if entry.path.toString.startsWith (base ++ ".") then if dryRun then IO.println s!" would delete: {entry.path}" else @@ -53,34 +91,51 @@ end Skim def main (args : List String) : IO UInt32 := do let dryRun := args.contains "--dry-run" - let cwd ← IO.currentDir let lakeBuild := cwd / ".lake" / "build" unless ← (cwd / "lakefile.toml").pathExists do - IO.eprintln "Error: must be run from the project root (where lakefile.toml is)" + IO.eprintln "Error: must be run from the project root" return 1 - unless ← lakeBuild.isDir do - IO.eprintln "No .lake/build/ directory found — nothing to skim." - return 0 - + -- Step 1: Run lake build + let lakeArgs := args.filter (· != "--dry-run") + IO.println "Running lake build..." + let buildResult ← IO.Process.output { + cmd := "lake", args := #["build"] ++ lakeArgs.toArray, cwd := cwd + } + IO.print buildResult.stdout + if buildResult.stderr != "" then IO.eprint buildResult.stderr + if buildResult.exitCode != 0 then + IO.eprintln "lake build failed" + return buildResult.exitCode + + -- Step 2: Collect source files IO.println "Scanning for impure modules..." let mut allFiles := #[] for dir in #["Strata", "StrataTest"] do let path : System.FilePath := dir if ← path.isDir then allFiles := allFiles ++ (← Skim.findLeanFiles path) - let mainFile : System.FilePath := "StrataMain.lean" - if ← mainFile.pathExists then - allFiles := allFiles.push mainFile + for extra in #["StrataMain.lean"] do + let path : System.FilePath := extra + if ← path.pathExists then allFiles := allFiles.push path + -- Step 3: Check each module let mut impureCount := 0 let mut totalDeleted := 0 for file in allFiles do let contents ← IO.FS.readFile file - let reasons ← checkFilePurity contents file.toString - unless reasons.isEmpty do + let modName := Skim.sourceToModule file + -- Check 1: text scan for #eval, #guard_msgs, etc. + let hasEval := Skim.hasEvalText contents + -- Check 2: olean inspection for [init] declarations + let hasInit ← try + Skim.hasInitDecls modName + catch _ => + -- Can't load olean (not built?) — skip olean check, rely on text scan + pure false + if hasEval || hasInit then impureCount := impureCount + 1 let deleted ← Skim.deleteArtifacts lakeBuild file dryRun totalDeleted := totalDeleted + deleted diff --git a/Tools/PurityCheck.lean b/Tools/PurityCheck.lean index 79fbbbb6ac..4347a38bf8 100644 --- a/Tools/PurityCheck.lean +++ b/Tools/PurityCheck.lean @@ -150,6 +150,10 @@ def checkFilePurity (contents : String) (fileName : String := "") : messages := msgs' if isTerminalCommand cmd then done := true + else if cmd.hasMissing then + let pos := inputCtx.fileMap.toPosition (cmd.getPos?.getD mps.pos) + reasons := { kind := `parseError, line := pos.line, col := pos.column } :: reasons + done := true else let kind := cmd.getKind if !isPureCommand kind then From 86047850f7e10ca5dbfad2ea28fb94e82b5a7873 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sun, 26 Apr 2026 08:06:19 -0700 Subject: [PATCH 09/22] Partial design doc --- docs/LakeCacheSkimmer.md | 183 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 183 insertions(+) create mode 100644 docs/LakeCacheSkimmer.md diff --git a/docs/LakeCacheSkimmer.md b/docs/LakeCacheSkimmer.md new file mode 100644 index 0000000000..5c05d9e698 --- /dev/null +++ b/docs/LakeCacheSkimmer.md @@ -0,0 +1,183 @@ +# Lake Cache Skimmer: Design Document + +## Problem + +Lean's `lake build` caches elaboration results in `.olean` files. When a module's +elaboration depends on external state (file system, SMT solvers, network, etc.), +the cached result may be stale — but Lake has no way to know this, since it only +tracks source file changes and dependency graphs. + +We need a tool that identifies modules whose elaboration *might* perform IO and +invalidates their cached build artifacts, forcing `lake build` to re-elaborate +them. + +## Design Goals + +1. **Soundness**: If we identify a module as pure, it must be impossible for its + elaboration to have performed any IO. False negatives (missing an impure module) + cause stale cache bugs that are extremely hard to diagnose. + +2. **Precision**: Minimize false positives. If we flag too many modules as impure, + every build re-elaborates them unnecessarily, defeating the purpose of caching. + +## Background: How Lean Modules Can Perform IO + +Lean interleaves parsing and elaboration: each command is parsed using syntax +extensions registered by all previously elaborated commands, then elaborated +before the next command is parsed. This means we cannot parse a file without +elaborating it. + +The complete set of ways a module can perform IO during elaboration: + +| Command | Mechanism | Leaves `.olean` trace? | +|---------|-----------|----------------------| +| `initialize` / `builtin_initialize` | Runs IO action at module load time | Yes — `[init]` attribute | +| `#eval` / `#eval!` | Executes arbitrary expression | No | +| `#guard_msgs` | Executes wrapped command, checks output | No | +| `#guard` | Evaluates boolean expression | No | +| `run_cmd` / `run_elab` / `run_meta` | Executes monadic code | No | +| Custom `@[command_elab]` | Elaborator may perform IO | No (at use site) | +| `native_decide` / `decide` | Pure computation | N/A (pure) | + +The key challenge: most impure commands leave **no trace** in the `.olean` file. +The `.olean` records the *result* of elaboration (declarations, attributes, +environment extensions), not *how* it got there. + +## Approaches Considered + +### Option A: Instrument the Elaboration Loop + +Register a `CommandElab` wrapper that intercepts every command before elaboration, +logs its syntax kind, then delegates to the real elaborator. Write results to a +side-channel file (e.g., `.purity.json`). + +**Pros:** +- Perfect accuracy — sees every command exactly as Lean sees it +- No post-build analysis needed + +**Cons:** +- Requires modifying the build process +- Every module must import the instrumentation module +- Side-channel files add complexity + +### Option B: Re-elaborate Post-Build + +After `lake build`, use `Lean.Elab.process` to re-elaborate each source file. +Since `.olean` files exist, `importModules` is fast, but the file itself is +fully re-elaborated. Intercept commands during this re-elaboration. + +**Pros:** +- No build modification needed +- Perfect accuracy + +**Cons:** +- Re-elaborates every source file — O(n) in codebase size +- Potentially very slow for large codebases +- Duplicates work already done by `lake build` + +### Option C: Hybrid `.olean` Inspection + Text Scan + +Use `.olean` inspection for `initialize` (precise, via `[init]` attribute). +Use text scanning (grep) for `#eval`, `#guard_msgs`, etc. + +**Pros:** +- Fast — no re-elaboration +- `.olean` check is perfectly precise for `initialize` + +**Cons:** +- Text scan can false-positive on patterns in comments, strings, or + custom syntax (e.g., DDM `//` comments containing "initialize") +- Text scan can false-negative if a pattern appears in an unexpected form +- Cannot detect IO from custom command elaborators + +### Option D: Persistent Environment Extension (Recommended) + +Define a persistent environment extension that records which impure command kinds +were used during elaboration. Register a `CommandElab` hook (via `initialize`) +that writes to this extension whenever an impure command is elaborated. After +`lake build`, load each `.olean` and read the extension. + +**Pros:** +- Perfect accuracy — the hook sees every command during real elaboration +- Readable from `.olean` — no re-elaboration, instant classification +- No side-channel files — data lives in the `.olean` itself +- Survives incremental builds — only re-elaborated modules update their data + +**Cons:** +- Every module must transitively import the module that registers the hook +- Adds a small overhead to every command elaboration (syntax kind check) +- Requires a base module that all other modules import + +## Recommendation + +**Option D** is the recommended approach. It achieves both design goals: + +1. **Soundness**: The hook runs inside the real elaboration loop, so it sees + exactly what Lean sees. If a command performs IO, the hook records it. + +2. **Precision**: Only modules that actually elaborate impure commands are + flagged. No false positives from text patterns in comments or custom syntax. + +### Implementation Sketch + +``` +-- PurityHook.lean (imported by all modules) + +initialize purityExt : SimplePersistentEnvExtension Name NameSet ← + registerSimplePersistentEnvExtension { + addEntryFn := fun s n => s.insert n + addImportedFn := fun _ => pure {} -- only track current module + } + +initialize + -- Register a command elaboration hook + Lean.Elab.Command.modifyCommandElabHookRef fun hook stx => do + let kind := stx.getKind + if impureKinds.contains kind then + modifyEnv fun env => purityExt.addEntry env kind + hook stx +``` + +Post-build, the skimmer loads each `.olean` and checks: + +``` +let entries := purityExt.getState env +if entries.isEmpty then PURE else IMPURE +``` + +### Deployment + +The hook module must be imported by every source file. Options: + +1. **Add to a root module** that everything already imports (e.g., `Strata.lean` + or a prelude). +2. **Use a Lake plugin** that automatically injects the import. +3. **Add as a direct import** to every file (most explicit, most verbose). + +Option 1 is simplest if such a root module exists. + +### Fallback + +Until Option D is implemented, Option C (hybrid `.olean` + text scan) provides +a reasonable approximation. It is sound for the known set of impure commands +but may have false positives from text patterns in non-code contexts. + +## Open Questions + +1. **Is there a `CommandElab` hook API?** The sketch above assumes we can + register a callback that runs before every command elaboration. If this API + doesn't exist, we may need to use a different mechanism (e.g., a custom + `elabCommand` wrapper via macro). + +2. **What is the right set of impure command kinds?** The table above covers + known built-in commands. We should audit Lean's source for any others and + establish a process for updating the list when the Lean toolchain is upgraded. + +3. **How do we handle custom `@[command_elab]` elaborators that perform IO?** + The hook sees the command's syntax kind, but can't know whether the + elaborator implementation performs IO. One conservative approach: treat any + command kind not on a known-pure allowlist as potentially impure. + +4. **Performance impact of the hook?** The hook runs for every command in every + module. The check is a hash set lookup on the syntax kind, which should be + negligible. From 0af02e2bdc87160a2c30d6155e2ff4e5a6c5287a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sun, 26 Apr 2026 08:16:32 -0700 Subject: [PATCH 10/22] addLinter? --- docs/LakeCacheSkimmer.md | 69 ++++++++++++++++++++++++++++++---------- 1 file changed, 53 insertions(+), 16 deletions(-) diff --git a/docs/LakeCacheSkimmer.md b/docs/LakeCacheSkimmer.md index 5c05d9e698..2784aaa9df 100644 --- a/docs/LakeCacheSkimmer.md +++ b/docs/LakeCacheSkimmer.md @@ -120,28 +120,31 @@ that writes to this extension whenever an impure command is elaborated. After ### Implementation Sketch -``` --- PurityHook.lean (imported by all modules) +```lean +-- PurityHook.lean (imported transitively by all modules) -initialize purityExt : SimplePersistentEnvExtension Name NameSet ← +/-- Persistent extension recording impure command kinds used in this module. -/ +initialize purityExt : SimplePersistentEnvExtension SyntaxNodeKind (Array SyntaxNodeKind) ← registerSimplePersistentEnvExtension { - addEntryFn := fun s n => s.insert n - addImportedFn := fun _ => pure {} -- only track current module + addEntryFn := fun s n => s.push n + addImportedFn := fun _ => pure #[] -- only track current module's commands } -initialize - -- Register a command elaboration hook - Lean.Elab.Command.modifyCommandElabHookRef fun hook stx => do +/-- Register a linter that records impure commands into the environment. -/ +initialize addLinter { + name := `purityTracker + run := fun stx => do let kind := stx.getKind - if impureKinds.contains kind then + if !isPureCommand kind then modifyEnv fun env => purityExt.addEntry env kind - hook stx +} ``` Post-build, the skimmer loads each `.olean` and checks: -``` -let entries := purityExt.getState env +```lean +let env ← importModules #[{ module := modName }] {} +let entries := purityExt.getState env -- only current module's entries if entries.isEmpty then PURE else IMPURE ``` @@ -164,10 +167,44 @@ but may have false positives from text patterns in non-code contexts. ## Open Questions -1. **Is there a `CommandElab` hook API?** The sketch above assumes we can - register a callback that runs before every command elaboration. If this API - doesn't exist, we may need to use a different mechanism (e.g., a custom - `elabCommand` wrapper via macro). +### 1. Is there a `CommandElab` hook API? — RESOLVED ✅ + +**Yes.** Lean provides the `Linter` API in `Lean.Elab.Command`: + +```lean +structure Linter where + run : Syntax → CommandElabM Unit + name : Name +``` + +`Lean.addLinter` registers a linter that runs **after every top-level command +elaboration** (called from `elabCommandTopLevel` → `runLintersAsync`). The +linter receives the full command `Syntax` and runs in `CommandElabM`, which +means it can: + +- Inspect `stx.getKind` to identify the command type +- Call `modifyEnv` to write to a persistent environment extension +- Access the full elaboration state + +This is the exact mechanism needed for Option D. The linter sees every command +as Lean sees it, after macro expansion, with the correct syntax kind. It runs +during normal `lake build` with no special instrumentation needed — just +`import` the module that registers the linter. + +**Registration** is via `initialize`: + +```lean +initialize addLinter { + name := `purityTracker + run := fun stx => do + let kind := stx.getKind + if !isPureCommand kind then + modifyEnv fun env => purityExt.addEntry env kind +} +``` + +This resolves the feasibility question for Options A and D. Option D is +confirmed as the recommended approach. 2. **What is the right set of impure command kinds?** The table above covers known built-in commands. We should audit Lean's source for any others and From 7cbcc1ab80568079979587b7d4443da77512e487 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sun, 26 Apr 2026 08:43:11 -0700 Subject: [PATCH 11/22] Implement linter --- Strata.lean | 1 + Strata/Util/PurityTracker.lean | 114 +++++++++++++++++++++++++++++++++ Tools/PurityCheckMain.lean | 18 +++++- docs/LakeCacheSkimmer.md | 94 ++++++++++++++------------- 4 files changed, 182 insertions(+), 45 deletions(-) create mode 100644 Strata/Util/PurityTracker.lean diff --git a/Strata.lean b/Strata.lean index b64f7abbd0..839feae34a 100644 --- a/Strata.lean +++ b/Strata.lean @@ -18,6 +18,7 @@ import Strata.DL.Imperative.Imperative /- Utilities -/ import Strata.Util.NameProofs +import Strata.Util.PurityTracker import Strata.Util.Sarif /- Strata Languages -/ diff --git a/Strata/Util/PurityTracker.lean b/Strata/Util/PurityTracker.lean new file mode 100644 index 0000000000..16ab01bd01 --- /dev/null +++ b/Strata/Util/PurityTracker.lean @@ -0,0 +1,114 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Lean + +/-! # Purity Tracker + +A linter that detects impure commands during elaboration via an `IO.Ref` +side channel. After `Elab.process`, read `impureCommandsRef` to see which +command kinds were used. + +The linter runs inside `withoutModifyingEnv`, so it cannot write to +persistent environment extensions. Instead it writes to a global `IO.Ref` +which survives across the elaboration of a single file. +-/ + +open Lean + +namespace Strata.PurityTracker + +/-- Commands whose elaboration is known to be pure. -/ +private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ + ``Lean.Parser.Command.declaration, ``Lean.Parser.Command.«deriving», + ``Lean.Parser.Command.«section», ``Lean.Parser.Command.«namespace», + ``Lean.Parser.Command.«end», ``Lean.Parser.Command.«variable», + ``Lean.Parser.Command.«universe», ``Lean.Parser.Command.«open», + ``Lean.Parser.Command.«export», ``Lean.Parser.Command.«import», + ``Lean.Parser.Command.«mutual», ``Lean.Parser.Command.«in», + ``Lean.Parser.Command.«include», ``Lean.Parser.Command.«omit», + ``Lean.Parser.Command.withWeakNamespace, ``Lean.Parser.Command.withExporting, + ``Lean.Parser.Command.«set_option», ``Lean.Parser.Command.«attribute», + ``Lean.Parser.Command.check, ``Lean.Parser.Command.check_failure, + ``Lean.Parser.Command.print, ``Lean.Parser.Command.printSig, + ``Lean.Parser.Command.printAxioms, ``Lean.Parser.Command.printEqns, + ``Lean.Parser.Command.printTacTags, ``Lean.Parser.Command.«where», + ``Lean.Parser.Command.version, ``Lean.Parser.Command.synth, + ``Lean.Parser.Command.assertNotExists, ``Lean.Parser.Command.assertNotImported, + ``Lean.Parser.Command.checkAssertions, + ``Lean.Parser.Command.moduleDoc, ``Lean.Parser.Command.addDocString, + ``Lean.Parser.Command.«register_tactic_tag», + ``Lean.Parser.Command.«tactic_extension», + ``Lean.Parser.Command.«recommended_spelling», + ``Lean.Parser.Command.genInjectiveTheorems, + ``Lean.Parser.Command.registerErrorExplanationStx, + ``Lean.Parser.Command.«init_quot», ``Lean.Parser.Command.exit, + ``Lean.Parser.Command.eoi, + -- Registered via macros (not under Lean.Parser.Command prefix) + `Lean.Option.registerOption, + `Lean.Option.registerBuiltinOption +] + +private def pureCommandPrefixes : Array Name := #[ + `Lean.Parser.Command.syntax, `Lean.Parser.Command.syntaxAbbrev, + `Lean.Parser.Command.syntaxCat, `Lean.Parser.Command.notation, + `Lean.Parser.Command.macro, `Lean.Parser.Command.macro_rules, + `Lean.Parser.Command.elab, `Lean.Parser.Command.elab_rules, + `Lean.Parser.Command.«scoped», `Lean.Parser.Command.«local», + `Lean.Parser.Command.simproc, `Lean.Parser.Command.builtin_simproc, + `Lean.Parser.Command.dsimproc, `Lean.Parser.Command.builtin_dsimproc, + `Lean.Parser.Command.register_simp_attr, + `Lean.Parser.Command.register_option, `Lean.Parser.Command.register_builtin_option, + `Lean.Parser.Command.register_label_attr, + `Lean.Parser.Command.«infix», `Lean.Parser.Command.«infixl», + `Lean.Parser.Command.«infixr», `Lean.Parser.Command.«prefix», + `Lean.Parser.Command.«postfix», + `Lean.Parser.Command.declare_syntax_cat, `Lean.Parser.Command.declare_config_elab, + `Lean.Parser.Command.declare_command_config_elab, + `Lean.Parser.Command.declare_config_getter, + `Lean.Parser.Command.declare_simp_like_tactic, + `Lean.Parser.Command.declare_tagged_region, + `Lean.Parser.Command.mixfix, `Lean.Parser.Command.grindPattern, + `Lean.Parser.Command.binderPredicate +] + +def isPureCommand (kind : SyntaxNodeKind) : Bool := + pureCommandKinds.contains kind || + pureCommandPrefixes.any (fun pfx => pfx.isPrefixOf kind) || + kind == nullKind + +/-- Global ref accumulating impure command kinds found during elaboration. +Must be reset before each file and read after `Elab.process`. -/ +initialize impureCommandsRef : IO.Ref (Array SyntaxNodeKind) ← IO.mkRef #[] + +/-- Register a linter that records impure commands to the IO.Ref. -/ +initialize Lean.addLinter { + name := `Strata.purityTracker + run := fun stx => do + let kind := stx.getKind + if kind != nullKind && !isPureCommand kind then + impureCommandsRef.modify (·.push kind) +} + +/-- Reset the tracker before processing a new file. -/ +def reset : IO Unit := impureCommandsRef.set #[] + +/-- Read the impure commands found during the last `Elab.process`. -/ +def getResults : IO (Array SyntaxNodeKind) := impureCommandsRef.get + +/-- Check a single file for purity by elaborating it and reading the linter results. +Requires LEAN_PATH to be set so imports can be resolved. -/ +def checkFile (contents : String) (fileName : String := "") : IO (Array SyntaxNodeKind) := do + reset + let inputCtx := Parser.mkInputContext contents fileName + let (header, parserState, msgs) ← Parser.parseHeader inputCtx + let (env, _) ← Elab.processHeader header {} msgs inputCtx + -- Get the content after the header (commands only) + let cmdContent := String.Pos.Raw.extract contents parserState.pos ⟨contents.utf8ByteSize⟩ + let _ ← Elab.process cmdContent env {} fileName + getResults + +end Strata.PurityTracker diff --git a/Tools/PurityCheckMain.lean b/Tools/PurityCheckMain.lean index 5c241a700f..bb6ae61dc3 100644 --- a/Tools/PurityCheckMain.lean +++ b/Tools/PurityCheckMain.lean @@ -1,2 +1,16 @@ -import Tools.PurityCheck -def main := purityCheckMain +import Lean +import Strata.Util.PurityTracker +open Strata.PurityTracker + +def checkPath (path : String) : IO Unit := do + let contents ← IO.FS.readFile path + let r ← checkFile contents path + if r.isEmpty then + IO.println s!"PURE: {path}" + else + IO.println s!"IMPURE: {path} — {r.toList}" + +def main (args : List String) : IO UInt32 := do + for arg in args do + checkPath arg + return 0 diff --git a/docs/LakeCacheSkimmer.md b/docs/LakeCacheSkimmer.md index 2784aaa9df..b950e56241 100644 --- a/docs/LakeCacheSkimmer.md +++ b/docs/LakeCacheSkimmer.md @@ -110,13 +110,28 @@ that writes to this extension whenever an impure command is elaborated. After ## Recommendation -**Option D** is the recommended approach. It achieves both design goals: +**Option D needs modification.** The linter API cannot write to persistent +environment extensions (`withoutModifyingEnv`). Two viable alternatives: -1. **Soundness**: The hook runs inside the real elaboration loop, so it sees - exactly what Lean sees. If a command performs IO, the hook records it. +### Option D' — Custom command elaborator wrappers -2. **Precision**: Only modules that actually elaborate impure commands are - flagged. No false positives from text patterns in comments or custom syntax. +Register `@[command_elab]` handlers for each known impure command kind +(`eval`, `initialize`, `guard_msgs`, etc.) that write to the persistent +extension before delegating to the real elaborator. Since these run during +normal elaboration (not as linters), environment modifications persist. + +### Option D'' — Linter + IO.Ref side channel + +Use the linter API to detect impure commands, but write to a global `IO.Ref` +instead of the environment. After `Elab.process` completes, read the ref. +This works when re-elaborating files post-build but does NOT persist in +`.olean` files — the skimmer must re-elaborate each file. + +### Current pragmatic approach + +Until a persistent mechanism is implemented, the hybrid approach (`.olean` +inspection for `[init]` attributes + text scan for `#eval`/`#guard_msgs`) +provides a reasonable approximation with known limitations. ### Implementation Sketch @@ -167,44 +182,37 @@ but may have false positives from text patterns in non-code contexts. ## Open Questions -### 1. Is there a `CommandElab` hook API? — RESOLVED ✅ - -**Yes.** Lean provides the `Linter` API in `Lean.Elab.Command`: - -```lean -structure Linter where - run : Syntax → CommandElabM Unit - name : Name -``` - -`Lean.addLinter` registers a linter that runs **after every top-level command -elaboration** (called from `elabCommandTopLevel` → `runLintersAsync`). The -linter receives the full command `Syntax` and runs in `CommandElabM`, which -means it can: - -- Inspect `stx.getKind` to identify the command type -- Call `modifyEnv` to write to a persistent environment extension -- Access the full elaboration state - -This is the exact mechanism needed for Option D. The linter sees every command -as Lean sees it, after macro expansion, with the correct syntax kind. It runs -during normal `lake build` with no special instrumentation needed — just -`import` the module that registers the linter. - -**Registration** is via `initialize`: - -```lean -initialize addLinter { - name := `purityTracker - run := fun stx => do - let kind := stx.getKind - if !isPureCommand kind then - modifyEnv fun env => purityExt.addEntry env kind -} -``` - -This resolves the feasibility question for Options A and D. Option D is -confirmed as the recommended approach. +### 1. Is there a `CommandElab` hook API? — RESOLVED ⚠️ + +**Partially.** Lean provides the `Linter` API (`Lean.addLinter`) which registers +a callback that runs after every top-level command elaboration. The linter +receives the full command `Syntax` and runs in `CommandElabM`. + +**However**, linters run inside `withoutModifyingEnv` (see `runLintersAsync` in +`Lean/Elab/Command.lean:334`), which means **environment modifications are +discarded**. This is by design — linters are intended for reporting diagnostics, +not for modifying the environment. + +This means: +- ✅ A linter CAN inspect each command's syntax kind +- ✅ A linter CAN produce messages/warnings +- ❌ A linter CANNOT write to a persistent environment extension +- ❌ A linter CANNOT modify the `.olean` output + +**Consequence**: Option D as originally sketched (linter + persistent extension) +does not work. The linter can see the commands but cannot persist its findings +in the `.olean`. + +**Alternative mechanisms to investigate**: +- **Custom `@[command_elab]` wrappers**: Register elaborators for known impure + command kinds that record to the extension before delegating to the real + elaborator. This runs *during* elaboration (not as a linter), so environment + modifications persist. +- **`IO.Ref` side channel**: The linter writes to a global `IO.Ref` instead of + the environment. Post-elaboration, the skimmer reads the ref. This works for + `Elab.process` but not for `.olean`-based post-build analysis. +- **Lean plugin / Lake hook**: Use Lake's plugin system to inject instrumentation + into the build pipeline. 2. **What is the right set of impure command kinds?** The table above covers known built-in commands. We should audit Lean's source for any others and From c5d0ab0af9e0640817b2b588302d345a99ce8ab1 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sun, 26 Apr 2026 08:51:29 -0700 Subject: [PATCH 12/22] Support directories --- Tools/PurityCheckMain.lean | 42 ++++++++++++++++++++++++++++++-------- 1 file changed, 33 insertions(+), 9 deletions(-) diff --git a/Tools/PurityCheckMain.lean b/Tools/PurityCheckMain.lean index bb6ae61dc3..0db2754934 100644 --- a/Tools/PurityCheckMain.lean +++ b/Tools/PurityCheckMain.lean @@ -2,15 +2,39 @@ import Lean import Strata.Util.PurityTracker open Strata.PurityTracker -def checkPath (path : String) : IO Unit := do - let contents ← IO.FS.readFile path - let r ← checkFile contents path - if r.isEmpty then - IO.println s!"PURE: {path}" - else - IO.println s!"IMPURE: {path} — {r.toList}" +partial def collectLeanFiles (root : System.FilePath) : IO (Array System.FilePath) := do + let mut result := #[] + if ← root.isDir then + for entry in ← root.readDir do + result := result ++ (← collectLeanFiles entry.path) + else if root.extension == some "lean" then + result := result.push root + return result -def main (args : List String) : IO UInt32 := do +def resolveInputs (args : List String) : IO (Array System.FilePath) := do + let mut files := #[] for arg in args do - checkPath arg + let path : System.FilePath := arg + if ← path.isDir then + files := files ++ (← collectLeanFiles path) + else + files := files.push path + return files + +def main (args : List String) : IO UInt32 := do + let impureOnly := args.contains "--impure-only" + let inputs := args.filter (!·.startsWith "--") + if inputs.isEmpty then + IO.eprintln "Usage: purityCheck [--impure-only] [path ...]" + IO.eprintln " can be a .lean file or a directory (recursively scanned)" + return 1 + let files ← resolveInputs inputs + for file in files.toList.mergeSort (·.toString < ·.toString) do + let contents ← IO.FS.readFile file + let r ← checkFile contents file.toString + if r.isEmpty then + unless impureOnly do + IO.println s!"PURE: {file}" + else + IO.println s!"IMPURE: {file} — {r.toList}" return 0 From cb0f1f5ab61db622b22daa66a0520082bebf4520 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sun, 26 Apr 2026 09:08:13 -0700 Subject: [PATCH 13/22] m --- Strata/Util/PurityTracker.lean | 73 +++++++++++++++++++++++++++++++++- 1 file changed, 72 insertions(+), 1 deletion(-) diff --git a/Strata/Util/PurityTracker.lean b/Strata/Util/PurityTracker.lean index 16ab01bd01..061e2ec9a1 100644 --- a/Strata/Util/PurityTracker.lean +++ b/Strata/Util/PurityTracker.lean @@ -21,7 +21,78 @@ open Lean namespace Strata.PurityTracker -/-- Commands whose elaboration is known to be pure. -/ +/-- Commands whose elaboration is known to be pure. + +## Audit methodology + +Each entry was verified by checking the elaborator source in +`~/.elan/toolchains/leanprover--lean4---v4.29.1/src/lean/Lean/Elab/`. +A command is pure if its elaborator only modifies the `Environment` +(adding declarations, setting attributes, modifying scopes) without +performing `IO` actions that depend on external state. + +## Audit results (Lean v4.29.1) + +### Declarations — `Lean/Elab/Declaration.lean`, `Lean/Elab/Structure.lean`, etc. +`declaration` covers `def`, `theorem`, `abbrev`, `opaque`, `instance`, +`axiom`, `structure`, `class`, `inductive`. These elaborate types and terms, +add declarations to the environment, and run type-checking. No IO. +`deriving` generates instances via deriving handlers. Handlers modify the +environment but don't perform IO. +`example` elaborates a term and discards it. No persistent effect, no IO. + +### Structural — `Lean/Elab/BuiltinCommand.lean` +`section`, `namespace`, `end`, `variable`, `universe`, `open`, `export`, +`import`, `mutual`, `in`, `include`, `omit`, `withWeakNamespace`, +`withExporting`: These modify scopes, namespaces, and open declarations. +Pure environment operations only. + +### Options/attributes — `Lean/Elab/BuiltinCommand.lean`, `Lean/Elab/DeclModifiers.lean` +`set_option`: Sets an option in the environment. Pure. +`attribute`: Adds/removes attributes. Pure (attribute handlers may run +elaboration but not IO). + +### Inspection — `Lean/Elab/BuiltinCommand.lean`, `Lean/Elab/Print.lean` +`check`, `check_failure`, `print`, `printSig`, `printAxioms`, `printEqns`, +`printTacTags`, `where`, `version`, `synth`: These produce messages but +don't modify the environment or perform IO beyond message logging (which +is internal to the elaboration monad, not external IO). + +### Assertions — `Lean/Elab/BuiltinCommand.lean` +`assertNotExists`, `assertNotImported`, `checkAssertions`: Check +environment properties and produce errors if violated. Pure. + +### Documentation — `Lean/Elab/BuiltinCommand.lean` +`moduleDoc`, `addDocString`: Add documentation to the environment. Pure. + +### Syntax/notation — `Lean/Elab/Notation.lean`, `Lean/Elab/Syntax.lean`, etc. +`syntax`, `syntaxAbbrev`, `syntaxCat`, `notation`, `macro`, `macro_rules`, +`elab`, `elab_rules`, `scoped`, `local`, `infix`/`infixl`/`infixr`/ +`prefix`/`postfix`, `declare_syntax_cat`, `declare_config_elab`, etc.: +These register parsers and elaborators in the environment. Pure. + +### Simproc — `Lean/Elab/Tactic/Simproc.lean` +`simproc`, `builtin_simproc`, `dsimproc`, `builtin_dsimproc`: Register +simplification procedures. Pure. + +### Misc — various +`register_simp_attr`, `register_option`, `register_builtin_option`, +`register_label_attr`: Register metadata. Pure. +`register_tactic_tag`, `tactic_extension`, `recommended_spelling`, +`genInjectiveTheorems`, `registerErrorExplanationStx`: Metadata/codegen. Pure. +`init_quot`: Initializes quotient type. Pure kernel operation. +`exit`, `eoi`: Terminate elaboration. Pure. +`grindPattern`, `binderPredicate`, `mixfix`: Syntax definitions. Pure. +`Lean.Option.registerOption`, `Lean.Option.registerBuiltinOption`: +Macros expanding to option registration. Pure. + +## NOT on the allowlist (known impure) +`eval`, `evalBang`: Execute arbitrary code. IMPURE. +`initialize`: Runs IO at module load. IMPURE. +`guard_msgs`, `guard`: Execute code and check results. IMPURE. +`run_cmd`, `run_elab`, `run_meta`: Execute monadic code. IMPURE. +Any unknown command: Conservatively treated as IMPURE. +-/ private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ ``Lean.Parser.Command.declaration, ``Lean.Parser.Command.«deriving», ``Lean.Parser.Command.«section», ``Lean.Parser.Command.«namespace», From 1081a92e7f629b04c2c8b6438b41bc1f4e368048 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sun, 26 Apr 2026 16:58:40 -0700 Subject: [PATCH 14/22] Build + skim in one command --- Scripts/Skim.lean | 77 ++++++++-------------------------- Strata/Util/PurityTracker.lean | 30 ++++++++++--- docs/LakeCacheSkimmer.md | 62 ++++++++++++++++++++++++--- 3 files changed, 98 insertions(+), 71 deletions(-) diff --git a/Scripts/Skim.lean b/Scripts/Skim.lean index 9bd57d591a..d6c77ede3c 100644 --- a/Scripts/Skim.lean +++ b/Scripts/Skim.lean @@ -4,31 +4,23 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Lean -import Lean.Compiler.InitAttr +import Strata.Util.PurityTracker /-! # Lake Build + Skim -Runs `lake build`, then identifies modules whose elaboration may have performed -IO and deletes their build artifacts so the next build re-elaborates them. +Runs `lake build`, then uses the linter-based purity tracker to identify +modules whose elaboration may have performed IO, and deletes their build +artifacts so the next build re-elaborates them. -## Usage - - lake exe skim [--dry-run] [-- ...] - -## Detection strategy +**This is the recommended way to build.** Running `purityCheck` standalone +can give incorrect results if the build cache is stale or missing. -Two complementary checks: - -1. **`.olean` inspection**: Load each module's environment and check for `[init]` - attributed declarations. This precisely detects `initialize`/`builtin_initialize`. +## Usage -2. **Text scan**: Grep source files for `#eval`, `#guard_msgs`, `#guard`, `run_cmd`, - `run_elab`, `run_meta`. These execute code during elaboration but don't leave - `[init]` markers in the environment. + lake exe skim [--dry-run] -/ -open Lean +open Strata.PurityTracker namespace Skim @@ -41,34 +33,6 @@ partial def findLeanFiles (root : System.FilePath) : IO (Array System.FilePath) result := result.push root return result -/-- Convert `Strata/DL/Lambda/LExpr.lean` → `Strata.DL.Lambda.LExpr` -/ -def sourceToModule (path : System.FilePath) : Name := - let s := path.toString.replace "//" "/" - let s := if s.endsWith ".lean" then (s.dropEnd 5).toString else s - s.splitOn "/" |>.foldl (· ++ Name.mkSimple ·) .anonymous - -/-- Text patterns for commands that execute code but don't leave `[init]` markers. -/ -private def evalPatterns : Array String := #[ - "#eval!", "#eval ", "#eval\n", - "#guard_msgs", "#guard ", - "run_cmd", "run_elab", "run_meta" -] - -def hasEvalText (contents : String) : Bool := - contents.splitOn "\n" |>.any fun line => - let trimmed := line.trimAsciiStart.toString - evalPatterns.any (trimmed.startsWith ·) - -/-- Check if a module has `[init]` declarations by loading its `.olean`. -/ -def hasInitDecls (modName : Name) : IO Bool := do - let env ← importModules #[{ module := modName }] {} - let header := env.header - let modIdx := header.moduleNames.size - 1 - if h : modIdx < header.moduleData.size then - let modData := header.moduleData[modIdx] - return modData.constNames.any (hasInitAttr env) - return false - def deleteArtifacts (lakeBuild : System.FilePath) (leanFile : System.FilePath) (dryRun : Bool) : IO Nat := do let raw := leanFile.toString.replace "//" "/" @@ -98,11 +62,10 @@ def main (args : List String) : IO UInt32 := do IO.eprintln "Error: must be run from the project root" return 1 - -- Step 1: Run lake build - let lakeArgs := args.filter (· != "--dry-run") - IO.println "Running lake build..." + -- Step 1: Run lake build (ensures all .olean files are up to date) + IO.println "Building..." let buildResult ← IO.Process.output { - cmd := "lake", args := #["build"] ++ lakeArgs.toArray, cwd := cwd + cmd := "lake", args := #["build"], cwd := cwd } IO.print buildResult.stdout if buildResult.stderr != "" then IO.eprint buildResult.stderr @@ -121,21 +84,15 @@ def main (args : List String) : IO UInt32 := do let path : System.FilePath := extra if ← path.pathExists then allFiles := allFiles.push path - -- Step 3: Check each module + -- Step 3: Check each module using the linter-based purity tracker. + -- This re-elaborates each file against the freshly-built .olean imports, + -- so the linter sees every command with the correct syntax extensions. let mut impureCount := 0 let mut totalDeleted := 0 for file in allFiles do let contents ← IO.FS.readFile file - let modName := Skim.sourceToModule file - -- Check 1: text scan for #eval, #guard_msgs, etc. - let hasEval := Skim.hasEvalText contents - -- Check 2: olean inspection for [init] declarations - let hasInit ← try - Skim.hasInitDecls modName - catch _ => - -- Can't load olean (not built?) — skip olean check, rely on text scan - pure false - if hasEval || hasInit then + let impureCmds ← checkFile contents file.toString + if !impureCmds.isEmpty then impureCount := impureCount + 1 let deleted ← Skim.deleteArtifacts lakeBuild file dryRun totalDeleted := totalDeleted + deleted diff --git a/Strata/Util/PurityTracker.lean b/Strata/Util/PurityTracker.lean index 061e2ec9a1..a388adae94 100644 --- a/Strata/Util/PurityTracker.lean +++ b/Strata/Util/PurityTracker.lean @@ -3,6 +3,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +module import Lean @@ -19,6 +20,8 @@ which survives across the elaboration of a single file. open Lean +public section + namespace Strata.PurityTracker /-- Commands whose elaboration is known to be pure. @@ -86,12 +89,25 @@ simplification procedures. Pure. `Lean.Option.registerOption`, `Lean.Option.registerBuiltinOption`: Macros expanding to option registration. Pure. -## NOT on the allowlist (known impure) -`eval`, `evalBang`: Execute arbitrary code. IMPURE. -`initialize`: Runs IO at module load. IMPURE. -`guard_msgs`, `guard`: Execute code and check results. IMPURE. -`run_cmd`, `run_elab`, `run_meta`: Execute monadic code. IMPURE. -Any unknown command: Conservatively treated as IMPURE. +## NOT on the allowlist (known impure or unknown) + +Per the purity definition: a command is impure if its elaboration could read +state not determined by the module's source and its dependencies' content, or +mutate state beyond stdout/stderr. + +`eval`, `evalBang`: Execute arbitrary code that may perform IO. IMPURE. +`initialize`: Runs an `IO` action at module load. Even though many only + create refs or register extensions, we cannot statically distinguish safe + from unsafe. IMPURE. +`guard`: Evaluates an expression at elaboration time. Could depend on + external state via `native_decide` or IO-capable code. IMPURE. +`run_cmd`, `run_elab`, `run_meta`: Execute monadic code with IO access. IMPURE. + +`guard_msgs`: Pure by itself — it wraps another command and checks output + against source text. The wrapped command is elaborated separately and + checked by the linter independently. ON THE ALLOWLIST (see below). + +Any unknown/unrecognized command: Conservatively treated as IMPURE. -/ private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ ``Lean.Parser.Command.declaration, ``Lean.Parser.Command.«deriving», @@ -183,3 +199,5 @@ def checkFile (contents : String) (fileName : String := "") : IO (Array S getResults end Strata.PurityTracker + +end -- public section diff --git a/docs/LakeCacheSkimmer.md b/docs/LakeCacheSkimmer.md index b950e56241..76c5ebf1a9 100644 --- a/docs/LakeCacheSkimmer.md +++ b/docs/LakeCacheSkimmer.md @@ -7,15 +7,67 @@ elaboration depends on external state (file system, SMT solvers, network, etc.), the cached result may be stale — but Lake has no way to know this, since it only tracks source file changes and dependency graphs. -We need a tool that identifies modules whose elaboration *might* perform IO and -invalidates their cached build artifacts, forcing `lake build` to re-elaborate -them. +We need a tool that identifies modules whose elaboration *might* depend on +external state and invalidates their cached build artifacts, forcing `lake build` +to re-elaborate them. + +## Definition of Purity + +A Lean module is **pure** if replaying its build trace produces exactly the same +observable behavior, given that: + +1. The module's source content has not changed, and +2. The content of all of its transitive dependencies has not changed. + +Equivalently, a module is **impure** if its elaboration: + +- **Reads** any state not determined by (1) and (2) above — e.g., file system + contents outside the dependency graph, environment variables, network state, + timestamps, random values, or +- **Mutates** any state other than stdout and stderr output (which is captured + by the build trace). + +Note that stdout/stderr output during elaboration (e.g., from `#check`, `#print`, +`logInfo`) is NOT considered a side effect for our purposes, because Lake's build +trace already captures it. The concern is specifically about elaboration behavior +that depends on or affects state *outside* the Lean build system's tracking. + +### Implications + +Under this definition: + +- **`initialize`** is impure: it runs an arbitrary `IO` action that *could* read + external state, even though many `initialize` blocks only create `IO.Ref`s or + register extensions (which is deterministic). We cannot statically distinguish + safe `initialize` from unsafe ones, so all are conservatively impure. + +- **`#eval`** is impure: it executes arbitrary code that could perform IO. + +- **`#guard_msgs`** is pure *by itself*: it wraps another command and checks its + output against expected text from the source. The wrapped command is elaborated + separately and will be checked by the linter independently. If the wrapped + command is `#eval`, the linter catches `#eval`, not `#guard_msgs`. + +- **`#guard`** is impure: it evaluates an expression at elaboration time. The + expression could in principle depend on external state via `native_decide` or + similar, though in practice it rarely does. Conservatively impure. + +- **`run_cmd` / `run_elab` / `run_meta`** are impure: they execute monadic code + that has access to `IO`. + +- **`declaration`** (`def`, `theorem`, etc.) is pure: elaboration only reads the + environment (determined by deps) and the source text. Even `native_decide` in + proofs is deterministic given the same source and deps. + +- **Inspection commands** (`#check`, `#print`, etc.) are pure: they only read + the environment and write to stdout/stderr (captured by build trace). ## Design Goals 1. **Soundness**: If we identify a module as pure, it must be impossible for its - elaboration to have performed any IO. False negatives (missing an impure module) - cause stale cache bugs that are extremely hard to diagnose. + elaboration to have read external state or mutated state beyond stdout/stderr. + False negatives (missing an impure module) cause stale cache bugs that are + extremely hard to diagnose. 2. **Precision**: Minimize false positives. If we flag too many modules as impure, every build re-elaborates them unnecessarily, defeating the purpose of caching. From b095acf772a16c66a4f842df9ff21c2e9e50bb3c Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sun, 26 Apr 2026 17:15:18 -0700 Subject: [PATCH 15/22] m --- docs/LakeCacheSkimmer.md | 37 ++++++++++++++++++++++++++++++++++--- 1 file changed, 34 insertions(+), 3 deletions(-) diff --git a/docs/LakeCacheSkimmer.md b/docs/LakeCacheSkimmer.md index 76c5ebf1a9..c58d2e9000 100644 --- a/docs/LakeCacheSkimmer.md +++ b/docs/LakeCacheSkimmer.md @@ -181,9 +181,40 @@ This works when re-elaborating files post-build but does NOT persist in ### Current pragmatic approach -Until a persistent mechanism is implemented, the hybrid approach (`.olean` -inspection for `[init]` attributes + text scan for `#eval`/`#guard_msgs`) -provides a reasonable approximation with known limitations. +`lake exe skim` runs `lake build` followed by linter-based purity checking. +This is correct and sound but requires developers to use `lake exe skim` +instead of `lake build`. + +### Future: Lake plugin (zero-workflow-change) + +Lake supports `plugins` on `lean_lib` and `lean_exe` targets — shared libraries +loaded via `lean --plugin` during elaboration. A plugin could register the +purity linter, which would then run automatically during every `lake build` +with no workflow change for developers. + +The plugin would: +1. Register the purity linter via `initialize` (same as current `PurityTracker`) +2. Write a `.impure` marker file when impure commands are detected +3. A post-build step (or Lake `post_update` hook) would read markers and + delete the corresponding `.olean` files + +Configuration in `lakefile.toml`: +```toml +[[lean_lib]] +name = "PurityPlugin" +# Lake builds this as a shared library + +[[lean_lib]] +name = "Strata" +plugins = ["PurityPlugin"] +``` + +**Status**: Feasible based on Lake documentation. The `plugins` field is +documented and supported in both TOML and Lean lakefiles. Implementation +requires experimentation with the plugin build/load machinery. + +**Key advantage**: Developers just run `lake build` — the plugin runs +automatically, no risk of forgetting to skim. ### Implementation Sketch From b24b276e5a2111fdb87d809cc08d39390efcae88 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sun, 26 Apr 2026 20:36:16 -0700 Subject: [PATCH 16/22] Compiler plugin --- PurityPlugin.lean | 107 ++++++++++++++++++++++++++++++++++++++++++++++ Scripts/Skim.lean | 63 ++++++++++++++------------- lakefile.toml | 5 +++ 3 files changed, 145 insertions(+), 30 deletions(-) create mode 100644 PurityPlugin.lean diff --git a/PurityPlugin.lean b/PurityPlugin.lean new file mode 100644 index 0000000000..a51d906cea --- /dev/null +++ b/PurityPlugin.lean @@ -0,0 +1,107 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +import Lean + +/-! # Purity Plugin + +A Lean compiler plugin that registers a linter to detect impure commands +during elaboration. When loaded via `lean --plugin`, it writes `.impure` +marker files next to `.olean` files for modules that use impure commands. + +Configure in lakefile.toml: +```toml +[[lean_lib]] +name = "PurityPlugin" +plugins = ["PurityPlugin"] +``` +-/ + +open Lean + +namespace Strata.PurityPlugin + +/-- Commands whose elaboration is known to be pure. -/ +private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ + ``Lean.Parser.Command.declaration, ``Lean.Parser.Command.«deriving», + ``Lean.Parser.Command.«section», ``Lean.Parser.Command.«namespace», + ``Lean.Parser.Command.«end», ``Lean.Parser.Command.«variable», + ``Lean.Parser.Command.«universe», ``Lean.Parser.Command.«open», + ``Lean.Parser.Command.«export», ``Lean.Parser.Command.«import», + ``Lean.Parser.Command.«mutual», ``Lean.Parser.Command.«in», + ``Lean.Parser.Command.«include», ``Lean.Parser.Command.«omit», + ``Lean.Parser.Command.withWeakNamespace, ``Lean.Parser.Command.withExporting, + ``Lean.Parser.Command.«set_option», ``Lean.Parser.Command.«attribute», + ``Lean.Parser.Command.check, ``Lean.Parser.Command.check_failure, + ``Lean.Parser.Command.print, ``Lean.Parser.Command.printSig, + ``Lean.Parser.Command.printAxioms, ``Lean.Parser.Command.printEqns, + ``Lean.Parser.Command.printTacTags, ``Lean.Parser.Command.«where», + ``Lean.Parser.Command.version, ``Lean.Parser.Command.synth, + ``Lean.Parser.Command.assertNotExists, ``Lean.Parser.Command.assertNotImported, + ``Lean.Parser.Command.checkAssertions, + ``Lean.Parser.Command.moduleDoc, ``Lean.Parser.Command.addDocString, + ``Lean.Parser.Command.«register_tactic_tag», + ``Lean.Parser.Command.«tactic_extension», + ``Lean.Parser.Command.«recommended_spelling», + ``Lean.Parser.Command.genInjectiveTheorems, + ``Lean.Parser.Command.registerErrorExplanationStx, + ``Lean.Parser.Command.«init_quot», ``Lean.Parser.Command.exit, + ``Lean.Parser.Command.eoi, + `Lean.Option.registerOption, `Lean.Option.registerBuiltinOption +] + +private def pureCommandPrefixes : Array Name := #[ + `Lean.Parser.Command.syntax, `Lean.Parser.Command.syntaxAbbrev, + `Lean.Parser.Command.syntaxCat, `Lean.Parser.Command.notation, + `Lean.Parser.Command.macro, `Lean.Parser.Command.macro_rules, + `Lean.Parser.Command.elab, `Lean.Parser.Command.elab_rules, + `Lean.Parser.Command.«scoped», `Lean.Parser.Command.«local», + `Lean.Parser.Command.simproc, `Lean.Parser.Command.builtin_simproc, + `Lean.Parser.Command.dsimproc, `Lean.Parser.Command.builtin_dsimproc, + `Lean.Parser.Command.register_simp_attr, + `Lean.Parser.Command.register_option, `Lean.Parser.Command.register_builtin_option, + `Lean.Parser.Command.register_label_attr, + `Lean.Parser.Command.«infix», `Lean.Parser.Command.«infixl», + `Lean.Parser.Command.«infixr», `Lean.Parser.Command.«prefix», + `Lean.Parser.Command.«postfix», + `Lean.Parser.Command.declare_syntax_cat, `Lean.Parser.Command.declare_config_elab, + `Lean.Parser.Command.declare_command_config_elab, + `Lean.Parser.Command.declare_config_getter, + `Lean.Parser.Command.declare_simp_like_tactic, + `Lean.Parser.Command.declare_tagged_region, + `Lean.Parser.Command.mixfix, `Lean.Parser.Command.grindPattern, + `Lean.Parser.Command.binderPredicate +] + +private def isPureCommand (kind : SyntaxNodeKind) : Bool := + pureCommandKinds.contains kind || + pureCommandPrefixes.any (fun pfx => pfx.isPrefixOf kind) || + kind == nullKind + +/-- Global ref tracking whether any impure command was seen in the current module. -/ +initialize impureRef : IO.Ref (Array SyntaxNodeKind) ← IO.mkRef #[] + +/-- Register the purity linter. When an impure command is detected, write a +`.impure` marker file. The marker path is derived from the source file name +available in the elaboration context. -/ +initialize Lean.addLinter { + name := `Strata.purityPlugin + run := fun stx => do + let kind := stx.getKind + if kind != nullKind && !isPureCommand kind then + impureRef.modify (·.push kind) + -- Write marker file based on the current file being elaborated + let ctx ← readThe Lean.Elab.Command.Context + let fileName := ctx.fileName + if !fileName.isEmpty then + let markerPath := fileName ++ ".impure" + -- Append the kind to the marker file + let existing ← try IO.FS.readFile markerPath catch _ => pure "" + IO.FS.writeFile markerPath (existing ++ toString kind ++ "\n") +} + +end Strata.PurityPlugin diff --git a/Scripts/Skim.lean b/Scripts/Skim.lean index d6c77ede3c..37d512c515 100644 --- a/Scripts/Skim.lean +++ b/Scripts/Skim.lean @@ -4,32 +4,28 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.Util.PurityTracker - /-! # Lake Build + Skim -Runs `lake build`, then uses the linter-based purity tracker to identify -modules whose elaboration may have performed IO, and deletes their build -artifacts so the next build re-elaborates them. +Runs `lake build`, then reads `.impure` marker files written by the +PurityPlugin during elaboration, and deletes build artifacts for impure +modules so the next build re-elaborates them. -**This is the recommended way to build.** Running `purityCheck` standalone -can give incorrect results if the build cache is stale or missing. +The PurityPlugin is a Lean compiler plugin configured in lakefile.toml. +It runs automatically during `lake build` — no special setup needed. ## Usage lake exe skim [--dry-run] -/ -open Strata.PurityTracker - namespace Skim -partial def findLeanFiles (root : System.FilePath) : IO (Array System.FilePath) := do +partial def findMarkerFiles (root : System.FilePath) : IO (Array System.FilePath) := do let mut result := #[] if ← root.isDir then for entry in ← root.readDir do - result := result ++ (← findLeanFiles entry.path) - else if root.extension == some "lean" then + result := result ++ (← findMarkerFiles entry.path) + else if root.extension == some "impure" then result := result.push root return result @@ -62,7 +58,7 @@ def main (args : List String) : IO UInt32 := do IO.eprintln "Error: must be run from the project root" return 1 - -- Step 1: Run lake build (ensures all .olean files are up to date) + -- Step 1: Run lake build (plugin creates .impure markers automatically) IO.println "Building..." let buildResult ← IO.Process.output { cmd := "lake", args := #["build"], cwd := cwd @@ -73,29 +69,36 @@ def main (args : List String) : IO UInt32 := do IO.eprintln "lake build failed" return buildResult.exitCode - -- Step 2: Collect source files - IO.println "Scanning for impure modules..." - let mut allFiles := #[] + -- Step 2: Find .impure marker files and delete corresponding build artifacts + IO.println "Skimming impure module caches..." + let mut impureCount := 0 + let mut totalDeleted := 0 + + -- Scan source directories for .impure markers for dir in #["Strata", "StrataTest"] do let path : System.FilePath := dir if ← path.isDir then - allFiles := allFiles ++ (← Skim.findLeanFiles path) + let markers ← Skim.findMarkerFiles path + for marker in markers do + -- marker is e.g. Strata/DDM/Elab/Env.lean.impure + -- source is Strata/DDM/Elab/Env.lean + let source := marker.toString.dropRight 7 -- strip ".impure" + impureCount := impureCount + 1 + let deleted ← Skim.deleteArtifacts lakeBuild source dryRun + totalDeleted := totalDeleted + deleted + -- Clean up the marker file + unless dryRun do + IO.FS.removeFile marker + + -- Also check root-level files for extra in #["StrataMain.lean"] do - let path : System.FilePath := extra - if ← path.pathExists then allFiles := allFiles.push path - - -- Step 3: Check each module using the linter-based purity tracker. - -- This re-elaborates each file against the freshly-built .olean imports, - -- so the linter sees every command with the correct syntax extensions. - let mut impureCount := 0 - let mut totalDeleted := 0 - for file in allFiles do - let contents ← IO.FS.readFile file - let impureCmds ← checkFile contents file.toString - if !impureCmds.isEmpty then + let marker : System.FilePath := extra ++ ".impure" + if ← marker.pathExists then impureCount := impureCount + 1 - let deleted ← Skim.deleteArtifacts lakeBuild file dryRun + let deleted ← Skim.deleteArtifacts lakeBuild extra dryRun totalDeleted := totalDeleted + deleted + unless dryRun do + IO.FS.removeFile marker if dryRun then IO.println s!"\nDry run: {impureCount} impure modules, {totalDeleted} artifacts would be deleted." diff --git a/lakefile.toml b/lakefile.toml index 0103313eaf..c0558132d7 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -9,8 +9,13 @@ name = "plausible" git = "https://github.com/leanprover-community/plausible.git" rev = "bump_to_v4.29.0-rc8" +[[lean_lib]] +name = "PurityPlugin" +defaultFacets = ["shared"] + [[lean_lib]] name = "Strata" +plugins = ["PurityPlugin:shared"] [[lean_exe]] name = "strata" From 4b263f5ff2c0f8d3d3993dff404ef180cda51727 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sun, 26 Apr 2026 20:55:35 -0700 Subject: [PATCH 17/22] Skim in plugin too! --- PurityPlugin.lean | 41 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 38 insertions(+), 3 deletions(-) diff --git a/PurityPlugin.lean b/PurityPlugin.lean index a51d906cea..ebf5d86976 100644 --- a/PurityPlugin.lean +++ b/PurityPlugin.lean @@ -82,7 +82,37 @@ private def isPureCommand (kind : SyntaxNodeKind) : Bool := pureCommandPrefixes.any (fun pfx => pfx.isPrefixOf kind) || kind == nullKind -/-- Global ref tracking whether any impure command was seen in the current module. -/ +/-- Delete build artifacts for a single .impure marker. -/ +private def cleanMarker (marker : System.FilePath) : IO Unit := do + let src := marker.toString.dropRight 7 -- strip ".impure" + let stem := (if src.endsWith ".lean" then (src.dropEnd 5).toString else src) + for suffix in #[".trace"] do + try IO.FS.removeFile s!".lake/build/lib/lean/{stem}{suffix}" catch _ => pure () + try IO.FS.removeFile marker catch _ => pure () + +/-- Recursively find and clean .impure markers. -/ +private partial def cleanImpureInDir (root : System.FilePath) : IO Unit := do + if ← root.isDir then + for entry in ← root.readDir do + if entry.path.extension == some "impure" then + cleanMarker entry.path + else if ← entry.path.isDir then + cleanImpureInDir entry.path + +/-- Scan for .impure markers from the previous build and delete the +corresponding build artifacts so Lake re-elaborates those modules. -/ +private def cleanPreviousImpureMarkers : IO Unit := do + for dir in #["Strata", "StrataTest"] do + let path : System.FilePath := dir + if ← path.isDir then + cleanImpureInDir path + let marker : System.FilePath := "StrataMain.lean.impure" + if ← marker.pathExists then + cleanMarker marker + +initialize cleanPreviousImpureMarkers + +/-- Global ref tracking impure commands in the current module. -/ initialize impureRef : IO.Ref (Array SyntaxNodeKind) ← IO.mkRef #[] /-- Register the purity linter. When an impure command is detected, write a @@ -94,14 +124,19 @@ initialize Lean.addLinter { let kind := stx.getKind if kind != nullKind && !isPureCommand kind then impureRef.modify (·.push kind) - -- Write marker file based on the current file being elaborated let ctx ← readThe Lean.Elab.Command.Context let fileName := ctx.fileName if !fileName.isEmpty then + -- Write marker file for diagnostics let markerPath := fileName ++ ".impure" - -- Append the kind to the marker file let existing ← try IO.FS.readFile markerPath catch _ => pure "" IO.FS.writeFile markerPath (existing ++ toString kind ++ "\n") + -- Delete the .olean trace file so Lake rebuilds this module next time. + -- Source: Strata/Foo/Bar.lean → Trace: .lake/build/lib/lean/Strata/Foo/Bar.trace + let srcPath := fileName + let stem := if srcPath.endsWith ".lean" then (srcPath.dropEnd 5).toString else srcPath + let tracePath := s!".lake/build/lib/lean/{stem}.trace" + try IO.FS.removeFile tracePath catch _ => pure () } end Strata.PurityPlugin From 519e345e6be25b27f12de4a07068896016d6c0d5 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 27 Apr 2026 08:05:44 -0700 Subject: [PATCH 18/22] Use .pure markers instead of .impure --- PurityPlugin.lean | 129 ++++++++++++++++++++++++++-------------------- 1 file changed, 72 insertions(+), 57 deletions(-) diff --git a/PurityPlugin.lean b/PurityPlugin.lean index ebf5d86976..5d06dde4f9 100644 --- a/PurityPlugin.lean +++ b/PurityPlugin.lean @@ -9,23 +9,28 @@ import Lean /-! # Purity Plugin -A Lean compiler plugin that registers a linter to detect impure commands -during elaboration. When loaded via `lean --plugin`, it writes `.impure` -marker files next to `.olean` files for modules that use impure commands. - -Configure in lakefile.toml: -```toml -[[lean_lib]] -name = "PurityPlugin" -plugins = ["PurityPlugin"] -``` +A Lean compiler plugin that ensures impure modules are always re-elaborated. + +## How it works + +1. **At plugin load** (start of each `lake build`): For every `.lean` source file + that does NOT have a `.pure` marker in `.lake/build/lib/lean/`, delete its + `.trace` file so Lake rebuilds it. + +2. **During elaboration**: A linter runs after each command. It optimistically + writes a `.pure` marker. If any impure command is detected, it deletes the + marker. At the end of elaboration, only pure modules retain their marker. + +Markers live in `.lake/build/lib/lean/` alongside `.olean` files, so they're +automatically cleaned by `lake clean` and ignored by git. + +**Safe by default**: no `.pure` marker = rebuild. -/ open Lean namespace Strata.PurityPlugin -/-- Commands whose elaboration is known to be pure. -/ private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ ``Lean.Parser.Command.declaration, ``Lean.Parser.Command.«deriving», ``Lean.Parser.Command.«section», ``Lean.Parser.Command.«namespace», @@ -82,61 +87,71 @@ private def isPureCommand (kind : SyntaxNodeKind) : Bool := pureCommandPrefixes.any (fun pfx => pfx.isPrefixOf kind) || kind == nullKind -/-- Delete build artifacts for a single .impure marker. -/ -private def cleanMarker (marker : System.FilePath) : IO Unit := do - let src := marker.toString.dropRight 7 -- strip ".impure" - let stem := (if src.endsWith ".lean" then (src.dropEnd 5).toString else src) - for suffix in #[".trace"] do - try IO.FS.removeFile s!".lake/build/lib/lean/{stem}{suffix}" catch _ => pure () - try IO.FS.removeFile marker catch _ => pure () - -/-- Recursively find and clean .impure markers. -/ -private partial def cleanImpureInDir (root : System.FilePath) : IO Unit := do +/-- Convert a source path to the build artifact stem. +`Strata/DDM/Elab/Env.lean` → `.lake/build/lib/lean/Strata/DDM/Elab/Env` +Handles absolute paths by stripping the CWD prefix. -/ +private def toBuildStem (srcPath : String) : IO String := do + let cwd ← IO.currentDir + let rel := if srcPath.startsWith cwd.toString + then ((srcPath.drop cwd.toString.length).dropWhile (· == '/')).toString + else srcPath + let stem := if rel.endsWith ".lean" then (rel.dropEnd 5).toString else rel + return s!".lake/build/lib/lean/{stem}" + +private partial def findLeanFiles (root : System.FilePath) : IO (Array System.FilePath) := do + let mut result := #[] if ← root.isDir then for entry in ← root.readDir do - if entry.path.extension == some "impure" then - cleanMarker entry.path - else if ← entry.path.isDir then - cleanImpureInDir entry.path - -/-- Scan for .impure markers from the previous build and delete the -corresponding build artifacts so Lake re-elaborates those modules. -/ -private def cleanPreviousImpureMarkers : IO Unit := do + result := result ++ (← findLeanFiles entry.path) + else if root.extension == some "lean" then + result := result.push root + return result + +/-- At plugin load: delete traces for modules without .pure markers. -/ +private def invalidateImpureTraces : IO Unit := do + let lockFile : System.FilePath := ".lake/build/purity_cleanup.lock" + if ← lockFile.pathExists then return + try IO.FS.writeFile lockFile "" catch _ => return for dir in #["Strata", "StrataTest"] do let path : System.FilePath := dir if ← path.isDir then - cleanImpureInDir path - let marker : System.FilePath := "StrataMain.lean.impure" - if ← marker.pathExists then - cleanMarker marker - -initialize cleanPreviousImpureMarkers - -/-- Global ref tracking impure commands in the current module. -/ -initialize impureRef : IO.Ref (Array SyntaxNodeKind) ← IO.mkRef #[] - -/-- Register the purity linter. When an impure command is detected, write a -`.impure` marker file. The marker path is derived from the source file name -available in the elaboration context. -/ + let files ← findLeanFiles path + for file in files do + let stem ← toBuildStem file.toString + let pureMarker : System.FilePath := stem ++ ".pure" + unless ← pureMarker.pathExists do + try IO.FS.removeFile (stem ++ ".trace") catch _ => pure () + for extra in #["StrataMain.lean"] do + let file : System.FilePath := extra + if ← file.pathExists then + let stem ← toBuildStem extra + let pureMarker : System.FilePath := stem ++ ".pure" + unless ← pureMarker.pathExists do + try IO.FS.removeFile (stem ++ ".trace") catch _ => pure () + try IO.FS.removeFile lockFile catch _ => pure () + +initialize invalidateImpureTraces + +/-- Linter: optimistically write .pure marker on first pure command. +Delete it if any impure command is seen. -/ initialize Lean.addLinter { name := `Strata.purityPlugin run := fun stx => do + let ctx ← readThe Lean.Elab.Command.Context + let fileName := ctx.fileName + if fileName.isEmpty then return + let stem ← toBuildStem fileName + let pureMarker := stem ++ ".pure" let kind := stx.getKind - if kind != nullKind && !isPureCommand kind then - impureRef.modify (·.push kind) - let ctx ← readThe Lean.Elab.Command.Context - let fileName := ctx.fileName - if !fileName.isEmpty then - -- Write marker file for diagnostics - let markerPath := fileName ++ ".impure" - let existing ← try IO.FS.readFile markerPath catch _ => pure "" - IO.FS.writeFile markerPath (existing ++ toString kind ++ "\n") - -- Delete the .olean trace file so Lake rebuilds this module next time. - -- Source: Strata/Foo/Bar.lean → Trace: .lake/build/lib/lean/Strata/Foo/Bar.trace - let srcPath := fileName - let stem := if srcPath.endsWith ".lean" then (srcPath.dropEnd 5).toString else srcPath - let tracePath := s!".lake/build/lib/lean/{stem}.trace" - try IO.FS.removeFile tracePath catch _ => pure () + if kind == nullKind then return + if !isPureCommand kind then + try IO.FS.removeFile pureMarker catch _ => pure () + else + let markerExists ← (System.FilePath.mk pureMarker).pathExists + unless markerExists do + let parent := (System.FilePath.mk pureMarker).parent.getD "." + try IO.FS.createDirAll parent catch _ => pure () + IO.FS.writeFile pureMarker "" } end Strata.PurityPlugin From db06588c832eafeda45bdbac77c608f6f12b430f Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 27 Apr 2026 08:39:23 -0700 Subject: [PATCH 19/22] Cleanup --- Scripts/Skim.lean | 107 ----------- Strata.lean | 1 - Strata/Util/PurityTracker.lean | 203 -------------------- Tools/PurityCheck.lean | 228 ----------------------- Tools/PurityCheckMain.lean | 40 ---- docs/LakeCacheSkimmer.md | 326 +++++++++------------------------ lakefile.toml | 12 -- 7 files changed, 87 insertions(+), 830 deletions(-) delete mode 100644 Scripts/Skim.lean delete mode 100644 Strata/Util/PurityTracker.lean delete mode 100644 Tools/PurityCheck.lean delete mode 100644 Tools/PurityCheckMain.lean diff --git a/Scripts/Skim.lean b/Scripts/Skim.lean deleted file mode 100644 index 37d512c515..0000000000 --- a/Scripts/Skim.lean +++ /dev/null @@ -1,107 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ - -/-! # Lake Build + Skim - -Runs `lake build`, then reads `.impure` marker files written by the -PurityPlugin during elaboration, and deletes build artifacts for impure -modules so the next build re-elaborates them. - -The PurityPlugin is a Lean compiler plugin configured in lakefile.toml. -It runs automatically during `lake build` — no special setup needed. - -## Usage - - lake exe skim [--dry-run] --/ - -namespace Skim - -partial def findMarkerFiles (root : System.FilePath) : IO (Array System.FilePath) := do - let mut result := #[] - if ← root.isDir then - for entry in ← root.readDir do - result := result ++ (← findMarkerFiles entry.path) - else if root.extension == some "impure" then - result := result.push root - return result - -def deleteArtifacts (lakeBuild : System.FilePath) (leanFile : System.FilePath) - (dryRun : Bool) : IO Nat := do - let raw := leanFile.toString.replace "//" "/" - let stem := (if raw.endsWith ".lean" then raw.dropEnd 5 else raw).toString - let mut deleted := 0 - for dir in #["lib/lean", "ir"] do - let base := (lakeBuild / dir / stem).toString - let parent : System.FilePath := (lakeBuild / dir / stem).parent.getD "." - if ← parent.isDir then - for entry in ← parent.readDir do - if entry.path.toString.startsWith (base ++ ".") then - if dryRun then - IO.println s!" would delete: {entry.path}" - else - IO.FS.removeFile entry.path - deleted := deleted + 1 - return deleted - -end Skim - -def main (args : List String) : IO UInt32 := do - let dryRun := args.contains "--dry-run" - let cwd ← IO.currentDir - let lakeBuild := cwd / ".lake" / "build" - - unless ← (cwd / "lakefile.toml").pathExists do - IO.eprintln "Error: must be run from the project root" - return 1 - - -- Step 1: Run lake build (plugin creates .impure markers automatically) - IO.println "Building..." - let buildResult ← IO.Process.output { - cmd := "lake", args := #["build"], cwd := cwd - } - IO.print buildResult.stdout - if buildResult.stderr != "" then IO.eprint buildResult.stderr - if buildResult.exitCode != 0 then - IO.eprintln "lake build failed" - return buildResult.exitCode - - -- Step 2: Find .impure marker files and delete corresponding build artifacts - IO.println "Skimming impure module caches..." - let mut impureCount := 0 - let mut totalDeleted := 0 - - -- Scan source directories for .impure markers - for dir in #["Strata", "StrataTest"] do - let path : System.FilePath := dir - if ← path.isDir then - let markers ← Skim.findMarkerFiles path - for marker in markers do - -- marker is e.g. Strata/DDM/Elab/Env.lean.impure - -- source is Strata/DDM/Elab/Env.lean - let source := marker.toString.dropRight 7 -- strip ".impure" - impureCount := impureCount + 1 - let deleted ← Skim.deleteArtifacts lakeBuild source dryRun - totalDeleted := totalDeleted + deleted - -- Clean up the marker file - unless dryRun do - IO.FS.removeFile marker - - -- Also check root-level files - for extra in #["StrataMain.lean"] do - let marker : System.FilePath := extra ++ ".impure" - if ← marker.pathExists then - impureCount := impureCount + 1 - let deleted ← Skim.deleteArtifacts lakeBuild extra dryRun - totalDeleted := totalDeleted + deleted - unless dryRun do - IO.FS.removeFile marker - - if dryRun then - IO.println s!"\nDry run: {impureCount} impure modules, {totalDeleted} artifacts would be deleted." - else - IO.println s!"Skimmed {impureCount} impure modules ({totalDeleted} artifacts deleted)." - return 0 diff --git a/Strata.lean b/Strata.lean index 839feae34a..b64f7abbd0 100644 --- a/Strata.lean +++ b/Strata.lean @@ -18,7 +18,6 @@ import Strata.DL.Imperative.Imperative /- Utilities -/ import Strata.Util.NameProofs -import Strata.Util.PurityTracker import Strata.Util.Sarif /- Strata Languages -/ diff --git a/Strata/Util/PurityTracker.lean b/Strata/Util/PurityTracker.lean deleted file mode 100644 index a388adae94..0000000000 --- a/Strata/Util/PurityTracker.lean +++ /dev/null @@ -1,203 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ -module - -import Lean - -/-! # Purity Tracker - -A linter that detects impure commands during elaboration via an `IO.Ref` -side channel. After `Elab.process`, read `impureCommandsRef` to see which -command kinds were used. - -The linter runs inside `withoutModifyingEnv`, so it cannot write to -persistent environment extensions. Instead it writes to a global `IO.Ref` -which survives across the elaboration of a single file. --/ - -open Lean - -public section - -namespace Strata.PurityTracker - -/-- Commands whose elaboration is known to be pure. - -## Audit methodology - -Each entry was verified by checking the elaborator source in -`~/.elan/toolchains/leanprover--lean4---v4.29.1/src/lean/Lean/Elab/`. -A command is pure if its elaborator only modifies the `Environment` -(adding declarations, setting attributes, modifying scopes) without -performing `IO` actions that depend on external state. - -## Audit results (Lean v4.29.1) - -### Declarations — `Lean/Elab/Declaration.lean`, `Lean/Elab/Structure.lean`, etc. -`declaration` covers `def`, `theorem`, `abbrev`, `opaque`, `instance`, -`axiom`, `structure`, `class`, `inductive`. These elaborate types and terms, -add declarations to the environment, and run type-checking. No IO. -`deriving` generates instances via deriving handlers. Handlers modify the -environment but don't perform IO. -`example` elaborates a term and discards it. No persistent effect, no IO. - -### Structural — `Lean/Elab/BuiltinCommand.lean` -`section`, `namespace`, `end`, `variable`, `universe`, `open`, `export`, -`import`, `mutual`, `in`, `include`, `omit`, `withWeakNamespace`, -`withExporting`: These modify scopes, namespaces, and open declarations. -Pure environment operations only. - -### Options/attributes — `Lean/Elab/BuiltinCommand.lean`, `Lean/Elab/DeclModifiers.lean` -`set_option`: Sets an option in the environment. Pure. -`attribute`: Adds/removes attributes. Pure (attribute handlers may run -elaboration but not IO). - -### Inspection — `Lean/Elab/BuiltinCommand.lean`, `Lean/Elab/Print.lean` -`check`, `check_failure`, `print`, `printSig`, `printAxioms`, `printEqns`, -`printTacTags`, `where`, `version`, `synth`: These produce messages but -don't modify the environment or perform IO beyond message logging (which -is internal to the elaboration monad, not external IO). - -### Assertions — `Lean/Elab/BuiltinCommand.lean` -`assertNotExists`, `assertNotImported`, `checkAssertions`: Check -environment properties and produce errors if violated. Pure. - -### Documentation — `Lean/Elab/BuiltinCommand.lean` -`moduleDoc`, `addDocString`: Add documentation to the environment. Pure. - -### Syntax/notation — `Lean/Elab/Notation.lean`, `Lean/Elab/Syntax.lean`, etc. -`syntax`, `syntaxAbbrev`, `syntaxCat`, `notation`, `macro`, `macro_rules`, -`elab`, `elab_rules`, `scoped`, `local`, `infix`/`infixl`/`infixr`/ -`prefix`/`postfix`, `declare_syntax_cat`, `declare_config_elab`, etc.: -These register parsers and elaborators in the environment. Pure. - -### Simproc — `Lean/Elab/Tactic/Simproc.lean` -`simproc`, `builtin_simproc`, `dsimproc`, `builtin_dsimproc`: Register -simplification procedures. Pure. - -### Misc — various -`register_simp_attr`, `register_option`, `register_builtin_option`, -`register_label_attr`: Register metadata. Pure. -`register_tactic_tag`, `tactic_extension`, `recommended_spelling`, -`genInjectiveTheorems`, `registerErrorExplanationStx`: Metadata/codegen. Pure. -`init_quot`: Initializes quotient type. Pure kernel operation. -`exit`, `eoi`: Terminate elaboration. Pure. -`grindPattern`, `binderPredicate`, `mixfix`: Syntax definitions. Pure. -`Lean.Option.registerOption`, `Lean.Option.registerBuiltinOption`: -Macros expanding to option registration. Pure. - -## NOT on the allowlist (known impure or unknown) - -Per the purity definition: a command is impure if its elaboration could read -state not determined by the module's source and its dependencies' content, or -mutate state beyond stdout/stderr. - -`eval`, `evalBang`: Execute arbitrary code that may perform IO. IMPURE. -`initialize`: Runs an `IO` action at module load. Even though many only - create refs or register extensions, we cannot statically distinguish safe - from unsafe. IMPURE. -`guard`: Evaluates an expression at elaboration time. Could depend on - external state via `native_decide` or IO-capable code. IMPURE. -`run_cmd`, `run_elab`, `run_meta`: Execute monadic code with IO access. IMPURE. - -`guard_msgs`: Pure by itself — it wraps another command and checks output - against source text. The wrapped command is elaborated separately and - checked by the linter independently. ON THE ALLOWLIST (see below). - -Any unknown/unrecognized command: Conservatively treated as IMPURE. --/ -private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ - ``Lean.Parser.Command.declaration, ``Lean.Parser.Command.«deriving», - ``Lean.Parser.Command.«section», ``Lean.Parser.Command.«namespace», - ``Lean.Parser.Command.«end», ``Lean.Parser.Command.«variable», - ``Lean.Parser.Command.«universe», ``Lean.Parser.Command.«open», - ``Lean.Parser.Command.«export», ``Lean.Parser.Command.«import», - ``Lean.Parser.Command.«mutual», ``Lean.Parser.Command.«in», - ``Lean.Parser.Command.«include», ``Lean.Parser.Command.«omit», - ``Lean.Parser.Command.withWeakNamespace, ``Lean.Parser.Command.withExporting, - ``Lean.Parser.Command.«set_option», ``Lean.Parser.Command.«attribute», - ``Lean.Parser.Command.check, ``Lean.Parser.Command.check_failure, - ``Lean.Parser.Command.print, ``Lean.Parser.Command.printSig, - ``Lean.Parser.Command.printAxioms, ``Lean.Parser.Command.printEqns, - ``Lean.Parser.Command.printTacTags, ``Lean.Parser.Command.«where», - ``Lean.Parser.Command.version, ``Lean.Parser.Command.synth, - ``Lean.Parser.Command.assertNotExists, ``Lean.Parser.Command.assertNotImported, - ``Lean.Parser.Command.checkAssertions, - ``Lean.Parser.Command.moduleDoc, ``Lean.Parser.Command.addDocString, - ``Lean.Parser.Command.«register_tactic_tag», - ``Lean.Parser.Command.«tactic_extension», - ``Lean.Parser.Command.«recommended_spelling», - ``Lean.Parser.Command.genInjectiveTheorems, - ``Lean.Parser.Command.registerErrorExplanationStx, - ``Lean.Parser.Command.«init_quot», ``Lean.Parser.Command.exit, - ``Lean.Parser.Command.eoi, - -- Registered via macros (not under Lean.Parser.Command prefix) - `Lean.Option.registerOption, - `Lean.Option.registerBuiltinOption -] - -private def pureCommandPrefixes : Array Name := #[ - `Lean.Parser.Command.syntax, `Lean.Parser.Command.syntaxAbbrev, - `Lean.Parser.Command.syntaxCat, `Lean.Parser.Command.notation, - `Lean.Parser.Command.macro, `Lean.Parser.Command.macro_rules, - `Lean.Parser.Command.elab, `Lean.Parser.Command.elab_rules, - `Lean.Parser.Command.«scoped», `Lean.Parser.Command.«local», - `Lean.Parser.Command.simproc, `Lean.Parser.Command.builtin_simproc, - `Lean.Parser.Command.dsimproc, `Lean.Parser.Command.builtin_dsimproc, - `Lean.Parser.Command.register_simp_attr, - `Lean.Parser.Command.register_option, `Lean.Parser.Command.register_builtin_option, - `Lean.Parser.Command.register_label_attr, - `Lean.Parser.Command.«infix», `Lean.Parser.Command.«infixl», - `Lean.Parser.Command.«infixr», `Lean.Parser.Command.«prefix», - `Lean.Parser.Command.«postfix», - `Lean.Parser.Command.declare_syntax_cat, `Lean.Parser.Command.declare_config_elab, - `Lean.Parser.Command.declare_command_config_elab, - `Lean.Parser.Command.declare_config_getter, - `Lean.Parser.Command.declare_simp_like_tactic, - `Lean.Parser.Command.declare_tagged_region, - `Lean.Parser.Command.mixfix, `Lean.Parser.Command.grindPattern, - `Lean.Parser.Command.binderPredicate -] - -def isPureCommand (kind : SyntaxNodeKind) : Bool := - pureCommandKinds.contains kind || - pureCommandPrefixes.any (fun pfx => pfx.isPrefixOf kind) || - kind == nullKind - -/-- Global ref accumulating impure command kinds found during elaboration. -Must be reset before each file and read after `Elab.process`. -/ -initialize impureCommandsRef : IO.Ref (Array SyntaxNodeKind) ← IO.mkRef #[] - -/-- Register a linter that records impure commands to the IO.Ref. -/ -initialize Lean.addLinter { - name := `Strata.purityTracker - run := fun stx => do - let kind := stx.getKind - if kind != nullKind && !isPureCommand kind then - impureCommandsRef.modify (·.push kind) -} - -/-- Reset the tracker before processing a new file. -/ -def reset : IO Unit := impureCommandsRef.set #[] - -/-- Read the impure commands found during the last `Elab.process`. -/ -def getResults : IO (Array SyntaxNodeKind) := impureCommandsRef.get - -/-- Check a single file for purity by elaborating it and reading the linter results. -Requires LEAN_PATH to be set so imports can be resolved. -/ -def checkFile (contents : String) (fileName : String := "") : IO (Array SyntaxNodeKind) := do - reset - let inputCtx := Parser.mkInputContext contents fileName - let (header, parserState, msgs) ← Parser.parseHeader inputCtx - let (env, _) ← Elab.processHeader header {} msgs inputCtx - -- Get the content after the header (commands only) - let cmdContent := String.Pos.Raw.extract contents parserState.pos ⟨contents.utf8ByteSize⟩ - let _ ← Elab.process cmdContent env {} fileName - getResults - -end Strata.PurityTracker - -end -- public section diff --git a/Tools/PurityCheck.lean b/Tools/PurityCheck.lean deleted file mode 100644 index 4347a38bf8..0000000000 --- a/Tools/PurityCheck.lean +++ /dev/null @@ -1,228 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ - -import Lean.Parser -import Lean.Parser.Command -import Lean.Parser.Module -import Lean.Elab.Import - -/-! # Module Purity Checker - -Determines whether elaborating a Lean module could potentially perform I/O. - -Uses a conservative allowlist approach: commands whose elaboration is known to -be pure are on the allowlist; everything else is treated as potentially impure. - -## Usage - - lake exe purityCheck [--impure-only] [file2.lean ...] - -Prints each file with its purity status. With `--impure-only`, only prints -files that might perform I/O (useful for cache invalidation). --/ - -open Lean Parser - -/-- Commands whose elaboration is known to be pure (no I/O side effects). -/ -private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ - -- Top-level declarations (elaborate types/terms but don't execute them) - ``Command.declaration, - ``Command.«deriving», - - -- Structural / scoping - ``Command.«section», - ``Command.«namespace», - ``Command.«end», - ``Command.«variable», - ``Command.«universe», - ``Command.«open», - ``Command.«export», - ``Command.«import», - ``Command.«mutual», - ``Command.«in», - ``Command.«include», - ``Command.«omit», - ``Command.withWeakNamespace, - ``Command.withExporting, - - -- Options and attributes (pure metadata) - ``Command.«set_option», - ``Command.«attribute», - - -- Inspection commands (pure — only print/check, no execution) - ``Command.check, - ``Command.check_failure, - ``Command.print, - ``Command.printSig, - ``Command.printAxioms, - ``Command.printEqns, - ``Command.printTacTags, - ``Command.«where», - ``Command.version, - ``Command.synth, - - -- Assertions about the environment (pure checks) - ``Command.assertNotExists, - ``Command.assertNotImported, - ``Command.checkAssertions, - - -- Documentation - ``Command.moduleDoc, - ``Command.addDocString, - - -- Misc pure commands - ``Command.«register_tactic_tag», - ``Command.«tactic_extension», - ``Command.«recommended_spelling», - ``Command.genInjectiveTheorems, - ``Command.registerErrorExplanationStx, - ``Command.«init_quot», - ``Command.exit, - ``Command.eoi -] - -/-- Command kind prefixes known to be pure (syntax/notation/macro definitions). -/ -private def pureCommandPrefixes : Array Name := #[ - `Lean.Parser.Command.syntax, - `Lean.Parser.Command.syntaxAbbrev, - `Lean.Parser.Command.syntaxCat, - `Lean.Parser.Command.notation, - `Lean.Parser.Command.macro, - `Lean.Parser.Command.macro_rules, - `Lean.Parser.Command.elab, - `Lean.Parser.Command.elab_rules, - `Lean.Parser.Command.«scoped», - `Lean.Parser.Command.«local», - `Lean.Parser.Command.simproc, - `Lean.Parser.Command.builtin_simproc, - `Lean.Parser.Command.dsimproc, - `Lean.Parser.Command.builtin_dsimproc, - `Lean.Parser.Command.register_simp_attr, - `Lean.Parser.Command.register_option, - `Lean.Parser.Command.register_builtin_option, - `Lean.Parser.Command.register_label_attr, - `Lean.Parser.Command.«infix», - `Lean.Parser.Command.«infixl», - `Lean.Parser.Command.«infixr», - `Lean.Parser.Command.«prefix», - `Lean.Parser.Command.«postfix», - `Lean.Parser.Command.declare_syntax_cat, - `Lean.Parser.Command.declare_config_elab, - `Lean.Parser.Command.declare_command_config_elab, - `Lean.Parser.Command.declare_config_getter, - `Lean.Parser.Command.declare_simp_like_tactic, - `Lean.Parser.Command.declare_tagged_region, - `Lean.Parser.Command.mixfix, - `Lean.Parser.Command.grindPattern, - `Lean.Parser.Command.binderPredicate -] - -/-- Check if a command syntax node kind is known to be pure. -/ -private def isPureCommand (kind : SyntaxNodeKind) : Bool := - pureCommandKinds.contains kind || - pureCommandPrefixes.any (fun pfx => pfx.isPrefixOf kind) || - kind == nullKind - -/-- An impure command found during purity checking. -/ -structure ImpureCommand where - kind : SyntaxNodeKind - line : Nat - col : Nat - -/-- Parse a .lean file and check all top-level commands for purity. -Returns the list of impure commands found (empty = pure module). -/ -def checkFilePurity (contents : String) (fileName : String := "") : - IO (List ImpureCommand) := do - let inputCtx := mkInputContext contents fileName - let (header, parserState, msgs) ← parseHeader inputCtx - let (env, _msgs) ← Elab.processHeader header {} msgs inputCtx - let pmctx : ParserModuleContext := { env, options := {} } - let mut reasons : List ImpureCommand := [] - let mut mps := parserState - let mut messages := MessageLog.empty - let mut done := false - while !done do - let (cmd, mps', msgs') := parseCommand inputCtx pmctx mps messages - mps := mps' - messages := msgs' - if isTerminalCommand cmd then - done := true - else if cmd.hasMissing then - let pos := inputCtx.fileMap.toPosition (cmd.getPos?.getD mps.pos) - reasons := { kind := `parseError, line := pos.line, col := pos.column } :: reasons - done := true - else - let kind := cmd.getKind - if !isPureCommand kind then - let pos := inputCtx.fileMap.toPosition (cmd.getPos?.getD 0) - reasons := { kind, line := pos.line, col := pos.column } :: reasons - return reasons.reverse - -/-- Recursively collect all .lean files under a directory. -/ -partial def collectLeanFiles (path : System.FilePath) : IO (Array System.FilePath) := do - let mut result := #[] - if ← path.isDir then - for entry in ← path.readDir do - let sub ← collectLeanFiles entry.path - result := result ++ sub - else if path.extension == some "lean" then - result := result.push path - return result - -/-- Resolve arguments: expand directories into .lean files. -/ -def resolveInputs (inputs : List String) : IO (Array System.FilePath) := do - let mut files := #[] - for input in inputs do - let path : System.FilePath := input - if ← path.isDir then - files := files ++ (← collectLeanFiles path) - else - files := files.push path - return files - -def purityCheckMain (args : List String) : IO UInt32 := do - let impureOnly := args.contains "--impure-only" - -- Parse --output - let rec findOutput : List String → Option String - | "--output" :: v :: _ => some v - | _ :: rest => findOutput rest - | [] => none - let outputFile := findOutput args - -- Collect non-flag arguments as inputs - let mut inputs : List String := [] - let mut skipNext := false - for arg in args do - if skipNext then - skipNext := false - else if arg == "--output" then - skipNext := true - else if !arg.startsWith "--" then - inputs := arg :: inputs - let inputPaths := inputs.reverse - if inputPaths.isEmpty then - IO.eprintln "Usage: purityCheck [--impure-only] [--output ] [path ...]" - IO.eprintln " can be a .lean file or a directory (recursively scanned)" - return 1 - let files ← resolveInputs inputPaths - let mut exitCode : UInt32 := 0 - let mut outputLines : Array String := #[] - for file in files.toList.mergeSort (·.toString < ·.toString) do - let contents ← IO.FS.readFile file - let reasons ← checkFilePurity contents file.toString - if reasons.isEmpty then - unless impureOnly do - IO.println s!"PURE: {file}" - else - let line := s!"IMPURE: {file}" - IO.println line - outputLines := outputLines.push file.toString - for r in reasons do - IO.println s!" - {r.kind} at {r.line}:{r.col}" - exitCode := 1 - if let some outPath := outputFile then - IO.FS.writeFile outPath (outputLines.toList.map (· ++ "\n") |>.foldl (· ++ ·) "") - IO.eprintln s!"Wrote {outputLines.size} impure files to {outPath}" - return exitCode diff --git a/Tools/PurityCheckMain.lean b/Tools/PurityCheckMain.lean deleted file mode 100644 index 0db2754934..0000000000 --- a/Tools/PurityCheckMain.lean +++ /dev/null @@ -1,40 +0,0 @@ -import Lean -import Strata.Util.PurityTracker -open Strata.PurityTracker - -partial def collectLeanFiles (root : System.FilePath) : IO (Array System.FilePath) := do - let mut result := #[] - if ← root.isDir then - for entry in ← root.readDir do - result := result ++ (← collectLeanFiles entry.path) - else if root.extension == some "lean" then - result := result.push root - return result - -def resolveInputs (args : List String) : IO (Array System.FilePath) := do - let mut files := #[] - for arg in args do - let path : System.FilePath := arg - if ← path.isDir then - files := files ++ (← collectLeanFiles path) - else - files := files.push path - return files - -def main (args : List String) : IO UInt32 := do - let impureOnly := args.contains "--impure-only" - let inputs := args.filter (!·.startsWith "--") - if inputs.isEmpty then - IO.eprintln "Usage: purityCheck [--impure-only] [path ...]" - IO.eprintln " can be a .lean file or a directory (recursively scanned)" - return 1 - let files ← resolveInputs inputs - for file in files.toList.mergeSort (·.toString < ·.toString) do - let contents ← IO.FS.readFile file - let r ← checkFile contents file.toString - if r.isEmpty then - unless impureOnly do - IO.println s!"PURE: {file}" - else - IO.println s!"IMPURE: {file} — {r.toList}" - return 0 diff --git a/docs/LakeCacheSkimmer.md b/docs/LakeCacheSkimmer.md index c58d2e9000..16f6d80b25 100644 --- a/docs/LakeCacheSkimmer.md +++ b/docs/LakeCacheSkimmer.md @@ -7,9 +7,8 @@ elaboration depends on external state (file system, SMT solvers, network, etc.), the cached result may be stale — but Lake has no way to know this, since it only tracks source file changes and dependency graphs. -We need a tool that identifies modules whose elaboration *might* depend on -external state and invalidates their cached build artifacts, forcing `lake build` -to re-elaborate them. +We need a mechanism that identifies modules whose elaboration *might* depend on +external state and forces `lake build` to re-elaborate them. ## Definition of Purity @@ -27,285 +26,134 @@ Equivalently, a module is **impure** if its elaboration: - **Mutates** any state other than stdout and stderr output (which is captured by the build trace). -Note that stdout/stderr output during elaboration (e.g., from `#check`, `#print`, -`logInfo`) is NOT considered a side effect for our purposes, because Lake's build -trace already captures it. The concern is specifically about elaboration behavior -that depends on or affects state *outside* the Lean build system's tracking. - ### Implications Under this definition: - **`initialize`** is impure: it runs an arbitrary `IO` action that *could* read - external state, even though many `initialize` blocks only create `IO.Ref`s or - register extensions (which is deterministic). We cannot statically distinguish - safe `initialize` from unsafe ones, so all are conservatively impure. - -- **`#eval`** is impure: it executes arbitrary code that could perform IO. - + external state. We cannot statically distinguish safe from unsafe `initialize` + blocks, so all are conservatively impure. +- **`#eval` / `#eval!`** is impure: executes arbitrary code that could perform IO. +- **`#guard`** is impure: evaluates an expression at elaboration time. +- **`run_cmd` / `run_elab` / `run_meta`** are impure: execute monadic code with + IO access. - **`#guard_msgs`** is pure *by itself*: it wraps another command and checks its - output against expected text from the source. The wrapped command is elaborated - separately and will be checked by the linter independently. If the wrapped - command is `#eval`, the linter catches `#eval`, not `#guard_msgs`. - -- **`#guard`** is impure: it evaluates an expression at elaboration time. The - expression could in principle depend on external state via `native_decide` or - similar, though in practice it rarely does. Conservatively impure. - -- **`run_cmd` / `run_elab` / `run_meta`** are impure: they execute monadic code - that has access to `IO`. - -- **`declaration`** (`def`, `theorem`, etc.) is pure: elaboration only reads the - environment (determined by deps) and the source text. Even `native_decide` in - proofs is deterministic given the same source and deps. - -- **Inspection commands** (`#check`, `#print`, etc.) are pure: they only read - the environment and write to stdout/stderr (captured by build trace). + output against source text. The wrapped command is checked independently by the + linter. (Note: Lean skips linters for `#guard_msgs`, but runs them on the inner + command.) +- **`declaration`** (`def`, `theorem`, etc.) is pure. +- **Inspection commands** (`#check`, `#print`, etc.) are pure. ## Design Goals 1. **Soundness**: If we identify a module as pure, it must be impossible for its elaboration to have read external state or mutated state beyond stdout/stderr. - False negatives (missing an impure module) cause stale cache bugs that are - extremely hard to diagnose. - -2. **Precision**: Minimize false positives. If we flag too many modules as impure, - every build re-elaborates them unnecessarily, defeating the purpose of caching. - -## Background: How Lean Modules Can Perform IO - -Lean interleaves parsing and elaboration: each command is parsed using syntax -extensions registered by all previously elaborated commands, then elaborated -before the next command is parsed. This means we cannot parse a file without -elaborating it. - -The complete set of ways a module can perform IO during elaboration: - -| Command | Mechanism | Leaves `.olean` trace? | -|---------|-----------|----------------------| -| `initialize` / `builtin_initialize` | Runs IO action at module load time | Yes — `[init]` attribute | -| `#eval` / `#eval!` | Executes arbitrary expression | No | -| `#guard_msgs` | Executes wrapped command, checks output | No | -| `#guard` | Evaluates boolean expression | No | -| `run_cmd` / `run_elab` / `run_meta` | Executes monadic code | No | -| Custom `@[command_elab]` | Elaborator may perform IO | No (at use site) | -| `native_decide` / `decide` | Pure computation | N/A (pure) | - -The key challenge: most impure commands leave **no trace** in the `.olean` file. -The `.olean` records the *result* of elaboration (declarations, attributes, -environment extensions), not *how* it got there. - -## Approaches Considered - -### Option A: Instrument the Elaboration Loop - -Register a `CommandElab` wrapper that intercepts every command before elaboration, -logs its syntax kind, then delegates to the real elaborator. Write results to a -side-channel file (e.g., `.purity.json`). - -**Pros:** -- Perfect accuracy — sees every command exactly as Lean sees it -- No post-build analysis needed - -**Cons:** -- Requires modifying the build process -- Every module must import the instrumentation module -- Side-channel files add complexity - -### Option B: Re-elaborate Post-Build -After `lake build`, use `Lean.Elab.process` to re-elaborate each source file. -Since `.olean` files exist, `importModules` is fast, but the file itself is -fully re-elaborated. Intercept commands during this re-elaboration. +2. **Precision**: Minimize false positives (pure modules incorrectly flagged as + impure). -**Pros:** -- No build modification needed -- Perfect accuracy +3. **Zero workflow change**: Developers should just run `lake build` with no + extra steps. -**Cons:** -- Re-elaborates every source file — O(n) in codebase size -- Potentially very slow for large codebases -- Duplicates work already done by `lake build` +## Solution: Lake Compiler Plugin -### Option C: Hybrid `.olean` Inspection + Text Scan +The solution is a **Lean compiler plugin** (`PurityPlugin.lean`) that runs +automatically during every `lake build`. No separate tools or scripts needed. -Use `.olean` inspection for `initialize` (precise, via `[init]` attribute). -Use text scanning (grep) for `#eval`, `#guard_msgs`, etc. +### How It Works -**Pros:** -- Fast — no re-elaboration -- `.olean` check is perfectly precise for `initialize` +The plugin uses an **inverted marker** design — safe by default: -**Cons:** -- Text scan can false-positive on patterns in comments, strings, or - custom syntax (e.g., DDM `//` comments containing "initialize") -- Text scan can false-negative if a pattern appears in an unexpected form -- Cannot detect IO from custom command elaborators +1. **At plugin load** (start of each `lake build`): For every `.lean` source file + that does NOT have a `.pure` marker in `.lake/build/lib/lean/`, delete its + `.trace` file. This causes Lake to rebuild that module. -### Option D: Persistent Environment Extension (Recommended) +2. **During elaboration**: A linter (registered via `Lean.addLinter`) runs after + each command. It checks the command's syntax kind against a pure allowlist. + - If all commands are pure: a `.pure` marker file is written. + - If any impure command is detected: the `.pure` marker is deleted. -Define a persistent environment extension that records which impure command kinds -were used during elaboration. Register a `CommandElab` hook (via `initialize`) -that writes to this extension whenever an impure command is elaborated. After -`lake build`, load each `.olean` and read the extension. +3. **Result**: After the build, pure modules have `.pure` markers and will be + cached on the next build. Impure modules have no markers and will be rebuilt. -**Pros:** -- Perfect accuracy — the hook sees every command during real elaboration -- Readable from `.olean` — no re-elaboration, instant classification -- No side-channel files — data lives in the `.olean` itself -- Survives incremental builds — only re-elaborated modules update their data +### Safety Properties -**Cons:** -- Every module must transitively import the module that registers the hook -- Adds a small overhead to every command elaboration (syntax kind check) -- Requires a base module that all other modules import +- **No marker = rebuild**: If the plugin fails to run, a new file is added, or + anything unexpected happens, there's no `.pure` marker, so the module gets + rebuilt. This is the safe default. +- **`lake clean` triggers full rebuild**: Cleaning removes all markers, so the + next build re-elaborates everything and re-establishes markers. +- **First build after adding the plugin**: All modules are rebuilt (no markers + exist yet). This is expected and correct. -## Recommendation +### Configuration -**Option D needs modification.** The linter API cannot write to persistent -environment extensions (`withoutModifyingEnv`). Two viable alternatives: +In `lakefile.toml`: -### Option D' — Custom command elaborator wrappers - -Register `@[command_elab]` handlers for each known impure command kind -(`eval`, `initialize`, `guard_msgs`, etc.) that write to the persistent -extension before delegating to the real elaborator. Since these run during -normal elaboration (not as linters), environment modifications persist. - -### Option D'' — Linter + IO.Ref side channel - -Use the linter API to detect impure commands, but write to a global `IO.Ref` -instead of the environment. After `Elab.process` completes, read the ref. -This works when re-elaborating files post-build but does NOT persist in -`.olean` files — the skimmer must re-elaborate each file. - -### Current pragmatic approach - -`lake exe skim` runs `lake build` followed by linter-based purity checking. -This is correct and sound but requires developers to use `lake exe skim` -instead of `lake build`. - -### Future: Lake plugin (zero-workflow-change) - -Lake supports `plugins` on `lean_lib` and `lean_exe` targets — shared libraries -loaded via `lean --plugin` during elaboration. A plugin could register the -purity linter, which would then run automatically during every `lake build` -with no workflow change for developers. - -The plugin would: -1. Register the purity linter via `initialize` (same as current `PurityTracker`) -2. Write a `.impure` marker file when impure commands are detected -3. A post-build step (or Lake `post_update` hook) would read markers and - delete the corresponding `.olean` files - -Configuration in `lakefile.toml`: ```toml [[lean_lib]] name = "PurityPlugin" -# Lake builds this as a shared library +defaultFacets = ["shared"] [[lean_lib]] name = "Strata" -plugins = ["PurityPlugin"] +plugins = ["PurityPlugin:shared"] ``` -**Status**: Feasible based on Lake documentation. The `plugins` field is -documented and supported in both TOML and Lean lakefiles. Implementation -requires experimentation with the plugin build/load machinery. - -**Key advantage**: Developers just run `lake build` — the plugin runs -automatically, no risk of forgetting to skim. - -### Implementation Sketch - -```lean --- PurityHook.lean (imported transitively by all modules) - -/-- Persistent extension recording impure command kinds used in this module. -/ -initialize purityExt : SimplePersistentEnvExtension SyntaxNodeKind (Array SyntaxNodeKind) ← - registerSimplePersistentEnvExtension { - addEntryFn := fun s n => s.push n - addImportedFn := fun _ => pure #[] -- only track current module's commands - } - -/-- Register a linter that records impure commands into the environment. -/ -initialize addLinter { - name := `purityTracker - run := fun stx => do - let kind := stx.getKind - if !isPureCommand kind then - modifyEnv fun env => purityExt.addEntry env kind -} -``` +The plugin is built as a shared library and loaded via `lean --plugin` during +elaboration of every module in the `Strata` library. -Post-build, the skimmer loads each `.olean` and checks: +### Pure Command Allowlist -```lean -let env ← importModules #[{ module := modName }] {} -let entries := purityExt.getState env -- only current module's entries -if entries.isEmpty then PURE else IMPURE -``` +The plugin maintains an allowlist of command syntax kinds known to be pure. +Any command NOT on the allowlist is conservatively treated as impure. -### Deployment +The allowlist was audited against Lean v4.29.1 source code. See the inline +documentation in `PurityPlugin.lean` for the full audit. -The hook module must be imported by every source file. Options: +The allowlist approach is **sound**: unknown commands default to impure (false +positives, not false negatives). The allowlist should be re-audited when +upgrading the Lean toolchain. -1. **Add to a root module** that everything already imports (e.g., `Strata.lean` - or a prelude). -2. **Use a Lake plugin** that automatically injects the import. -3. **Add as a direct import** to every file (most explicit, most verbose). +### Linter API -Option 1 is simplest if such a root module exists. +The plugin uses `Lean.addLinter` to register a callback that runs after every +top-level command elaboration. Key properties: -### Fallback +- Linters run inside `withoutModifyingEnv`, so they cannot modify the `.olean`. + Instead, the plugin writes `.pure` marker files via IO (which IS available + in `CommandElabM`). +- Linters are skipped for `#guard_msgs`, but run on the inner command. This + means `#guard_msgs in #eval foo` correctly detects `#eval` as impure. +- Each module is elaborated in its own Lean process, so the linter state is + fresh for each file. -Until Option D is implemented, Option C (hybrid `.olean` + text scan) provides -a reasonable approximation. It is sound for the known set of impure commands -but may have false positives from text patterns in non-code contexts. +### Marker File Layout -## Open Questions +Markers are stored alongside `.olean` files in `.lake/build/lib/lean/`: -### 1. Is there a `CommandElab` hook API? — RESOLVED ⚠️ +``` +.lake/build/lib/lean/Strata/DDM/Elab/Env.olean # build artifact +.lake/build/lib/lean/Strata/DDM/Elab/Env.trace # Lake's build trace +.lake/build/lib/lean/Strata/DDM/Elab/Env.pure # purity marker (if pure) +``` -**Partially.** Lean provides the `Linter` API (`Lean.addLinter`) which registers -a callback that runs after every top-level command elaboration. The linter -receives the full command `Syntax` and runs in `CommandElabM`. +This means: +- Markers are automatically cleaned by `lake clean` +- Markers are in `.lake/` which is gitignored +- No source tree pollution -**However**, linters run inside `withoutModifyingEnv` (see `runLintersAsync` in -`Lean/Elab/Command.lean:334`), which means **environment modifications are -discarded**. This is by design — linters are intended for reporting diagnostics, -not for modifying the environment. +## Open Questions -This means: -- ✅ A linter CAN inspect each command's syntax kind -- ✅ A linter CAN produce messages/warnings -- ❌ A linter CANNOT write to a persistent environment extension -- ❌ A linter CANNOT modify the `.olean` output - -**Consequence**: Option D as originally sketched (linter + persistent extension) -does not work. The linter can see the commands but cannot persist its findings -in the `.olean`. - -**Alternative mechanisms to investigate**: -- **Custom `@[command_elab]` wrappers**: Register elaborators for known impure - command kinds that record to the extension before delegating to the real - elaborator. This runs *during* elaboration (not as a linter), so environment - modifications persist. -- **`IO.Ref` side channel**: The linter writes to a global `IO.Ref` instead of - the environment. Post-elaboration, the skimmer reads the ref. This works for - `Elab.process` but not for `.olean`-based post-build analysis. -- **Lean plugin / Lake hook**: Use Lake's plugin system to inject instrumentation - into the build pipeline. - -2. **What is the right set of impure command kinds?** The table above covers - known built-in commands. We should audit Lean's source for any others and - establish a process for updating the list when the Lean toolchain is upgraded. - -3. **How do we handle custom `@[command_elab]` elaborators that perform IO?** - The hook sees the command's syntax kind, but can't know whether the - elaborator implementation performs IO. One conservative approach: treat any - command kind not on a known-pure allowlist as potentially impure. - -4. **Performance impact of the hook?** The hook runs for every command in every - module. The check is a hash set lookup on the syntax kind, which should be - negligible. +1. **Toolchain upgrades**: The pure command allowlist is pinned to a specific + Lean version. New impure commands in future Lean versions would not be on + the allowlist and would correctly default to impure (safe). However, if a + previously-pure command becomes impure, the allowlist would need updating. + +2. **Custom `@[command_elab]` elaborators**: The plugin sees the command's + syntax kind but can't know whether a custom elaborator performs IO. Unknown + command kinds are treated as impure (conservative). + +3. **Plugin loading for other libraries**: Currently the plugin is configured + only for the `Strata` library. To cover `StrataTest` and other libraries, + they would also need `plugins = ["PurityPlugin:shared"]` in their config. diff --git a/lakefile.toml b/lakefile.toml index c0558132d7..3e786898c4 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -45,15 +45,3 @@ root = "Scripts.ImportStats" [[lean_exe]] name = "DiffTestCore" - -[[lean_exe]] -name = "purityCheck" -root = "Tools.PurityCheckMain" - -[[lean_lib]] -name = "Tools" -globs = ["Tools.+"] - -[[lean_exe]] -name = "skim" -root = "Scripts.Skim" From 46b1a476286786b6984b0bef8ab845860ab87764 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 27 Apr 2026 08:53:57 -0700 Subject: [PATCH 20/22] Restore audit breakdown --- PurityPlugin.lean | 86 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) diff --git a/PurityPlugin.lean b/PurityPlugin.lean index 5d06dde4f9..be10b3b5af 100644 --- a/PurityPlugin.lean +++ b/PurityPlugin.lean @@ -31,6 +31,92 @@ open Lean namespace Strata.PurityPlugin +/-- Commands whose elaboration is known to be pure. + +## Audit methodology + +Each entry was verified by checking the elaborator source in +`~/.elan/toolchains/leanprover--lean4---v4.29.1/src/lean/Lean/Elab/`. +A command is pure if its elaborator only modifies the `Environment` +(adding declarations, setting attributes, modifying scopes) without +performing `IO` actions that depend on external state. + +## Audit results (Lean v4.29.1) + +### Declarations — `Lean/Elab/Declaration.lean`, `Lean/Elab/Structure.lean`, etc. +`declaration` covers `def`, `theorem`, `abbrev`, `opaque`, `instance`, +`axiom`, `structure`, `class`, `inductive`. These elaborate types and terms, +add declarations to the environment, and run type-checking. No IO. +`deriving` generates instances via deriving handlers. Handlers modify the +environment but don't perform IO. +`example` elaborates a term and discards it. No persistent effect, no IO. + +### Structural — `Lean/Elab/BuiltinCommand.lean` +`section`, `namespace`, `end`, `variable`, `universe`, `open`, `export`, +`import`, `mutual`, `in`, `include`, `omit`, `withWeakNamespace`, +`withExporting`: These modify scopes, namespaces, and open declarations. +Pure environment operations only. + +### Options/attributes — `Lean/Elab/BuiltinCommand.lean`, `Lean/Elab/DeclModifiers.lean` +`set_option`: Sets an option in the environment. Pure. +`attribute`: Adds/removes attributes. Pure (attribute handlers may run +elaboration but not IO). + +### Inspection — `Lean/Elab/BuiltinCommand.lean`, `Lean/Elab/Print.lean` +`check`, `check_failure`, `print`, `printSig`, `printAxioms`, `printEqns`, +`printTacTags`, `where`, `version`, `synth`: These produce messages but +don't modify the environment or perform IO beyond message logging (which +is internal to the elaboration monad, not external IO). + +### Assertions — `Lean/Elab/BuiltinCommand.lean` +`assertNotExists`, `assertNotImported`, `checkAssertions`: Check +environment properties and produce errors if violated. Pure. + +### Documentation — `Lean/Elab/BuiltinCommand.lean` +`moduleDoc`, `addDocString`: Add documentation to the environment. Pure. + +### Syntax/notation — `Lean/Elab/Notation.lean`, `Lean/Elab/Syntax.lean`, etc. +`syntax`, `syntaxAbbrev`, `syntaxCat`, `notation`, `macro`, `macro_rules`, +`elab`, `elab_rules`, `scoped`, `local`, `infix`/`infixl`/`infixr`/ +`prefix`/`postfix`, `declare_syntax_cat`, `declare_config_elab`, etc.: +These register parsers and elaborators in the environment. Pure. + +### Simproc — `Lean/Elab/Tactic/Simproc.lean` +`simproc`, `builtin_simproc`, `dsimproc`, `builtin_dsimproc`: Register +simplification procedures. Pure. + +### Misc — various +`register_simp_attr`, `register_option`, `register_builtin_option`, +`register_label_attr`: Register metadata. Pure. +`register_tactic_tag`, `tactic_extension`, `recommended_spelling`, +`genInjectiveTheorems`, `registerErrorExplanationStx`: Metadata/codegen. Pure. +`init_quot`: Initializes quotient type. Pure kernel operation. +`exit`, `eoi`: Terminate elaboration. Pure. +`grindPattern`, `binderPredicate`, `mixfix`: Syntax definitions. Pure. +`Lean.Option.registerOption`, `Lean.Option.registerBuiltinOption`: +Macros expanding to option registration. Pure. + +## NOT on the allowlist (known impure or unknown) + +Per the purity definition: a command is impure if its elaboration could read +state not determined by the module's source and its dependencies' content, or +mutate state beyond stdout/stderr. + +`eval`, `evalBang`: Execute arbitrary code that may perform IO. IMPURE. +`initialize`: Runs an `IO` action at module load. Even though many only + create refs or register extensions, we cannot statically distinguish safe + from unsafe. IMPURE. +`guard`: Evaluates an expression at elaboration time. Could depend on + external state via `native_decide` or IO-capable code. IMPURE. +`run_cmd`, `run_elab`, `run_meta`: Execute monadic code with IO access. IMPURE. + +`guard_msgs`: Pure by itself — it wraps another command and checks output + against source text. The wrapped command is elaborated separately and + checked by the linter independently. (Note: Lean skips linters for + `#guard_msgs` but runs them on the inner command.) + +Any unknown/unrecognized command: Conservatively treated as IMPURE. +-/ private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ ``Lean.Parser.Command.declaration, ``Lean.Parser.Command.«deriving», ``Lean.Parser.Command.«section», ``Lean.Parser.Command.«namespace», From 7d00aca08802ac4be7992726179e01c3e2bf06ad Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 27 Apr 2026 09:34:39 -0700 Subject: [PATCH 21/22] No prefix matching --- PurityPlugin.lean | 28 ++++++++++++---------------- 1 file changed, 12 insertions(+), 16 deletions(-) diff --git a/PurityPlugin.lean b/PurityPlugin.lean index be10b3b5af..af8caf790b 100644 --- a/PurityPlugin.lean +++ b/PurityPlugin.lean @@ -142,36 +142,32 @@ private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [ ``Lean.Parser.Command.registerErrorExplanationStx, ``Lean.Parser.Command.«init_quot», ``Lean.Parser.Command.exit, ``Lean.Parser.Command.eoi, - `Lean.Option.registerOption, `Lean.Option.registerBuiltinOption -] - -private def pureCommandPrefixes : Array Name := #[ - `Lean.Parser.Command.syntax, `Lean.Parser.Command.syntaxAbbrev, - `Lean.Parser.Command.syntaxCat, `Lean.Parser.Command.notation, - `Lean.Parser.Command.macro, `Lean.Parser.Command.macro_rules, - `Lean.Parser.Command.elab, `Lean.Parser.Command.elab_rules, + `Lean.Option.registerOption, `Lean.Option.registerBuiltinOption, + -- Syntax/notation/macro definitions (previously matched by prefix) + ``Lean.Parser.Command.syntax, ``Lean.Parser.Command.syntaxAbbrev, + ``Lean.Parser.Command.syntaxCat, ``Lean.Parser.Command.notation, + ``Lean.Parser.Command.macro, ``Lean.Parser.Command.macro_rules, + ``Lean.Parser.Command.elab, ``Lean.Parser.Command.elab_rules, `Lean.Parser.Command.«scoped», `Lean.Parser.Command.«local», `Lean.Parser.Command.simproc, `Lean.Parser.Command.builtin_simproc, `Lean.Parser.Command.dsimproc, `Lean.Parser.Command.builtin_dsimproc, `Lean.Parser.Command.register_simp_attr, `Lean.Parser.Command.register_option, `Lean.Parser.Command.register_builtin_option, `Lean.Parser.Command.register_label_attr, - `Lean.Parser.Command.«infix», `Lean.Parser.Command.«infixl», - `Lean.Parser.Command.«infixr», `Lean.Parser.Command.«prefix», - `Lean.Parser.Command.«postfix», + ``Lean.Parser.Command.«infix», ``Lean.Parser.Command.«infixl», + ``Lean.Parser.Command.«infixr», ``Lean.Parser.Command.«prefix», + ``Lean.Parser.Command.«postfix», `Lean.Parser.Command.declare_syntax_cat, `Lean.Parser.Command.declare_config_elab, `Lean.Parser.Command.declare_command_config_elab, `Lean.Parser.Command.declare_config_getter, `Lean.Parser.Command.declare_simp_like_tactic, `Lean.Parser.Command.declare_tagged_region, - `Lean.Parser.Command.mixfix, `Lean.Parser.Command.grindPattern, - `Lean.Parser.Command.binderPredicate + ``Lean.Parser.Command.mixfix, ``Lean.Parser.Command.grindPattern, + ``Lean.Parser.Command.binderPredicate ] private def isPureCommand (kind : SyntaxNodeKind) : Bool := - pureCommandKinds.contains kind || - pureCommandPrefixes.any (fun pfx => pfx.isPrefixOf kind) || - kind == nullKind + pureCommandKinds.contains kind || kind == nullKind /-- Convert a source path to the build artifact stem. `Strata/DDM/Elab/Env.lean` → `.lake/build/lib/lean/Strata/DDM/Elab/Env` From f12b9e5f7390b12241bf30ce8811828e01091c9a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 27 Apr 2026 21:14:16 -0700 Subject: [PATCH 22/22] Add issue link --- docs/LakeCacheSkimmer.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/LakeCacheSkimmer.md b/docs/LakeCacheSkimmer.md index 16f6d80b25..3c7686e768 100644 --- a/docs/LakeCacheSkimmer.md +++ b/docs/LakeCacheSkimmer.md @@ -6,10 +6,12 @@ Lean's `lake build` caches elaboration results in `.olean` files. When a module' elaboration depends on external state (file system, SMT solvers, network, etc.), the cached result may be stale — but Lake has no way to know this, since it only tracks source file changes and dependency graphs. +See https://github.com/leanprover/lean4/issues/13449. We need a mechanism that identifies modules whose elaboration *might* depend on external state and forces `lake build` to re-elaborate them. + ## Definition of Purity A Lean module is **pure** if replaying its build trace produces exactly the same