diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 71241c8af..86057dcb9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -55,12 +55,9 @@ jobs: - name: Export Lean import graph run: | set -euo pipefail - mkdir -p .ci/lean/EvalTools - lean -R . -o .ci/lean/EvalTools/Markers.olean EvalTools/Markers.lean - LEAN_PATH="$PWD/.ci/lean" lean -R . \ - -o .ci/lean/EvalTools/ModuleCoverage.olean EvalTools/ModuleCoverage.lean - LEAN_PATH="$PWD/.ci/lean" lean --run EvalTools/CIImportGraph.lean \ - > .ci/import-graph.json + mkdir -p .ci + lake build EvalTools.CIImportGraph + lake env lean --run EvalTools/CIImportGraph.lean > .ci/import-graph.json - name: Select affected catalog problems id: changes diff --git a/EvalTools/CheckComparatorInstallation.lean b/EvalTools/CheckComparatorInstallation.lean index 8ee60b05c..5b42a6627 100644 --- a/EvalTools/CheckComparatorInstallation.lean +++ b/EvalTools/CheckComparatorInstallation.lean @@ -3,6 +3,8 @@ import EvalTools.Subprocess namespace EvalTools +open LeanEvalGenerator.Core + set_option autoImplicit false structure Semver where diff --git a/EvalTools/CheckEvalWorkflow.lean b/EvalTools/CheckEvalWorkflow.lean index a07a3cf9f..f42636fd5 100644 --- a/EvalTools/CheckEvalWorkflow.lean +++ b/EvalTools/CheckEvalWorkflow.lean @@ -10,6 +10,8 @@ open Lean namespace EvalTools +open LeanEvalGenerator.Core + set_option autoImplicit false private def TWO_PLUS_TWO_ID : String := "two_plus_two" diff --git a/EvalTools/CheckProblemBuild.lean b/EvalTools/CheckProblemBuild.lean index e7c7ac9d0..94aa45f66 100644 --- a/EvalTools/CheckProblemBuild.lean +++ b/EvalTools/CheckProblemBuild.lean @@ -2,6 +2,8 @@ import EvalTools.Manifest namespace EvalTools +open LeanEvalGenerator.Core + set_option autoImplicit false private def hasSubstr (haystack pattern : String) : Bool := diff --git a/EvalTools/Generate.lean b/EvalTools/Generate.lean index 652813fb2..d6ec44bca 100644 --- a/EvalTools/Generate.lean +++ b/EvalTools/Generate.lean @@ -1,3522 +1,5 @@ -import Lake.Toml -import Lake.Util.Message -import Lean -import EvalTools.Manifest -import EvalTools.Markers -import EvalTools.Subprocess - -set_option linter.deprecated false - -open Lean -open Lean.Parser -open Lake -open Lake.Toml +import LeanEvalGenerator.Core.Generate namespace EvalTools -set_option autoImplicit false - -/-! ## Constants -/ - -def fixedAxioms : Array String := - #["propext", "Quot.sound", "Classical.choice"] - -def expectedFiles : Array String := #[ - "README.md", - "lean-toolchain", - "lakefile.toml", - "ChallengeDeps.lean", - "Challenge.lean", - "Solution.lean", - "Submission.lean", - "Submission/Helpers.lean", - "WorkspaceTest.lean", - "config.json", - "holes.json" -] - -def ignoredPathNames : Array String := #[".lake", "build", ".cache", "lake-manifest.json"] - -/-! ## Workspace test template -/ - -def loadWorkspaceTestTemplate (root : System.FilePath) : IO String := - IO.FS.readFile (root / "templates" / "WorkspaceTest.lean") - -/-! ## Mathlib dependency -/ - -structure DependencySpec where - name : String - git : String - rev : String - deriving Inhabited - -private structure RawRequire where - name : String - git : Option String := none - rev : Option String := none - deriving Inhabited - -private instance : DecodeToml RawRequire where - decode v := do - let t ← v.decodeTable - let name : String ← t.decode `name - let git? : Option String ← t.decode? `git - let rev? : Option String ← t.decode? `rev - return { name := name, git := git?, rev := rev? } - -def loadRootMathlibDependency (root : System.FilePath) : IO DependencySpec := do - let path := root / "lakefile.toml" - let contents ← IO.FS.readFile path - let inputCtx := mkInputContext contents path.toString - let table ← - match (← Lake.Toml.loadToml inputCtx |>.toBaseIO) with - | .ok table => pure table - | .error err => throw <| IO.userError (← Lake.mkMessageLogString err) - let decoded : - EStateM.Result Unit (Array DecodeError) (Array RawRequire) := - (Lake.Toml.Table.decode (α := Array RawRequire) table `require).run #[] - let requires ← - match decoded with - | .ok arr errors => - if errors.isEmpty then pure arr - else throw <| IO.userError (decodeErrorsToString errors) - | .error _ errors => - throw <| IO.userError (decodeErrorsToString errors) - let mathlib := requires.filter fun r => r.name == "mathlib" - if mathlib.isEmpty then - throw <| IO.userError s!"Could not find a mathlib dependency in {path}" - if mathlib.size > 1 then - throw <| IO.userError s!"Found multiple mathlib dependencies in {path}" - let entry := mathlib[0]! - let git ← match entry.git with - | some g => - let g := g.trim - if g.isEmpty then - throw <| IO.userError s!"mathlib dependency in {path} is missing a non-empty 'git' field" - else pure g - | none => - throw <| IO.userError s!"mathlib dependency in {path} is missing a non-empty 'git' field" - let rev ← match entry.rev with - | some r => - let r := r.trim - if r.isEmpty then - throw <| IO.userError s!"mathlib dependency in {path} is missing a non-empty 'rev' field" - else pure r - | none => - throw <| IO.userError s!"mathlib dependency in {path} is missing a non-empty 'rev' field" - return { name := "mathlib", git := git, rev := rev } - -/-! ## ExtractedTheorem (subprocess result) -/ - -structure ExtractedTheorem where - declarationName : String - module : String - startLine : Nat - startColumn : Nat - endLine : Nat - endColumn : Nat - explicitParameters : Option (Array String) := none - sameModuleDependencies : Array String - holeDependentDependencies : Array String := #[] - kind : String - deriving Inhabited - -def parseExtractedTheorem (payload : String) : Except String ExtractedTheorem := do - let json ← Json.parse payload - let declarationName ← json.getObjValAs? String "declarationName" - let module ← json.getObjValAs? String "module" - let kind ← json.getObjValAs? String "kind" - let range ← json.getObjVal? "sourceRange" - let startLine ← range.getObjValAs? Nat "startLine" - let startColumn ← range.getObjValAs? Nat "startColumn" - let endLine ← range.getObjValAs? Nat "endLine" - let endColumn ← range.getObjValAs? Nat "endColumn" - let explicitParameters ← match json.getObjVal? "explicitParameters" with - | .error _ => pure none - -- `null` for a declaration whose signature the extractor could not read. - | .ok paramsJson => - match paramsJson.getArr? with - | .error _ => pure none - | .ok paramsJson => do - let mut params : Array String := #[] - for paramJson in paramsJson do - params := params.push (← paramJson.getStr?) - pure (some params) - let depNames : Array String ← - match json.getObjVal? "sameModuleDependencies" with - | .error _ => pure #[] - | .ok arrJ => do - let arr ← arrJ.getArr? - let mut acc : Array String := #[] - for d in arr do - let s ← d.getStr? - acc := acc.push s - pure acc - let holeDependentDepNames : Array String ← - match json.getObjVal? "holeDependentDependencies" with - | .error _ => pure #[] - | .ok arrJ => do - let arr ← arrJ.getArr? - let mut acc : Array String := #[] - for d in arr do - acc := acc.push (← d.getStr?) - pure acc - return { - declarationName, module, startLine, startColumn, endLine, endColumn, explicitParameters - sameModuleDependencies := depNames - holeDependentDependencies := holeDependentDepNames - kind - } - -def buildExtractor (root : System.FilePath) (entries : Array EvalProblemMetadata) : - IO Unit := do - let modules := uniqueModules entries - let _ ← runCmdCheckedCaptured "lake" - (#["build"] ++ modules ++ #["extract_theorem"]) root - "Failed to build Lean theorem extractor" - pure () - -def extractOne (root : System.FilePath) (entry : EvalProblemMetadata) (hole : String) : - IO ExtractedTheorem := do - let binPath := root / ".lake" / "build" / "bin" / "extract_theorem" - let out ← runCmdCheckedCaptured "lake" - (#["env", binPath.toString, entry.moduleName, hole] ++ entry.holes) root - s!"Lean extraction failed for '{entry.id}' hole '{hole}'" - match parseExtractedTheorem out.stdout with - | .ok e => pure e - | .error err => - throw <| IO.userError - s!"Lean extractor returned invalid JSON for '{entry.id}' hole '{hole}': {err}" - -/-! ## Source paths -/ - -def moduleSourcePath (root : System.FilePath) (moduleName : String) : System.FilePath := Id.run do - let parts := moduleName.splitOn "." - let mut path := root - for p in parts do - path := path / p - return path.addExtension "lean" - -def ileanPath (root : System.FilePath) (moduleName : String) : System.FilePath := Id.run do - let parts := moduleName.splitOn "." - let mut path := root / ".lake" / "build" / "lib" / "lean" - for p in parts do - path := path / p - return path.addExtension "ilean" - -/-! ## Source-as-Array-Char utilities - -Source-text manipulation works on `Array Char` so we can use `Nat` indices -directly — that is, `Source` is indexed by *codepoint*. `.ilean` columns are -UTF-16 code units and so need converting (`Source.offsetForLineUtf16Column`); -`Lean.Position` columns are already codepoints. This matches Python's -codepoint-indexed string semantics, which the -upstream `scripts/generate_projects.py` relies on (e.g. when applying offsets -from `.ilean`, which records codepoint columns). -/ - -abbrev Source := Array Char - -def Source.ofString (s : String) : Source := s.toList.toArray - -def Source.toString (s : Source) : String := String.mk s.toList - -def Source.size (s : Source) : Nat := Array.size s - -/-- Slice `s[start:end]` as a String. -/ -def Source.slice (s : Source) (start endIdx : Nat) : String := - let endIdx := min endIdx s.size - let start := min start endIdx - String.mk (s.toList.drop start |>.take (endIdx - start)) - -/-- The codepoint index at which 1-indexed `line` starts in `s`. -/ -private def Source.lineStartOffset (s : Source) (line : Nat) : IO Nat := do - if line < 1 then - throw <| IO.userError s!"Invalid source line {line}" - let mut currentLine : Nat := 1 - let mut idx : Nat := 0 - let n := s.size - while currentLine < line do - -- find next '\n' - let mut found := false - while idx < n do - if s[idx]! == '\n' then - idx := idx + 1 - found := true - break - idx := idx + 1 - if !found then - throw <| IO.userError s!"Source ended before line {line}" - currentLine := currentLine + 1 - return idx - -/-- Convert (1-indexed line, 0-indexed **codepoint** column) into a codepoint -index in `s`. Mirrors `offset_for_line_column` in -`scripts/generate_projects.py`. - -This is the convention of `Lean.Position`, so it is the one to use for every -range that reaches us through `findDeclarationRanges?` — that is, everything -carried on an `ExtractedTheorem`. Ranges read from a `.ilean` use the *other* -convention; see `Source.offsetForLineUtf16Column`. -/ -def Source.offsetForLineColumn (s : Source) (line col : Nat) : IO Nat := do - return (← s.lineStartOffset line) + col - -/-- Convert (1-indexed line, 0-indexed **UTF-16 code unit** column) into a -codepoint index in `s`. - -`.ilean` files store LSP ranges, and LSP columns count UTF-16 code units, while -`Source` is an `Array Char` indexed by codepoint. The two agree only inside the -Basic Multilingual Plane, and diverge on exactly the characters a Lean corpus is -likely to contain: the mathematical alphanumerics (`𝓧`, `𝔽`, `𝒞`, `𝔻`, `𝔸`, -`𝓡`, …) are all outside it and so count twice. - -Reading such a column as a codepoint offset runs past the end of its line. A -declaration's computed range then swallowed the following blank line and the -opening `/-` of the next comment, leaving an orphaned `-/` that parsed as -`unexpected token '-'`. - -Throws rather than clamping. A column past the end of its line, or one landing -inside a surrogate pair, means the `.ilean` disagrees with the source being -resolved against it — a stale build, or a file edited since. Returning the -nearest plausible offset would truncate a *trusted* declaration while still -emitting text that looks reasonable. -/ -def Source.offsetForLineUtf16Column (s : Source) (line col : Nat) : IO Nat := do - let mut idx ← s.lineStartOffset line - let n := s.size - let mut units : Nat := 0 - while units < col do - if idx ≥ n || s[idx]! == '\n' then - throw <| IO.userError - s!"`.ilean` column {col} runs past the end of line {line}; the metadata \ - is stale relative to the source. Rebuild the module and retry." - units := units + (if s[idx]!.val > 0xFFFF then 2 else 1) - idx := idx + 1 - if units != col then - throw <| IO.userError - s!"`.ilean` column {col} on line {line} lands inside a surrogate pair; \ - the metadata is stale relative to the source. Rebuild and retry." - return idx - -/-- Find the first occurrence of `needle` (a `List Char`) in `s` starting at -`start`, returning the codepoint index where the match starts. -/ -def Source.find (s : Source) (start : Nat) (needle : List Char) : Option Nat := Id.run do - let n := s.size - let m := needle.length - if m == 0 then return some start - let mut i := start - while i + m ≤ n do - let mut j := 0 - let mut matched := true - for c in needle do - if s[i + j]! != c then - matched := false - break - j := j + 1 - if matched then return some i - i := i + 1 - return none - -/-- Find the LAST occurrence of `needle` in `s` strictly before `endIdx`. -/ -def Source.rfind (s : Source) (endIdx : Nat) (needle : List Char) : Option Nat := Id.run do - let n := min endIdx s.size - let m := needle.length - if m == 0 then return some n - if m > n then return none - let mut i : Nat := n - m + 1 - while i > 0 do - let pos := i - 1 - let mut j := 0 - let mut matched := true - for c in needle do - if s[pos + j]! != c then - matched := false - break - j := j + 1 - if matched then return some pos - i := i - 1 - return none - -/-- True if `s[i:]` starts with `needle`. -/ -def Source.startsWithAt (s : Source) (i : Nat) (needle : List Char) : Bool := Id.run do - let n := s.size - let m := needle.length - if i + m > n then return false - let mut j := 0 - for c in needle do - if s[i + j]! != c then return false - j := j + 1 - return true - -/-! ## Text utilities (line-based) -/ - -/-- Index just past the closing delimiter of the block comment beginning at -`start` (which must point at a block-comment opener), accounting for nested -block comments. Returns `source.size` if the comment is unterminated. -/ -def blockCommentEnd (source : Source) (start : Nat) : Nat := Id.run do - let n := source.size - let openCh := "/-".toList - let closeCh := "-/".toList - let mut i := start - let mut depth : Nat := 0 - while i < n do - if Source.startsWithAt source i openCh then - depth := depth + 1 - i := i + 2 - else if Source.startsWithAt source i closeCh then - depth := depth - 1 - i := i + 2 - if depth == 0 then - return i - else - i := i + 1 - return n - -/-! ## Lexical scanning - -Anything that walks Lean source looking for a particular character — a `]` -closing an attribute, a `:=` introducing a body — has to know which occurrences -are code and which sit inside a comment or a literal. `Source.opaqueLexemeEnd?` -is the single place that knows how to step over the latter. -/ - -/-- Word boundary at codepoint index `i`: index is past-the-end, at position -0, or preceded by a non-word char. -/ -def Source.atWordStart (s : Source) (i : Nat) : Bool := - i == 0 || ( - let c := s[i - 1]! - !(c.isAlphanum || c == '_' || c == '\'')) - -def Source.atWordEnd (s : Source) (i : Nat) : Bool := - i ≥ s.size || ( - let c := s[i]! - !(c.isAlphanum || c == '_' || c == '\'')) - -/-- If `start` begins a line or block comment, return the codepoint index just -past it. Block comments nest; an unterminated comment ends at `s.size`. -/ -private def Source.commentEnd? (s : Source) (start : Nat) : Option Nat := - if Source.startsWithAt s start "--".toList then - some <| Id.run do - let mut i := start - while i < s.size && s[i]! != '\n' do - i := i + 1 - return i - else if Source.startsWithAt s start "/-".toList then - some (blockCommentEnd s start) - else - none - -/-- Skip whitespace and Lean comments from `start`. Block comments are nested. -/ -def Source.skipTrivia (s : Source) (start : Nat) : Nat := Id.run do - let mut i := start - while i < s.size do - if s[i]!.isWhitespace then - i := i + 1 - else if let some stop := Source.commentEnd? s i then - i := max stop (i + 1) - else - break - return i - -/-- If `start` begins a raw string literal — `r"…"`, `r#"…"#`, `r##"…"##`, … — -return the index just past it. Raw strings have no escapes and are closed only -by a quote followed by as many `#` as opened them. -/ -private def Source.rawStringEnd? (s : Source) (start : Nat) : Option Nat := Id.run do - if s[start]? != some 'r' || !Source.atWordStart s start then return none - let mut hashes : Nat := 0 - let mut i := start + 1 - while i < s.size && s[i]! == '#' do - hashes := hashes + 1 - i := i + 1 - if s[i]? != some '"' then return none - i := i + 1 - while i < s.size do - if s[i]! == '"' then - let mut j := i + 1 - let mut seen : Nat := 0 - while seen < hashes && s[j]? == some '#' do - seen := seen + 1 - j := j + 1 - if seen == hashes then return some j - i := i + 1 - return some s.size - -/-- If `start` begins a character literal, return its end. Apostrophes used in -identifiers are rejected by requiring a closing quote in the literal shape. -/ -private def Source.charLiteralEnd? (s : Source) (start : Nat) : Option Nat := - if start + 2 < s.size && s[start + 2]! == '\'' then some (start + 3) - else if start + 3 < s.size && s[start + 1]! == '\\' && s[start + 3]! == '\'' then - some (start + 4) - else none - -/-- Skip a French-quoted identifier such as `«a := by»`. -/ -private def Source.quotedIdentifierEnd (s : Source) (start : Nat) : Nat := Id.run do - let mut i := start + 1 - while i < s.size do - if s[i]! == '»' then return i + 1 - i := i + 1 - return s.size - -/-- Skip a double-quoted string in which a brace is just a brace. `start` must -point at the opening quote; the result is `s.size` if the string is -unterminated. -/ -private def Source.plainStringEnd (s : Source) (start : Nat) : Nat := Id.run do - let mut i := start + 1 - while i < s.size do - if s[i]! == '\\' then - i := min (i + 2) s.size - else if s[i]! == '"' then - return i + 1 - else - i := i + 1 - return s.size - -/-- Commands whose string argument Lean parses as an interpolated string even -though it carries no `!`. Kept to the one that occurs in this repository: -`logInfo "{"` and its siblings fall back to an ordinary term, so listing them -would misread a brace far more often than it would read one right. -/ -private def interpolatedStringCommands : Array String := - #["throwError"] - -/-- True when the token in front of the string opening at `start` says the -string interpolates, so that a `{` in it opens a term rather than standing for -itself: a `!`-suffixed prefix (`s!`, `m!`, `f!`) or one of -`interpolatedStringCommands`. - -The test is deliberately one-sided. Lean settles interpolation in the parser, so -no lookback can be exact — `throwErrorAt stx "…"` interpolates behind an -argument this does not see, and a user macro taking `interpolatedStr` is -invisible. Reading braces as holes when they are not is the costlier mistake, as -it runs the scan past the end of a perfectly ordinary `"{"`, so a string is read -plainly unless something says otherwise. `Source.declarationFollows` is what -keeps the remaining misreadings from doing damage. -/ -private def Source.stringIsInterpolated (s : Source) (start : Nat) : Bool := Id.run do - let mut i := start - while i > 0 && s[i - 1]!.isWhitespace do - i := i - 1 - let tokenEnd := i - while i > 0 && - (let c := s[i - 1]!; c.isAlphanum || c == '_' || c == '\'' || c == '.' || c == '!') do - i := i - 1 - if i == tokenEnd then return false - if s[tokenEnd - 1]! == '!' then return true - let mut token := "" - for k in [i : tokenEnd] do - token := token.push s[k]! - return interpolatedStringCommands.contains ((token.splitOn ".").getLast!) - -/-- What the scanner in `Source.interpolatedStringEnd?` is reading: the term -inside an interpolation hole, a string whose braces open further holes, or a -string whose braces stand for themselves. -/ -private inductive StringScanMode where - | hole - | interpolated - | plain - deriving BEq, Inhabited - -/-- Skip a double-quoted string reading each `{…}` as a hole carrying a term, -and return `none` if the literal never closes that way. `start` must point at the -opening quote. - -A string opened inside a hole carries holes of its own only if it is itself -interpolated: in `s!"{f "a{b"}"` the inner literal's brace stands for itself, and -reading it as a hole would leave the outer string looking unterminated. -/ -private def Source.interpolatedStringEnd? (s : Source) (start : Nat) : Option Nat := Id.run do - let n := s.size - let mut i := start + 1 - -- One entry per nested construct, innermost last. - let mut modes : Array StringScanMode := #[.interpolated] - while i < n do - let mode := modes.back! - if mode != .hole then - if s[i]! == '\\' then i := min (i + 2) n - else if s[i]! == '"' then - modes := modes.pop - i := i + 1 - if modes.isEmpty then return some i - else if s[i]! == '{' && mode == .interpolated then - modes := modes.push .hole - i := i + 1 - else i := i + 1 - else if let some stop := Source.commentEnd? s i then i := max stop (i + 1) - else if let some stop := Source.rawStringEnd? s i then i := stop - else if s[i]! == '"' then - modes := modes.push (if Source.stringIsInterpolated s i then .interpolated else .plain) - i := i + 1 - else if s[i]! == '\'' then i := (Source.charLiteralEnd? s i).getD (i + 1) - else if s[i]! == '«' then i := Source.quotedIdentifierEnd s i - else if s[i]! == '{' then modes := modes.push .hole; i := i + 1 - else if s[i]! == '}' then modes := modes.pop; i := i + 1 - else i := i + 1 - return none - -/-- Skip a double-quoted string. `start` must point at the opening quote. An -interpolated string that never closes as one is read plainly, so a `{` the -lookback misjudged costs nothing. -/ -private def Source.stringLiteralEnd (s : Source) (start : Nat) : Nat := - if Source.stringIsInterpolated s start then - (Source.interpolatedStringEnd? s start).getD (Source.plainStringEnd s start) - else - Source.plainStringEnd s start - -/-- If the string opening at `start` is one whose two readings disagree about -where it ends, return the further of the two. - -That disagreement is the whole of what `Source.stringIsInterpolated` has to -guess at, and it is what every way this scanner can be made to edit string -contents needs: a hole holding a string, read plainly, puts the hole's text in -front of the scanner as if it were code. Refusing to strip anything inside the -span the two readings dispute removes the guess from the answer — whichever -reading is right, that text was somebody's string or somebody's code, and this -pass declines to say which. - -A reading that never closes disagrees too, and by more than any other: it says -the literal runs to the end of the input, so that is the span. It costs nothing -to say so. A string carrying a brace it does not close is what it takes, and -appending a marker to each of Mathlib's 8312 files strips all 8312. -/ -private def Source.disputedStringEnd? (s : Source) (start : Nat) : Option Nat := - match Source.interpolatedStringEnd? s start with - | none => some s.size - | some interpolated => - let plain := Source.plainStringEnd s start - if interpolated == plain then none else some (max interpolated plain) - -/-- If `start` begins a syntax quotation `` `(…) ``, return the codepoint index -just past its closing parenthesis. What a quotation holds is syntax the -declaration *builds*, not syntax applied to it, so an `@[eval_problem]` inside -one belongs to the macro's output and must survive. -/ -private def Source.quotationEnd? (s : Source) (start : Nat) : Option Nat := Id.run do - if s[start]? != some '`' || s[start + 1]? != some '(' then return none - let mut i := start + 2 - let mut depth : Nat := 1 - while i < s.size do - if let some stop := Source.commentEnd? s i then i := max stop (i + 1) - else if let some stop := Source.rawStringEnd? s i then i := stop - else if s[i]! == '"' then i := Source.stringLiteralEnd s i - else if s[i]! == '\'' then i := (Source.charLiteralEnd? s i).getD (i + 1) - else if s[i]! == '«' then i := Source.quotedIdentifierEnd s i - else if s[i]! == '(' then depth := depth + 1; i := i + 1 - else if s[i]! == ')' then - depth := depth - 1 - i := i + 1 - if depth == 0 then return some i - else i := i + 1 - return some s.size - -/-- If `start` begins a lexeme whose interior must not be read as code — a line -or block comment, a string, raw string or character literal, a French-quoted -identifier, or a syntax quotation — return the codepoint index just past it; -`none` for ordinary code. - -The result is always strictly greater than `start`, so a scanner can step to it -unconditionally. An unterminated lexeme ends at `s.size`. -/ -def Source.opaqueLexemeEnd? (s : Source) (start : Nat) : Option Nat := Id.run do - if start ≥ s.size then return none - let stop? : Option Nat := - Source.commentEnd? s start |>.orElse fun _ => - Source.rawStringEnd? s start |>.orElse fun _ => - Source.quotationEnd? s start |>.orElse fun _ => - match s[start]! with - | '"' => some (Source.stringLiteralEnd s start) - | '\'' => Source.charLiteralEnd? s start - | '«' => some (Source.quotedIdentifierEnd s start) - | _ => none - return stop?.map (max · (start + 1)) - -/-- Return `(endOfLastImport, bodyStart)` as codepoint indices in `source`. -Comments and whitespace are treated as header trivia, including nested block -comments. Thus comments before or between imports are included in -`endOfLastImport`, while a module doc comment after the last import remains -available to callers slicing from that offset. -/ -def scanHeader (source : Source) : Nat × Nat := Id.run do - let n := source.size - let mut i : Nat := 0 - let mut endOfLastImport : Nat := 0 - while i < n do - while i < n && source[i]!.isWhitespace do - i := i + 1 - if i == n then return (endOfLastImport, n) - if Source.startsWithAt source i "--".toList then - while i < n && source[i]! != '\n' do - i := i + 1 - continue - if Source.startsWithAt source i "/-".toList then - i := blockCommentEnd source i - continue - let importEnd := i + "import".length - if Source.startsWithAt source i "import".toList - && importEnd < n && source[importEnd]!.isWhitespace then - while i < n && source[i]! != '\n' do - i := i + 1 - if i < n then i := i + 1 - endOfLastImport := i - continue - return (endOfLastImport, i) - return (endOfLastImport, n) - -/-- Codepoint index just after the last import in the source header. -/ -def importPreludeLength (source : Source) : Nat := - (scanHeader source).1 - -/-- The name of the marker attribute, as it is spelled in source. -/ -private def evalProblemAttrName : String := "eval_problem" - -/-- A parsed `@[…]` attribute block. -/ -private structure AttributeBlock where - /-- Codepoint index just past the closing `]`. -/ - stop : Nat - /-- Codepoint spans of the comma-separated attribute instances. Each runs from - just after the previous separator to the separator or `]` that ends it, so it - carries whatever trivia the author wrote around the attribute. -/ - items : Array (Nat × Nat) - -/-- Parse the attribute block opening at `start`, which must point at `@[`. - -The closing `]` and the separating commas are recognised only at bracket depth -zero and outside comments and literals, so neither `deprecated "use foo] bar"` -nor `simp [a, b]` can end the block or split its list early. - -`none` if the block is unterminated. -/ -private def Source.attributeBlockEnd? (s : Source) (start : Nat) : Option AttributeBlock := - Id.run do - let n := s.size - let mut i := start + 2 - let mut itemStart := i - let mut items : Array (Nat × Nat) := #[] - let mut depth : Nat := 0 - while i < n do - if let some lexemeEnd := Source.opaqueLexemeEnd? s i then - i := lexemeEnd - else - match s[i]! with - | '[' | '(' | '{' | '⟨' => depth := depth + 1; i := i + 1 - | ')' | '}' | '⟩' => depth := depth - 1; i := i + 1 - | ']' => - if depth == 0 then - return some { stop := i + 1, items := items.push (itemStart, i) } - depth := depth - 1; i := i + 1 - | ',' => - if depth == 0 then - items := items.push (itemStart, i) - itemStart := i + 1 - i := i + 1 - | _ => i := i + 1 - return none - -/-- Modifiers Lean allows between an attribute block and the keyword that -introduces the declaration it modifies. -/ -private def declarationModifiers : Array String := - #["private", "protected", "noncomputable", "unsafe", "partial", "nonrec", - "scoped", "local", "public", "meta"] - -/-- Keywords that introduce a declaration an attribute block can modify. -/ -private def declarationKeywords : Array String := - #["theorem", "lemma", "def", "abbrev", "instance", "example", "axiom", - "opaque", "structure", "class", "inductive", "coinductive", "alias", - "mutual", "macro", "macro_rules", "elab", "elab_rules", "syntax", "notation", - "infix", "infixl", "infixr", "prefix", "postfix", "initialize", - "builtin_initialize", "register_simp_attr", "register_option", - "declare_syntax_cat", "irreducible_def", "instance_reducible"] - -/-- True when a declaration follows the attribute block ending at `stop`. - -Lean accepts `@[…]` only in front of a declaration, so this corroborates the -scanner's reading against the grammar: text that merely looks like the marker, -in a string the scanner has misread as code, is not usually followed by one. - -Read together with the command-position test in `stripProblemMarkers`, this is -what bounds the damage every remaining way this file's lexer can be wrong — an -interpolation it did not expect, a syntax extension it cannot know about. Both -tests are on text, so neither is sound the way the parser would be; what they -buy is that a misreading costs a marker left in place, which the generated -workspace reports as `unknown attribute [eval_problem]`, rather than an edit to -somebody's source that nothing announces. An unlisted declaration keyword costs -the same, which is why erring towards a longer list is right. -/ -private def Source.declarationFollows (s : Source) (stop : Nat) : Bool := Id.run do - let mut i := Source.skipTrivia s stop - while i < s.size do - if Source.startsWithAt s i "@[".toList then - -- Lean allows any number of attribute blocks in front of a declaration. - match Source.attributeBlockEnd? s i with - | some block => i := Source.skipTrivia s (max block.stop (i + 1)) - | none => return false - else - for keyword in declarationKeywords do - if Source.startsWithAt s i keyword.toList && Source.atWordEnd s (i + keyword.length) then - return true - let mut next := i - for modifier in declarationModifiers do - if next == i && Source.startsWithAt s i modifier.toList - && Source.atWordEnd s (i + modifier.length) then - next := Source.skipTrivia s (i + modifier.length) - if next == i then return false - i := max next (i + 1) - return false - -/-- True when the attribute instance spanning `[start, stop)` is the marker and -nothing else. Lean lets trivia sit anywhere in the list, so -`@[/- why -/ eval_problem]` applies the marker just as `@[eval_problem]` does, -and it accepts the French-quoted spelling `@[«eval_problem»]` as the same name. -/ -private def Source.itemIsMarker (s : Source) (start stop : Nat) : Bool := Id.run do - let nameStart := min (Source.skipTrivia s start) stop - let quoted := Source.startsWithAt s nameStart ("«" ++ evalProblemAttrName ++ "»").toList - let nameStop := - if quoted then nameStart + evalProblemAttrName.length + 2 - else nameStart + evalProblemAttrName.length - if !quoted then - if !(Source.startsWithAt s nameStart evalProblemAttrName.toList) then return false - if !(Source.atWordEnd s nameStop) then return false - if nameStop > stop then return false - return min (Source.skipTrivia s nameStop) stop == stop - -/-- True when the attribute instance spanning `[start, stop)` names no attribute -at all. Lean rejects `@[simp,]`, but the stripper should not turn such a block -into `@[]` and call it progress. -/ -private def Source.itemIsEmpty (s : Source) (start stop : Nat) : Bool := - Source.skipTrivia s start ≥ stop - -/-- True when `s[start:stop)` is entirely whitespace. -/ -private def Source.isBlankRange (s : Source) (start stop : Nat) : Bool := Id.run do - let mut i := start - while i < min stop s.size do - if !s[i]!.isWhitespace then return false - i := i + 1 - return true - -/-- Codepoint index at which the line containing `i` begins. -/ -private def Source.lineStartAt (s : Source) (i : Nat) : Nat := Id.run do - let mut j := min i s.size - while j > 0 && s[j - 1]! != '\n' do - j := j - 1 - return j - -/-- Codepoint index just past the newline that ends the line containing `i`, or -`s.size` if that line is unterminated. -/ -private def Source.lineEndAt (s : Source) (i : Nat) : Nat := Id.run do - let mut j := min i s.size - while j < s.size do - j := j + 1 - if s[j - 1]! == '\n' then return j - return s.size - -/-- The span to delete for text at `[start, stop)` that has nothing but -whitespace for company on its lines: those whole lines, together with the blank -lines bracketing them. This is what makes a marker on a line of its own leave -no gap behind. - -`floor` bounds how far back the span may reach, so a deletion can never eat -into text an earlier deletion already claimed. -/ -private def Source.blankEatingSpan (s : Source) (start stop floor : Nat) : Nat × Nat := - Id.run do - let mut a := max floor (Source.lineStartAt s start) - while a > floor do - let previous := max floor (Source.lineStartAt s (a - 1)) - if !Source.isBlankRange s previous a then break - a := previous - let mut b := Source.lineEndAt s stop - while b < s.size do - let next := Source.lineEndAt s b - if !Source.isBlankRange s b next then break - b := next - return (a, b) - -/-- Codepoint index of the first character at or after `start` that is neither a -space nor a tab. -/ -private def Source.skipInlineSpace (s : Source) (start : Nat) : Nat := Id.run do - let mut i := start - while i < s.size && (s[i]! == ' ' || s[i]! == '\t') do - i := i + 1 - return i - -/-- Codepoint index of the first non-whitespace character at or after `start`. -/ -private def Source.skipWhitespace (s : Source) (start : Nat) : Nat := Id.run do - let mut i := start - while i < s.size && s[i]!.isWhitespace do - i := i + 1 - return i - -/-- Codepoint index of the first character at or before `start`, and not before -`floor`, that is preceded by neither a space nor a tab. -/ -private def Source.rewindInlineSpace (s : Source) (start floor : Nat) : Nat := Id.run do - let mut i := start - while i > floor && (s[i - 1]! == ' ' || s[i - 1]! == '\t') do - i := i - 1 - return i - -/-- The span to delete to remove the marker text at `[start, stop)` — a whole -attribute block, or an import command — from the source around it. -/ -private def Source.markerRemoval (s : Source) (start stop floor : Nat) : Nat × Nat := - let blankBefore := Source.isBlankRange s (Source.lineStartAt s start) start - let blankAfter := Source.isBlankRange s stop (Source.lineEndAt s stop) - if blankBefore && blankAfter then - Source.blankEatingSpan s start stop floor - else if blankAfter then - -- A prefix command such as `include x in` precedes the marker and the line - -- ends with it, so the space that separated the two goes as well. - (Source.rewindInlineSpace s start floor, Source.skipInlineSpace s stop) - else - -- The declaration shares the line with the marker: only the marker and the - -- gap after it go, leaving any indentation in place. - (start, Source.skipInlineSpace s stop) - -/-- The spans to delete to remove the attribute instances at indices `markers` -from `block`, given that at least one instance survives. - -Each removal takes a separating comma with it: the one after the instance where -there is a later survivor, and otherwise the one before it, so exactly as many -commas go as instances. Everything else is left as the author wrote it — -reprinting the survivors instead would drop the line break after a comment among -them and so comment out the closing `]`. -/ -private def Source.markerItemRemovals (s : Source) (block : AttributeBlock) - (markers : List Nat) : Array (Nat × Nat) := Id.run do - -- The instances from `tail` on are all markers, so they share the one comma - -- in front of them; those before it each take the comma that follows. - let mut tail := block.items.size - while tail > 0 && markers.contains (tail - 1) do - tail := tail - 1 - let mut removals : Array (Nat × Nat) := #[] - for k in markers do - if k < tail then - -- Up to the next instance's first character, so its indentation goes too. - -- Only whitespace: a comment there introduces the instance that survives. - removals := removals.push (block.items[k]!.1, Source.skipWhitespace s (block.items[k]!.2 + 1)) - if tail < block.items.size then - -- Back over the spaces before the comma, but not over a line break: that - -- break may be what ends a comment in the instance before it. - let survivor := block.items[tail - 1]! - removals := removals.push - (Source.rewindInlineSpace s survivor.2 survivor.1, block.items[block.items.size - 1]!.2) - -- Consecutive markers share the whitespace between them, so their spans can - -- meet: `@[eval_problem, eval_problem, simp]` has the first run on to the - -- second's name while the second starts at the comma before it. Coalesce. - let mut coalesced : Array (Nat × Nat) := #[] - for (a, b) in removals do - match coalesced.back? with - | some (previousStart, previousStop) => - if a ≤ previousStop then - coalesced := coalesced.set! (coalesced.size - 1) (previousStart, max previousStop b) - else - coalesced := coalesced.push (a, b) - | none => coalesced := coalesced.push (a, b) - return coalesced - -/-- If an `import` command begins at `i`, return the module it names and the -codepoint index just past the command, any comment trailing it on the same line -included. Trivia may sit anywhere in the command, so `import /- why -/ Foo` and -an `import` whose module name is on the next line are both read. - -`none` if a token other than a comment follows the module name on its line: a -second command sharing the line is not this one's to delete. That matches what -`scanHeader` assumes of the header it walks. -/ -private def Source.importAt? (s : Source) (i : Nat) : Option (String × Nat) := Id.run do - if !(Source.startsWithAt s i "import".toList) then return none - let mut j := i + "import".length - if !(Source.atWordEnd s j) then return none - j := Source.skipTrivia s j - let nameStart := j - while j < s.size && - (let c := s[j]!; c.isAlphanum || c == '_' || c == '\'' || c == '.') do - j := j + 1 - if j == nameStart then return none - let mut name := "" - for k in [nameStart : j] do - name := name.push s[k]! - -- A comment closing on the same line trails the import and goes with it. One - -- that runs past the line is left alone, and a doc comment always is: `import - -- Foo /-- … -/` documents the declaration after it, not the import. - let lineStop := Source.lineEndAt s j - let mut stop := j - let mut atEnd := false - while !atEnd do - let next := Source.skipInlineSpace s j - if Source.startsWithAt s next "/--".toList || Source.startsWithAt s next "/-!".toList then - -- Documents the declaration after it, not the import; the command ends - -- at the module name and the comment stays where the author put it. - atEnd := true - else match Source.commentEnd? s next with - | some commentStop => - if commentStop > lineStop then - atEnd := true - else - j := max commentStop (next + 1) - stop := j - | none => - if next < s.size && s[next]! != '\n' then return none - atEnd := true - return some (name, stop) - -/-- If an `import` command this pass drops begins at `i`, return the codepoint -index just past it. `freshLine` records that only trivia precedes `i` on its -line, which is where an `import` is a command rather than a stray identifier. -/ -private def strippedImportStop? (s : Source) (i : Nat) (freshLine : Bool) - (locals : Array String) : Option Nat := - if !freshLine then none - else match Source.importAt? s i with - | some (name, stop) => - if name == "EvalTools.Markers" || locals.contains name then some stop else none - | none => none - -/-- Strip `@[eval_problem]` attributes, `import EvalTools.Markers` lines, and -`import ` lines for each repo-local module `m` in `localImports` from -`source`. Where a stripped marker occupied whole lines, the blank lines -immediately before and after it are dropped too — mirroring the greedy `\s*` -runs that bracketed the attribute in Python's `_strip_problem_markers` regex. - -The scan is lexical rather than line-oriented, so it sees the marker in every -position Lean accepts it and nowhere else: - -* the attribute may share its line with the declaration - (`@[eval_problem] theorem foo …`) or with a prefix command - (`set_option autoImplicit false in @[eval_problem] theorem foo …`); -* it may span several lines, and may carry trivia (`@[/- why -/ eval_problem]`); -* its list is split on commas at bracket depth zero, and closed by the first - `]` at that depth, so `@[eval_problem, deprecated "use foo] instead"]` and - `@[eval_problem, simp [a, b]]` keep their siblings intact; -* siblings are spliced out of the source rather than reprinted, so a comment - among them keeps the line break that terminates it; -* text inside a string literal, a comment or a syntax quotation is never - mistaken for code, so neither a multiline string containing - `@[eval_problem]` nor a macro building one is touched. - -A deleted line leaves the newline that introduced it, so stripping the last -line of a file does not run the one before it into the end of the text. - -Lexing Lean without its parser cannot be exact — whether a `{` in a string opens -an interpolation hole is settled by the grammar, and the grammar is extensible. -Three things keep that inexactness from editing somebody's string. A marker is -stripped only in command position and only in front of a declaration; and no -span two readings of a string literal disagree about is stripped from at all. -The first two are tests on text, which a string can reproduce; the third is not -a test on the marker but on how the scanner came to be looking at it, and -reaching marker-shaped text inside a literal takes exactly the disagreement it -refuses to resolve. - -What is left over is a marker left in place, which the generated workspace -reports as `unknown attribute [eval_problem]` when it is built. That is the -failure this is tuned for: exactness here wants the parser, which wants an -environment, which this signature does not have. - -Two ways in remain, both needing a `syntax` declaration to reach: a token -carrying a `)` closes a quotation early, and a token carrying a `"` or a brace -can put the two readings of a string back into agreement on the wrong answer. -Neither is reachable by lexing alone, which is why they are the boundary of what -this approach can do rather than a bug in it. -/ -def stripProblemMarkers (source : String) (localImports : Array String := #[]) : String := - Id.run do - let s := Source.ofString source - let n := s.size - -- Codepoint spans to delete, in increasing order and disjoint. - let mut edits : Array (Nat × Nat) := #[] - -- End of the last edit, so no later deletion reaches back over it. - let mut floor : Nat := 0 - let mut i : Nat := 0 - -- Whether only trivia precedes `i` on its line — an `import` is a command - -- only there, though a comment may sit in front of it. - let mut freshLine := true - -- Whether a command could begin at `i`: at the head of its line, after the - -- `in` of a prefix command, or after an attribute block. Only there does - -- `@[…]` modify a declaration, so only there is it a marker to strip. - let mut commandStart := true - -- End of the furthest span two readings of a string literal disagree about. - -- Nothing inside one is stripped: the scanner does not know whether it is - -- looking at code or at the contents of somebody's string. - let mut disputedUntil : Nat := 0 - while i < n do - if let some commentEnd := Source.commentEnd? s i then - i := max commentEnd (i + 1) - else if let some lexemeEnd := Source.opaqueLexemeEnd? s i then - if s[i]! == '"' then - if let some disputedEnd := Source.disputedStringEnd? s i then - disputedUntil := max disputedUntil disputedEnd - freshLine := false - commandStart := false - i := lexemeEnd - else if let some importStop := - strippedImportStop? s i (freshLine && i ≥ disputedUntil) localImports then - let (a, b) := Source.markerRemoval s i importStop floor - edits := edits.push (a, b) - floor := b - freshLine := b > 0 && s[b - 1]! == '\n' - commandStart := freshLine - i := b - else if Source.startsWithAt s i "@[".toList then - freshLine := false - match Source.attributeBlockEnd? s i with - | none => - commandStart := false - i := i + 2 - | some block => - let inCommandPosition := commandStart && i ≥ disputedUntil - let markers := - if inCommandPosition && Source.declarationFollows s block.stop then - (List.range block.items.size).filter fun k => - let (a, b) := block.items[k]! - Source.itemIsMarker s a b - else - [] - let survives := (List.range block.items.size).any fun k => - let (a, b) := block.items[k]! - !markers.contains k && !Source.itemIsEmpty s a b - -- Another attribute block may follow this one — but only where this one - -- was itself at the head of a command. - commandStart := inCommandPosition - if markers.isEmpty then - i := block.stop - else if !survives then - let (a, b) := Source.markerRemoval s i block.stop floor - edits := edits.push (a, b) - floor := b - freshLine := b > 0 && s[b - 1]! == '\n' - i := b - else - edits := edits ++ Source.markerItemRemovals s block markers - floor := block.stop - i := block.stop - else if Source.startsWithAt s i "in".toList && Source.atWordStart s i - && Source.atWordEnd s (i + 2) then - -- The `in` of `open … in`, `set_option … in`, `include … in`: what - -- follows begins a command, so an attribute may sit there. - freshLine := false - commandStart := true - i := i + 2 - else - if s[i]! == '\n' then - freshLine := true - commandStart := true - else if !s[i]!.isWhitespace then - freshLine := false - commandStart := false - i := i + 1 - let mut parts : Array String := #[] - let mut pos : Nat := 0 - for (a, b) in edits do - parts := parts.push (Source.slice s pos a) - pos := b - return String.join (parts.push (Source.slice s pos n)).toList - -/-- Find the offset (codepoint index) of the first top-level `end ...` line at -or after `start`. Returns `source.size` if none found. Mirrors -`find_top_level_end_offset`. -/ -def findTopLevelEndOffset (source : Source) (start : Nat) : Nat := Id.run do - let n := source.size - let mut i := start - while i < n do - -- start of a line. Check if line (verbatim, no leading whitespace) matches - -- `end` optionally followed by `\s+` and then end-of-line. - let lineStart := i - -- find end of line - let mut j := i - while j < n && source[j]! != '\n' do - j := j + 1 - let lineEnd := j - -- right-trim - let mut k := lineEnd - while k > lineStart && source[k - 1]!.isWhitespace do - k := k - 1 - -- match `end` exactly or `end ` - let endChars := "end".toList - let isEnd : Bool := Id.run do - if !(Source.startsWithAt source lineStart endChars) then return false - let afterEnd := lineStart + 3 - if afterEnd == k then return true - if afterEnd < k && (source[afterEnd]! == ' ' || source[afterEnd]! == '\t') then - -- there must be some non-whitespace token before k - let mut p := afterEnd - while p < k && source[p]!.isWhitespace do - p := p + 1 - return p < k - return false - if isEnd then return lineStart - -- next line - if j < n then i := j + 1 else i := j - return n - -/-! ## Source imports -/ - -/-- The modules a source file imports, in source order, parsed with Lean's own -header parser. - -Hand-rolling this is a trap. A line scan misses - - import - Mathlib.Real - -a whitespace-token scan additionally misreads `import all Init.Core` as -importing `all`, `import/-c-/Init` as importing nothing (comments separate -tokens without whitespace), and `import «Foo Bar»` as importing `«Foo` (escaped -identifiers may contain spaces). The real grammar is -`[public]? [meta]? import [all]? ident`. `Lean.Parser.parseHeader` gets -all of this right by construction, and stays right when the grammar changes. - -Throws on a header the generator cannot faithfully reproduce, rather than -approximating it: the workspace files it writes are plain (non-`module`) Lean, -so `module`, `prelude`, `public import`, `meta import` and `import all` would -all be silently flattened into something with different visibility or a -different environment. No problem module in the catalog uses these today. -/ -def sourceImports (source : String) (context : String := "") : - IO (Array String) := do - let inputCtx := Lean.Parser.mkInputContext source context - let (header, _, messages) ← Lean.Parser.parseHeader inputCtx - if messages.hasErrors then - throw <| IO.userError s!"Could not parse the import header of {context}." - let parsedImports := Lean.Elab.HeaderSyntax.imports header (includeInit := false) - let importsWithImplicitInit := Lean.Elab.HeaderSyntax.imports header (includeInit := true) - if importsWithImplicitInit.size == parsedImports.size then - throw <| IO.userError - s!"{context} uses a `prelude` header, which a plain generated workspace \ - cannot reproduce." - if Lean.Elab.HeaderSyntax.isModule header then - throw <| IO.userError - s!"{context} uses a `module` header. Generated workspaces are plain Lean \ - files, so module-system visibility would not be reproduced." - let mut out : Array String := #[] - for imp in parsedImports do - if imp.importAll || imp.isMeta then - throw <| IO.userError - s!"{context} uses `import all` or `meta import` ({imp.module}), which a \ - plain generated workspace cannot reproduce." - out := out.push imp.module.toString - return out - -partial def repoLocalImportModulesAux (root : System.FilePath) (moduleName : String) - (seen : IO.Ref (Std.HashSet String)) : IO (Array String) := do - let path := moduleSourcePath root moduleName - if !(← path.pathExists) then return #[] - let source ← IO.FS.readFile path - let mut out : Array String := #[] - for imported in (← sourceImports source moduleName) do - if imported.startsWith "Mathlib." || imported == "Mathlib" then continue - if imported == "EvalTools" || imported.startsWith "EvalTools." then continue - if imported == moduleName then continue - if (← seen.get).contains imported then continue - let importedPath := moduleSourcePath root imported - if !(← importedPath.pathExists) then continue - seen.modify (·.insert imported) - let nested ← repoLocalImportModulesAux root imported seen - out := out ++ nested - out := out.push imported - return out - -def repoLocalImportModules (root : System.FilePath) (moduleName : String) : - IO (Array String) := do - let seen ← IO.mkRef ({} : Std.HashSet String) - repoLocalImportModulesAux root moduleName seen - -/-- Walk the import graph from `moduleName` in source order, emitting each -non-repository module the first time it is reached. - -Repo-local modules are recursed into rather than emitted: their declarations are -inlined into `ChallengeDeps.lean`, so it is their *imports* the workspace needs. -Following them in source order, depth first, is the closest flattening of the -order Lean itself would discover the modules in — emitting all local modules' -imports before the problem's own would put them in the wrong order, which can -matter for instance priority and other environment-extension state. - -`EvalTools.Markers` itself is dropped: it supplies the `@[eval_problem]` -attribute, which a standalone workspace neither has nor needs. Its external -imports are retained, however, because they are part of the environment in -which the problem module elaborated. Any *other* `EvalTools` import is refused -rather than silently dropped, since it would be carrying a real definition -into the statement. -/ -private partial def collectWorkspaceImports (root : System.FilePath) (moduleName : String) - (visited : IO.Ref (Std.HashSet String)) (out : IO.Ref (Array String)) : IO Unit := do - let path := moduleSourcePath root moduleName - if !(← path.pathExists) then return - for imported in (← sourceImports (← IO.FS.readFile path) moduleName) do - if imported == "EvalTools.Markers" then - -- Do not expose the repository-only marker attribute, but do preserve - -- the environment supplied by Markers. This matters for modules whose - -- only explicit import is EvalTools.Markers: dropping it outright would - -- incorrectly reduce their generated environment to Init. - unless (← visited.get).contains imported do - visited.modify (·.insert imported) - collectWorkspaceImports root imported visited out - continue - if imported == "EvalTools" || imported.startsWith "EvalTools." then - throw <| IO.userError - s!"Module '{moduleName}' imports '{imported}'. Only `EvalTools.Markers` is \ - supported: a generated workspace has no `EvalTools` library, so anything \ - else would be dropped from the statement's environment." - if imported == moduleName then continue - if (← (moduleSourcePath root imported).pathExists) then - -- Repo-local: inlined into ChallengeDeps, so recurse for its imports. - if (← visited.get).contains imported then continue - visited.modify (·.insert imported) - collectWorkspaceImports root imported visited out - else - unless (← out.get).contains imported do - out.modify (·.push imported) - -/-- The `import` header a generated workspace needs to reproduce the trusted -module's elaboration context. - -Substituting `import Mathlib` is not sound for a module written against narrow -imports: the full library brings names and tokens into scope that the author -never had. `gcd` becomes ambiguous between `Int.gcd` and `GCDMonoid.gcd`; `over` -becomes a reserved token, so a structure field written `[over : X.Over _]` stops -parsing. The statement a solver is given has to be read in the environment the -trusted statement was written in. - -A module that imports nothing external gets an empty header, not `import -Mathlib` — it elaborated against Lean's default environment, and adding Mathlib -would reintroduce exactly the ambiguities this is here to avoid. - -Known limitation: flattening several repo-local modules into one -`ChallengeDeps.lean` necessarily gives all of them the union of their imports, -so an inlined module can see a name that only a later one introduced. Avoiding -that would mean emitting one workspace module per source module. -/ -def problemImportHeader (root : System.FilePath) (moduleName : String) : IO String := do - let visited ← IO.mkRef ({} : Std.HashSet String) - let out ← IO.mkRef (#[] : Array String) - collectWorkspaceImports root moduleName visited out - let imports ← out.get - return String.join (imports.toList.map fun m => s!"import {m}\n") - -/-! ## ILean metadata -/ - -/-- A declaration's source range from the `.ilean`, as -`[startLine, startColumn, endLine, endColumn]` (`.ilean` records these -0-indexed; we convert lines to 1-indexed, the convention both offset functions -take). -The range spans the *whole* declaration, doc comment through the end of the -body, so `(endLine, endColumn)` is the precise end — no heuristic needed. - -The columns are LSP columns, counting UTF-16 code units, so they must be -resolved with `Source.offsetForLineUtf16Column` and never with -`Source.offsetForLineColumn`. -/ -structure IleanDeclEntry where - name : String - startLine : Nat - startColumn : Nat - endLine : Nat - endColumn : Nat - deriving Inhabited - -def loadIleanDeclRanges (root : System.FilePath) (moduleName : String) : - IO (Array IleanDeclEntry) := do - let path := ileanPath root moduleName - if !(← path.pathExists) then - throw <| IO.userError - s!"Compiled metadata for module '{moduleName}' not found: {path}" - let contents ← IO.FS.readFile path - let json ← match Json.parse contents with - | .ok j => pure j - | .error err => - throw <| IO.userError - s!"Invalid JSON in compiled metadata for module '{moduleName}': {err}" - let decls ← match json.getObjVal? "decls" with - | .ok d => pure d - | .error _ => return #[] - let obj ← match decls.getObj? with - | .ok o => pure o - | .error _ => return #[] - let mut out : Array IleanDeclEntry := #[] - for ⟨name, value⟩ in obj.toArray do - match value.getArr? with - | .error _ => continue - | .ok arr => - if arr.size < 4 then continue - match arr[0]!.getNat?, arr[1]!.getNat?, arr[2]!.getNat?, arr[3]!.getNat? with - | .ok line, .ok col, .ok endLine, .ok endCol => - out := out.push - { name, startLine := line + 1, startColumn := col - endLine := endLine + 1, endColumn := endCol } - | _, _, _, _ => continue - return out - -/-! ## Header scanning, namespace ops -/ - -/-- Insert `line` (must end in `\n`) just after the last import line at the -top of `source`. Mirrors `_inject_after_imports`. -/ -def injectAfterImports (source line : String) - (fallbackHeader : String := "import Mathlib\n") : String := Id.run do - let src := Source.ofString source - let (insertAt, _) := scanHeader src - if insertAt == 0 then - return fallbackHeader ++ line ++ source - let before := Source.slice src 0 insertAt - let after := Source.slice src insertAt src.size - return before ++ line ++ after - -/-- Top-level namespace names declared in `body`, in source order. Mirrors -`_top_level_namespaces`. -/ -def topLevelNamespaces (body userNamespace : String) : Array String := Id.run do - let mut byOrder : Array String := #[] - let mut seen : Std.HashSet String := {} - let mut depth : Int := 0 - for raw in body.splitOn "\n" do - let lstripped := raw.trimAsciiStart.toString - if lstripped.startsWith "--" then continue - if lstripped.startsWith "namespace " then - let rest := (lstripped.drop "namespace ".length).trimAscii.toString - let name := ((rest.splitOn " ").head!).trimAscii.toString - if depth == 0 && name != userNamespace && !seen.contains name then - byOrder := byOrder.push name - seen := seen.insert name - depth := depth + 1 - continue - -- `end` followed by space (or just `end`); Python uses `^end\b` - if lstripped.startsWith "end " || lstripped == "end" then - depth := depth - 1 - continue - return byOrder - -/-- `s[0:limit]` with every comment blanked out, newlines preserved so the -line structure survives. Handles `--` to end of line and nested block comments. -/ -def blankComments (s : Source) (limit : Nat) : String := Id.run do - let mut out : String := "" - let mut i : Nat := 0 - let mut depth : Nat := 0 - let n := min limit s.size - while i < n do - let c := s[i]! - if depth == 0 && Source.startsWithAt s i "--".toList then - while i < n && s[i]! != '\n' do - i := i + 1 - else if Source.startsWithAt s i "/-".toList then - depth := depth + 1 - i := i + 2 - else if depth > 0 && Source.startsWithAt s i "-/".toList then - depth := depth - 1 - i := i + 2 - else - if depth == 0 then out := out.push c - else if c == '\n' then out := out.push c - i := i + 1 - return out - -/-- True iff `s` begins with the complete keyword `kw`. -/ -private def startsWithKeyword (s kw : String) : Bool := - if !(s.startsWith kw) then false - else - let chars := s.toList.drop kw.length - match chars with - | [] => true - | c :: _ => !(c.isAlphanum || c == '_' || c == '\'') - -/-- Remove command modifiers that may precede a scope-opening command. Keeping -this normalization shared prevents the namespace/open and variable/syntax -walkers from assigning the matching `end` to different frames. -/ -private def stripScopeCommandModifiers (s : String) : String := Id.run do - let modifiers := #["noncomputable", "private", "protected", "scoped"] - let mut rest := s.trimAscii.toString - let mut changed := true - while changed do - changed := false - for modifier in modifiers do - if startsWithKeyword rest modifier then - rest := (rest.drop modifier.length).trimAsciiStart.toString - changed := true - break - return rest - -/-- Wrap `source`'s body in `namespace Submission ... end Submission`. -Mirrors `_wrap_body_in_submission_namespace`. -/ -def wrapBodyInSubmissionNamespace (source userNamespace : String) - (extraOpens : Array String := #[]) : String := Id.run do - let src := Source.ofString source - let (_, bodyStart) := scanHeader src - if bodyStart ≥ src.size then return source - let head := Source.slice src 0 bodyStart - let mut body := Source.slice src bodyStart src.size - if !body.endsWith "\n" then body := body ++ "\n" - -- Open `extraOpens` (the `_root_`-qualified enclosing namespaces of trusted - -- helpers now living in `ChallengeDeps`) together with the source's own - -- top-level namespaces (so cross-namespace references in the wrapped body - -- still resolve). `extraOpens` come first and are authoritative: a bare - -- auto-open of the same base name is redundant (it would resolve to the - -- wrapped `Submission.X`, not the helper's `_root_.X`) and is dropped. - let normalize := fun (s : String) => - if s.startsWith "_root_." then (s.drop 7).toString else s - let mut openNamespaces : Array String := #[] - let mut seenBase : Std.HashSet String := {} - for ns in extraOpens ++ topLevelNamespaces body userNamespace do - let base := normalize ns - if seenBase.contains base then continue - openNamespaces := openNamespaces.push ns - seenBase := seenBase.insert base - let opens := openNamespaces.foldl (fun acc ns => acc ++ s!"open {ns}\n") "" - -- Lean permits scopes (most often `noncomputable section`, but also a - -- namespace) to run to EOF. The source module then needs no explicit `end`, - -- but after placing that body inside `namespace Submission` an appended - -- `end Submission` would try to close the still-current source scope. Close - -- precisely the scopes that the original source intentionally left to EOF - -- before closing our wrapper. - let uncommented := blankComments (Source.ofString body) body.length - let scopeNameAfter := fun (line keyword : String) => - let rest := (line.drop keyword.length).trimAscii.toString - if rest.isEmpty then none else some rest - let mut scopeNames : Array (Option String) := #[] - for line in uncommented.splitOn "\n" do - let stripped := line.trimAscii.toString - let command := stripScopeCommandModifiers stripped - if startsWithKeyword command "namespace" then - scopeNames := scopeNames.push (scopeNameAfter command "namespace") - else if startsWithKeyword command "section" then - scopeNames := scopeNames.push (scopeNameAfter command "section") - else if startsWithKeyword stripped "end" && !scopeNames.isEmpty then - scopeNames := scopeNames.pop - let closes := "".intercalate <| scopeNames.toList.reverse.map fun name? => - match name? with - | some name => s!"end {name}\n" - | none => "end\n" - return head ++ "\nnamespace Submission\n\n" ++ opens ++ body ++ "\n" ++ closes ++ - "end Submission\n" - -/-! ## Theorem statement / binder parsing -/ - -/-- True when `needle` occurs in `haystack` as a whole identifier component — -not as part of a longer name. Used to decide whether kept source text actually -cites a declaration, so `id_hom` is not matched by `my_id_hom_lemma`. - -A leading `.` *is* allowed, because a source reference is usually qualified: -`PartialMap.id_domain` cites the declaration whose last component is -`id_domain`. Treating `.` as an identifier character would reject exactly the -references we are looking for. -/ -def containsIdentifier (haystack needle : String) : Bool := Id.run do - if needle.isEmpty then return false - let h := haystack.toList.toArray - let n := needle.toList.toArray - let isIdentChar : Char → Bool := fun c => c.isAlphanum || c == '_' || c == '\'' - if h.size < n.size then return false - for i in [0:h.size - n.size + 1] do - let mut matched := true - for j in [0:n.size] do - if h[i + j]! != n[j]! then - matched := false - break - if matched then - let beforeOk := i == 0 || !(isIdentChar h[i - 1]!) - let afterIdx := i + n.size - let afterOk := afterIdx ≥ h.size || !(isIdentChar h[afterIdx]!) - if beforeOk && afterOk then return true - return false - -def lastComponentStr (name : String) : String := - match (name.splitOn ".").getLast? with - | some s => s - | none => name - -/-- Find the first occurrence of `theorem ` (with word boundaries) at or -after `start`, returning the codepoint index just past the name. Mirrors the -header regex in `extract_statement_text`. -/ -def Source.findTheoremHeader (s : Source) (start : Nat) (name : String) : Option Nat := Id.run do - let needle := s!"theorem {name}".toList - let nameSize := name.length - let needleLen := needle.length - let mut i := start - let n := s.size - while i + needleLen ≤ n do - if Source.startsWithAt s i needle then - let prevOk := i == 0 || s[i - 1]!.isWhitespace - let endPos := i + needleLen - let afterOk := Source.atWordEnd s endPos - let _ := nameSize -- silence unused warning - if prevOk && afterOk then - return some endPos - i := i + 1 - return none - -/-- Locate the body marker of an eval-problem theorem without assuming the -literal spelling `:= by`. Candidates inside comments, strings, and brackets are -ignored, so a default binder value such as `(h : P := by tac)` cannot be -mistaken for the declaration body; arbitrary trivia may follow `:=`; and both -the usual `by sorry` body and a direct `sorry` body are accepted. - -An eval-problem hole's body is a `sorry`, so a candidate whose body is exactly -`sorry` (behind `by` or not) and runs to the end of the declaration wins over -every other candidate: a *statement* may itself contain a top-level -`haveI … := by …`, and that tactic block is not the body. - -Failing that — the `ci_regenerate_main_check` canary really is proved by -`trivial` — a candidate opening a tactic block is used, but only if it is the -only one. With a body that is not a `sorry` there is nothing left to tell an -assignment in the statement apart from an assignment in the proof, so `none` is -returned and the caller reports that it could not recover the statement. -/ -structure TheoremBody where - /-- Codepoint index of the `:=` that introduces the declaration's body. -/ - marker : Nat - /-- Whether that body is a bare `sorry`, possibly behind `by`. -/ - isBareSorry : Bool - deriving Inhabited - -def Source.findTheoremBodyMarker (s : Source) (start : Nat) : Option TheoremBody := Id.run do - let mut i := start - let mut roundDepth := 0 - let mut squareDepth := 0 - let mut braceDepth := 0 - let mut angleDepth := 0 - let mut sorryMarker : Option Nat := none - let mut tacticMarker : Option Nat := none - let mut tacticMarkers := 0 - while i < s.size do - if let some lexemeEnd := Source.opaqueLexemeEnd? s i then - i := lexemeEnd - else if s[i]! == '(' then roundDepth := roundDepth + 1; i := i + 1 - else if s[i]! == ')' then roundDepth := roundDepth - 1; i := i + 1 - else if s[i]! == '[' then squareDepth := squareDepth + 1; i := i + 1 - else if s[i]! == ']' then squareDepth := squareDepth - 1; i := i + 1 - else if s[i]! == '{' then braceDepth := braceDepth + 1; i := i + 1 - else if s[i]! == '}' then braceDepth := braceDepth - 1; i := i + 1 - else if s[i]! == '⟨' then angleDepth := angleDepth + 1; i := i + 1 - else if s[i]! == '⟩' then angleDepth := angleDepth - 1; i := i + 1 - else if roundDepth == 0 && squareDepth == 0 && braceDepth == 0 && angleDepth == 0 - && Source.startsWithAt s i ":=".toList then - let bodyStart := Source.skipTrivia s (i + 2) - let tacticBody := Source.startsWithAt s bodyStart "by".toList - && Source.atWordEnd s (bodyStart + "by".length) - let termStart := - if tacticBody then Source.skipTrivia s (bodyStart + "by".length) else bodyStart - if Source.startsWithAt s termStart "sorry".toList - && Source.atWordEnd s (termStart + "sorry".length) - && Source.skipTrivia s (termStart + "sorry".length) == s.size then - sorryMarker := some i - else if tacticBody then - tacticMarker := some i - tacticMarkers := tacticMarkers + 1 - i := i + 2 - else - i := i + 1 - return match sorryMarker with - | some marker => some { marker, isBareSorry := true } - | none => - if tacticMarkers == 1 then tacticMarker.map ({ marker := ·, isBareSorry := false }) - else none - -/-- Extract the theorem statement text from a sliced declaration body. -The body marker is found lexically so direct `:= sorry` holes and flexible -whitespace/comment formatting are supported. -/ -def extractStatementText (problemId : String) (sourcePath : System.FilePath) - (declarationText theoremName : String) : IO String := do - let src := Source.ofString declarationText - let some headerEnd := Source.findTheoremHeader src 0 theoremName - | throw <| IO.userError - s!"Could not recover theorem statement text for '{problemId}' from {sourcePath}" - let some body := Source.findTheoremBodyMarker src headerEnd - | throw <| IO.userError - s!"Could not recover theorem statement text for '{problemId}' from {sourcePath}" - if body.marker < headerEnd then - throw <| IO.userError - s!"Could not recover theorem statement text for '{problemId}' from {sourcePath}" - return (Source.slice src headerEnd body.marker).trimAscii.toString - -/-- True when the sliced declaration's body is a bare `sorry`, possibly behind -`by`. Only then does the elaborated value carry one lambda per signature -binder, so only then is the extractor's parameter list meaningful: `by intro x; -sorry` elaborates to a lambda over `sorryAx` as well, but its lambda belongs to -the statement. -/ -def hasBareSorryBody (declarationText : String) : Bool := - match Source.findTheoremBodyMarker (Source.ofString declarationText) 0 with - | some body => body.isBareSorry - | none => false - -/-- Parse leading binders off a theorem-statement string. Returns pairs of -`(opener, body)` for each leading `(...)`, `{...}`, or `[...]` group. -/ -def leadingBinders (statement : String) : Array (Char × String) := Id.run do - let s := Source.ofString statement - let n := s.size - let mut binders : Array (Char × String) := #[] - let mut i : Nat := 0 - let mut done := false - while i < n && !done do - while i < n && s[i]!.isWhitespace do - i := i + 1 - if i ≥ n then break - let opener := s[i]! - let closer? : Option Char := - match opener with - | '(' => some ')' - | '{' => some '}' - | '[' => some ']' - | _ => none - match closer? with - | none => done := true - | some closer => - let start := i - let mut depth : Nat := 0 - let mut closed := false - let mut j := i - while j < n do - let ch := s[j]! - if ch == opener then - depth := depth + 1 - else if ch == closer then - depth := depth - 1 - if depth == 0 then - let body := (Source.slice s (start + 1) j).trimAscii.toString - binders := binders.push (opener, body) - j := j + 1 - closed := true - break - j := j + 1 - i := j - if !closed then done := true - return binders - -/-- Split `s` into whitespace-delimited tokens (empty tokens dropped). -/ -private def splitWhitespace (s : String) : Array String := Id.run do - let mut out : Array String := #[] - let mut current : String := "" - for c in s.toList do - if c.isWhitespace then - if !current.isEmpty then - out := out.push current - current := "" - else - current := current.push c - if !current.isEmpty then - out := out.push current - return out - -def explicitBinderApplicationArgs (statement : String) : Array String := Id.run do - let mut args : Array String := #[] - for (opener, body) in leadingBinders statement do - if opener != '(' then continue - let parts := body.splitOn ":" - if parts.length < 2 then continue - for name in splitWhitespace parts[0]! do - args := args.push name - return args - -/-- Strip the `:= ` off the end of a sliced declaration. Mirrors -`_hole_decl_signature`. -/ -def holeDeclSignature (declText basename : String) : IO String := do - let stripped := (stripProblemMarkers declText).trimAscii.toString - let src := Source.ofString stripped - let some idx := Source.rfind src src.size ":=".toList - | throw <| IO.userError - s!"Hole '{basename}' declaration has no `:=` to split: {stripped.quote}" - let prefix' := (Source.slice src 0 idx).trimAsciiEnd.toString - return prefix' ++ " := " - -/-- Find ` ` for any keyword in `keywords`, with word -boundaries. Returns the codepoint position of the start of the keyword and -the position just past the basename. -/ -def Source.findKeywordBasename (s : Source) (keywords : Array String) (basename : String) : - Option (Nat × Nat) := Id.run do - let n := s.size - let basenameLen := basename.length - let basenameChars := basename.toList - let mut i : Nat := 0 - while i < n do - if Source.atWordStart s i then - for kw in keywords do - let kwChars := kw.toList - let kwLen := kw.length - if Source.startsWithAt s i kwChars then - let afterKw := i + kwLen - if afterKw < n && s[afterKw]!.isWhitespace then - -- consume whitespace - let mut j := afterKw - while j < n && s[j]!.isWhitespace do - j := j + 1 - if Source.startsWithAt s j basenameChars then - let endBase := j + basenameLen - if Source.atWordEnd s endBase then - return some (i, endBase) - i := i + 1 - return none - -/-- Rewrite a non-theorem hole signature for the `Solution.lean` delegation: -inject `@[reducible] noncomputable` immediately before the declaration -keyword. The delegation must be `noncomputable` because honest solutions to -data holes are frequently noncomputable (e.g. `genus` in the Jacobian -challenge), and a computable `def` whose body references a noncomputable -`Submission.` fails to compile; comparator never sees computability, -so the marker is invisible to scoring. An existing `noncomputable` modifier -in the source signature is folded into the rewrite — Lean's grammar puts -attributes before `noncomputable`, so leaving it in place would produce the -invalid `noncomputable @[reducible] def`. Returns `none` when no -`def`/`instance`/`abbrev` keyword anchors the basename. -/ -def injectSolutionHoleModifiers (signature basename : String) : Option String := do - let sigSrc := Source.ofString signature - let (kwStart, _) ← Source.findKeywordBasename sigSrc #["def", "instance", "abbrev"] basename - let prefixText := Source.slice sigSrc 0 kwStart - let trimmed := prefixText.trimAsciiEnd.toString - let noncomputableKw := "noncomputable" - let prefixText := - if trimmed == noncomputableKw then - "" - else if trimmed.endsWith noncomputableKw && - (trimmed.dropRight noncomputableKw.length).back.isWhitespace then - trimmed.dropRight noncomputableKw.length - else - prefixText - let trimmedPrefix := prefixText.trimAsciiEnd.toString - if trimmedPrefix.endsWith "]" then - -- Attributes are one prefix block in Lean's grammar; two consecutive - -- `@[...]` blocks do not compose. Merge `reducible` into an existing final - -- block, filtering any competing reducibility marker, instead of emitting - -- a second block. - let trimmedSrc := Source.ofString trimmedPrefix - if let some attrStart := Source.rfind trimmedSrc trimmedSrc.size "@[".toList then - let contentsStart := attrStart + 2 - let beforeContents := Source.slice trimmedSrc 0 contentsStart - let contents := Source.slice trimmedSrc contentsStart (trimmedSrc.size - 1) - let attrs := contents.splitOn "," |>.map (fun a => a.trimAscii.toString) |>.filter fun a => - a != "reducible" && a != "instance_reducible" && a != "semireducible" - let trailing := (prefixText.drop trimmedPrefix.length).toString - return beforeContents ++ ", ".intercalate ("reducible" :: attrs) ++ "]" ++ trailing ++ - "noncomputable " ++ Source.slice sigSrc kwStart sigSrc.size - return prefixText ++ "@[reducible] noncomputable " ++ Source.slice sigSrc kwStart sigSrc.size - -/-! ## Command classification - -Recognising the keyword a command opens with is shared between the block -scanners below: the `open` scanner and the `variable`/notation scanner both -need to know where one command ends and the next begins. -/ - -private def isLineStartingWithWhitespace (line : String) : Bool := - match line.toList with - | [] => false - | c :: _ => c.isWhitespace - -/-- Drop leading trivia and attribute lists from a declaration slice, so what -gets classified is the declaration's own keyword. - -A slice taken from an `.ilean` range starts at the *beginning* of the -declaration, which is the doc comment and/or attribute list, not the keyword. So -a documented notation reads `/-- … -/\nnotation "𝔻" => …` and an attributed one -reads `@[inherit_doc] notation "∇_["m"]" => …`. Classifying either directly -finds no keyword, and the notation was then treated as an ordinary declaration -and stripped out of `ChallengeDeps.lean`, leaving its users to fail with -`Unknown identifier` or a syntax error at the notation's own tokens. -/ -private def stripLeadingCommentsAndAttributes (declarationText : String) : String := Id.run do - let src := Source.ofString declarationText - let n := src.size - let mut i := Source.skipTrivia src 0 - -- `@[...]`, possibly several, each followed by more trivia. - while i < n && Source.startsWithAt src i "@[".toList do - let mut depth := 0 - let mut j := i + 1 -- at '[' - let mut closed := false - while j < n && !closed do - if src[j]! == '[' then depth := depth + 1 - else if src[j]! == ']' then - depth := depth - 1 - if depth == 0 then closed := true - j := j + 1 - if !closed then return (Source.slice src i n) - i := Source.skipTrivia src j - return (Source.slice src i n) - -/-- Syntax declarations are source context, not mathematical helpers, but -extracted statements and kept declarations may depend on their notation. -/ -def isSyntaxContextDeclaration (declarationText : String) : Bool := Id.run do - let text := (stripLeadingCommentsAndAttributes declarationText).trimAsciiStart.toString - let prefixes := #[ - "notation", "local notation", "scoped notation", - "infix", "infixl", "infixr", "prefix", "postfix", - "local infix", "local infixl", "local infixr", "local prefix", "local postfix", - "scoped infix", "scoped infixl", "scoped infixr", "scoped prefix", "scoped postfix", - "syntax", "local syntax", "scoped syntax", "macro", "macro_rules" - ] - for kw in prefixes do - if startsWithKeyword text kw then return true - return false - -def isLocalSyntaxContextDeclaration (declarationText : String) : Bool := Id.run do - let text := (stripLeadingCommentsAndAttributes declarationText).trimAsciiStart.toString - let prefixes := #[ - "local notation", "local infix", "local infixl", "local infixr", - "local prefix", "local postfix", "local syntax" - ] - for kw in prefixes do - if startsWithKeyword text kw then return true - return false - -/-- Top-level command keywords that begin a fresh declaration/command. A -whitespace-indented line opening with one of these is never a continuation of a -preceding `open`/`variable`/`universe` block (Lean permits indented top-level -commands), so the block scanners must stop before absorbing it. - -Lean's command syntax is extensible, so no list of keywords is complete. The -cost of a miss is asymmetric: a command mistaken for a continuation is absorbed -into the block ahead of it, and `set_option … in` absorbed into an `open` even -makes the open look like the scoped form. Hence the keywords that open a command -without declaring a name — `set_option`, `export`, `include` — are listed -alongside the declaration keywords, as is the `#name` that opens a diagnostic -command (`#[…]` is an array literal, so the `#` alone does not qualify). -/ -private def startsWithCommandKeyword (stripped : String) : Bool := Id.run do - if stripped.startsWith "@[" then return true - if stripped.startsWith "#" then - match (stripped.toList.drop 1).head? with - | some c => if c.isAlpha then return true - | none => pure () - if isSyntaxContextDeclaration stripped then return true - let kws := #["def", "theorem", "lemma", "instance", "abbrev", "opaque", - "axiom", "class", "structure", "inductive", "namespace", "section", "end", - "variable", "universe", "open", "example", "noncomputable", "private", - "protected", "scoped", "attribute", "macro", "notation", "syntax", - "set_option", "export", "include", "omit", "mutual", "local", "unsafe", - "partial", "nonrec", "initialize"] - for kw in kws do - if startsWithKeyword stripped kw then return true - return false - -/-! ## Context opens -/ - -/-- Drop block comments `/- … -/` (nested-aware) that open and close on the -same line. Multi-line block comments are left alone — they're handled by -peeking through whole comment-only lines in the line scanner. -/ -private def stripSingleLineBlockComments (s : String) : String := Id.run do - let chars := s.toList.toArray - let n := chars.size - let mut out : String := "" - let mut i : Nat := 0 - let mut depth : Nat := 0 - while i < n do - if i + 1 < n && chars[i]! == '/' && chars[i + 1]! == '-' then - depth := depth + 1 - i := i + 2 - else if depth > 0 && i + 1 < n && chars[i]! == '-' && chars[i + 1]! == '/' then - depth := depth - 1 - i := i + 2 - else - if depth == 0 then out := out.push chars[i]! - i := i + 1 - return out - -/-- Drop a trailing `--` line comment from `s`. Used together with -`stripSingleLineBlockComments` to keep `in` tokens that appear in comments -from being mistaken for the `open … in` scoping keyword. -/ -private def stripLineComment (s : String) : String := - match s.splitOn "--" with - | x :: _ => x - | [] => s - -/-- The tokens of `line` with comments removed. -/ -private def commandTokens (line : String) : Array String := - splitWhitespace (stripLineComment (stripSingleLineBlockComments line)) - --- Drop the prefix of length `n` from `s` as a `String`. -private def stringDrop (s : String) (n : Nat) : String := - String.mk (s.toList.drop n) - --- Find the contents of `s` after the first occurrence of `"-/"`. If the --- closer appears, returns `(afterMarker, false)`; otherwise returns --- `("", true)` to signal the block comment is still open at end-of-line. -private def skipToBlockCommentClose (s : String) : String × Bool := - let parts := s.splitOn "-/" - match parts with - | [] => ("", true) - | [_] => ("", true) - | _ :: rest => ("-/".intercalate rest, false) - --- Strip a single block comment from the start of `lineRemainder`, returning --- `(remainderAfterComment, stillOpen)`. Caller must ensure `lineRemainder` --- starts with the block-comment opener `/-`. -private def consumeBlockCommentStart (lineRemainder : String) : String × Bool := - skipToBlockCommentClose (stringDrop lineRemainder 2) - --- Strip text up to and including the next block-comment closer, returning --- what's left on this line and whether the block comment is still open. -private def consumeBlockCommentContinuation (lineRemainder : String) : String × Bool := - skipToBlockCommentClose lineRemainder - -/-- The code left on `line` once leading block-comment text is stripped, given -whether a `/- … -/` comment was still open at the end of the previous line, -paired with the comment state at the end of this one. `none` means the line -carries no code: it is comment all the way to its end. - -The line scanners classify a line by the keyword it starts with, so prose has -to be removed first. A module docstring that wraps a sentence onto a line -beginning with `open` or `end` is otherwise read as a command — the first -hoists prose into the generated workspace, where it does not parse, and the -second pops the enclosing namespace and discards the context with it. -/ -private def stripBlockComments (line : String) (inBlockComment : Bool) : - Option String × Bool := Id.run do - let mut work := line - if inBlockComment then - let (rest, stillOpen) := consumeBlockCommentContinuation work - if stillOpen then return (none, true) - work := rest - -- Strip any further `/- … -/` segments that close on this line, and detect - -- an opener that does not. - let mut classified := work - while true do - let trimmed := classified.trimAsciiStart.toString - if trimmed.startsWith "/-" then - let (rest', stillOpen) := consumeBlockCommentStart trimmed - if stillOpen then return (none, true) - classified := rest' - else - break - return (some classified, false) - -/-- True if `line` opens a block comment it does not close. The line scanners -read one line at a time, so they cannot see into such a comment; a line that -opens one is the last they can classify. -/ -private def hasUnclosedBlockComment (line : String) : Bool := Id.run do - let chars := line.toList.toArray - let n := chars.size - let mut depth : Nat := 0 - let mut i : Nat := 0 - while i < n do - if i + 1 < n && chars[i]! == '/' && chars[i + 1]! == '-' then - depth := depth + 1 - i := i + 2 - else if depth > 0 && i + 1 < n && chars[i]! == '-' && chars[i + 1]! == '/' then - depth := depth - 1 - i := i + 2 - else if depth == 0 && i + 1 < n && chars[i]! == '-' && chars[i + 1]! == '-' then - -- A line comment hides any `/-` after it. - return false - else - i := i + 1 - return depth > 0 - -/-- The lines of the command block opening at `lines[startIdx]!` (0-indexed), -together with the index just past it; `limit` bounds the scan. - -A command may spread over several lines, with its arguments indented beneath the -opening keyword. A line at column zero starts a new command, and so does a -whitespace-indented line opening with a command keyword — Lean permits indented -top-level commands, and a module written wholly inside an indented `namespace` -is otherwise read as one enormous command. A blank or comment-only line ends the -scan too: Lean would read across either, but a command written that way is -vanishingly rare, and stopping keeps this scanner's reach the same as the -`variable`/notation scanner's. A line that leaves a block comment open ends it -for the same reason — what follows is prose, not arguments. -/ -private def commandBlockLines (lines : Array String) (startIdx limit : Nat) : - Array String × Nat := Id.run do - let mut block := #[lines[startIdx]!] - let mut idx := startIdx + 1 - if hasUnclosedBlockComment lines[startIdx]! then return (block, idx) - while idx < limit do - let candidate := lines[idx]! - let stripped := candidate.trimAscii.toString - if stripped.isEmpty then break - if !isLineStartingWithWhitespace candidate then break - if stripped.startsWith "--" || stripped.startsWith "/-" then break - if startsWithCommandKeyword stripped then break - block := block.push candidate - idx := idx + 1 - if hasUnclosedBlockComment candidate then break - return (block, idx) - -/-- True if the `open` command spelled by `blockLines` is the scoped `open … in` -form, which binds to the one command following it rather than to the rest of the -enclosing section. Detected by an `in` token anywhere after the leading `open` -keyword; the block's lines are scanned together, since - - open Bundle Filter - MeasureTheory in - -is a single command whose `in` lands on the continuation line. Top-level opens -like `open Foo` or `open scoped Classical` return false. -/ -private def isScopedOpenBlock (blockLines : Array String) : Bool := Id.run do - let mut toks : Array String := #[] - for line in blockLines do - toks := toks ++ commandTokens line - for i in [1:toks.size] do - if toks[i]! == "in" then return true - return false - -/-- True if `stripped` is a scoped `open … in …` line — the single-command -form that binds an open to one following expression. Detected by an `in` -token appearing somewhere after the leading `open` keyword. Top-level opens -like `open Foo` or `open scoped Classical` return false. -/ -def isScopedOpenLine (stripped : String) : Bool := - stripped.startsWith "open " && isScopedOpenBlock #[stripped] - -/-- True if `block` is the single-command ` … in` form, which binds to -the declaration following it rather than to the rest of the enclosing section. -/ -def isScopedCommandBlock (block : String) : Bool := - (commandTokens block).back? == some "in" - -/-- True if the upcoming lines starting at `peekIdx` (0-indexed) form the -continuation of a scoped `open … in` — that is, after any blank or -comment-only lines, the next syntactic line is `in` or begins with `in `. -Used to catch the multi-line variant where `in` is on its own line. -/ -private def followingLineIsScopingIn (lines : Array String) (peekIdx : Nat) : Bool := Id.run do - let mut i := peekIdx - while i < lines.size do - let s := (lines[i]!).trimAscii.toString - if s.isEmpty || s.startsWith "--" then - i := i + 1 - else - return s == "in" || s.startsWith "in " - return false - -def extractContextOpens (problemId : String) (sourcePath : System.FilePath) - (source : String) (extracted? : Option ExtractedTheorem) - (includeNamespaces : Bool) : IO String := do - let _ := problemId - let _ := sourcePath - let lines := (source.splitOn "\n").toArray - let targetLine? : Option Nat := extracted?.map fun e => e.startLine - let mut namespaceStack : Array String := #[] - let mut openLayers : Array (Array String) := #[#[]] - -- Parallel to `openLayers`: was each frame opened by `namespace` (contributing - -- a name) or by `section` (contributing only a scope)? - let mut frameIsNamespace : Array Bool := #[] - let mut inBody := false - let mut done := false - -- Is a `/- … -/` comment open at the start of the line being read? - let mut inBlockComment := false - -- One past the last line absorbed as the continuation of an earlier command. - let mut resumeAt : Nat := 0 - -- Nothing at or beyond the target declaration's first line is context. - let limit : Nat := match targetLine? with - | some t => min lines.size (t - 1) - | none => lines.size - for idx in [1:lines.size + 1] do - if done then break - if let some t := targetLine? then - if idx ≥ t then break - let line := lines[idx - 1]! - -- Comment state is tracked on every line, including lines absorbed into an - -- earlier command block: one of those may itself open a comment. - let (code?, stillOpen) := stripBlockComments line inBlockComment - inBlockComment := stillOpen || code?.any hasUnclosedBlockComment - if idx < resumeAt then continue - -- A line that is comment all the way to its end carries no command. - let some code := code? | continue - let stripped := code.trimAscii.toString - let scopeCommand := stripScopeCommandModifiers stripped - if !inBody then - if stripped.startsWith "import " || stripped.isEmpty then continue - inBody := true - if targetLine?.isNone then - let declKeywords := #["theorem", "lemma", "def", "abbrev", "opaque", - "axiom", "instance", "class", "structure"] - let isDecl := Id.run do - if stripped.startsWith "@[" then return true - for kw in declKeywords do - if stripped.startsWith kw then - let after := (stripped.drop kw.length).toString - if after.isEmpty then return true - -- check next char is non-word - let c := after.toList.head! - if !(c.isAlphanum || c == '_' || c == '\'') then return true - return false - if isDecl then - done := true - continue - if scopeCommand.startsWith "namespace " then - let rest := (scopeCommand.drop "namespace ".length).trimAscii.toString - let name := ((rest.splitOn " ").head!).trimAscii.toString - namespaceStack := namespaceStack.push name - openLayers := openLayers.push #[] - frameIsNamespace := frameIsNamespace.push true - else if startsWithKeyword scopeCommand "section" then - -- A `section` opens a scope for `open` just as a `namespace` does, but - -- contributes no name. Tracking only namespaces meant the matching `end` - -- popped a *namespace* frame instead, discarding the `open` lines held in - -- it: a module shaped `namespace N / open … / section S / … / end S` - -- emitted no opens at all. The sibling walker for `variable`/notation - -- already counts both. - openLayers := openLayers.push #[] - frameIsNamespace := frameIsNamespace.push false - else if startsWithKeyword stripped "end" then - if openLayers.size > 1 then - openLayers := openLayers.pop - if frameIsNamespace.back? == some true && namespaceStack.size > 0 then - namespaceStack := namespaceStack.pop - frameIsNamespace := frameIsNamespace.pop - else if stripped.startsWith "open " then - -- An `open` is taken whole: its namespaces may be spread over several - -- lines, and emitting only the first of them silently narrowed the - -- context the declaration was written against. - let (block, nextIdx) := commandBlockLines lines (idx - 1) limit - resumeAt := nextIdx + 1 - if isScopedOpenBlock block then continue - -- Multi-line scoped form: `open Foo` on one line, `in ` on a - -- following (possibly blank/comment-padded) line. Skip the whole - -- thing rather than emitting a dangling `open Foo` as top-level. - if followingLineIsScopingIn lines nextIdx then continue - let layerIdx := openLayers.size - 1 - let layer := openLayers[layerIdx]! ++ block - openLayers := openLayers.set! layerIdx layer - let mut contextLines : Array String := #[] - for layer in openLayers do - for ln in layer do - contextLines := contextLines.push ln - if includeNamespaces && namespaceStack.size > 0 then - let nsLine := "open " ++ ".".intercalate namespaceStack.toList - contextLines := #[nsLine] ++ contextLines - if contextLines.isEmpty then return "" - return "\n".intercalate contextLines.toList ++ "\n\n" - -/-! ## Context variables - -Walk the source up to the theorem and collect every `variable` declaration -that is still in scope at that point. The lidskii regression (issue #276) is -the canonical example: a theorem can refer to identifiers like `n` that are -introduced by a preceding `variable {n : Type*} ...` declaration, and the -elaborated theorem inherits those binders even though they do not appear in -the source slice between `theorem ` and `:= by`. Re-emitting the -`variable` lines in the generated workspace restores the elaboration context -needed to type-check the extracted statement. - -Multi-line `variable` declarations are kept verbatim: after a `variable` -header line we keep absorbing lines that begin with whitespace, which matches -how Lean's parser treats indented continuations of a binder list. -/ - -/-- Names introduced by the named (non-instance) leading binders of a -declaration-like text such as a theorem signature or the body of a -`variable` declaration. -/ -def binderIntroducedNames (text : String) : Array String := Id.run do - let mut names : Array String := #[] - for (opener, body) in leadingBinders text do - -- Instance-implicit binders are usually anonymous (`[Fintype n]`); skip - -- them — the names they reference come from other binders. - if opener == '[' then continue - let parts := body.splitOn ":" - if parts.length < 2 then continue - for name in splitWhitespace parts[0]! do - names := names.push name - return names - -/-- True iff every name introduced by `varText` (a `variable ...` line, with -the `variable` prefix still attached) is already bound by `theoremBinderNames`. -Such a `variable` is shadowed by the theorem's explicit binders and so -Lean would emit it as an "unused variable" if we re-emitted it. -/ -private def variableShadowedByTheorem (varText : String) - (theoremBinderNames : Array String) : Bool := Id.run do - let trimmed := varText.trimAscii.toString - if !(startsWithKeyword trimmed "variable") then return false - let body := (trimmed.drop "variable".length).toString - let varNames := binderIntroducedNames body - if varNames.isEmpty then return false - for name in varNames do - if !theoremBinderNames.contains name then return false - return true - -/-- Walk `source` up to `extracted?`'s start line, collecting top-level command -blocks that begin with `keyword` (e.g. `variable` or `universe`), respecting -`section`/`namespace` scoping: a block declared inside a `section`/`namespace` -goes out of scope at the matching `end`. Multi-line blocks absorb following -whitespace-indented continuation lines. Each collected block is filtered through -`keep`; only blocks for which `keep` returns true are emitted. Returns the kept -blocks joined by newlines with a trailing blank line, or `""` if none. -/ -private def extractScopedCommandBlocksWhere (source : String) - (extracted? : Option ExtractedTheorem) (isMatch : String → Bool) - (keep : String → Bool) : String := Id.run do - let lines := source.splitOn "\n" - let targetLine? : Option Nat := extracted?.map fun e => e.startLine - let mut layers : Array (Array String) := #[#[]] - let mut frameDepth : Nat := 0 - let mut inBlockComment := false - let mut idx : Nat := 0 - while idx < lines.length do - let lineNum := idx + 1 - if let some t := targetLine? then - if lineNum ≥ t then break - let line := lines[idx]! - -- Walk the line tracking block-comment state. We only consider the - -- non-comment remainder when classifying the line. - let (code?, stillOpen) := stripBlockComments line inBlockComment - inBlockComment := stillOpen - let some classified := code? | do - idx := idx + 1 - continue - let stripped := classified.trimAscii.toString - let scopeCommand := stripScopeCommandModifiers stripped - if stripped.isEmpty || stripped.startsWith "--" then - idx := idx + 1 - continue - if startsWithKeyword scopeCommand "namespace" || startsWithKeyword scopeCommand "section" then - frameDepth := frameDepth + 1 - layers := layers.push #[] - idx := idx + 1 - else if startsWithKeyword stripped "end" then - if frameDepth > 0 then - frameDepth := frameDepth - 1 - layers := layers.pop - idx := idx + 1 - else if isMatch stripped then - let mut block := line - idx := idx + 1 - while idx < lines.length do - let lineNum' := idx + 1 - if let some t := targetLine? then - if lineNum' ≥ t then break - let next := lines[idx]! - if next.trimAscii.toString.isEmpty then break - if !isLineStartingWithWhitespace next then break - if startsWithCommandKeyword next.trimAsciiStart.toString then break - block := block ++ "\n" ++ next - idx := idx + 1 - if keep block then - let layerIdx := layers.size - 1 - let layer := layers[layerIdx]!.push block - layers := layers.set! layerIdx layer - else - idx := idx + 1 - let mut flat : Array String := #[] - for layer in layers do - for v in layer do - flat := flat.push v - if flat.isEmpty then return "" - return "\n".intercalate flat.toList ++ "\n\n" - -def extractScopedCommandBlocks (source : String) (extracted? : Option ExtractedTheorem) - (keyword : String) (keep : String → Bool) : String := - extractScopedCommandBlocksWhere source extracted? - (fun stripped => startsWithKeyword stripped keyword) keep - -def extractContextVariables (source : String) (extracted? : Option ExtractedTheorem) - (theoremBinderNames : Array String) : String := - -- One layer per `section`/`namespace` we are still inside, matching Lean's - -- scoping for `variable`. Blocks shadowed by the theorem's own binders are - -- dropped (they would otherwise be flagged as unused). - extractScopedCommandBlocks source extracted? "variable" - (fun block => - !isScopedCommandBlock block && !variableShadowedByTheorem block theoremBinderNames) - -/-- Collect top-level `universe` commands in scope at the theorem. A source -module may declare `universe u v` and refer to `u`/`v` in a theorem whose -reconstructed `Challenge.lean` slice (`theorem … := by sorry`) would otherwise -have no binder for them, failing with `unknown universe level`. Re-emitting the -in-scope `universe` commands restores them. -/ -def extractContextUniverses (source : String) (extracted? : Option ExtractedTheorem) : String := - extractScopedCommandBlocks source extracted? "universe" (fun _ => true) - -/-- Collect the `include` and `omit` commands in scope at the theorem. These -decide which of the surrounding `variable` binders the declaration actually -takes, so re-emitting the `variable` commands without them would give the -generated declaration a different signature from the source one — and the -delegation arguments derived from the source declaration would not fit. -/ -def extractContextIncludes (source : String) (extracted? : Option ExtractedTheorem) : String := - extractScopedCommandBlocksWhere source extracted? - (fun stripped => startsWithKeyword stripped "include" || startsWithKeyword stripped "omit") - -- The `include … in` form binds to the declaration after it. Hoisting one - -- out of an earlier declaration would change our signature; the one that - -- belongs to our own declaration comes through `extractDeclarationPrefix`. - (fun block => !isScopedCommandBlock block) - -/-- Collect notation, syntax, and macro commands still in scope at the target -declaration. Generated statements retain their source notation, so these -commands must accompany them just like scoped variables and universes do. -/ -def extractContextSyntaxDeclarations (source : String) - (extracted? : Option ExtractedTheorem) : String := - extractScopedCommandBlocksWhere source extracted? isSyntaxContextDeclaration (fun _ => true) - -def extractContextLocalSyntaxDeclarations (source : String) - (extracted? : Option ExtractedTheorem) : String := - extractScopedCommandBlocksWhere source extracted? isLocalSyntaxContextDeclaration (fun _ => true) - -/-- Collect the in-scope `variable` commands together with the -notation/syntax/macro commands, preserving their source order. - -Emitting them as two separate blocks reorders them, and the order matters in -both directions: a notation may mention a variable, as in - - variable {d : ℕ} - local notation "ℝᵈ" => EuclideanSpace ℝ (Fin d) - -and a later `variable` may be written using a notation. Emitting the notation -first made the quotation precheck fail with `Unknown identifier 'd'` and left -the macro without an elaborator. `syntaxMatches` selects which syntax commands to -carry, so callers can keep the `local`-only behaviour when the non-local ones -have already gone into `ChallengeDeps.lean`. -/ -def extractContextVariablesAndSyntax (source : String) - (extracted? : Option ExtractedTheorem) (theoremBinderNames : Array String) - (syntaxMatches : String → Bool) : String := - extractScopedCommandBlocksWhere source extracted? - (fun stripped => startsWithKeyword stripped "variable" || syntaxMatches stripped) - (fun block => - if startsWithKeyword block.trimAsciiStart.toString "variable" then - !isScopedCommandBlock block && !variableShadowedByTheorem block theoremBinderNames - else true) - -/-! ## Delegation arguments -/ - -/-- Explicit (parenthesised) binder names introduced by the `variable` commands -in `block`, the text produced by `extractContextVariables`. These are the outer -parameters the generated files re-declare ahead of the restated signature, so -they are the only names a delegation may legitimately apply beyond the -declaration's own binders. -/ -def variableBlockExplicitNames (block : String) : Array String := Id.run do - let mut names : Array String := #[] - let mut current : Option String := none - for line in block.splitOn "\n" do - let stripped := line.trimAsciiStart.toString - if startsWithKeyword stripped "variable" then - if let some command := current then - names := names ++ explicitBinderApplicationArgs command - current := some (stripped.drop "variable".length).toString - else if let some command := current then - current := some (command ++ "\n" ++ line) - if let some command := current then - names := names ++ explicitBinderApplicationArgs command - return names - -/-- The arguments the generated delegation must apply to `Submission.`. - -`sourceArgs` are the explicit binders parsed out of the declaration's own -source signature. A module may introduce further explicit parameters through -outer `variable` commands; Lean retains those in the elaborated declaration and -the generated files re-declare them, so they precede `sourceArgs` in -application order. `signatureParams?` is the extractor's report of the full -list. - -The extractor's list is only trusted when it agrees with what the source -shows: it must end with `sourceArgs`, and every name ahead of them must be -introduced by one of the re-emitted `variable` commands. - -When the two views disagree there is no safe answer, because the disagreement -is itself evidence that one of them is wrong: delegating on either would emit a -workspace that does not compile. `none` is returned so the caller can fail -instead. - -`signatureParams?` is `none` for a declaration the extractor could not read. -The source binders are then all we have, and they are enough only when no outer -`variable` command could have contributed a parameter we cannot see. -/ -def delegationArgs? (signatureParams? : Option (Array String)) - (variableNames sourceArgs : Array String) : Option (Array String) := Id.run do - let some params := signatureParams? - | return if variableNames.isEmpty then some sourceArgs else none - if params.size < sourceArgs.size then return none - let outerCount := params.size - sourceArgs.size - if params.extract outerCount params.size != sourceArgs then return none - if !(params.extract 0 outerCount).all (fun p => variableNames.contains p) then return none - return some params - -/-! ## Render ChallengeDeps.lean -/ - -/-- The byte range `[start, stop)` of a single source declaration in `sourceText`, -keyed by the declaration's full name. `stop` is either the next declaration's -`start` (taken from `.ilean`) or the matching top-level `end ...` line. -/ -structure DeclSpan where - name : String - start : Nat - stop : Nat - /-- The precise end of the declaration (doc comment through end of body), - taken directly from the `.ilean` range. Unlike `stop` (the next - declaration's start, which overshoots), this ends exactly at the last - token, so removing `[start, declEnd)` deletes the whole declaration — - including a multi-paragraph doc comment — without truncating at an - interior blank line. -/ - declEnd : Nat - deriving Inhabited - -/-- Map `.ilean` declaration entries onto character-offset spans against -`sourceSrc`. Split out from `loadDeclSpans` so the column-convention routing is -reachable from tests without a compiled fixture on disk. -/ -def declSpansOfIleanEntries (sourceSrc : Source) (declRanges : Array IleanDeclEntry) : - IO (Array DeclSpan) := do - let mut startsBuf : Array (String × Nat × Nat) := #[] - for ileanEntry in declRanges do - -- `.ilean` columns are UTF-16, not codepoints; see `IleanDeclEntry`. - let off ← sourceSrc.offsetForLineUtf16Column ileanEntry.startLine ileanEntry.startColumn - let endOff ← sourceSrc.offsetForLineUtf16Column ileanEntry.endLine ileanEntry.endColumn - startsBuf := startsBuf.push (ileanEntry.name, off, endOff) - let starts := startsBuf.qsort (fun a b => a.2.1 < b.2.1) - let mut spans : Array DeclSpan := #[] - for i in [0:starts.size] do - let (name, start, declEnd) := starts[i]! - let stop := - if i + 1 < starts.size then starts[i+1]!.2.1 - else findTopLevelEndOffset sourceSrc start - spans := spans.push { name, start, stop, declEnd } - return spans - -/-- Load every top-level declaration range from the module's `.ilean`, mapped -into character-offset spans against `sourceSrc`. Used everywhere the generator -needs to slice the source by declaration. -/ -def loadDeclSpans (root : System.FilePath) (entry : EvalProblemMetadata) - (sourceSrc : Source) : IO (Array DeclSpan) := do - declSpansOfIleanEntries sourceSrc (← loadIleanDeclRanges root entry.moduleName) - -/-- Apply a list of `(start, stop, replacement)` edits to `sourceText`. Edits -are sorted right-to-left and applied in that order so earlier offsets remain -valid. Edits must not overlap. Use `replacement = ""` for a pure deletion. -/ -def applyEdits (sourceText : String) (edits : Array (Nat × Nat × String)) : String := Id.run do - let edits := edits.qsort (fun a b => a.1 > b.1) - let mut result := sourceText - for (start, stop, replacement) in edits do - let src := Source.ofString result - result := Source.slice src 0 start ++ replacement ++ Source.slice src stop src.size - return result - -/-- Reducibility attributes may only be set in the module that defines their -target. When trusted helpers move to `ChallengeDeps`, these context commands -are copied there too, but also remain in the edited Challenge/Submission/Solution -source. Drop the duplicate: importing `ChallengeDeps` already carries the -requested reducibility status. Commented examples are ignored by pairing source -lines with a comment-blanked view. -/ -def removeDuplicatedReducibilityAttributes (sourceText : String) - (movedHelpers : Std.HashSet String) : String := Id.run do - let original := sourceText.splitOn "\n" - let visible := (blankComments (Source.ofString sourceText) sourceText.length).splitOn "\n" - let mut out : Array String := #[] - for i in [0:original.length] do - let line := original[i]! - let shown := visible[i]!.trimAsciiStart.toString - let actual := line.trimAsciiStart.toString - let isReducibilityCommand := startsWithKeyword shown "attribute" && - (shown.startsWith "attribute [reducible]" || - shown.startsWith "attribute [instance_reducible]") - if isReducibilityCommand && actual.startsWith "attribute" then - let shownParts := shown.splitOn "]" - let actualParts := actual.splitOn "]" - if shownParts.length > 1 && actualParts.length > 1 then - let targets := splitWhitespace ("]".intercalate (shownParts.drop 1)) - let isMoved := fun target => movedHelpers.toList.any fun helper => - helper == target || helper.endsWith ("." ++ target) - let kept := targets.filter fun target => !isMoved target - if kept.size != targets.size then - if kept.isEmpty then - out := out.push "" - else - let indent := - String.mk (line.toList.take (line.length - line.trimAsciiStart.toString.length)) - let commandPrefix := actualParts.head! ++ "]" - out := out.push (indent ++ commandPrefix ++ " " ++ " ".intercalate kept.toList) - continue - out := out.push line - return "\n".intercalate out.toList - -/-- Commands that can be written as ` … in ` to scope -themselves onto a single following declaration. -/ -private def scopingCommandKeywords : Array String := - #["variable", "set_option", "open", "attribute", "include", "omit", "local", "scoped"] - -/-- Split `[lowerBound, limit)` into lines, each paired with the tokens it -contributes outside comments. Comment state is carried forward across lines, so -a line inside a multi-line block comment contributes nothing — which is what -makes it recognisable as trivia when the caller walks back over it. -/ -private def gapLineTokens (source : Source) (lowerBound limit : Nat) : - Array (Nat × Array String) := Id.run do - let mut lines : Array (Nat × Array String) := #[] - let mut lineStart := lowerBound - let mut text : String := "" - let mut depth : Nat := 0 - let mut i := lowerBound - while i < limit do - if depth == 0 && Source.startsWithAt source i "--".toList then - while i < limit && source[i]! != '\n' do - i := i + 1 - else if Source.startsWithAt source i "/-".toList then - depth := depth + 1 - i := i + 2 - else if depth > 0 && Source.startsWithAt source i "-/".toList then - depth := depth - 1 - i := i + 2 - else if source[i]! == '\n' then - lines := lines.push (lineStart, splitWhitespace text) - text := "" - i := i + 1 - lineStart := i - else - if depth == 0 then text := text.push source[i]! - i := i + 1 - return lines.push (lineStart, splitWhitespace text) - -/-- Move a removal range's start back over the command prefixes that scope onto -the declaration being removed — `set_option … in`, `open … in`, and friends. A -`.ilean` declaration range begins at the declaration proper, so such a prefix -is not covered by it and would otherwise be stranded with no command to apply -to. - -A prefix is recognised by its last token being `in`, and is then followed back -to the line opening the command, so one spread over several lines is consumed -whole, as is one sharing the declaration's own line. Blank and comment-only -lines are crossed, but are only dropped if a prefix is found beyond them. -`lowerBound` is the end of the previous declaration; the search never crosses -it, so text belonging to a declaration we are keeping can never be consumed. -/ -def extendOverScopingPrefixes (source : Source) (lowerBound start : Nat) : Nat := Id.run do - let lines := gapLineTokens source lowerBound start - let opensCommand : Nat → Bool := fun idx => - match (lines[idx]!.2)[0]? with - | some token => scopingCommandKeywords.contains token - | none => false - let mut result := start - let mut idx := lines.size - while idx > 0 do - let (lineStart, tokens) := lines[idx - 1]! - if tokens.isEmpty then - -- Trivia is crossed in the hope of a prefix beyond it, and only dropped - -- if one is found. - idx := idx - 1 - else if tokens.back? != some "in" then - return result - else - -- Follow the prefix back to the line that opens the command. Stay put - -- rather than guess if there is no such line within the gap. - let mut commandIdx := idx - 1 - while commandIdx > 0 && !opensCommand commandIdx do - commandIdx := commandIdx - 1 - result := if opensCommand commandIdx then lines[commandIdx]!.1 else lineStart - idx := commandIdx - return result - -/-- The end of the last declaration ending at or before `offset`, or -`bodyStart` if there is none. Bounds a backward scan so that it cannot reach -into the text of another declaration. -/ -def previousDeclarationEnd (spans : Array DeclSpan) (bodyStart offset : Nat) : Nat := - spans.foldl (init := bodyStart) fun acc span => - if span.declEnd ≤ offset then max acc span.declEnd else acc - -/-- The command prefixes that scope onto the declaration starting at -`declarationStart` (`include … in`, `open … in`, `set_option … in`, …), as text -to re-emit ahead of a restated statement. - -These forms bind to one following declaration, which is why the context -collectors pass over them: hoisting one out of an earlier declaration would -change the meaning of ours. The one attached to our own declaration is a -different matter, and `include … in` especially so, since it decides which of -the surrounding `variable` binders the declaration takes. Dropping it gives the -restated statement a different signature from the source, and the delegation -derived from the source no longer fits. -/ -def extractDeclarationPrefix (source : Source) (lowerBound declarationStart : Nat) : String := - let prefixStart := extendOverScopingPrefixes source lowerBound declarationStart - let text := (Source.slice source prefixStart declarationStart).trimAscii.toString - if text.isEmpty then "" else text ++ "\n" - -/-- Shared core of single- and multi-hole `ChallengeDeps.lean` rendering. - -* `keepDeclarations` are the names whose source text we want to *retain* - (i.e. trusted helpers). -* `protectedRanges` overrides the `.ilean`-derived span for a named decl - with a precise `(start, stop)` byte range (used by single-hole for the - extracted theorem and by multi-hole for every hole, where `.ilean`'s - start-of-next heuristic is wrong for non-final decls). -/ -def renderChallengeDepsCore (root : System.FilePath) (entry : EvalProblemMetadata) - (sourceText : String) (localImports : Array String) - (keepDeclarations : Std.HashSet String) - (protectedRanges : Std.HashMap String (Nat × Nat)) : - IO (Option String) := do - let mut parts : Array String := #[] - for imported in localImports do - let importedPath := moduleSourcePath root imported - let importedText ← IO.FS.readFile importedPath - let importedSrc := Source.ofString importedText - let prelude := importPreludeLength importedSrc - let afterPrelude := Source.slice importedSrc prelude importedSrc.size - let body := (stripProblemMarkers afterPrelude).trimAsciiStart.toString - let body := if !body.isEmpty && !body.endsWith "\n" then body ++ "\n" else body - if !body.isEmpty then - parts := parts.push body - if !keepDeclarations.isEmpty then - let sourceSrc := Source.ofString sourceText - let bodyStart := importPreludeLength sourceSrc - let spans ← loadDeclSpans root entry sourceSrc - let mut removeRangesRaw : Array (Nat × Nat) := #[] - -- End of the last declaration we have walked past, so that a removal never - -- reaches back into the text of the declaration before it. - let mut previousEnd := bodyStart - for span in spans do - -- Delete only the declaration's precise `.ilean` range. Extending to the - -- next declaration also deletes intervening scoped context commands such - -- as `variable` and `local notation`, which kept helpers may require. - let (start, stop) := match protectedRanges[span.name]? with - | some (s, e) => (s, e) - | none => (span.start, span.declEnd) - let declarationText := Source.slice sourceSrc span.start span.declEnd - if !keepDeclarations.contains span.name && !isSyntaxContextDeclaration declarationText then - removeRangesRaw := removeRangesRaw.push - (extendOverScopingPrefixes sourceSrc previousEnd start, stop) - previousEnd := max previousEnd (max span.declEnd stop) - let removeRanges := removeRangesRaw.qsort - (fun a b => a.1 < b.1 || (a.1 == b.1 && a.2 < b.2)) - let mut pieces : Array String := #[] - let mut cursor := bodyStart - for (s, e) in removeRanges do - if e ≤ bodyStart then continue - let s := if s < bodyStart then bodyStart else s - if s < cursor then continue - pieces := pieces.push (Source.slice sourceSrc cursor s) - cursor := e - pieces := pieces.push (Source.slice sourceSrc cursor sourceSrc.size) - let body := (pieces.foldl (· ++ ·) "").trimAsciiStart.toString - let body := if !body.isEmpty && !body.endsWith "\n" then body ++ "\n" else body - if !body.isEmpty then - parts := parts.push body - if parts.isEmpty then return none - let joined := "\n".intercalate (parts.toList.map (·.trimAsciiEnd.toString)) - let importHeader ← problemImportHeader root entry.moduleName - return some (importHeader ++ "\n" ++ joined ++ "\n") - -/-- Render `ChallengeDeps.lean` for a single-hole problem. -/ -def renderChallengeDeps (root : System.FilePath) (entry : EvalProblemMetadata) - (extracted : ExtractedTheorem) (localImports : Array String) : - IO (Option String) := do - let sourcePath := moduleSourcePath root entry.moduleName - if !(← sourcePath.pathExists) then - throw <| IO.userError - s!"Source file for module '{entry.moduleName}' not found: {sourcePath}" - let sourceText ← IO.FS.readFile sourcePath - let keepDeclarations : Std.HashSet String := - extracted.sameModuleDependencies.foldl (·.insert ·) {} - let sourceSrc := Source.ofString sourceText - let theoremStart ← sourceSrc.offsetForLineColumn extracted.startLine extracted.startColumn - let theoremEnd ← sourceSrc.offsetForLineColumn extracted.endLine extracted.endColumn - let protectedRanges : Std.HashMap String (Nat × Nat) := - ({} : Std.HashMap String (Nat × Nat)).insert extracted.declarationName - (theoremStart, theoremEnd) - renderChallengeDepsCore root entry sourceText localImports keepDeclarations protectedRanges - - -/-- For each helper name in `helperNames`, return every ancestor of its enclosing -namespace `_root_`-qualified. Used -to inject `open ...` lines so that helpers — declared at root namespace in -`ChallengeDeps.lean` — resolve from unqualified references inside `namespace -Submission`. The `_root_.` qualification is essential: a bare `open Helpers` -inside `namespace Submission` would resolve to `Submission.Helpers` (which -holds the holes), not `_root_.Helpers` (which holds the helpers). Root-level -helpers (no dotted prefix) contribute no `open` — they resolve via `_root_` -automatically. - -Every ancestor is needed because wrapping changes namespace self-resolution. -For example, source inside `namespace AlgebraicGeometry.Scheme` can refer to the -parent's `Scheme` constant. Once that source is nested below `Submission`, -opening only `_root_.AlgebraicGeometry.Scheme` exposes its members but not the -`Scheme` constant itself; `_root_.AlgebraicGeometry` must also be open. -/ -def derivedHelperOpens (helperNames : Std.HashSet String) : Array String := Id.run do - let mut opens : Array String := #[] - let mut seen : Std.HashSet String := {} - for name in helperNames.toList.mergeSort do - let parts := name.splitOn "." - if parts.length ≤ 1 then continue - for count in [1:parts.length] do - let prefix' := ".".intercalate (parts.take count) - if seen.contains prefix' then continue - opens := opens.push s!"_root_.{prefix'}" - seen := seen.insert prefix' - return opens - -/-- Split trusted helpers into those that can be compiled in `ChallengeDeps` -and those that must remain inline because they depend on a problem hole. -/ -def partitionHelpersByHoleDependence (helperNames holeDependentNames : Std.HashSet String) : - Std.HashSet String × Std.HashSet String := Id.run do - let mut depsHelpers : Std.HashSet String := {} - let mut inlineHelpers : Std.HashSet String := {} - for name in helperNames.toList do - if holeDependentNames.contains name then - inlineHelpers := inlineHelpers.insert name - else - depsHelpers := depsHelpers.insert name - return (depsHelpers, inlineHelpers) - -/-! ## Python-compatible JSON pretty-printer - -`Lean.Json` stores objects in an `RBNode`, which reorders keys -alphabetically/by-tree-shape and disagrees with the insertion order Python's -`json.dumps` uses. To keep `generated/` JSON files reproducible across the -two implementations we build them via an ordered-pair representation and -pretty-print with our own routine. -/ - -/-- A JSON value that preserves object-key insertion order. -/ -inductive OJson where - | null : OJson - | bool : Bool → OJson - | num : Int → OJson - | str : String → OJson - | arr : Array OJson → OJson - | obj : Array (String × OJson) → OJson - deriving Inhabited - -private def hexNat4 (n : Nat) : String := - let digits := "0123456789abcdef" - let nib (k : Nat) : Char := digits.get ⟨k⟩ - String.mk [nib ((n >>> 12) &&& 0xF), nib ((n >>> 8) &&& 0xF), - nib ((n >>> 4) &&& 0xF), nib (n &&& 0xF)] - -/-- Escape a string the way Python's `json.dumps(...)` does with default -`ensure_ascii=True`: ASCII printables stay literal; controls and any -codepoint above U+007F become `\uXXXX` escapes, with codepoints above the BMP -encoded as a UTF-16 surrogate pair. -/ -private def escapeJsonString (s : String) : String := Id.run do - let mut out := "" - for c in s.toList do - match c with - | '"' => out := out ++ "\\\"" - | '\\' => out := out ++ "\\\\" - | '\n' => out := out ++ "\\n" - | '\r' => out := out ++ "\\r" - | '\t' => out := out ++ "\\t" - | '\x08' => out := out ++ "\\b" - | '\x0c' => out := out ++ "\\f" - | _ => - let cp := c.toNat - if cp < 0x20 then - out := out ++ "\\u" ++ hexNat4 cp - else if cp < 0x7F then - out := out.push c - else if cp ≤ 0xFFFF then - out := out ++ "\\u" ++ hexNat4 cp - else - -- UTF-16 surrogate pair - let adj := cp - 0x10000 - let hi := 0xD800 + (adj >>> 10) - let lo := 0xDC00 + (adj &&& 0x3FF) - out := out ++ "\\u" ++ hexNat4 hi ++ "\\u" ++ hexNat4 lo - return out - -/-- Pretty-print `OJson` matching Python's `json.dumps(value, indent=2)`. -/ -partial def OJson.pretty (j : OJson) (indent : Nat := 0) : String := - match j with - | .null => "null" - | .bool b => if b then "true" else "false" - | .num n => toString n - | .str s => "\"" ++ escapeJsonString s ++ "\"" - | .arr xs => - if xs.isEmpty then "[]" - else - let pad := "".pushn ' ' (indent + 2) - let closePad := "".pushn ' ' indent - let parts := xs.toList.map fun x => pad ++ OJson.pretty x (indent + 2) - "[\n" ++ ",\n".intercalate parts ++ "\n" ++ closePad ++ "]" - | .obj kvs => - if kvs.isEmpty then "{}" - else - let pad := "".pushn ' ' (indent + 2) - let closePad := "".pushn ' ' indent - let parts := kvs.toList.map fun (k, v) => - pad ++ "\"" ++ escapeJsonString k ++ "\": " ++ OJson.pretty v (indent + 2) - "{\n" ++ ",\n".intercalate parts ++ "\n" ++ closePad ++ "}" - -/-- Convenience constructors for `OJson`. -/ -def ojStr (s : String) : OJson := .str s -def ojBool (b : Bool) : OJson := .bool b -def ojNat (n : Nat) : OJson := .num (Int.ofNat n) -def ojArr (xs : Array OJson) : OJson := .arr xs -def ojObj (kvs : Array (String × OJson)) : OJson := .obj kvs -def ojStrArr (xs : Array String) : OJson := .arr (xs.map ojStr) - -/-! ## Holes metadata -/ - -/-- Build `holes.json`'s content. Mirrors `build_holes_metadata`. -/ -def buildHolesMetadata (root : System.FilePath) (entry : EvalProblemMetadata) - (extracteds : Array ExtractedTheorem) : IO String := do - let sourcePath := moduleSourcePath root entry.moduleName - if !(← sourcePath.pathExists) then - throw <| IO.userError - s!"Source file for module '{entry.moduleName}' not found: {sourcePath}" - let sourceText ← IO.FS.readFile sourcePath - let src := Source.ofString sourceText - let mut holes : Array OJson := #[] - for e in extracteds do - let startOff ← src.offsetForLineColumn e.startLine e.startColumn - let endOff ← src.offsetForLineColumn e.endLine e.endColumn - let bodyRaw := Source.slice src startOff endOff - let body := (stripProblemMarkers bodyRaw).trim - holes := holes.push <| ojObj #[ - ("name", ojStr e.declarationName), - ("basename", ojStr (lastComponentStr e.declarationName)), - ("kind", ojStr e.kind), - ("body", ojStr body) - ] - let payload := ojObj #[ - ("id", ojStr entry.id), - ("module", ojStr entry.moduleName), - ("holes", ojArr holes) - ] - return OJson.pretty payload ++ "\n" - -/-! ## Rendering workspaces -/ - -private def renderReadmeLines (entry : EvalProblemMetadata) - (extracteds : Array ExtractedTheorem) (multiHole : Bool) : Array String := Id.run do - let mut lines : Array String := #[ - s!"# `{entry.id}`", - "", - entry.title, - "", - s!"- Problem ID: `{entry.id}`", - s!"- Group: `{entry.group}`", - s!"- Status: `{entry.status}`", - s!"- Visible: {if entry.visible then "yes" else "no"}", - s!"- Statement Revision: {entry.statementRevision}", - s!"- Tags: {if entry.tags.isEmpty then "none" else ", ".intercalate entry.tags.toList}", - s!"- Submitter: {entry.submitter}" - ] - if multiHole then - let holeDescs := extracteds.toList.map fun e => s!"`{e.declarationName}` ({e.kind})" - lines := lines.push s!"- Holes ({extracteds.size}): {", ".intercalate holeDescs}" - if let some notes := entry.notes then - lines := lines.push s!"- Notes: {notes}" - if let some source := entry.source then - lines := lines.push s!"- Source: {source}" - if let some informal := entry.informalSolution then - lines := lines.push s!"- Informal solution: {informal}" - let body := - if multiHole then - #[ - "", - "Do not modify `Challenge.lean` or `Solution.lean`. Those files are part of the", - "trusted benchmark and fixed by the repository.", - "", - "This is a multi-hole problem: the challenge declares multiple `def`s,", - "`instance`s, and/or `theorem`s as `sorry`. Fill all of them in", - "`Submission.lean` (under `namespace Submission`) for comparator to accept", - "your solution.", - "", - "Participants may use declarations from the existing Mathlib imports. Broadening", - "the import header (especially to `import Mathlib`) can change elaboration of the", - "fixed statement; any added import must leave `lake build Solution` green. Helper", - "code not available through compatible imports must be inlined into the workspace.", - "", - "`lake test` runs comparator for this problem. The command expects a comparator", - "binary in `PATH`, or in the `COMPARATOR_BIN` environment variable." - ] - else - #[ - "", - "Do not modify `Challenge.lean` or `Solution.lean`. Those files are part of the", - "trusted benchmark and fixed by the repository.", - "", - "Write your solution in `Submission.lean` and any additional local modules under", - "`Submission/`.", - "", - "Participants may use declarations from the existing Mathlib imports. Broadening", - "the import header (especially to `import Mathlib`) can change elaboration of the", - "fixed statement; any added import must leave `lake build Solution` green. Helper", - "code not available through compatible imports must be inlined into the workspace.", - "", - "Multi-file submissions are allowed through `Submission.lean` and additional local", - "modules under `Submission/`.", - "", - "`lake test` runs comparator for this problem. The command expects a comparator", - "binary in `PATH`, or in the `COMPARATOR_BIN` environment variable." - ] - return lines ++ body - -private def lakefileToml (problemId : String) (mathlibDep : DependencySpec) - (withChallengeDeps : Bool) : String := - let challengeDepsLib := - if withChallengeDeps then - "[[lean_lib]]\nname = \"ChallengeDeps\"\n\n" - else "" - s!"name = \"{problemId}\"\n" ++ - "testDriver = \"workspace_test\"\n" ++ - "defaultTargets = [\"Challenge\", \"Solution\", \"Submission\"]\n\n" ++ - "[leanOptions]\n" ++ - "autoImplicit = false\n\n" ++ - "[[require]]\n" ++ - s!"name = \"{mathlibDep.name}\"\n" ++ - s!"git = \"{mathlibDep.git}\"\n" ++ - s!"rev = \"{mathlibDep.rev}\"\n\n" ++ - challengeDepsLib ++ - "[[lean_lib]]\nname = \"Challenge\"\n\n" ++ - "[[lean_lib]]\nname = \"Solution\"\n\n" ++ - "[[lean_lib]]\nname = \"Submission\"\n\n" ++ - "[[lean_exe]]\nname = \"workspace_test\"\nroot = \"WorkspaceTest\"\n" - -/-! ## Multi-hole rendering -/ - -private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProblemMetadata) - (extracteds : Array ExtractedTheorem) (toolchain : String) - (mathlibDep : DependencySpec) (workspaceTest : String) : - IO (Array (String × String)) := do - let sourcePath := moduleSourcePath root entry.moduleName - if !(← sourcePath.pathExists) then - throw <| IO.userError - s!"Source file for module '{entry.moduleName}' not found: {sourcePath}" - let sourceText ← IO.FS.readFile sourcePath - let src := Source.ofString sourceText - -- Hole byte ranges in raw source. - let mut holesRaw : Array (Nat × Nat × String × String) := #[] - for e in extracteds do - let s ← src.offsetForLineColumn e.startLine e.startColumn - let eo ← src.offsetForLineColumn e.endLine e.endColumn - holesRaw := holesRaw.push (s, eo, e.declarationName, e.kind) - let holesWithRanges := holesRaw.qsort (fun a b => a.1 < b.1) - let mut theoremNames : Array String := #[] - let mut definitionNames : Array String := #[] - for (_, _, name, kind) in holesWithRanges do - if kind == "theorem" then theoremNames := theoremNames.push name - else definitionNames := definitionNames.push name - -- Multi-hole problems may carry trusted helper declarations (decls in the - -- same module that some hole depends on but that are not themselves holes). - -- Factor them into `ChallengeDeps.lean` so `Submission` and `Solution` - -- reference the same canonical declaration; otherwise the helpers get - -- duplicated by the `namespace Submission` wrap and types fail to unify. - -- A hole that is also another hole's dependency is *not* a helper; the - -- delegation chain handles it. - let holeNames : Std.HashSet String := - extracteds.foldl (init := {}) fun acc e => acc.insert e.declarationName - let mut helperNames : Std.HashSet String := - extracteds.foldl (init := {}) fun acc e => - e.sameModuleDependencies.foldl - (fun a n => if holeNames.contains n then a else a.insert n) acc - let holeDependentNames : Std.HashSet String := - extracteds.foldl (init := {}) fun acc e => - e.holeDependentDependencies.foldl (fun a n => a.insert n) acc - let earliestHoleStart := holesWithRanges[0]!.1 - -- Load declaration spans from raw source once and validate every declared - -- helper is actually present (catches stale metadata / source mismatch - -- early rather than as a confusing Lean build error downstream). - let spans ← if helperNames.isEmpty then pure (#[] : Array DeclSpan) - else loadDeclSpans root entry src - -- Close the helper set over declarations *named in the source text* as well as - -- those reachable in the elaborated terms. - -- - -- The dependency closure comes from elaborated terms, deliberately, so that - -- typeclass synthesis is followed. But elaboration also *erases*: a `rfl` - -- lemma cited in a `simp [...]` list leaves no trace in the resulting proof - -- term, so it never enters the closure — while the helper's source text, which - -- is what gets copied into the workspace, still names it. In - -- `MotivicInvariants`, `PartialMap.id_domain` (a `rfl` lemma) vanished this way - -- while its sibling `id_hom`, cited in the same `simp` list, survived; the - -- copied helper then failed to build with `Unknown constant`. - -- - -- So scan the text being kept for same-module declaration names and pull those - -- in too, to a fixpoint, since a newly added helper's own text may name more. - -- Comments are blanked first so a name occurring only in prose is not pulled - -- in. Holes are never added: they are not helpers. - if !spans.isEmpty then - let mut changed := true - let mut rounds := 0 - while changed && rounds < spans.size + 1 do - changed := false - rounds := rounds + 1 - let mut keptText : String := "" - for sp in spans do - if helperNames.contains sp.name then - let text := Source.slice src sp.start sp.declEnd - let textSrc := Source.ofString text - keptText := keptText ++ "\n" ++ blankComments textSrc textSrc.size - for sp in spans do - if helperNames.contains sp.name || holeNames.contains sp.name then continue - let basename := lastComponentStr sp.name - unless basename.isEmpty do - if containsIdentifier keptText basename then - if sp.start ≥ earliestHoleStart then - throw <| IO.userError - s!"Trusted helper text refers to '{sp.name}', declared after a problem hole. \ - Its hole-dependence cannot be established from the elaborated dependency \ - closure, so it cannot safely be moved to ChallengeDeps." - helperNames := helperNames.insert sp.name - changed := true - if !helperNames.isEmpty then - let declNameSet : Std.HashSet String := - spans.foldl (init := {}) fun acc s => acc.insert s.name - -- A helper name `Foo.bar` whose strict prefix `Foo` is *both* a declared - -- name *and* itself a kept helper is an auto-generated companion of - -- `Foo` (constructor, field accessor, recursor, ...); stripping `Foo` - -- from source removes them transparently. Requiring the parent be in - -- `helperNames` (not just any declared name) prevents an unrelated stale - -- `Foo.bar.baz` from being silently accepted because some unrelated - -- `Foo` happens to be declared in the same module. - let hasKeptHelperParent : String → Bool := fun n => - let parts := n.splitOn "." - (List.range (parts.length - 1)).any fun i => - let p := ".".intercalate (parts.take (i + 1)) - helperNames.contains p && declNameSet.contains p - -- A helper with no `.ilean` span of its own was never written down: it is an - -- auto-generated companion of a declaration that *was*. `deriving` emits its - -- instances positioned inside the parent `def`; a `structure` emits - -- `.injEq`, `.ctorIdx`, `.noConfusionType`, `.sizeOf_spec`; `grind` used as - -- an auto-param default emits `…hcongr_*` with no source position at all. - -- - -- None of these can be sliced out of the source, so keeping one in the - -- helper set could only ever raise the error below. Dropping them is safe: - -- the generated files are built from source *text*, and a constant with no - -- source position cannot be named in that text, so dropping cannot leave a - -- dangling reference. If the text does name one, it names it because the - -- trusted source did — and that text is copied verbatim, so the declaration - -- that regenerates it is necessarily in the closure and retained. Surveying - -- the catalog, every such constant is a structure/class companion, and none - -- is an `instance`, which is the one case where a silently-missing - -- declaration could be papered over by instance search rather than failing. - let generated : Array String := helperNames.toList.foldl (init := #[]) fun acc n => - if declNameSet.contains n || hasKeptHelperParent n then acc else acc.push n - for n in generated do - helperNames := helperNames.erase n - let (depsHelpers, _) := - partitionHelpersByHoleDependence helperNames holeDependentNames - -- Remove a helper together with any `... in` command scoped onto it. A - -- declaration's `.ilean` range starts at its doc comment, so a prefix like - -- `open Classical in` lies outside it and would be left behind — where it then - -- binds to whatever command comes next. In practice that was the `variable` - -- command, which the orphan swallowed, so the binders were never declared and - -- the statement failed with `Unknown identifier`. The `ChallengeDeps` removal - -- path already extends over prefixes; this one did not. - let helperRanges : Array (Nat × Nat) := Id.run do - let sorted := spans.qsort (fun a b => a.start < b.start) - let mut out : Array (Nat × Nat) := #[] - let mut previousEnd := importPreludeLength src - for sp in sorted do - if depsHelpers.contains sp.name then - out := out.push (extendOverScopingPrefixes src previousEnd sp.start, sp.declEnd) - previousEnd := max previousEnd sp.declEnd - return out - let localImports ← repoLocalImportModules root entry.moduleName - -- Open the enclosing namespaces of the in-module helpers. When the problem - -- also pulls trusted deps from imported library modules (`localImports` - -- non-empty), those deps live in the holes' own enclosing namespace, which - -- then exists in `ChallengeDeps` at `_root_`; open it too so unqualified - -- references (e.g. `conwayKnot`) resolve. We must *not* open hole namespaces - -- when there are no such imports: a namespace containing only holes does not - -- exist at `_root_` once the holes move under `Submission`, and `open - -- _root_.` would be an unknown-namespace error (e.g. the all-holes - -- `jacobian_challenge_*` problems). Duplicates are dropped downstream. -/ - let helperOpens := derivedHelperOpens depsHelpers ++ - (if localImports.isEmpty then #[] else derivedHelperOpens holeNames) - -- Render ChallengeDeps via the shared core, passing precise hole ranges so - -- the helper-extraction slicing knows where the hole bodies live (the - -- `.ilean`-derived "next decl start" is wrong for non-final holes). - let mut holeRanges : Std.HashMap String (Nat × Nat) := {} - for (s, eo, name, _) in holesWithRanges do - holeRanges := holeRanges.insert name (s, eo) - let challengeDeps? ← - renderChallengeDepsCore root entry sourceText localImports depsHelpers holeRanges - let hasChallengeDeps := challengeDeps?.isSome - -- Compute Solution's edit set against raw source: helper removals plus - -- hole-body replacements (delegations to `Submission.`). Applied in - -- a single right-to-left pass so all offsets stay valid even if a hole - -- appears earlier in source than a helper. - let helperEdits : Array (Nat × Nat × String) := - helperRanges.map fun (s, e) => (s, e, "") - let mut solutionEdits : Array (Nat × Nat × String) := helperEdits - for (startOff, endOff, fullName, kind) in holesWithRanges do - let declText := Source.slice src startOff endOff - let basename := lastComponentStr fullName - let mut signature ← holeDeclSignature declText basename - if kind != "theorem" then - match injectSolutionHoleModifiers signature basename with - | none => - throw <| IO.userError - s!"Could not anchor `@[reducible] noncomputable` injection in signature for \ - hole '{fullName}'." - | some rewritten => - signature := rewritten - let declSrc := Source.ofString declText - let some (_, kwEnd) := Source.findKeywordBasename declSrc - #["def", "instance", "theorem", "opaque", "lemma", "abbrev", "class", "example"] basename - | throw <| IO.userError - s!"Could not locate basename '{basename}' in source decl for hole '{fullName}'." - let between := Source.slice declSrc kwEnd declSrc.size - let betweenSrc := Source.ofString between - let some lastEq := Source.rfind betweenSrc betweenSrc.size ":=".toList - | throw <| IO.userError s!"Source decl for hole '{fullName}' has no `:=` body marker." - let statement := Source.slice betweenSrc 0 lastEq - let sourceArgs := explicitBinderApplicationArgs statement - let explicitArgs ← match extracteds.find? (fun e => e.declarationName == fullName) with - | some extracted => - let variableNames := - variableBlockExplicitNames (extractContextVariables sourceText (some extracted) #[]) - let signatureParams? := - if hasBareSorryBody declText then extracted.explicitParameters else none - match delegationArgs? signatureParams? variableNames sourceArgs with - | some args => pure args - | none => - throw <| IO.userError - s!"Could not match the elaborated parameters of hole '{fullName}' against its \ - source signature; the generated delegation would under-apply it." - | none => pure sourceArgs - let applied := - if explicitArgs.isEmpty then s!"Submission.{fullName}" - else s!"Submission.{fullName} " ++ " ".intercalate explicitArgs.toList - let newDecl := signature ++ applied - solutionEdits := solutionEdits.push (startOff, endOff, newDecl) - let solutionText := applyEdits sourceText solutionEdits - let solutionText := - if hasChallengeDeps then - removeDuplicatedReducibilityAttributes solutionText depsHelpers - else solutionText - -- Challenge and Submission only need helper removals. - let helperStripped := applyEdits sourceText helperEdits - let helperStripped := - if hasChallengeDeps then removeDuplicatedReducibilityAttributes helperStripped depsHelpers - else helperStripped - let moduleImports ← problemImportHeader root entry.moduleName - let baseImport := if hasChallengeDeps then "import ChallengeDeps\n\n" else moduleImports ++ "\n" - let challengeBodyStripped := stripProblemMarkers helperStripped localImports - let challengeBody := - if !(challengeBodyStripped.trimAsciiStart.toString.startsWith "import ") then - baseImport ++ challengeBodyStripped - else if hasChallengeDeps then - injectAfterImports challengeBodyStripped "import ChallengeDeps\n" - else challengeBodyStripped - let solutionBody := stripProblemMarkers solutionText localImports - let solutionBody := injectAfterImports solutionBody "import Submission\n" baseImport - let solutionBody := - if hasChallengeDeps then injectAfterImports solutionBody "import ChallengeDeps\n" - else solutionBody - -- Submission: source minus helpers, wrapped in `namespace Submission`, with - -- `Submission.Helpers` and (if present) `ChallengeDeps` imported. When - -- ChallengeDeps is present, inject one `open ` per distinct helper - -- enclosing namespace so unqualified helper references inside the wrap - -- resolve to `_root_..` rather than the (non-existent) - -- `Submission..`. - let submissionStripped := stripProblemMarkers helperStripped localImports - let submissionWithHelpers := - injectAfterImports submissionStripped "import Submission.Helpers\n" baseImport - let submissionWithHelpers := - if hasChallengeDeps then injectAfterImports submissionWithHelpers "import ChallengeDeps\n" - else submissionWithHelpers - let userNamespace := lastComponentStr entry.moduleName - let submissionBody := - wrapBodyInSubmissionNamespace submissionWithHelpers userNamespace (extraOpens := helperOpens) - -- config - let mut configPairs : Array (String × OJson) := #[ - ("challenge_module", ojStr "Challenge"), - ("solution_module", ojStr "Solution"), - ("theorem_names", ojStrArr theoremNames), - ("permitted_axioms", ojStrArr fixedAxioms), - ("enable_nanoda", ojBool false) - ] - if !definitionNames.isEmpty then - configPairs := configPairs.push ("definition_names", ojStrArr definitionNames) - let config := ojObj configPairs - let toolchain' := if toolchain.endsWith "\n" then toolchain else toolchain ++ "\n" - let challenge := - if challengeBody.endsWith "\n" then challengeBody else challengeBody ++ "\n" - let readmeLines := renderReadmeLines entry extracteds (multiHole := true) - let readme := "\n".intercalate readmeLines.toList ++ "\n" - let mut files : Array (String × String) := #[ - ("README.md", readme), - ("lean-toolchain", toolchain'), - ("lakefile.toml", lakefileToml entry.id mathlibDep (withChallengeDeps := hasChallengeDeps)), - ("Challenge.lean", challenge), - ("Solution.lean", solutionBody), - ("Submission.lean", submissionBody), - ("Submission/Helpers.lean", "namespace Submission.Helpers\n\nend Submission.Helpers\n"), - ("WorkspaceTest.lean", workspaceTest), - ("config.json", OJson.pretty config ++ "\n") - ] - if let some cd := challengeDeps? then - files := files.push ("ChallengeDeps.lean", cd) - return files - -/-! ## Single-hole rendering -/ - -private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProblemMetadata) - (extracted : ExtractedTheorem) (toolchain : String) (mathlibDep : DependencySpec) - (workspaceTest : String) : IO (Array (String × String)) := do - let sourcePath := moduleSourcePath root entry.moduleName - let sourceText ← IO.FS.readFile sourcePath - let src := Source.ofString sourceText - let theoremName := lastComponentStr extracted.declarationName - let startOff ← src.offsetForLineColumn extracted.startLine extracted.startColumn - let endOff ← src.offsetForLineColumn extracted.endLine extracted.endColumn - let declText := Source.slice src startOff endOff - let theoremStatement ← extractStatementText entry.id sourcePath declText theoremName - let localImports ← repoLocalImportModules root entry.moduleName - let challengeDeps? ← renderChallengeDeps root entry extracted localImports - let hasChallengeDeps := challengeDeps?.isSome - let moduleImports ← problemImportHeader root entry.moduleName - let challengeImport := - if hasChallengeDeps then "import ChallengeDeps\n\n" else moduleImports ++ "\n" - let solutionImports := - if hasChallengeDeps then "import ChallengeDeps\nimport Submission\n\n" - else moduleImports ++ "import Submission\n\n" - let submissionImports := - if hasChallengeDeps then "import ChallengeDeps\nimport Submission.Helpers\n\n" - else moduleImports ++ "import Submission.Helpers\n\n" - let theoremBinderNames := binderIntroducedNames theoremStatement - let contextUniverseBlock := - extractContextUniverses sourceText (some extracted) - let contextVariablesBlock := - extractContextVariables sourceText (some extracted) theoremBinderNames - -- `variable` and notation must keep their source order relative to one - -- another; see `extractContextVariablesAndSyntax`. - let contextVarsWithSyntax := - extractContextVariablesAndSyntax sourceText (some extracted) theoremBinderNames - isSyntaxContextDeclaration - let contextVarsWithLocalSyntax := - extractContextVariablesAndSyntax sourceText (some extracted) theoremBinderNames - isLocalSyntaxContextDeclaration - let contextIncludeBlock := - extractContextIncludes sourceText (some extracted) - -- A prefix scoped onto the target declaration itself belongs with the - -- restated statement, not with the surrounding context. - let declarationSpans ← loadDeclSpans root entry src - let declarationPrefix := extractDeclarationPrefix src - (previousDeclarationEnd declarationSpans (importPreludeLength src) startOff) startOff - let signatureParams? := - if hasBareSorryBody declText then extracted.explicitParameters else none - let some solutionArgs := delegationArgs? signatureParams? - (variableBlockExplicitNames contextVariablesBlock) - (explicitBinderApplicationArgs theoremStatement) - | throw <| IO.userError - s!"Could not match the elaborated parameters of '{extracted.declarationName}' against \ - its source signature; the generated delegation would under-apply it." - let solutionExact := - if solutionArgs.isEmpty then s!"Submission.{theoremName}" - else s!"Submission.{theoremName} " ++ " ".intercalate solutionArgs.toList - let includeNamespaces := hasChallengeDeps || !localImports.isEmpty - let contextOpenBlock ← - extractContextOpens entry.id sourcePath sourceText (some extracted) includeNamespaces - let contextOpenBlock := - if !contextOpenBlock.isEmpty && !contextOpenBlock.endsWith "\n\n" then - contextOpenBlock ++ "\n" - else contextOpenBlock - let toolchain' := if toolchain.endsWith "\n" then toolchain else toolchain ++ "\n" - let config := ojObj #[ - ("challenge_module", ojStr "Challenge"), - ("solution_module", ojStr "Solution"), - ("theorem_names", ojArr #[ojStr theoremName]), - ("permitted_axioms", ojStrArr fixedAxioms), - ("enable_nanoda", ojBool false) - ] - let readmeLines := renderReadmeLines entry #[extracted] (multiHole := false) - let readme := "\n".intercalate readmeLines.toList ++ "\n" - let challengeFile := - challengeImport ++ contextOpenBlock ++ contextUniverseBlock ++ - (if hasChallengeDeps then contextVarsWithLocalSyntax else contextVarsWithSyntax) ++ - contextIncludeBlock ++ declarationPrefix ++ - s!"theorem {theoremName} {theoremStatement} := by\n sorry\n" - let solutionFile := - solutionImports ++ contextOpenBlock ++ contextUniverseBlock ++ - contextVarsWithLocalSyntax ++ contextIncludeBlock ++ declarationPrefix ++ - s!"theorem {theoremName} {theoremStatement} := by\n exact {solutionExact}\n" - let submissionFile := - submissionImports ++ contextOpenBlock ++ contextUniverseBlock ++ - (if hasChallengeDeps then contextVarsWithLocalSyntax else contextVarsWithSyntax) ++ - contextIncludeBlock ++ - "namespace Submission\n\n" ++ declarationPrefix ++ - s!"theorem {theoremName} {theoremStatement} := by\n sorry\n\n" ++ - "end Submission\n" - let mut files : Array (String × String) := #[ - ("README.md", readme), - ("lean-toolchain", toolchain'), - ("lakefile.toml", lakefileToml entry.id mathlibDep (withChallengeDeps := hasChallengeDeps)), - ("Challenge.lean", challengeFile), - ("Solution.lean", solutionFile), - ("Submission.lean", submissionFile), - ("Submission/Helpers.lean", "namespace Submission.Helpers\n\nend Submission.Helpers\n"), - ("WorkspaceTest.lean", workspaceTest), - ("config.json", OJson.pretty config ++ "\n") - ] - if let some cd := challengeDeps? then - files := files.push ("ChallengeDeps.lean", cd) - return files - -/-- Render every file in a generated workspace. Mirrors `render_workspace`. -/ -def renderWorkspace (root : System.FilePath) (entry : EvalProblemMetadata) - (extracteds : Array ExtractedTheorem) (toolchain : String) - (mathlibDep : DependencySpec) (workspaceTest : String) : - IO (Array (String × String)) := do - let isMultiHole := - extracteds.size != 1 || extracteds[0]!.kind != "theorem" - let baseFiles ← - if isMultiHole then - renderWorkspaceMultiHole root entry extracteds toolchain mathlibDep workspaceTest - else - renderWorkspaceSingleHole root entry extracteds[0]! toolchain mathlibDep workspaceTest - let holesJson ← buildHolesMetadata root entry extracteds - return baseFiles.push ("holes.json", holesJson) - -/-! ## Workspace I/O -/ - -/-- All files under `dir` (recursively), as paths relative to `dir`, posix -style (forward slashes). Skips entries whose first component is in -`ignoredPathNames`. Mirrors `gather_extra_paths`'s `extras` computation. -/ -partial def listFilesRecursive (dir : System.FilePath) : IO (Array System.FilePath) := do - if !(← dir.isDir) then return #[] - let mut out : Array System.FilePath := #[] - for entry in (← dir.readDir) do - if (← entry.path.isDir) then - let nested ← listFilesRecursive entry.path - for n in nested do - out := out.push (entry.fileName / n) - else - out := out.push entry.fileName - return out - -/-- Returns the list of paths (relative to `problemDir`) that are present in -the directory but not part of `expectedFiles`, sorted. -/ -def gatherExtraPaths (problemDir : System.FilePath) : IO (Array System.FilePath) := do - if !(← problemDir.pathExists) then return #[] - let all ← listFilesRecursive problemDir - let all := all.qsort (fun a b => a.toString < b.toString) - let expected : Std.HashSet String := expectedFiles.foldl (·.insert ·) {} - let mut out : Array System.FilePath := #[] - for p in all do - let posix := "/".intercalate (p.components.map id) - let firstComp := p.components.head! - if ignoredPathNames.contains firstComp then continue - if expected.contains posix then continue - out := out.push p - return out - -/-- Write the rendered files into `problemDir`, replacing any stale content. -Mirrors `write_workspace`. -/ -def writeWorkspace (problemDir : System.FilePath) - (files : Array (String × String)) : IO Unit := do - IO.FS.createDirAll problemDir - let provided : Std.HashSet String := files.foldl (fun acc (p, _) => acc.insert p) {} - for relPath in expectedFiles do - if provided.contains relPath then continue - let dest := problemDir / relPath - if (← dest.pathExists) then - let info ← dest.metadata - if info.type == .file then - IO.FS.removeFile dest - for extra in (← gatherExtraPaths problemDir) do - IO.FS.removeFile (problemDir / extra) - for (relPath, content) in files do - let dest := problemDir / relPath - if let some parent := dest.parent then - IO.FS.createDirAll parent - IO.FS.writeFile dest content - -/-- Return a list of mismatches between expected files and what's on disk. -Mirrors `check_workspace`. -/ -def checkWorkspace (problemDir : System.FilePath) (relToRoot : String) - (files : Array (String × String)) : IO (Array String) := do - let mut mismatches : Array String := #[] - let provided : Std.HashSet String := files.foldl (fun acc (p, _) => acc.insert p) {} - for relPath in expectedFiles do - if provided.contains relPath then continue - let dest := problemDir / relPath - if (← dest.pathExists) then - mismatches := mismatches.push s!"unexpected {relToRoot}/{relPath}" - for (relPath, expectedContent) in files do - let dest := problemDir / relPath - if !(← dest.pathExists) then - mismatches := mismatches.push s!"missing {relToRoot}/{relPath}" - continue - let info ← dest.metadata - if info.type != .file then - mismatches := mismatches.push s!"missing {relToRoot}/{relPath}" - continue - let actual ← IO.FS.readFile dest - if actual != expectedContent then - mismatches := mismatches.push s!"stale {relToRoot}/{relPath}" - for extra in (← gatherExtraPaths problemDir) do - let posix := "/".intercalate (extra.components.map id) - mismatches := mismatches.push s!"unexpected {relToRoot}/{posix}" - return mismatches - -/-! ## Validate hole shape -/ - -/-- Sanity-check that each manifest hole appears as a top-level -`theorem/def/instance/opaque` declaration in its source module. Mirrors -`validate_hole_shape`. -/ -def validateHoleShape (root : System.FilePath) (entries : Array EvalProblemMetadata) : - IO Unit := do - for entry in entries do - let sourcePath := moduleSourcePath root entry.moduleName - if !(← sourcePath.pathExists) then - throw <| IO.userError - s!"Source file for module '{entry.moduleName}' not found: {sourcePath}" - let sourceText ← IO.FS.readFile sourcePath - let src := Source.ofString sourceText - for hole in entry.holes do - let basename := lastComponentStr hole - match Source.findKeywordBasename src #["theorem", "opaque", "def", "instance"] basename with - | some _ => continue - | none => - let display := - let sp := sourcePath.toString - let rp := root.toString ++ "/" - if sp.startsWith rp then sp.drop rp.length |>.toString else sp - throw <| IO.userError - s!"Problem '{entry.id}' lists hole '{basename}' which is not declared as a top-level theorem/def/instance in {display}." - -/-! ## Sync unknown / index -/ - -/-- Remove (or report) workspace directories under `generated/` that aren't in -`selectedIds`. Mirrors `sync_unknown_problem_dirs`. -/ -def syncUnknownProblemDirs (root : System.FilePath) (selectedIds : Std.HashSet String) - (check : Bool) : IO (Array String) := do - let generated := root / "generated" - IO.FS.createDirAll generated - let mut mismatches : Array String := #[] - let entries ← generated.readDir - let entries := entries.qsort (fun a b => a.fileName < b.fileName) - for e in entries do - if e.fileName == "index.json" then continue - if !(← e.path.isDir) then continue - if selectedIds.contains e.fileName then continue - if check then - mismatches := mismatches.push s!"unexpected generated directory generated/{e.fileName}" - else - IO.FS.removeDirAll e.path - return mismatches - -/-- Write or check `generated/index.json`. Mirrors `write_or_check_index`. -/ -def writeOrCheckIndex (root : System.FilePath) (entries : Array OJson) (check : Bool) : - IO (Array String) := do - let generated := root / "generated" - let indexPath := generated / "index.json" - let content := OJson.pretty (ojArr entries) ++ "\n" - if check then - if !(← indexPath.pathExists) then - return #["missing generated/index.json"] - let actual ← IO.FS.readFile indexPath - if actual != content then - return #["stale generated/index.json"] - return #[] - IO.FS.createDirAll generated - IO.FS.writeFile indexPath content - return #[] - -/-- The `generated/index.json` row determined by one manifest entry. Keep this -in one place so full generation and the cheap global consistency check cannot -disagree about the index format. -/ -def generatedIndexEntry (entry : EvalProblemMetadata) : OJson := - ojObj #[ - ("id", ojStr entry.id), - ("title", ojStr entry.title), - ("group", ojStr entry.group), - ("status", ojStr entry.status), - ("visible", ojBool entry.visible), - ("statement_revision", ojNat entry.statementRevision), - ("tags", ojStrArr entry.tags), - ("submitter", ojStr entry.submitter), - ("module", ojStr entry.moduleName), - ("holes", ojStrArr entry.holes), - ("generated_path", ojStr s!"generated/{entry.id}") - ] - -/-- Check the global generated-tree invariants that per-problem generation -cannot establish: the index must exactly match the manifest, and every -generated workspace directory must belong to a manifest problem. This does no -extraction, module compilation, or workspace generation. -/ -def validateGeneratedCatalog (root : System.FilePath) : IO Unit := do - let problems ← loadManifest root - let selectedIds : Std.HashSet String := - problems.foldl (fun acc p => acc.insert p.id) {} - let mut mismatches ← syncUnknownProblemDirs root selectedIds (check := true) - mismatches := mismatches ++ - (← writeOrCheckIndex root (problems.map generatedIndexEntry) (check := true)) - if !mismatches.isEmpty then - throw <| IO.userError <| "\n".intercalate mismatches.toList - IO.println "Generated index is up to date; no unexpected workspace directories exist." - -/-! ## Generate orchestrator -/ - -/-- Main `generate` entry point. Mirrors `scripts/generate_projects.py:generate`. -/ -def generate (root : System.FilePath) (selectedProblemId : Option String) (check : Bool) : - IO Unit := do - let problems ← loadManifest root - let selectedProblems ← - match selectedProblemId with - | some id => - let filtered := problems.filter (·.id == id) - if filtered.isEmpty then - throw <| IO.userError s!"Unknown problem id '{id}'" - pure filtered - | none => - validateManifestAgainstInventory root problems - let selectedIds : Std.HashSet String := - problems.foldl (fun acc p => acc.insert p.id) {} - let mismatches ← syncUnknownProblemDirs root selectedIds check - if !mismatches.isEmpty then - throw <| IO.userError <| "\n".intercalate mismatches.toList - pure problems - validateHoleShape root selectedProblems - let toolchain ← IO.FS.readFile (root / "lean-toolchain") - let mathlibDep ← loadRootMathlibDependency root - buildExtractor root selectedProblems - let workspaceTest ← loadWorkspaceTestTemplate root - let mut mismatches : Array String := #[] - for entry in selectedProblems do - let mut extracteds : Array ExtractedTheorem := #[] - for hole in entry.holes do - let e ← extractOne root entry hole - extracteds := extracteds.push e - let files ← renderWorkspace root entry extracteds toolchain mathlibDep workspaceTest - let problemDir := root / "generated" / entry.id - let relDisplay := s!"generated/{entry.id}" - if check then - mismatches := mismatches ++ (← checkWorkspace problemDir relDisplay files) - else - writeWorkspace problemDir files - if selectedProblemId.isNone then - mismatches := mismatches ++ - (← writeOrCheckIndex root (problems.map generatedIndexEntry) check) - if !mismatches.isEmpty then - throw <| IO.userError <| "\n".intercalate mismatches.toList - if check then - IO.println "Generated workspaces are up to date." - else - IO.println s!"Generated {selectedProblems.size} problem workspace(s)." - end EvalTools diff --git a/EvalTools/Main.lean b/EvalTools/Main.lean index 0ad7cb609..85e9c910f 100644 --- a/EvalTools/Main.lean +++ b/EvalTools/Main.lean @@ -15,6 +15,8 @@ open Cli namespace EvalTools +open LeanEvalGenerator.Core + set_option autoImplicit false def runRootCmd (p : Parsed) : IO UInt32 := do @@ -62,7 +64,7 @@ def runGenerateCmd (p : Parsed) : IO UInt32 := do let problem? : Option String := p.flag? "problem" |>.map fun f => f.as! String let check := p.hasFlag "check" try - EvalTools.generate root problem? check + LeanEvalGenerator.Core.generate root problem? check return 0 catch e => IO.eprintln (toString e) @@ -71,7 +73,7 @@ def runGenerateCmd (p : Parsed) : IO UInt32 := do def runValidateGeneratedCatalogCmd (_ : Parsed) : IO UInt32 := do let root ← requireRepoRoot try - EvalTools.validateGeneratedCatalog root + LeanEvalGenerator.Core.validateGeneratedCatalog root return 0 catch e => IO.eprintln (toString e) diff --git a/EvalTools/Manifest.lean b/EvalTools/Manifest.lean index 2b75e794c..3955305fb 100644 --- a/EvalTools/Manifest.lean +++ b/EvalTools/Manifest.lean @@ -1,253 +1,5 @@ -import Lean -import EvalTools.Markers -import EvalTools.Subprocess - -open Lean +import LeanEvalGenerator.Core.Manifest namespace EvalTools -set_option autoImplicit false - -/-- Path of the manifest directory, relative to the repository root. -Each problem lives in its own file `manifests/problems/.toml`. -/ -def defaultManifestRelativePath : System.FilePath := - "manifests" / "problems" - -private def isAsciiAlnum (c : Char) : Bool := - c.isAlpha || c.isDigit - -/-- Mirrors the Python `ID_PATTERN = re.compile(r"^[A-Za-z0-9][A-Za-z0-9_-]*$")`. -/ -private def isValidProblemId (s : String) : Bool := - !s.isEmpty - && isAsciiAlnum s.front - && s.all (fun c => isAsciiAlnum c || c == '_' || c == '-') - -/-- Stem of a `*.toml` file (basename without the trailing `.toml`). -/ -private def tomlStem (path : System.FilePath) : String := - let base := path.fileName.getD "" - if base.endsWith ".toml" then (base.dropEnd 5).toString else base - -/-- Load and validate the manifest directory. Walks -`manifests/problems/*.toml` in sorted order, parses each file as a -single problem entry, and enforces: - -* `id` matches the filename stem (catches copy-paste typos); -* `id` satisfies the ASCII `ID_PATTERN` from `scripts/generate_projects.py`; -* required fields and non-empty `holes` (via `parseManifestEntry`); -* `id` and `(module, hole)` uniqueness across all entries. -/ -def loadManifest (root : System.FilePath) : IO (Array EvalProblemMetadata) := do - let manifestDir := root / defaultManifestRelativePath - unless ← manifestDir.isDir do - throw <| IO.userError - s!"Manifest directory `{manifestDir}` does not exist or is not a directory." - let mut rawFiles : Array System.FilePath := #[] - for entry in (← manifestDir.readDir) do - -- Reject rather than skip: a manifest saved as `.lean` used to drop out - -- of the catalog silently, taking its problem module with it (issue #519). - -- The exemption is `.DS_Store` alone, not dotfiles in general: the - -- `@[eval_problem]` elaborator reads every `*.toml` here (`Markers.lean`), - -- so skipping a hidden `.foo.toml` would let it claim a tagged declaration - -- that never reaches the catalog. - if entry.fileName == ".DS_Store" then - continue - if ← entry.path.isDir then - throw <| IO.userError - s!"`{entry.path}` is a directory; `manifests/problems/` holds one `.toml` file per problem." - unless entry.path.extension == some "toml" do - throw <| IO.userError - s!"`{entry.path}` is not a `.toml` file; `manifests/problems/` holds one `.toml` file per problem." - rawFiles := rawFiles.push entry.path - let files := rawFiles.qsort fun a b => - (a.fileName.getD "") < (b.fileName.getD "") - let mut entries : Array EvalProblemMetadata := #[] - let mut seenIds : Std.HashSet String := {} - let mut seenRefs : Std.HashSet (String × String) := {} - for file in files do - let contents ← IO.FS.readFile file - let entry ← - match ← parseManifestEntry contents file.toString with - | .ok m => pure m - | .error err => throw <| IO.userError err - let expectedId := tomlStem file - unless entry.id == expectedId do - throw <| IO.userError - s!"Manifest entry in `{file}` has id `{entry.id}` but filename stem is `{expectedId}`; the two must match." - unless isValidProblemId entry.id do - throw <| IO.userError - s!"Problem id '{entry.id}' is invalid. Use only letters, digits, '_' or '-'." - if seenIds.contains entry.id then - throw <| IO.userError s!"Duplicate problem id `{entry.id}` across files in `manifests/problems/`." - seenIds := seenIds.insert entry.id - for hole in entry.holes do - let key := (entry.moduleName, hole) - if seenRefs.contains key then - throw <| IO.userError - s!"Duplicate hole reference `{entry.moduleName}:{hole}` across files in `manifests/problems/`." - seenRefs := seenRefs.insert key - entries := entries.push entry - return entries - -/-- Preserve the order of first occurrence (matches Python's `unique_modules`). -/ -def uniqueModules (entries : Array EvalProblemMetadata) : Array String := Id.run do - let mut seen : Std.HashSet String := {} - let mut out : Array String := #[] - for entry in entries do - unless seen.contains entry.moduleName do - seen := seen.insert entry.moduleName - out := out.push entry.moduleName - return out - -/-- Result row from the `eval_inventory` tool. Mirrors -`scripts/generate_projects.py`'s `InventoryEntry`. -/ -structure ManifestInventoryEntry where - module : String - declarationName : String - basename : String - kind : String - deriving Inhabited, ToJson - -/-- Parse the JSON emitted by `eval_inventory`. -/ -def parseInventoryEntries (payload : String) : - Except String (Array ManifestInventoryEntry) := do - let json ← Json.parse payload - let arr ← json.getArr? - let mut out : Array ManifestInventoryEntry := #[] - for raw in arr do - let module ← raw.getObjValAs? String "module" - let declarationName ← raw.getObjValAs? String "declarationName" - let basename ← raw.getObjValAs? String "basename" - let kind ← raw.getObjValAs? String "kind" - out := out.push - { module := module, declarationName := declarationName, - basename := basename, kind := kind } - return out - -/-- Resolve an optional module restriction against the manifest, rejecting -typos rather than silently producing an incomplete CI shard. -/ -def selectManifestModules (entries : Array EvalProblemMetadata) - (requested : Array String) : IO (Array String) := do - let available := uniqueModules entries - if requested.isEmpty then - return available - let known := available.foldl (fun set name => set.insert name) ({} : Std.HashSet String) - let mut seen : Std.HashSet String := {} - let mut selected := #[] - for moduleName in requested do - unless known.contains moduleName do - throw <| IO.userError s!"Requested problem module is not present in the manifest: {moduleName}" - unless seen.contains moduleName do - seen := seen.insert moduleName - selected := selected.push moduleName - return selected - -/-- Build the Lake targets and run the `eval_inventory` executable over every -module referenced by `entries`. - -Build the inventory executable first, then (unless a preceding trusted step -already did so) each problem module separately. Passing every problem module to -one `lake build` lets Lake schedule the entire catalog at once, which can -exhaust machine resources on a clean checkout. -/ -def runInventoryTool (root : System.FilePath) (modules : Array String) - (buildModules : Bool := true) : - IO (Array ManifestInventoryEntry) := do - let _ ← runCmdCheckedCaptured "lake" - #["build", "eval_inventory"] root - "Failed to build Lean problem inventory tool" - if buildModules then - for moduleName in modules do - let _ ← runCmdCheckedCaptured "lake" - #["build", moduleName] root - s!"Failed to build Lean problem module '{moduleName}'" - let binPath := root / ".lake" / "build" / "bin" / "eval_inventory" - let out ← runCmdCheckedCaptured "lake" - (#["env", binPath.toString] ++ modules) root - "Lean problem inventory failed" - match parseInventoryEntries out.stdout with - | .ok entries => pure entries - | .error err => throw <| IO.userError s!"Problem inventory returned invalid JSON: {err}" - -/-- Load and concatenate the per-shard inventory JSON files downloaded by the -aggregate CI job. -/ -def loadInventoryDirectory (directory : System.FilePath) : IO (Array ManifestInventoryEntry) := do - unless ← directory.isDir do - throw <| IO.userError s!"Problem inventory directory does not exist: {directory}" - let files := (← directory.readDir).qsort fun a b => a.fileName < b.fileName - let mut inventory := #[] - for file in files do - if ← file.path.isDir then - throw <| IO.userError s!"Unexpected directory in problem inventory: {file.path}" - unless file.path.extension == some "json" do - throw <| IO.userError s!"Unexpected non-JSON problem inventory file: {file.path}" - let payload ← IO.FS.readFile file.path - match parseInventoryEntries payload with - | .ok entries => inventory := inventory ++ entries - | .error err => - throw <| IO.userError s!"Problem inventory `{file.path}` is invalid: {err}" - return inventory - -/-- Write the tagged-declaration inventory for `requestedModules`. Problem -modules must already have been built by the warning-sensitive shard step. -/ -def writeProblemInventory (root output : System.FilePath) - (requestedModules : Array String) : IO Unit := do - let entries ← loadManifest root - let modules ← selectManifestModules entries requestedModules - let inventory ← runInventoryTool root modules (buildModules := false) - IO.FS.writeFile output (Json.pretty (toJson inventory) ++ "\n") - -/-- Validate a manifest against inventory rows already collected by CI shards. -/ -def validateManifestAgainstInventoryEntries - (entries : Array EvalProblemMetadata) - (inventory : Array ManifestInventoryEntry) : IO Unit := do - let expectedModules := uniqueModules entries - let inventoriedModules := inventory.foldl - (fun set entry => set.insert entry.module) ({} : Std.HashSet String) - let missingModules := expectedModules.filter (!inventoriedModules.contains ·) - unless missingModules.isEmpty do - throw <| IO.userError <| - "Problem inventory is missing manifest module(s): " - ++ ", ".intercalate missingModules.toList - let expectedSet := expectedModules.foldl - (fun set moduleName => set.insert moduleName) ({} : Std.HashSet String) - let unexpectedModules := inventory.filterMap fun entry => - if expectedSet.contains entry.module then none else some entry.module - unless unexpectedModules.isEmpty do - let names := unexpectedModules.qsort (· < ·) - throw <| IO.userError <| - "Problem inventory contains module(s) absent from the manifest: " - ++ ", ".intercalate names.toList - let mut byModule : Std.HashMap String (Array ManifestInventoryEntry) := {} - for inv in inventory do - byModule := byModule.insert inv.module - ((byModule.getD inv.module #[]).push inv) - let mut matched : Std.HashSet String := {} - for problem in entries do - let moduleInventory := byModule.getD problem.moduleName #[] - for hole in problem.holes do - let candidates := moduleInventory.filter fun inv => - inv.basename == hole || inv.declarationName == hole - if candidates.isEmpty then - throw <| IO.userError - s!"Manifest entry '{problem.id}' references hole '{hole}' which has no @[eval_problem] declaration in module '{problem.moduleName}'." - if candidates.size > 1 then - throw <| IO.userError - s!"Manifest entry '{problem.id}' hole '{hole}' is ambiguous in module '{problem.moduleName}'. Use a fully qualified name." - matched := matched.insert candidates[0]!.declarationName - let untracked := inventory.filterMap fun inv => - if matched.contains inv.declarationName then none else some inv.declarationName - if !untracked.isEmpty then - let sorted := untracked.qsort (· < ·) - let joined := ", ".intercalate sorted.toList - throw <| IO.userError - s!"Tagged @[eval_problem] declaration(s) are missing from manifests/problems/: {joined}" - -/-- Match Python's `gp.validate_manifest_against_inventory`: ensure every -manifest hole resolves to exactly one `@[eval_problem]`-tagged declaration, -and every such declaration appears in the manifest. -/ -def validateManifestAgainstInventory - (root : System.FilePath) (entries : Array EvalProblemMetadata) - (buildModules : Bool := true) : IO Unit := do - let modules := uniqueModules entries - let inventory ← runInventoryTool root modules buildModules - validateManifestAgainstInventoryEntries entries inventory - end EvalTools diff --git a/EvalTools/Markers.lean b/EvalTools/Markers.lean index f56e3e3be..34245f107 100644 --- a/EvalTools/Markers.lean +++ b/EvalTools/Markers.lean @@ -1,377 +1,8 @@ import Lake.Toml import Lake.Util.Message import Lean - -open Lean -open Lean.Parser -open Lake -open Lake.Toml -open Std - -set_option autoImplicit false +import LeanEvalGenerator.Core.Markers namespace EvalTools -structure EvalProblemMetadata where - id : String - title : String - /-- Policy group containing this problem. Valid values are checked by the - manifest decoder and the catalog validator. -/ - group : String - /-- Current lifecycle status (`draft`, `active`, or `archived`). -/ - status : String - /-- Whether the problem is shown in public catalog surfaces. -/ - visible : Bool - /-- Monotonic revision of the trusted statement. -/ - statementRevision : Nat - /-- Stable registry keys from `manifests/tags.toml`. -/ - tags : Array String - moduleName : String - /-- The names of the `@[eval_problem]`-tagged declarations in `moduleName` that - comprise this problem; comparator's `theorem_names` and `definition_names` - are derived from this list (split by declaration kind). At least one entry - is required. -/ - holes : Array String - submitter : String - notes : Option String := none - source : Option String := none - informalSolution : Option String := none - -/-- The manifest directory, relative to the repository root. Each problem -lives in its own file `manifests/problems/.toml` with top-level keys. -/ -def manifestRelativePath : System.FilePath := - "manifests" / "problems" - -/-- Read a manifest `module` field as a module name: every `.` separates -components, so `LeanEval.Foo.Bar` is `LeanEval/Foo/Bar.lean` and never -`LeanEval/Foo.Bar.lean`. The inventory and extractor executables resolve the -same field the same way; the two must agree or they address different files. -/ -def parseModuleName (text : String) : Name := - text.splitOn "." |>.foldl Name.str .anonymous - -/-- Walk up from `dir` searching for the manifest directory -`manifests/problems/`. Returns the directory itself if found. -/ -partial def findManifestPath? (dir : System.FilePath) : IO (Option System.FilePath) := do - let candidate := dir / manifestRelativePath - if ← candidate.isDir then - return some candidate - match dir.parent with - | none => return none - | some parent => - if parent == dir then - return none - findManifestPath? parent - -def requireNonempty (field value : String) : EDecodeM String := do - if value.isEmpty then - throwDecodeErrorAt Syntax.missing s!"Manifest field `{field}` must be non-empty." - pure value - -def allowedProblemGroups : Array String := - #["formalization-evaluation", "software-verification", "open-conjectures"] - -def allowedProblemStatuses : Array String := - #["draft", "active", "archived"] - -def requireOneOf (field value : String) (allowed : Array String) : EDecodeM String := do - unless allowed.contains value do - throwDecodeErrorAt Syntax.missing - s!"Manifest field `{field}` must be one of {", ".intercalate allowed.toList}; got `{value}`." - pure value - -instance : DecodeToml EvalProblemMetadata where - decode v := do - let t ← v.decodeTable - let id ← requireNonempty "id" (← t.decode `id) - let title ← requireNonempty "title" (← t.decode `title) - let group ← requireOneOf "group" (← t.decode `group) allowedProblemGroups - let status ← requireOneOf "status" (← t.decode `status) allowedProblemStatuses - let statementRevision : Nat ← t.decode `statement_revision - if statementRevision == 0 then - throwDecodeErrorAt Syntax.missing - s!"Manifest entry `{id}` has statement_revision = 0; revisions start at 1." - let tags : Array String ← t.decode `tags - for tag in tags do - if tag.isEmpty then - throwDecodeErrorAt Syntax.missing - s!"Manifest entry `{id}` has an empty string in `tags`." - let moduleName ← requireNonempty "module" (← t.decode `module) - let holes : Array String ← t.decode `holes - if holes.isEmpty then - throwDecodeErrorAt Syntax.missing - s!"Manifest entry `{id}` has empty `holes` array; list at least one declaration." - for h in holes do - if h.isEmpty then - throwDecodeErrorAt Syntax.missing - s!"Manifest entry `{id}` has an empty string in `holes`." - let submitter ← requireNonempty "submitter" (← t.decode `submitter) - let notes? : Option String ← t.decode? `notes - let source? : Option String ← t.decode? `source - let informalSolution? : Option String ← t.decode? `informal_solution - return { - id := id - title := title - group := group - status := status - visible := ← t.decode `visible - statementRevision := statementRevision - tags := tags - moduleName := moduleName - holes := holes - submitter := submitter - notes := notes?.bind fun s => if s.isEmpty then none else some s - source := source?.bind fun s => if s.isEmpty then none else some s - informalSolution := informalSolution?.bind fun s => if s.isEmpty then none else some s - } - -def decodeErrorsToString (errors : Array DecodeError) : String := - "\n".intercalate <| errors.toList.map fun err => err.msg - -/-- Parse a single per-problem TOML file (top-level keys: `id`, `title`, -`group`, `status`, `visible`, `statement_revision`, `tags`, `module`, `holes`, -`submitter`, optional `notes`, `source`, `informal_solution`, and lifecycle -history arrays). The caller is responsible for `id ↔ filename` and -cross-file uniqueness checks (see `EvalTools.loadManifest`). -/ -def parseManifestEntry (contents : String) (fileName : String) : - IO (Except String EvalProblemMetadata) := do - let inputCtx := mkInputContext contents fileName - let table ← - match (← Lake.Toml.loadToml inputCtx |>.toBaseIO) with - | Except.ok table => pure table - | Except.error err => return Except.error (← Lake.mkMessageLogString err) - let decoded : - EStateM.Result Unit (Array DecodeError) EvalProblemMetadata := - (DecodeToml.decode (α := EvalProblemMetadata) (Lake.Toml.Value.table Syntax.missing table)).run #[] - match decoded with - | EStateM.Result.ok entry errors => - if errors.isEmpty then - return Except.ok entry - else - return Except.error (decodeErrorsToString errors) - | EStateM.Result.error _ errors => - return Except.error (decodeErrorsToString errors) - -def moduleNameForDecl (env : Environment) (declName : Name) : String := - match env.getModuleIdxFor? declName with - | some idx => toString <| env.header.moduleNames[idx.toNat]! - | none => toString env.mainModule - -def holeMatches (declName : Name) (holeField : String) : Bool := - holeField == declName.toString || holeField == declName.getString! - -def validateMatchingManifestEntry - (declName : Name) (entries : Array EvalProblemMetadata) (moduleName : String) : - Except String EvalProblemMetadata := do - let matchingEntries := entries.filter fun entry => - entry.moduleName == moduleName && entry.holes.any (holeMatches declName ·) - if matchingEntries.isEmpty then - throw - s!"The declaration `{declName}` is marked with @[eval_problem], but no file in `manifests/problems/` lists it in `holes`.\nAdd a corresponding `manifests/problems/.toml` file." - if matchingEntries.size > 1 then - throw - s!"The declaration `{declName}` is marked with @[eval_problem], but `manifests/problems/` has multiple matching entries in module `{moduleName}`." - match matchingEntries[0]? with - | some metadata => return metadata - | none => throw "internal error: missing manifest entry after nonempty match set" - -def formatManifestHover (metadata : EvalProblemMetadata) : String := - Id.run do - let mut lines := #[ - "Benchmark problem metadata.", - "", - s!"- id: `{metadata.id}`", - s!"- title: {metadata.title}", - s!"- group: `{metadata.group}`", - s!"- status: `{metadata.status}`", - s!"- visible: `{metadata.visible}`", - s!"- statement revision: `{metadata.statementRevision}`", - s!"- tags: {", ".intercalate (metadata.tags.toList.map (s!"`{·}`"))}", - s!"- module: `{metadata.moduleName}`", - s!"- holes: {", ".intercalate (metadata.holes.toList.map (s!"`{·}`"))}", - s!"- submitter: {metadata.submitter}" - ] - if let some notes := metadata.notes then - lines := lines.push s!"- notes: {notes}" - if let some source := metadata.source then - lines := lines.push s!"- source: {source}" - if let some informalSolution := metadata.informalSolution then - lines := lines.push s!"- informal_solution: {informalSolution}" - "\n".intercalate lines.toList - -def mkEvalProblemExpr (env : Environment) (declName : Name) : Expr := - match env.find? declName with - | some info => .const declName (info.levelParams.map Level.param) - | none => .const declName [] - -def pushEvalProblemHoverInfo (declName : Name) (attrStx : Syntax) (metadata : EvalProblemMetadata) : - AttrM Unit := do - let tokenStx := attrStx[0] - let env ← getEnv - let info : Elab.Info := .ofDelabTermInfo { - toTermInfo := { - elaborator := `eval_problem - stx := tokenStx - lctx := {} - expectedType? := none - expr := mkEvalProblemExpr env declName - isBinder := false - isDisplayableTerm := false - } - mkDocString? := some (fun _ => pure (formatManifestHover metadata)) - explicit := true - } - Elab.pushInfoLeaf info - -def binderInfoDescription (binderInfo : BinderInfo) : String := - match binderInfo with - | .default => "explicit" - | .implicit => "implicit" - | .strictImplicit => "strict implicit" - | .instImplicit => "instance implicit" - -structure TheoremBinder where - name : Name - type : Expr - binderInfo : BinderInfo - fvar : Expr - -partial def collectTheoremBinders (type : Expr) : MetaM (Array TheoremBinder × Expr) := do - let rec go (type : Expr) (acc : Array TheoremBinder) : MetaM (Array TheoremBinder × Expr) := do - match type.consumeMData with - | .forallE binderName binderType body binderInfo => - let binderType ← Meta.whnfD binderType - Meta.withLocalDecl binderName binderInfo binderType fun localDecl => do - let acc := acc.push { - name := binderName - type := binderType - binderInfo := binderInfo - fvar := localDecl - } - go (body.instantiate1 localDecl) acc - | _ => pure (acc, type) - go type #[] - -def exprDependsOnFVar (expr fvar : Expr) : Bool := - (expr.find? fun subexpr => subexpr == fvar).isSome - -def collectForbiddenImplicitBinders (type : Expr) : MetaM (Array (Name × Expr × BinderInfo)) := do - let (binders, resultType) ← collectTheoremBinders type - let explicitBinderTypes := - binders.foldl (init := #[]) fun acc binder => - if binder.binderInfo == .default then - acc.push binder.type - else - acc - let forbidden := binders.filterMap fun binder => - if binder.binderInfo != .implicit && binder.binderInfo != .strictImplicit then - none - else if binder.type.isSort then - none - else - let inferable := - explicitBinderTypes.any (fun explicitType => exprDependsOnFVar explicitType binder.fvar) || - exprDependsOnFVar resultType binder.fvar - if inferable then - none - else - some (binder.name, binder.type, binder.binderInfo) - pure forbidden - -def validateEvalProblemBinders (declName : Name) (type : Expr) : AttrM Unit := do - let forbiddenBinders ← - ({ env := ← getEnv, opts := ← getOptions } : PPContext).runMetaM do - collectForbiddenImplicitBinders type - if forbiddenBinders.isEmpty then - return - let binderLines ← - ({ env := ← getEnv, opts := ← getOptions } : PPContext).runMetaM do - forbiddenBinders.mapM fun (binderName, binderType, binderInfo) => do - let binderTypeFmt ← Meta.ppExpr binderType - let binderName := - if binderName == Name.anonymous then "_" else binderName.toString - pure s!"- `{binderName}` : {binderTypeFmt} ({binderInfoDescription binderInfo})" - let details := "\n".intercalate binderLines.toList - throwError - "{String.intercalate "\n" - [s!"The theorem `{declName}` uses implicit value parameters that are not inferable from the explicit hypotheses or the conclusion, which @[eval_problem] does not allow." - , "Generated benchmark wrappers must be able to call the theorem by ordinary application, without named arguments or `@`." - , "Keep implicit type parameters like `{α : Type*}` and instance parameters like `[Field K]`." - , "For benchmark inputs that are not recoverable from later explicit binders, use explicit binders `(x : τ)` instead of implicit ones `{x : τ}`." - , s!"Non-inferable implicit binders:\n{details}"]}" - -def ensureEvalProblemManifestEntry (declName : Name) : AttrM EvalProblemMetadata := do - let env ← getEnv - match env.find? declName with - | some (.thmInfo info) => - validateEvalProblemBinders declName info.type - | some (.opaqueInfo info) => - validateEvalProblemBinders declName info.type - | some (.defnInfo _) => - -- Definition / instance holes: comparator only checks name, type, universe - -- levels, and safety of the hole, so the binder-shape restriction we - -- impose on theorems (so they can be applied positionally) does not apply. - pure () - | _ => - throwError - "The attribute @[eval_problem] may only be applied to theorem, opaque, def, or instance declarations, but `{declName}` is not one." - let cwd ← IO.currentDir - let some manifestDir ← findManifestPath? cwd - | throwError - "Could not find `manifests/problems/` while validating @[eval_problem] on `{declName}`." - let mut entries : Array EvalProblemMetadata := #[] - for entry in (← manifestDir.readDir) do - if entry.path.extension == some "toml" then - let contents ← IO.FS.readFile entry.path - match ← parseManifestEntry contents entry.path.toString with - | .ok m => entries := entries.push m - | .error err => throwError "{err}" - let moduleName := moduleNameForDecl env declName - match validateMatchingManifestEntry declName entries moduleName with - | .ok metadata => pure metadata - | .error err => throwError "{err}" - -initialize evalProblemExt : PersistentEnvExtension Name Name NameSet ← - registerPersistentEnvExtension { - name := `EvalTools.evalProblemExt - mkInitial := pure {} - addImportedFn := fun _ _ => pure {} - addEntryFn := fun (s : NameSet) n => s.insert n - exportEntriesFnEx := fun env es => - let entries : Array Name := es.foldl (fun acc entry => acc.push entry) #[] - let entries := entries.filter (env.contains (skipRealize := false)) - .uniform <| entries.qsort Name.quickLt - statsFn := fun s => "eval_problem attribute" ++ Format.line ++ "number of local entries: " ++ format s.size - asyncMode := .mainOnly - replay? := some fun _ newState newConsts s => - newConsts.foldl (init := s) fun acc c => - if newState.contains c then acc.insert c else acc - } - -initialize evalProblemAttr : AttributeImpl ← - let attrImpl : AttributeImpl := { - ref := `eval_problem - name := `eval_problem - descr := "Marks theorem declarations as benchmark problems and validates their manifest metadata." - applicationTime := AttributeApplicationTime.afterTypeChecking - add := fun decl stx kind => do - Attribute.Builtin.ensureNoArgs stx - unless kind == AttributeKind.global do - throwAttrMustBeGlobal `eval_problem kind - let env ← getEnv - unless (env.getModuleIdxFor? decl).isNone do - throwAttrDeclInImportedModule `eval_problem decl - unless evalProblemExt.toEnvExtension.asyncMayModify env decl do - throwAttrNotInAsyncCtx `eval_problem decl env.asyncPrefix? - let metadata ← ensureEvalProblemManifestEntry decl - pushEvalProblemHoverInfo decl stx metadata - modifyEnv fun env => evalProblemExt.addEntry (asyncDecl := decl) env decl - } - registerBuiltinAttribute attrImpl - pure attrImpl - -def hasEvalProblemTag (env : Environment) (declName : Name) : Bool := - match env.getModuleIdxFor? declName with - | some modIdx => (evalProblemExt.getModuleEntries env modIdx).binSearchContains declName Name.quickLt - | none => (evalProblemExt.getState (asyncDecl := declName) env).contains declName - end EvalTools diff --git a/EvalTools/ModuleCoverage.lean b/EvalTools/ModuleCoverage.lean index 2460429f6..0666b70f0 100644 --- a/EvalTools/ModuleCoverage.lean +++ b/EvalTools/ModuleCoverage.lean @@ -5,6 +5,8 @@ open Lean namespace EvalTools +open LeanEvalGenerator.Core + set_option autoImplicit false /-- Directory holding the trusted problem sources, relative to the repository diff --git a/EvalTools/ProblemInventory.lean b/EvalTools/ProblemInventory.lean index cadab7dfb..19263c3c4 100644 --- a/EvalTools/ProblemInventory.lean +++ b/EvalTools/ProblemInventory.lean @@ -2,6 +2,7 @@ import Lean import EvalTools.Markers open Lean +open LeanEvalGenerator.Core structure InventoryEntry where module : String @@ -26,7 +27,8 @@ def inventoryForModule (env : Environment) (moduleName : Name) : Array Inventory Id.run do let mut entries := #[] for (declName, constantInfo) in env.constants do - if env.getModuleIdxFor? declName == some moduleIdx && EvalTools.hasEvalProblemTag env declName then + if env.getModuleIdxFor? declName == some moduleIdx && + LeanEvalGenerator.Core.hasEvalProblemTag env declName then let kind? : Option String := match constantInfo with | .thmInfo _ | .opaqueInfo _ => some "theorem" | .defnInfo _ => @@ -45,7 +47,7 @@ def inventoryForModule (env : Environment) (moduleName : Name) : Array Inventory def main (args : List String) : IO UInt32 := do initSearchPath (← findSysroot) - let moduleNames := args.map EvalTools.parseModuleName + let moduleNames := args.map LeanEvalGenerator.Core.parseModuleName let env ← importModules (moduleNames.toArray.map fun moduleName => ({ module := moduleName } : Import)) {} let entries := moduleNames.foldl (fun acc moduleName => acc ++ inventoryForModule env moduleName) #[] IO.println <| Json.pretty <| toJson entries diff --git a/EvalTools/RunEval.lean b/EvalTools/RunEval.lean index 77ef5f0af..c9deca4ff 100644 --- a/EvalTools/RunEval.lean +++ b/EvalTools/RunEval.lean @@ -8,6 +8,8 @@ open Lean namespace EvalTools +open LeanEvalGenerator.Core + set_option autoImplicit false /-- Per-problem score, mirroring `run_eval.py`'s `ProblemScore` dataclass. -/ diff --git a/EvalTools/Subprocess.lean b/EvalTools/Subprocess.lean index 48610f85a..d5c1cdc01 100644 --- a/EvalTools/Subprocess.lean +++ b/EvalTools/Subprocess.lean @@ -1,59 +1,5 @@ -import Lean - -open Lean +import LeanEvalGenerator.Core.Subprocess namespace EvalTools -set_option autoImplicit false - -/-- Outcome of running a captured subprocess. -/ -structure ProcessOutput where - exitCode : UInt32 - stdout : String - stderr : String - -/-- Run a process to completion in `cwd`, capturing stdout and stderr. -/ -def runCmdCaptured (cmd : String) (args : Array String) (cwd : System.FilePath) : - IO ProcessOutput := do - let out ← IO.Process.output { - cmd := cmd - args := args - cwd := cwd - } - return { exitCode := out.exitCode, stdout := out.stdout, stderr := out.stderr } - -/-- Run a process and throw an `IO.userError` if it exits non-zero. The error -message is `errorPrefix` followed by the captured stderr+stdout (whichever is -non-empty), matching `scripts/generate_projects.py`'s `run(...)` helper. -/ -def runCmdCheckedCaptured - (cmd : String) (args : Array String) (cwd : System.FilePath) (errorPrefix : String) : - IO ProcessOutput := do - let out ← runCmdCaptured cmd args cwd - if out.exitCode != 0 then - let stderr := out.stderr.trimAscii.toString - let stdout := out.stdout.trimAscii.toString - let details := [stderr, stdout].filter (! ·.isEmpty) |> String.intercalate "\n" - if details.isEmpty then - throw <| IO.userError errorPrefix - else - throw <| IO.userError s!"{errorPrefix}:\n{details}" - return out - -/-- Run a process inheriting stdout/stderr/stdin streams, and throw an -`IO.userError` if it exits non-zero. -/ -def runCmdCheckedInherit - (cmd : String) (args : Array String) (cwd : System.FilePath) (errorPrefix : String) : - IO Unit := do - let child ← IO.Process.spawn { - cmd := cmd - args := args - cwd := cwd - stdin := .inherit - stdout := .inherit - stderr := .inherit - } - let exit ← child.wait - if exit != 0 then - throw <| IO.userError s!"{errorPrefix} (exit code {exit})." - end EvalTools diff --git a/EvalTools/ValidateManifest.lean b/EvalTools/ValidateManifest.lean index c808d6b16..af8978ce1 100644 --- a/EvalTools/ValidateManifest.lean +++ b/EvalTools/ValidateManifest.lean @@ -3,6 +3,8 @@ import EvalTools.ModuleCoverage namespace EvalTools +open LeanEvalGenerator.Core + set_option autoImplicit false /-- Implementation of `lake exe lean-eval validate-manifest`. Loads the diff --git a/EvalTools/ValidateSubmission.lean b/EvalTools/ValidateSubmission.lean index 159d540bb..00a78193e 100644 --- a/EvalTools/ValidateSubmission.lean +++ b/EvalTools/ValidateSubmission.lean @@ -6,6 +6,8 @@ open Lean namespace EvalTools +open LeanEvalGenerator.Core + set_option autoImplicit false /-- Mirrors the git change record from `git diff --name-status -z`. For diff --git a/generated/annals_absolute_profinite_rigidity/Challenge.lean b/generated/annals_absolute_profinite_rigidity/Challenge.lean index 3f2ae05d4..cfae5e3b4 100644 --- a/generated/annals_absolute_profinite_rigidity/Challenge.lean +++ b/generated/annals_absolute_profinite_rigidity/Challenge.lean @@ -5,5 +5,7 @@ open Group Polynomial universe u +set_option autoImplicit false + theorem theorem_7_1 : ProfinitelyRigid (BianchiGroup 3) := by sorry diff --git a/generated/annals_absolute_profinite_rigidity/Solution.lean b/generated/annals_absolute_profinite_rigidity/Solution.lean index d0101238d..d0ec83d65 100644 --- a/generated/annals_absolute_profinite_rigidity/Solution.lean +++ b/generated/annals_absolute_profinite_rigidity/Solution.lean @@ -6,5 +6,7 @@ open Group Polynomial universe u +set_option autoImplicit false + theorem theorem_7_1 : ProfinitelyRigid (BianchiGroup 3) := by exact Submission.theorem_7_1 diff --git a/generated/annals_absolute_profinite_rigidity/Submission.lean b/generated/annals_absolute_profinite_rigidity/Submission.lean index b5d05d596..3a8998cb2 100644 --- a/generated/annals_absolute_profinite_rigidity/Submission.lean +++ b/generated/annals_absolute_profinite_rigidity/Submission.lean @@ -6,6 +6,8 @@ open Group Polynomial universe u +set_option autoImplicit false + namespace Submission theorem theorem_7_1 : ProfinitelyRigid (BianchiGroup 3) := by diff --git a/generated/annals_algebraic_integers/Challenge.lean b/generated/annals_algebraic_integers/Challenge.lean index 403a658f5..bd286b3f4 100644 --- a/generated/annals_algebraic_integers/Challenge.lean +++ b/generated/annals_algebraic_integers/Challenge.lean @@ -3,5 +3,7 @@ import ChallengeDeps open AlgebraicIntegers open ComplexOrder +set_option autoImplicit false + theorem theorem_1_1 : lambda_SSS < 1.89831 := by sorry diff --git a/generated/annals_algebraic_integers/Solution.lean b/generated/annals_algebraic_integers/Solution.lean index 4cd9777a8..1bf44fa98 100644 --- a/generated/annals_algebraic_integers/Solution.lean +++ b/generated/annals_algebraic_integers/Solution.lean @@ -4,5 +4,7 @@ import Submission open AlgebraicIntegers open ComplexOrder +set_option autoImplicit false + theorem theorem_1_1 : lambda_SSS < 1.89831 := by exact Submission.theorem_1_1 diff --git a/generated/annals_algebraic_integers/Submission.lean b/generated/annals_algebraic_integers/Submission.lean index b562ed490..35b1b6c16 100644 --- a/generated/annals_algebraic_integers/Submission.lean +++ b/generated/annals_algebraic_integers/Submission.lean @@ -4,6 +4,8 @@ import Submission.Helpers open AlgebraicIntegers open ComplexOrder +set_option autoImplicit false + namespace Submission theorem theorem_1_1 : lambda_SSS < 1.89831 := by diff --git a/generated/annals_conjecture_of_marton/Challenge.lean b/generated/annals_conjecture_of_marton/Challenge.lean index 930620701..4f242110b 100644 --- a/generated/annals_conjecture_of_marton/Challenge.lean +++ b/generated/annals_conjecture_of_marton/Challenge.lean @@ -3,6 +3,7 @@ import ChallengeDeps open ConjectureOfMarton open Pointwise +set_option autoImplicit false variable (n : ℕ) theorem theorem_1_2 (A : Set (F n)) (K : ℝ) (h₀ : A.Nonempty) (h : (A + A).ncard ≤ K * A.ncard) : diff --git a/generated/annals_conjecture_of_marton/Solution.lean b/generated/annals_conjecture_of_marton/Solution.lean index b4cdec60f..515a1dd12 100644 --- a/generated/annals_conjecture_of_marton/Solution.lean +++ b/generated/annals_conjecture_of_marton/Solution.lean @@ -4,6 +4,7 @@ import Submission open ConjectureOfMarton open Pointwise +set_option autoImplicit false variable (n : ℕ) theorem theorem_1_2 (A : Set (F n)) (K : ℝ) (h₀ : A.Nonempty) (h : (A + A).ncard ≤ K * A.ncard) : diff --git a/generated/annals_conjecture_of_marton/Submission.lean b/generated/annals_conjecture_of_marton/Submission.lean index 034504ca8..59370bf50 100644 --- a/generated/annals_conjecture_of_marton/Submission.lean +++ b/generated/annals_conjecture_of_marton/Submission.lean @@ -4,6 +4,7 @@ import Submission.Helpers open ConjectureOfMarton open Pointwise +set_option autoImplicit false variable (n : ℕ) namespace Submission diff --git a/generated/annals_dirichlet_weyl_bound/Challenge.lean b/generated/annals_dirichlet_weyl_bound/Challenge.lean index 583e066da..646b6f5ae 100644 --- a/generated/annals_dirichlet_weyl_bound/Challenge.lean +++ b/generated/annals_dirichlet_weyl_bound/Challenge.lean @@ -3,6 +3,8 @@ import ChallengeDeps open DirichletWeylBound open Complex +set_option autoImplicit false + theorem corollary_1_3 (ε : ℝ) (hε : 0 < ε) : ∃ C : ℝ, ∀ q (_hq : q.IsCubeFree) [NeZero q] (χ : DirichletCharacter ℂ q) (_hχ : χ.IsPrimitive) (t : ℝ), ‖χ.LFunction (1 / 2 + I * t)‖ ≤ C * q ^ (1 / 6 + ε) * (1 + |t|) ^ (1 / 6 + ε) := by diff --git a/generated/annals_dirichlet_weyl_bound/Solution.lean b/generated/annals_dirichlet_weyl_bound/Solution.lean index d82cab473..f6db61e05 100644 --- a/generated/annals_dirichlet_weyl_bound/Solution.lean +++ b/generated/annals_dirichlet_weyl_bound/Solution.lean @@ -4,6 +4,8 @@ import Submission open DirichletWeylBound open Complex +set_option autoImplicit false + theorem corollary_1_3 (ε : ℝ) (hε : 0 < ε) : ∃ C : ℝ, ∀ q (_hq : q.IsCubeFree) [NeZero q] (χ : DirichletCharacter ℂ q) (_hχ : χ.IsPrimitive) (t : ℝ), ‖χ.LFunction (1 / 2 + I * t)‖ ≤ C * q ^ (1 / 6 + ε) * (1 + |t|) ^ (1 / 6 + ε) := by diff --git a/generated/annals_dirichlet_weyl_bound/Submission.lean b/generated/annals_dirichlet_weyl_bound/Submission.lean index 2c99e0013..bb69f9d4f 100644 --- a/generated/annals_dirichlet_weyl_bound/Submission.lean +++ b/generated/annals_dirichlet_weyl_bound/Submission.lean @@ -4,6 +4,8 @@ import Submission.Helpers open DirichletWeylBound open Complex +set_option autoImplicit false + namespace Submission theorem corollary_1_3 (ε : ℝ) (hε : 0 < ε) : ∃ C : ℝ, diff --git a/generated/annals_equiangular_lines_fixed_angle/Challenge.lean b/generated/annals_equiangular_lines_fixed_angle/Challenge.lean index 2eff1439e..f3d8bf6d7 100644 --- a/generated/annals_equiangular_lines_fixed_angle/Challenge.lean +++ b/generated/annals_equiangular_lines_fixed_angle/Challenge.lean @@ -4,6 +4,8 @@ open EquiangularLinesFixedAngle open Filter open scoped RealInnerProductSpace +set_option autoImplicit false + theorem theorem_1_2 (α : ℝ) (hα : α ∈ Set.Ioo 0 1) : let k := spectralRadiusOrder ((1 - α) / (2 * α)) (k < ⊤ → ∀ᶠ d in atTop, N α d = ⌊(k.toNat * (d - 1) : ℝ) / (k.toNat - 1 : ℝ)⌋₊) ∧ diff --git a/generated/annals_equiangular_lines_fixed_angle/Solution.lean b/generated/annals_equiangular_lines_fixed_angle/Solution.lean index 0327cc562..6a7f742ab 100644 --- a/generated/annals_equiangular_lines_fixed_angle/Solution.lean +++ b/generated/annals_equiangular_lines_fixed_angle/Solution.lean @@ -5,6 +5,8 @@ open EquiangularLinesFixedAngle open Filter open scoped RealInnerProductSpace +set_option autoImplicit false + theorem theorem_1_2 (α : ℝ) (hα : α ∈ Set.Ioo 0 1) : let k := spectralRadiusOrder ((1 - α) / (2 * α)) (k < ⊤ → ∀ᶠ d in atTop, N α d = ⌊(k.toNat * (d - 1) : ℝ) / (k.toNat - 1 : ℝ)⌋₊) ∧ diff --git a/generated/annals_equiangular_lines_fixed_angle/Submission.lean b/generated/annals_equiangular_lines_fixed_angle/Submission.lean index 4b5c22977..69062aa8b 100644 --- a/generated/annals_equiangular_lines_fixed_angle/Submission.lean +++ b/generated/annals_equiangular_lines_fixed_angle/Submission.lean @@ -5,6 +5,8 @@ open EquiangularLinesFixedAngle open Filter open scoped RealInnerProductSpace +set_option autoImplicit false + namespace Submission theorem theorem_1_2 (α : ℝ) (hα : α ∈ Set.Ioo 0 1) : diff --git a/generated/annals_erdos_faber_lovasz_conjecture/Challenge.lean b/generated/annals_erdos_faber_lovasz_conjecture/Challenge.lean index 8a8bb966d..e7ff22a6e 100644 --- a/generated/annals_erdos_faber_lovasz_conjecture/Challenge.lean +++ b/generated/annals_erdos_faber_lovasz_conjecture/Challenge.lean @@ -3,6 +3,7 @@ import ChallengeDeps open ErdosFaberLovaszConjecture open Filter +set_option autoImplicit false variable {V : Type*} theorem theorem_1_1 : diff --git a/generated/annals_erdos_faber_lovasz_conjecture/Solution.lean b/generated/annals_erdos_faber_lovasz_conjecture/Solution.lean index 7904d7ef2..4fbac6d6a 100644 --- a/generated/annals_erdos_faber_lovasz_conjecture/Solution.lean +++ b/generated/annals_erdos_faber_lovasz_conjecture/Solution.lean @@ -4,6 +4,7 @@ import Submission open ErdosFaberLovaszConjecture open Filter +set_option autoImplicit false variable {V : Type*} theorem theorem_1_1 : diff --git a/generated/annals_erdos_faber_lovasz_conjecture/Submission.lean b/generated/annals_erdos_faber_lovasz_conjecture/Submission.lean index 1f3d0e05b..f25f6b49d 100644 --- a/generated/annals_erdos_faber_lovasz_conjecture/Submission.lean +++ b/generated/annals_erdos_faber_lovasz_conjecture/Submission.lean @@ -4,6 +4,7 @@ import Submission.Helpers open ErdosFaberLovaszConjecture open Filter +set_option autoImplicit false variable {V : Type*} namespace Submission diff --git a/generated/annals_finite_time_singularity/Challenge.lean b/generated/annals_finite_time_singularity/Challenge.lean index 72ad4feaf..afaaac343 100644 --- a/generated/annals_finite_time_singularity/Challenge.lean +++ b/generated/annals_finite_time_singularity/Challenge.lean @@ -3,6 +3,7 @@ import ChallengeDeps open FiniteTimeSingularity open Set Gradient Matrix Filter Topology +set_option autoImplicit false local notation "ℝ³" => EuclideanSpace ℝ (Fin 3) local notation u "·∇ₓ" v => directionalDeriv v u local notation "∂ₜ" u => timeDeriv u diff --git a/generated/annals_finite_time_singularity/Solution.lean b/generated/annals_finite_time_singularity/Solution.lean index 607b0179b..a3bad2f85 100644 --- a/generated/annals_finite_time_singularity/Solution.lean +++ b/generated/annals_finite_time_singularity/Solution.lean @@ -4,6 +4,7 @@ import Submission open FiniteTimeSingularity open Set Gradient Matrix Filter Topology +set_option autoImplicit false local notation "ℝ³" => EuclideanSpace ℝ (Fin 3) local notation u "·∇ₓ" v => directionalDeriv v u local notation "∂ₜ" u => timeDeriv u diff --git a/generated/annals_finite_time_singularity/Submission.lean b/generated/annals_finite_time_singularity/Submission.lean index 23389d13c..b11e321df 100644 --- a/generated/annals_finite_time_singularity/Submission.lean +++ b/generated/annals_finite_time_singularity/Submission.lean @@ -4,6 +4,7 @@ import Submission.Helpers open FiniteTimeSingularity open Set Gradient Matrix Filter Topology +set_option autoImplicit false local notation "ℝ³" => EuclideanSpace ℝ (Fin 3) local notation u "·∇ₓ" v => directionalDeriv v u local notation "∂ₜ" u => timeDeriv u diff --git a/generated/annals_flat_littlewood_poly/Challenge.lean b/generated/annals_flat_littlewood_poly/Challenge.lean index 02e931d47..cbec98a2b 100644 --- a/generated/annals_flat_littlewood_poly/Challenge.lean +++ b/generated/annals_flat_littlewood_poly/Challenge.lean @@ -3,6 +3,8 @@ import ChallengeDeps open FlatLittlewoodPoly open scoped Polynomial +set_option autoImplicit false + theorem theorem_1_1 : ∃ Δ δ : ℝ, Δ > δ ∧ δ > 0 ∧ ∀ n ≥ 2, ∃ P : ℂ[X], IsLittlewoodPolynomial P ∧ P.natDegree = n ∧ diff --git a/generated/annals_flat_littlewood_poly/Solution.lean b/generated/annals_flat_littlewood_poly/Solution.lean index 50c80c833..c698d53da 100644 --- a/generated/annals_flat_littlewood_poly/Solution.lean +++ b/generated/annals_flat_littlewood_poly/Solution.lean @@ -4,6 +4,8 @@ import Submission open FlatLittlewoodPoly open scoped Polynomial +set_option autoImplicit false + theorem theorem_1_1 : ∃ Δ δ : ℝ, Δ > δ ∧ δ > 0 ∧ ∀ n ≥ 2, ∃ P : ℂ[X], IsLittlewoodPolynomial P ∧ P.natDegree = n ∧ diff --git a/generated/annals_flat_littlewood_poly/Submission.lean b/generated/annals_flat_littlewood_poly/Submission.lean index 5cffe891d..9ff6d1390 100644 --- a/generated/annals_flat_littlewood_poly/Submission.lean +++ b/generated/annals_flat_littlewood_poly/Submission.lean @@ -4,6 +4,8 @@ import Submission.Helpers open FlatLittlewoodPoly open scoped Polynomial +set_option autoImplicit false + namespace Submission theorem theorem_1_1 : diff --git a/generated/annals_fractal_uncertainty/Challenge.lean b/generated/annals_fractal_uncertainty/Challenge.lean index 8c78d234f..5f48c75da 100644 --- a/generated/annals_fractal_uncertainty/Challenge.lean +++ b/generated/annals_fractal_uncertainty/Challenge.lean @@ -4,6 +4,7 @@ open FractalUncertainty open MeasureTheory FourierTransform Metric open scoped ENNReal +set_option autoImplicit false variable {d : ℕ} local notation "ℝᵈ" => EuclideanSpace ℝ (Fin d) diff --git a/generated/annals_fractal_uncertainty/Solution.lean b/generated/annals_fractal_uncertainty/Solution.lean index db0bcdee6..9462264c3 100644 --- a/generated/annals_fractal_uncertainty/Solution.lean +++ b/generated/annals_fractal_uncertainty/Solution.lean @@ -5,6 +5,7 @@ open FractalUncertainty open MeasureTheory FourierTransform Metric open scoped ENNReal +set_option autoImplicit false variable {d : ℕ} local notation "ℝᵈ" => EuclideanSpace ℝ (Fin d) diff --git a/generated/annals_fractal_uncertainty/Submission.lean b/generated/annals_fractal_uncertainty/Submission.lean index 2733e73cc..0e46474e4 100644 --- a/generated/annals_fractal_uncertainty/Submission.lean +++ b/generated/annals_fractal_uncertainty/Submission.lean @@ -5,6 +5,7 @@ open FractalUncertainty open MeasureTheory FourierTransform Metric open scoped ENNReal +set_option autoImplicit false variable {d : ℕ} local notation "ℝᵈ" => EuclideanSpace ℝ (Fin d) diff --git a/generated/annals_good_lt_codes/Challenge.lean b/generated/annals_good_lt_codes/Challenge.lean index d86eba158..ca666b6d4 100644 --- a/generated/annals_good_lt_codes/Challenge.lean +++ b/generated/annals_good_lt_codes/Challenge.lean @@ -3,6 +3,7 @@ import ChallengeDeps open GoodLTC open NNReal +set_option autoImplicit false variable (n : ℕ) local notation "𝔽₂ⁿ" => Fin n → ZMod 2 variable {n} (C : BinaryCode n) diff --git a/generated/annals_good_lt_codes/Solution.lean b/generated/annals_good_lt_codes/Solution.lean index 7b7ab5e6b..60f134b0c 100644 --- a/generated/annals_good_lt_codes/Solution.lean +++ b/generated/annals_good_lt_codes/Solution.lean @@ -4,6 +4,7 @@ import Submission open GoodLTC open NNReal +set_option autoImplicit false variable (n : ℕ) local notation "𝔽₂ⁿ" => Fin n → ZMod 2 variable {n} (C : BinaryCode n) diff --git a/generated/annals_good_lt_codes/Submission.lean b/generated/annals_good_lt_codes/Submission.lean index 234fbd97b..f4560ad89 100644 --- a/generated/annals_good_lt_codes/Submission.lean +++ b/generated/annals_good_lt_codes/Submission.lean @@ -4,6 +4,7 @@ import Submission.Helpers open GoodLTC open NNReal +set_option autoImplicit false variable (n : ℕ) local notation "𝔽₂ⁿ" => Fin n → ZMod 2 variable {n} (C : BinaryCode n) diff --git a/generated/annals_hasse_principle_random_fano/Challenge.lean b/generated/annals_hasse_principle_random_fano/Challenge.lean index beb16ae24..b6e3cdaf9 100644 --- a/generated/annals_hasse_principle_random_fano/Challenge.lean +++ b/generated/annals_hasse_principle_random_fano/Challenge.lean @@ -4,6 +4,7 @@ open HassePrincipleRandomFano open MvPolynomial Filter NumberField Real open scoped LinearAlgebra.Projectivization +set_option autoImplicit false variable (d n : ℕ) theorem theorem_1_1 (hd : 2 ≤ d) (h₁ : d ≤ n) (h₂ : (d, n) ≠ (3, 3)) : diff --git a/generated/annals_hasse_principle_random_fano/Solution.lean b/generated/annals_hasse_principle_random_fano/Solution.lean index 7f73ea3a6..16bef67b7 100644 --- a/generated/annals_hasse_principle_random_fano/Solution.lean +++ b/generated/annals_hasse_principle_random_fano/Solution.lean @@ -5,6 +5,7 @@ open HassePrincipleRandomFano open MvPolynomial Filter NumberField Real open scoped LinearAlgebra.Projectivization +set_option autoImplicit false variable (d n : ℕ) theorem theorem_1_1 (hd : 2 ≤ d) (h₁ : d ≤ n) (h₂ : (d, n) ≠ (3, 3)) : diff --git a/generated/annals_hasse_principle_random_fano/Submission.lean b/generated/annals_hasse_principle_random_fano/Submission.lean index 9a92ee6f3..5fe4d9412 100644 --- a/generated/annals_hasse_principle_random_fano/Submission.lean +++ b/generated/annals_hasse_principle_random_fano/Submission.lean @@ -5,6 +5,7 @@ open HassePrincipleRandomFano open MvPolynomial Filter NumberField Real open scoped LinearAlgebra.Projectivization +set_option autoImplicit false variable (d n : ℕ) namespace Submission diff --git a/generated/annals_hessian_estimates/Challenge.lean b/generated/annals_hessian_estimates/Challenge.lean index b7f4315f9..2c206d68c 100644 --- a/generated/annals_hessian_estimates/Challenge.lean +++ b/generated/annals_hessian_estimates/Challenge.lean @@ -3,6 +3,7 @@ import ChallengeDeps open HessianEstimates open Laplacian Metric ContDiff MeasureTheory ENNReal +set_option autoImplicit false local notation "‖" f "‖_C¹(" s ")" => eC1NormOn f s volume local notation "‖" T "‖_F" => frobeniusNorm T local notation "ℝ⁴" => EuclideanSpace ℝ (Fin 4) diff --git a/generated/annals_hessian_estimates/Solution.lean b/generated/annals_hessian_estimates/Solution.lean index e0d69e4ed..ee8777d76 100644 --- a/generated/annals_hessian_estimates/Solution.lean +++ b/generated/annals_hessian_estimates/Solution.lean @@ -4,6 +4,7 @@ import Submission open HessianEstimates open Laplacian Metric ContDiff MeasureTheory ENNReal +set_option autoImplicit false local notation "‖" f "‖_C¹(" s ")" => eC1NormOn f s volume local notation "‖" T "‖_F" => frobeniusNorm T local notation "ℝ⁴" => EuclideanSpace ℝ (Fin 4) diff --git a/generated/annals_hessian_estimates/Submission.lean b/generated/annals_hessian_estimates/Submission.lean index 77dc0ce86..af554feb2 100644 --- a/generated/annals_hessian_estimates/Submission.lean +++ b/generated/annals_hessian_estimates/Submission.lean @@ -4,6 +4,7 @@ import Submission.Helpers open HessianEstimates open Laplacian Metric ContDiff MeasureTheory ENNReal +set_option autoImplicit false local notation "‖" f "‖_C¹(" s ")" => eC1NormOn f s volume local notation "‖" T "‖_F" => frobeniusNorm T local notation "ℝ⁴" => EuclideanSpace ℝ (Fin 4) diff --git a/generated/annals_inscribed_rectangles/Challenge.lean b/generated/annals_inscribed_rectangles/Challenge.lean index 4dfe77c99..6c9162ac9 100644 --- a/generated/annals_inscribed_rectangles/Challenge.lean +++ b/generated/annals_inscribed_rectangles/Challenge.lean @@ -4,6 +4,8 @@ open InscribedRectangles open Manifold Real MeasureTheory open scoped ContDiff +set_option autoImplicit false + theorem theorem_1 (γ : Circle → ℝ × ℝ) (hγ : IsSmoothEmbedding (𝓡 1) 𝓘(ℝ, ℝ × ℝ) ∞ γ) : volume (X γ) ≥ 1/3 := by sorry diff --git a/generated/annals_inscribed_rectangles/Solution.lean b/generated/annals_inscribed_rectangles/Solution.lean index 20b613251..5d2160076 100644 --- a/generated/annals_inscribed_rectangles/Solution.lean +++ b/generated/annals_inscribed_rectangles/Solution.lean @@ -5,6 +5,8 @@ open InscribedRectangles open Manifold Real MeasureTheory open scoped ContDiff +set_option autoImplicit false + theorem theorem_1 (γ : Circle → ℝ × ℝ) (hγ : IsSmoothEmbedding (𝓡 1) 𝓘(ℝ, ℝ × ℝ) ∞ γ) : volume (X γ) ≥ 1/3 := by exact Submission.theorem_1 γ hγ diff --git a/generated/annals_inscribed_rectangles/Submission.lean b/generated/annals_inscribed_rectangles/Submission.lean index 0822e4c1d..42c93800e 100644 --- a/generated/annals_inscribed_rectangles/Submission.lean +++ b/generated/annals_inscribed_rectangles/Submission.lean @@ -5,6 +5,8 @@ open InscribedRectangles open Manifold Real MeasureTheory open scoped ContDiff +set_option autoImplicit false + namespace Submission theorem theorem_1 (γ : Circle → ℝ × ℝ) (hγ : IsSmoothEmbedding (𝓡 1) 𝓘(ℝ, ℝ × ℝ) ∞ γ) : diff --git a/generated/annals_integer_multiplication/Challenge.lean b/generated/annals_integer_multiplication/Challenge.lean index c40a53a87..06a873ae0 100644 --- a/generated/annals_integer_multiplication/Challenge.lean +++ b/generated/annals_integer_multiplication/Challenge.lean @@ -3,6 +3,8 @@ import ChallengeDeps open IntegerMultiplication open Computability Turing Real +set_option autoImplicit false + theorem theorem_1_1 : ∃ T : TM2ComputableInTime (encodeProd encodeNat encodeNat) encodeNat (fun (x, y) ↦ x * y), (fun n ↦ (T.time n : ℝ)) =O[Filter.atTop] (fun n ↦ n * log n) := by diff --git a/generated/annals_integer_multiplication/Solution.lean b/generated/annals_integer_multiplication/Solution.lean index cca2606c3..bbbba8529 100644 --- a/generated/annals_integer_multiplication/Solution.lean +++ b/generated/annals_integer_multiplication/Solution.lean @@ -4,6 +4,8 @@ import Submission open IntegerMultiplication open Computability Turing Real +set_option autoImplicit false + theorem theorem_1_1 : ∃ T : TM2ComputableInTime (encodeProd encodeNat encodeNat) encodeNat (fun (x, y) ↦ x * y), (fun n ↦ (T.time n : ℝ)) =O[Filter.atTop] (fun n ↦ n * log n) := by diff --git a/generated/annals_integer_multiplication/Submission.lean b/generated/annals_integer_multiplication/Submission.lean index 77eb20006..c49e9f73c 100644 --- a/generated/annals_integer_multiplication/Submission.lean +++ b/generated/annals_integer_multiplication/Submission.lean @@ -4,6 +4,8 @@ import Submission.Helpers open IntegerMultiplication open Computability Turing Real +set_option autoImplicit false + namespace Submission theorem theorem_1_1 : diff --git a/generated/annals_large_value_estimates/Challenge.lean b/generated/annals_large_value_estimates/Challenge.lean index 2668ec0a8..cd8418152 100644 --- a/generated/annals_large_value_estimates/Challenge.lean +++ b/generated/annals_large_value_estimates/Challenge.lean @@ -3,6 +3,8 @@ import ChallengeDeps open LargeValueEstimates open Asymptotics Complex +set_option autoImplicit false + theorem theorem_1_1 : ∃ o : ℝ → ℝ, o =o[Filter.atTop] (1 : ℝ → ℝ) ∧ ∀ (b : ℕ → ℂ) (_hb : ∀ n, ‖b n‖ ≤ 1) (N : ℕ) (V : ℝ) (T : ℝ) (R : ℕ) (t : Fin R → ℝ), N > 0 → V > 0 → T > 1 → -- these assumptions are necessary but not stated in the paper diff --git a/generated/annals_large_value_estimates/Solution.lean b/generated/annals_large_value_estimates/Solution.lean index 441388348..30389a436 100644 --- a/generated/annals_large_value_estimates/Solution.lean +++ b/generated/annals_large_value_estimates/Solution.lean @@ -4,6 +4,8 @@ import Submission open LargeValueEstimates open Asymptotics Complex +set_option autoImplicit false + theorem theorem_1_1 : ∃ o : ℝ → ℝ, o =o[Filter.atTop] (1 : ℝ → ℝ) ∧ ∀ (b : ℕ → ℂ) (_hb : ∀ n, ‖b n‖ ≤ 1) (N : ℕ) (V : ℝ) (T : ℝ) (R : ℕ) (t : Fin R → ℝ), N > 0 → V > 0 → T > 1 → -- these assumptions are necessary but not stated in the paper diff --git a/generated/annals_large_value_estimates/Submission.lean b/generated/annals_large_value_estimates/Submission.lean index 93cb0ed31..dda4ce147 100644 --- a/generated/annals_large_value_estimates/Submission.lean +++ b/generated/annals_large_value_estimates/Submission.lean @@ -4,6 +4,8 @@ import Submission.Helpers open LargeValueEstimates open Asymptotics Complex +set_option autoImplicit false + namespace Submission theorem theorem_1_1 : ∃ o : ℝ → ℝ, o =o[Filter.atTop] (1 : ℝ → ℝ) ∧ diff --git a/generated/annals_linear_subspaces/Challenge.lean b/generated/annals_linear_subspaces/Challenge.lean index 823e550c5..f1efdd254 100644 --- a/generated/annals_linear_subspaces/Challenge.lean +++ b/generated/annals_linear_subspaces/Challenge.lean @@ -4,6 +4,7 @@ open LinearSubspaces open ENNReal Real Module exteriorPower InnerProductGeometry open scoped LinearAlgebra.Projectivization +set_option autoImplicit false variable {d : ℕ} local notation "ℝᵈ" => EuclideanSpace ℝ (Fin d) local notation "ℤᵈ" => intPoints diff --git a/generated/annals_linear_subspaces/Solution.lean b/generated/annals_linear_subspaces/Solution.lean index ecf712396..c2cbf9d18 100644 --- a/generated/annals_linear_subspaces/Solution.lean +++ b/generated/annals_linear_subspaces/Solution.lean @@ -5,6 +5,7 @@ open LinearSubspaces open ENNReal Real Module exteriorPower InnerProductGeometry open scoped LinearAlgebra.Projectivization +set_option autoImplicit false variable {d : ℕ} local notation "ℝᵈ" => EuclideanSpace ℝ (Fin d) local notation "ℤᵈ" => intPoints diff --git a/generated/annals_linear_subspaces/Submission.lean b/generated/annals_linear_subspaces/Submission.lean index b50e786a1..44869e037 100644 --- a/generated/annals_linear_subspaces/Submission.lean +++ b/generated/annals_linear_subspaces/Submission.lean @@ -5,6 +5,7 @@ open LinearSubspaces open ENNReal Real Module exteriorPower InnerProductGeometry open scoped LinearAlgebra.Projectivization +set_option autoImplicit false variable {d : ℕ} local notation "ℝᵈ" => EuclideanSpace ℝ (Fin d) local notation "ℤᵈ" => intPoints diff --git a/generated/annals_lorentzian_polynomials/Challenge.lean b/generated/annals_lorentzian_polynomials/Challenge.lean index 4575259d4..3e4436197 100644 --- a/generated/annals_lorentzian_polynomials/Challenge.lean +++ b/generated/annals_lorentzian_polynomials/Challenge.lean @@ -3,5 +3,7 @@ import ChallengeDeps open LorentzianPolynomials open Finsupp Matrix MvPolynomial UpperHalfPlane +set_option autoImplicit false + theorem theorem_2_25 (n d : ℕ) (hn : 0 < n) : closure (Ŀ n d) = L n d := by sorry diff --git a/generated/annals_lorentzian_polynomials/Solution.lean b/generated/annals_lorentzian_polynomials/Solution.lean index d45ac5164..dd456d538 100644 --- a/generated/annals_lorentzian_polynomials/Solution.lean +++ b/generated/annals_lorentzian_polynomials/Solution.lean @@ -4,5 +4,7 @@ import Submission open LorentzianPolynomials open Finsupp Matrix MvPolynomial UpperHalfPlane +set_option autoImplicit false + theorem theorem_2_25 (n d : ℕ) (hn : 0 < n) : closure (Ŀ n d) = L n d := by exact Submission.theorem_2_25 n d hn diff --git a/generated/annals_lorentzian_polynomials/Submission.lean b/generated/annals_lorentzian_polynomials/Submission.lean index b1fbae31d..931bb5b0b 100644 --- a/generated/annals_lorentzian_polynomials/Submission.lean +++ b/generated/annals_lorentzian_polynomials/Submission.lean @@ -4,6 +4,8 @@ import Submission.Helpers open LorentzianPolynomials open Finsupp Matrix MvPolynomial UpperHalfPlane +set_option autoImplicit false + namespace Submission theorem theorem_2_25 (n d : ℕ) (hn : 0 < n) : closure (Ŀ n d) = L n d := by diff --git a/generated/annals_mckay_conjecture/Challenge.lean b/generated/annals_mckay_conjecture/Challenge.lean index 66a90c0ec..2de795d60 100644 --- a/generated/annals_mckay_conjecture/Challenge.lean +++ b/generated/annals_mckay_conjecture/Challenge.lean @@ -3,6 +3,7 @@ import ChallengeDeps open McKayConjecture open CategoryTheory Module Subgroup +set_option autoImplicit false variable (ℓ : ℕ) (X : Type*) [Group X] [Finite X] theorem theorem_1_1 (hℓ : ℓ.Prime) (S : Sylow ℓ X) : diff --git a/generated/annals_mckay_conjecture/Solution.lean b/generated/annals_mckay_conjecture/Solution.lean index 03850eef2..3f54f247a 100644 --- a/generated/annals_mckay_conjecture/Solution.lean +++ b/generated/annals_mckay_conjecture/Solution.lean @@ -4,6 +4,7 @@ import Submission open McKayConjecture open CategoryTheory Module Subgroup +set_option autoImplicit false variable (ℓ : ℕ) (X : Type*) [Group X] [Finite X] theorem theorem_1_1 (hℓ : ℓ.Prime) (S : Sylow ℓ X) : diff --git a/generated/annals_mckay_conjecture/Submission.lean b/generated/annals_mckay_conjecture/Submission.lean index ff1a16f96..9d60c7e54 100644 --- a/generated/annals_mckay_conjecture/Submission.lean +++ b/generated/annals_mckay_conjecture/Submission.lean @@ -4,6 +4,7 @@ import Submission.Helpers open McKayConjecture open CategoryTheory Module Subgroup +set_option autoImplicit false variable (ℓ : ℕ) (X : Type*) [Group X] [Finite X] namespace Submission diff --git a/generated/annals_on_approximation_of_reals/Challenge.lean b/generated/annals_on_approximation_of_reals/Challenge.lean index 255cd98b2..881fd86af 100644 --- a/generated/annals_on_approximation_of_reals/Challenge.lean +++ b/generated/annals_on_approximation_of_reals/Challenge.lean @@ -3,6 +3,8 @@ import ChallengeDeps open OnApproximationOfReals open NNReal ENNReal +set_option autoImplicit false + theorem theorem_1_1 (n : ℕ) (hn : n ≥ 2) (ξ : ℝ) (hξ : Transcendental ℚ ξ) : letI a : ℝ := 1 / (2 - Real.log 2) (ω⋆ n ξ : EReal) ≥ (a : EReal) * n := by diff --git a/generated/annals_on_approximation_of_reals/Solution.lean b/generated/annals_on_approximation_of_reals/Solution.lean index 1da024dad..131fe277c 100644 --- a/generated/annals_on_approximation_of_reals/Solution.lean +++ b/generated/annals_on_approximation_of_reals/Solution.lean @@ -4,6 +4,8 @@ import Submission open OnApproximationOfReals open NNReal ENNReal +set_option autoImplicit false + theorem theorem_1_1 (n : ℕ) (hn : n ≥ 2) (ξ : ℝ) (hξ : Transcendental ℚ ξ) : letI a : ℝ := 1 / (2 - Real.log 2) (ω⋆ n ξ : EReal) ≥ (a : EReal) * n := by diff --git a/generated/annals_on_approximation_of_reals/Submission.lean b/generated/annals_on_approximation_of_reals/Submission.lean index 85cf3c30d..113eb9bb7 100644 --- a/generated/annals_on_approximation_of_reals/Submission.lean +++ b/generated/annals_on_approximation_of_reals/Submission.lean @@ -4,6 +4,8 @@ import Submission.Helpers open OnApproximationOfReals open NNReal ENNReal +set_option autoImplicit false + namespace Submission theorem theorem_1_1 (n : ℕ) (hn : n ≥ 2) (ξ : ℝ) (hξ : Transcendental ℚ ξ) : diff --git a/generated/annals_on_coherence_of_one_relator_groups/Challenge.lean b/generated/annals_on_coherence_of_one_relator_groups/Challenge.lean index a18442816..453b44ba0 100644 --- a/generated/annals_on_coherence_of_one_relator_groups/Challenge.lean +++ b/generated/annals_on_coherence_of_one_relator_groups/Challenge.lean @@ -2,6 +2,8 @@ import ChallengeDeps open OnCoherenceOfOneRelatorGroups +set_option autoImplicit false + theorem theorem_1_1 (G K : Type*) [Group G] [Field K] [CharZero K] (hG : Group.OneRelator G) : Group.Coherent G ∧ Ring.Coherent (MonoidAlgebra K G) := by sorry diff --git a/generated/annals_on_coherence_of_one_relator_groups/Solution.lean b/generated/annals_on_coherence_of_one_relator_groups/Solution.lean index d24e253d7..3ac5a860a 100644 --- a/generated/annals_on_coherence_of_one_relator_groups/Solution.lean +++ b/generated/annals_on_coherence_of_one_relator_groups/Solution.lean @@ -3,6 +3,8 @@ import Submission open OnCoherenceOfOneRelatorGroups +set_option autoImplicit false + theorem theorem_1_1 (G K : Type*) [Group G] [Field K] [CharZero K] (hG : Group.OneRelator G) : Group.Coherent G ∧ Ring.Coherent (MonoidAlgebra K G) := by exact Submission.theorem_1_1 G K hG diff --git a/generated/annals_on_coherence_of_one_relator_groups/Submission.lean b/generated/annals_on_coherence_of_one_relator_groups/Submission.lean index e50ca32f6..3a420590f 100644 --- a/generated/annals_on_coherence_of_one_relator_groups/Submission.lean +++ b/generated/annals_on_coherence_of_one_relator_groups/Submission.lean @@ -3,6 +3,8 @@ import Submission.Helpers open OnCoherenceOfOneRelatorGroups +set_option autoImplicit false + namespace Submission theorem theorem_1_1 (G K : Type*) [Group G] [Field K] [CharZero K] (hG : Group.OneRelator G) : diff --git a/generated/annals_on_property_t/Challenge.lean b/generated/annals_on_property_t/Challenge.lean index a89622b9b..d4518ace3 100644 --- a/generated/annals_on_property_t/Challenge.lean +++ b/generated/annals_on_property_t/Challenge.lean @@ -2,5 +2,7 @@ import ChallengeDeps open OnPropertyT +set_option autoImplicit false + theorem theorem_1 (n : ℕ) (hn : n ≥ 6) : PropertyT (MulAut (FreeGroup (Fin n))) := by sorry diff --git a/generated/annals_on_property_t/Solution.lean b/generated/annals_on_property_t/Solution.lean index aa55207cd..8130416c6 100644 --- a/generated/annals_on_property_t/Solution.lean +++ b/generated/annals_on_property_t/Solution.lean @@ -3,5 +3,7 @@ import Submission open OnPropertyT +set_option autoImplicit false + theorem theorem_1 (n : ℕ) (hn : n ≥ 6) : PropertyT (MulAut (FreeGroup (Fin n))) := by exact Submission.theorem_1 n hn diff --git a/generated/annals_on_property_t/Submission.lean b/generated/annals_on_property_t/Submission.lean index 66b17be11..85d5b7b4e 100644 --- a/generated/annals_on_property_t/Submission.lean +++ b/generated/annals_on_property_t/Submission.lean @@ -3,6 +3,8 @@ import Submission.Helpers open OnPropertyT +set_option autoImplicit false + namespace Submission theorem theorem_1 (n : ℕ) (hn : n ≥ 6) : PropertyT (MulAut (FreeGroup (Fin n))) := by diff --git a/generated/annals_optimal_moebius/Challenge.lean b/generated/annals_optimal_moebius/Challenge.lean index b08a40557..9d8055899 100644 --- a/generated/annals_optimal_moebius/Challenge.lean +++ b/generated/annals_optimal_moebius/Challenge.lean @@ -3,6 +3,7 @@ import ChallengeDeps open OptimalMoebius open Topology ContDiff +set_option autoImplicit false local notation "ℝ²" => EuclideanSpace ℝ (Fin 2) local notation "ℝ³" => EuclideanSpace ℝ (Fin 3) diff --git a/generated/annals_optimal_moebius/Solution.lean b/generated/annals_optimal_moebius/Solution.lean index 4e3c11214..84700006c 100644 --- a/generated/annals_optimal_moebius/Solution.lean +++ b/generated/annals_optimal_moebius/Solution.lean @@ -4,6 +4,7 @@ import Submission open OptimalMoebius open Topology ContDiff +set_option autoImplicit false local notation "ℝ²" => EuclideanSpace ℝ (Fin 2) local notation "ℝ³" => EuclideanSpace ℝ (Fin 3) diff --git a/generated/annals_optimal_moebius/Submission.lean b/generated/annals_optimal_moebius/Submission.lean index 9c7169477..700d0831d 100644 --- a/generated/annals_optimal_moebius/Submission.lean +++ b/generated/annals_optimal_moebius/Submission.lean @@ -4,6 +4,7 @@ import Submission.Helpers open OptimalMoebius open Topology ContDiff +set_option autoImplicit false local notation "ℝ²" => EuclideanSpace ℝ (Fin 2) local notation "ℝ³" => EuclideanSpace ℝ (Fin 3) diff --git a/generated/annals_pseudorandom_grassmann/Challenge.lean b/generated/annals_pseudorandom_grassmann/Challenge.lean index 5238239b4..b8a23b19d 100644 --- a/generated/annals_pseudorandom_grassmann/Challenge.lean +++ b/generated/annals_pseudorandom_grassmann/Challenge.lean @@ -3,6 +3,7 @@ import ChallengeDeps open PseudorandomGrassmann open Module Finset Filter +set_option autoImplicit false local notation "𝔽₂" => ZMod 2 open Classical in diff --git a/generated/annals_pseudorandom_grassmann/Solution.lean b/generated/annals_pseudorandom_grassmann/Solution.lean index d536d79ae..5623f7135 100644 --- a/generated/annals_pseudorandom_grassmann/Solution.lean +++ b/generated/annals_pseudorandom_grassmann/Solution.lean @@ -4,6 +4,7 @@ import Submission open PseudorandomGrassmann open Module Finset Filter +set_option autoImplicit false local notation "𝔽₂" => ZMod 2 open Classical in diff --git a/generated/annals_pseudorandom_grassmann/Submission.lean b/generated/annals_pseudorandom_grassmann/Submission.lean index 979629cbd..b0fa90e44 100644 --- a/generated/annals_pseudorandom_grassmann/Submission.lean +++ b/generated/annals_pseudorandom_grassmann/Submission.lean @@ -4,6 +4,7 @@ import Submission.Helpers open PseudorandomGrassmann open Module Finset Filter +set_option autoImplicit false local notation "𝔽₂" => ZMod 2 namespace Submission diff --git a/generated/annals_rademacher_enflo_type/Challenge.lean b/generated/annals_rademacher_enflo_type/Challenge.lean index 3b25d1f5b..440d385d7 100644 --- a/generated/annals_rademacher_enflo_type/Challenge.lean +++ b/generated/annals_rademacher_enflo_type/Challenge.lean @@ -4,6 +4,7 @@ open RademacherEnfloType open Function MeasureTheory ProbabilityTheory Measure NNReal open scoped ENNReal +set_option autoImplicit false variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] variable (X : Type*) [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] diff --git a/generated/annals_rademacher_enflo_type/Solution.lean b/generated/annals_rademacher_enflo_type/Solution.lean index 372880fb7..b0a2d52da 100644 --- a/generated/annals_rademacher_enflo_type/Solution.lean +++ b/generated/annals_rademacher_enflo_type/Solution.lean @@ -5,6 +5,7 @@ open RademacherEnfloType open Function MeasureTheory ProbabilityTheory Measure NNReal open scoped ENNReal +set_option autoImplicit false variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] variable (X : Type*) [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] diff --git a/generated/annals_rademacher_enflo_type/Submission.lean b/generated/annals_rademacher_enflo_type/Submission.lean index fb52eabb8..19dd91712 100644 --- a/generated/annals_rademacher_enflo_type/Submission.lean +++ b/generated/annals_rademacher_enflo_type/Submission.lean @@ -5,6 +5,7 @@ open RademacherEnfloType open Function MeasureTheory ProbabilityTheory Measure NNReal open scoped ENNReal +set_option autoImplicit false variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] variable (X : Type*) [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] diff --git a/generated/annals_rectangular_peg_problem/Challenge.lean b/generated/annals_rectangular_peg_problem/Challenge.lean index e5ec2e595..fa18b4975 100644 --- a/generated/annals_rectangular_peg_problem/Challenge.lean +++ b/generated/annals_rectangular_peg_problem/Challenge.lean @@ -4,6 +4,8 @@ open RectangularPegProblem open Manifold Complex Real open scoped ContDiff +set_option autoImplicit false + theorem theorem_1 (γ : Circle → ℂ) (z w : ℂ) (θ : Real.Angle) (hγ : IsSmoothEmbedding (𝓡 1) 𝓘(ℝ, ℂ) ∞ γ) : ∃ (θ' : Real.Angle), ∃ (z' w' : ℂ), Similar (R z w θ) (R z' w' θ') ∧ diff --git a/generated/annals_rectangular_peg_problem/Solution.lean b/generated/annals_rectangular_peg_problem/Solution.lean index 3ddf53320..58bc84799 100644 --- a/generated/annals_rectangular_peg_problem/Solution.lean +++ b/generated/annals_rectangular_peg_problem/Solution.lean @@ -5,6 +5,8 @@ open RectangularPegProblem open Manifold Complex Real open scoped ContDiff +set_option autoImplicit false + theorem theorem_1 (γ : Circle → ℂ) (z w : ℂ) (θ : Real.Angle) (hγ : IsSmoothEmbedding (𝓡 1) 𝓘(ℝ, ℂ) ∞ γ) : ∃ (θ' : Real.Angle), ∃ (z' w' : ℂ), Similar (R z w θ) (R z' w' θ') ∧ diff --git a/generated/annals_rectangular_peg_problem/Submission.lean b/generated/annals_rectangular_peg_problem/Submission.lean index 983953f08..e03af1628 100644 --- a/generated/annals_rectangular_peg_problem/Submission.lean +++ b/generated/annals_rectangular_peg_problem/Submission.lean @@ -5,6 +5,8 @@ open RectangularPegProblem open Manifold Complex Real open scoped ContDiff +set_option autoImplicit false + namespace Submission theorem theorem_1 (γ : Circle → ℂ) (z w : ℂ) (θ : Real.Angle) diff --git a/generated/annals_reverse_minkowski/Challenge.lean b/generated/annals_reverse_minkowski/Challenge.lean index 612a28fc6..c1e77a03a 100644 --- a/generated/annals_reverse_minkowski/Challenge.lean +++ b/generated/annals_reverse_minkowski/Challenge.lean @@ -3,6 +3,7 @@ import ChallengeDeps open ReverseMinkowski open Module Real Matrix +set_option autoImplicit false variable {n : ℕ} local notation "ℝⁿ" => EuclideanSpace ℝ (Fin n) diff --git a/generated/annals_reverse_minkowski/Solution.lean b/generated/annals_reverse_minkowski/Solution.lean index e654a758d..8a46dc689 100644 --- a/generated/annals_reverse_minkowski/Solution.lean +++ b/generated/annals_reverse_minkowski/Solution.lean @@ -4,6 +4,7 @@ import Submission open ReverseMinkowski open Module Real Matrix +set_option autoImplicit false variable {n : ℕ} local notation "ℝⁿ" => EuclideanSpace ℝ (Fin n) diff --git a/generated/annals_reverse_minkowski/Submission.lean b/generated/annals_reverse_minkowski/Submission.lean index aa1682fb9..a27bfc55e 100644 --- a/generated/annals_reverse_minkowski/Submission.lean +++ b/generated/annals_reverse_minkowski/Submission.lean @@ -4,6 +4,7 @@ import Submission.Helpers open ReverseMinkowski open Module Real Matrix +set_option autoImplicit false variable {n : ℕ} local notation "ℝⁿ" => EuclideanSpace ℝ (Fin n) diff --git a/generated/annals_simplicity_conjecture/Challenge.lean b/generated/annals_simplicity_conjecture/Challenge.lean index 161202937..b0307ca8e 100644 --- a/generated/annals_simplicity_conjecture/Challenge.lean +++ b/generated/annals_simplicity_conjecture/Challenge.lean @@ -3,5 +3,7 @@ import ChallengeDeps open SimplicityConjecture open Function Homeomorph MeasureTheory +set_option autoImplicit false + theorem theorem_1_2 : ¬ IsSimpleGroup Homeo := by sorry diff --git a/generated/annals_simplicity_conjecture/Solution.lean b/generated/annals_simplicity_conjecture/Solution.lean index f55a0439b..575e73da7 100644 --- a/generated/annals_simplicity_conjecture/Solution.lean +++ b/generated/annals_simplicity_conjecture/Solution.lean @@ -4,5 +4,7 @@ import Submission open SimplicityConjecture open Function Homeomorph MeasureTheory +set_option autoImplicit false + theorem theorem_1_2 : ¬ IsSimpleGroup Homeo := by exact Submission.theorem_1_2 diff --git a/generated/annals_simplicity_conjecture/Submission.lean b/generated/annals_simplicity_conjecture/Submission.lean index 9399da118..ae2e695d1 100644 --- a/generated/annals_simplicity_conjecture/Submission.lean +++ b/generated/annals_simplicity_conjecture/Submission.lean @@ -4,6 +4,8 @@ import Submission.Helpers open SimplicityConjecture open Function Homeomorph MeasureTheory +set_option autoImplicit false + namespace Submission theorem theorem_1_2 : ¬ IsSimpleGroup Homeo := by diff --git a/generated/annals_spread_of_a_finite_group/Challenge.lean b/generated/annals_spread_of_a_finite_group/Challenge.lean index a5c68e0dd..846b3d530 100644 --- a/generated/annals_spread_of_a_finite_group/Challenge.lean +++ b/generated/annals_spread_of_a_finite_group/Challenge.lean @@ -2,6 +2,8 @@ import ChallengeDeps open SpreadOfAFiniteGroup +set_option autoImplicit false + theorem theorem_1 (G : Type*) [Group G] [Finite G] : s G ≥ 2 ↔ ∀ (N : Subgroup G) [N.Normal] [Nontrivial N], IsCyclic (G ⧸ N) := by sorry diff --git a/generated/annals_spread_of_a_finite_group/Solution.lean b/generated/annals_spread_of_a_finite_group/Solution.lean index e77984848..bf85073e7 100644 --- a/generated/annals_spread_of_a_finite_group/Solution.lean +++ b/generated/annals_spread_of_a_finite_group/Solution.lean @@ -3,6 +3,8 @@ import Submission open SpreadOfAFiniteGroup +set_option autoImplicit false + theorem theorem_1 (G : Type*) [Group G] [Finite G] : s G ≥ 2 ↔ ∀ (N : Subgroup G) [N.Normal] [Nontrivial N], IsCyclic (G ⧸ N) := by exact Submission.theorem_1 G diff --git a/generated/annals_spread_of_a_finite_group/Submission.lean b/generated/annals_spread_of_a_finite_group/Submission.lean index af37c4806..b95b70e45 100644 --- a/generated/annals_spread_of_a_finite_group/Submission.lean +++ b/generated/annals_spread_of_a_finite_group/Submission.lean @@ -3,6 +3,8 @@ import Submission.Helpers open SpreadOfAFiniteGroup +set_option autoImplicit false + namespace Submission theorem theorem_1 (G : Type*) [Group G] [Finite G] : diff --git a/generated/annals_symplectic_monodromy/Challenge.lean b/generated/annals_symplectic_monodromy/Challenge.lean index 7cebfdb29..7bc135413 100644 --- a/generated/annals_symplectic_monodromy/Challenge.lean +++ b/generated/annals_symplectic_monodromy/Challenge.lean @@ -3,6 +3,8 @@ import ChallengeDeps open SymplecticMonodromy open MvPowerSeries +set_option autoImplicit false + theorem theorem_1_1 (n : ℕ) (f : unitInterval → MvPowerSeries (Fin n) ℂ) (cont : ∀ d, Continuous fun t ↦ coeff d (f t)) (h_const : ∀ t, constantCoeff (f t) = 0) (h : ∃ μ : ℕ, ∀ t, milnorNumber (f t) = μ) : ∀ t₁ t₂, (f t₁).order = (f t₂).order := by diff --git a/generated/annals_symplectic_monodromy/Solution.lean b/generated/annals_symplectic_monodromy/Solution.lean index 8fbdde2a6..9d662c18e 100644 --- a/generated/annals_symplectic_monodromy/Solution.lean +++ b/generated/annals_symplectic_monodromy/Solution.lean @@ -4,6 +4,8 @@ import Submission open SymplecticMonodromy open MvPowerSeries +set_option autoImplicit false + theorem theorem_1_1 (n : ℕ) (f : unitInterval → MvPowerSeries (Fin n) ℂ) (cont : ∀ d, Continuous fun t ↦ coeff d (f t)) (h_const : ∀ t, constantCoeff (f t) = 0) (h : ∃ μ : ℕ, ∀ t, milnorNumber (f t) = μ) : ∀ t₁ t₂, (f t₁).order = (f t₂).order := by diff --git a/generated/annals_symplectic_monodromy/Submission.lean b/generated/annals_symplectic_monodromy/Submission.lean index e845ab94b..b6a89af36 100644 --- a/generated/annals_symplectic_monodromy/Submission.lean +++ b/generated/annals_symplectic_monodromy/Submission.lean @@ -4,6 +4,8 @@ import Submission.Helpers open SymplecticMonodromy open MvPowerSeries +set_option autoImplicit false + namespace Submission theorem theorem_1_1 (n : ℕ) (f : unitInterval → MvPowerSeries (Fin n) ℂ) diff --git a/generated/annals_ulam/Challenge.lean b/generated/annals_ulam/Challenge.lean index a1417f8bc..9fb0847e9 100644 --- a/generated/annals_ulam/Challenge.lean +++ b/generated/annals_ulam/Challenge.lean @@ -4,6 +4,7 @@ open Ulam open MeasureTheory open scoped ContDiff Pointwise RealInnerProductSpace +set_option autoImplicit false variable {d : ℕ} local notation "ℝᵈ" => EuclideanSpace ℝ (Fin d) diff --git a/generated/annals_ulam/Solution.lean b/generated/annals_ulam/Solution.lean index 2bd70cc03..97312004e 100644 --- a/generated/annals_ulam/Solution.lean +++ b/generated/annals_ulam/Solution.lean @@ -5,6 +5,7 @@ open Ulam open MeasureTheory open scoped ContDiff Pointwise RealInnerProductSpace +set_option autoImplicit false variable {d : ℕ} local notation "ℝᵈ" => EuclideanSpace ℝ (Fin d) diff --git a/generated/annals_ulam/Submission.lean b/generated/annals_ulam/Submission.lean index 14c237191..8e0809413 100644 --- a/generated/annals_ulam/Submission.lean +++ b/generated/annals_ulam/Submission.lean @@ -5,6 +5,7 @@ open Ulam open MeasureTheory open scoped ContDiff Pointwise RealInnerProductSpace +set_option autoImplicit false variable {d : ℕ} local notation "ℝᵈ" => EuclideanSpace ℝ (Fin d) diff --git a/generated/annals_unit_conjecture/Challenge.lean b/generated/annals_unit_conjecture/Challenge.lean index c04f5659e..e5607d862 100644 --- a/generated/annals_unit_conjecture/Challenge.lean +++ b/generated/annals_unit_conjecture/Challenge.lean @@ -2,5 +2,7 @@ import ChallengeDeps open UnitConjecture +set_option autoImplicit false + theorem theorem_A : (∀ g : P, ∀ n ≠ 0, g ^ n = 1 → g = 1) ∧ IsUnit u ∧ ¬ ∃ g : P, u = g := by sorry diff --git a/generated/annals_unit_conjecture/Solution.lean b/generated/annals_unit_conjecture/Solution.lean index 3d687e13d..94277ce13 100644 --- a/generated/annals_unit_conjecture/Solution.lean +++ b/generated/annals_unit_conjecture/Solution.lean @@ -3,5 +3,7 @@ import Submission open UnitConjecture +set_option autoImplicit false + theorem theorem_A : (∀ g : P, ∀ n ≠ 0, g ^ n = 1 → g = 1) ∧ IsUnit u ∧ ¬ ∃ g : P, u = g := by exact Submission.theorem_A diff --git a/generated/annals_unit_conjecture/Submission.lean b/generated/annals_unit_conjecture/Submission.lean index 7b658cc87..8e1e32047 100644 --- a/generated/annals_unit_conjecture/Submission.lean +++ b/generated/annals_unit_conjecture/Submission.lean @@ -3,6 +3,8 @@ import Submission.Helpers open UnitConjecture +set_option autoImplicit false + namespace Submission theorem theorem_A : (∀ g : P, ∀ n ≠ 0, g ^ n = 1 → g = 1) ∧ IsUnit u ∧ ¬ ∃ g : P, u = g := by diff --git a/generated/annals_van_der_waerden_conjecture/Challenge.lean b/generated/annals_van_der_waerden_conjecture/Challenge.lean index 8632e2c26..65065e024 100644 --- a/generated/annals_van_der_waerden_conjecture/Challenge.lean +++ b/generated/annals_van_der_waerden_conjecture/Challenge.lean @@ -3,6 +3,8 @@ import ChallengeDeps open vanDerWaerdenConjecture open Function Polynomial Filter +set_option autoImplicit false + theorem theorem_1 (n : ℕ) (hn : 3 ≤ n) : (fun H ↦ (E n H : ℝ)) =O[atTop] (fun H ↦ (H ^ (n - 1) : ℝ)) := by sorry diff --git a/generated/annals_van_der_waerden_conjecture/Solution.lean b/generated/annals_van_der_waerden_conjecture/Solution.lean index 2f176a354..af8c21296 100644 --- a/generated/annals_van_der_waerden_conjecture/Solution.lean +++ b/generated/annals_van_der_waerden_conjecture/Solution.lean @@ -4,6 +4,8 @@ import Submission open vanDerWaerdenConjecture open Function Polynomial Filter +set_option autoImplicit false + theorem theorem_1 (n : ℕ) (hn : 3 ≤ n) : (fun H ↦ (E n H : ℝ)) =O[atTop] (fun H ↦ (H ^ (n - 1) : ℝ)) := by exact Submission.theorem_1 n hn diff --git a/generated/annals_van_der_waerden_conjecture/Submission.lean b/generated/annals_van_der_waerden_conjecture/Submission.lean index da18bbfa9..5af0e3a8b 100644 --- a/generated/annals_van_der_waerden_conjecture/Submission.lean +++ b/generated/annals_van_der_waerden_conjecture/Submission.lean @@ -4,6 +4,8 @@ import Submission.Helpers open vanDerWaerdenConjecture open Function Polynomial Filter +set_option autoImplicit false + namespace Submission theorem theorem_1 (n : ℕ) (hn : 3 ≤ n) : diff --git a/generated/annals_viscosity_solutions/Challenge.lean b/generated/annals_viscosity_solutions/Challenge.lean index e1d9e1c1e..0a457915c 100644 --- a/generated/annals_viscosity_solutions/Challenge.lean +++ b/generated/annals_viscosity_solutions/Challenge.lean @@ -3,6 +3,7 @@ import ChallengeDeps open ViscositySolutions open Filter Gradient Real Set +set_option autoImplicit false variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] variable {N : ℕ} local notation "ℝᴺ" => Fin N → ℝ diff --git a/generated/annals_viscosity_solutions/Solution.lean b/generated/annals_viscosity_solutions/Solution.lean index caa4d7797..e1c361bde 100644 --- a/generated/annals_viscosity_solutions/Solution.lean +++ b/generated/annals_viscosity_solutions/Solution.lean @@ -4,6 +4,7 @@ import Submission open ViscositySolutions open Filter Gradient Real Set +set_option autoImplicit false variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] variable {N : ℕ} local notation "ℝᴺ" => Fin N → ℝ diff --git a/generated/annals_viscosity_solutions/Submission.lean b/generated/annals_viscosity_solutions/Submission.lean index 7c2f37df4..4688e4768 100644 --- a/generated/annals_viscosity_solutions/Submission.lean +++ b/generated/annals_viscosity_solutions/Submission.lean @@ -4,6 +4,7 @@ import Submission.Helpers open ViscositySolutions open Filter Gradient Real Set +set_option autoImplicit false variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] variable {N : ℕ} local notation "ℝᴺ" => Fin N → ℝ diff --git a/generated/annals_wilkies_conjecture/Challenge.lean b/generated/annals_wilkies_conjecture/Challenge.lean index 14149192b..e82955714 100644 --- a/generated/annals_wilkies_conjecture/Challenge.lean +++ b/generated/annals_wilkies_conjecture/Challenge.lean @@ -3,6 +3,7 @@ import ChallengeDeps open WilkiesConjecture open FirstOrder Language IntermediateField +set_option autoImplicit false variable {n : ℕ} local notation "ℝⁿ" => Fin n → ℝ diff --git a/generated/annals_wilkies_conjecture/Solution.lean b/generated/annals_wilkies_conjecture/Solution.lean index 0b7b0f673..019852905 100644 --- a/generated/annals_wilkies_conjecture/Solution.lean +++ b/generated/annals_wilkies_conjecture/Solution.lean @@ -4,6 +4,7 @@ import Submission open WilkiesConjecture open FirstOrder Language IntermediateField +set_option autoImplicit false variable {n : ℕ} local notation "ℝⁿ" => Fin n → ℝ diff --git a/generated/annals_wilkies_conjecture/Submission.lean b/generated/annals_wilkies_conjecture/Submission.lean index 1a68b559e..bb377cdfc 100644 --- a/generated/annals_wilkies_conjecture/Submission.lean +++ b/generated/annals_wilkies_conjecture/Submission.lean @@ -4,6 +4,7 @@ import Submission.Helpers open WilkiesConjecture open FirstOrder Language IntermediateField +set_option autoImplicit false variable {n : ℕ} local notation "ℝⁿ" => Fin n → ℝ diff --git a/lake-manifest.json b/lake-manifest.json index a77e45541..9dcdf3c6a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a726789593eeac5c32ad82760061cd5bf6cae662", + "rev": "77373a539b31f8f304c852f288d7d8469cceebff", "name": "«lean-eval-generator»", "manifestFile": "lake-manifest.json", - "inputRev": "a726789593eeac5c32ad82760061cd5bf6cae662", + "inputRev": "77373a539b31f8f304c852f288d7d8469cceebff", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.toml b/lakefile.toml index 9f5400d22..5f2dc2b95 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -17,7 +17,7 @@ rev = "6130a47896ce867c6a4a55373441e59e565bad0f" [[require]] name = "lean-eval-generator" git = "https://github.com/leanprover/lean-eval-generator.git" -rev = "a726789593eeac5c32ad82760061cd5bf6cae662" +rev = "77373a539b31f8f304c852f288d7d8469cceebff" [[lean_lib]] name = "LeanEval" diff --git a/tests/lean/EvalToolsTests/GenerateTest.lean b/tests/lean/EvalToolsTests/GenerateTest.lean index 9754cdcb2..813768a6b 100644 --- a/tests/lean/EvalToolsTests/GenerateTest.lean +++ b/tests/lean/EvalToolsTests/GenerateTest.lean @@ -1,6 +1,7 @@ import EvalTools.Generate open EvalTools +open LeanEvalGenerator.Core set_option autoImplicit false diff --git a/tests/lean/EvalToolsTests/ModuleCoverageTest.lean b/tests/lean/EvalToolsTests/ModuleCoverageTest.lean index 74837ba21..05b21c7ad 100644 --- a/tests/lean/EvalToolsTests/ModuleCoverageTest.lean +++ b/tests/lean/EvalToolsTests/ModuleCoverageTest.lean @@ -2,6 +2,7 @@ import EvalTools.Manifest import EvalTools.ModuleCoverage open EvalTools +open LeanEvalGenerator.Core set_option autoImplicit false