From 2a1ba94caf4c028bcd5492d40f7beac8cebc6e8c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 5 Feb 2026 13:37:55 +0100 Subject: [PATCH] chore: ready shake for use on core (#12326) --- src/Lean/Elab/Declaration.lean | 3 ++- src/Lean/Elab/Syntax.lean | 29 +++++++++++++++++-------- src/Lean/Parser/Extension.lean | 4 ++-- src/lake/Lake/CLI/Main.lean | 25 +++++++++++----------- src/lake/Lake/CLI/Shake.lean | 33 +++++++++++++++-------------- tests/lean/run/extraModUses.lean | 36 ++++++++++++++++++++++++++++---- 6 files changed, 85 insertions(+), 45 deletions(-) diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index b76754722a..44492d4fdb 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -326,7 +326,8 @@ def elabMutual : CommandElab := fun stx => do else throwUnknownConstantAt ident name let declName ← ensureNonAmbiguous ident declNames - recordExtraModUseFromDecl (isMeta := false) declName + withExporting (isExporting := !isPrivateName declName && attrs.any (·.kind != .local)) do + recordExtraModUseFromDecl (isMeta := false) declName Term.applyAttributes declName attrs for attrName in toErase do Attribute.erase declName attrName diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 6c28249e4e..75651968f3 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -88,8 +88,12 @@ def checkLeftRec (stx : Syntax) : ToParserDescrM Bool := do def elabParserName? (stx : Syntax.Ident) (checkMeta := true) : TermElabM (Option Parser.ParserResolution) := do match ← Parser.resolveParserName stx with - | [n@(.category cat)] => - addCategoryInfo stx cat + | [n@(.category catId)] => + if let some cat := Parser.getParserCategory? (← getEnv) catId then + if !(← hasConst cat.declName) && (← withoutExporting <| hasConst cat.declName) then + throwError "unknown category `{catId}`, must be imported publicly" + recordExtraModUseFromDecl (isMeta := true) cat.declName + addCategoryInfo stx catId return n | [n@(.parser parser _)] => if checkMeta && getIRPhases (← getEnv) parser == .runtime then @@ -395,13 +399,16 @@ def elabSyntax (stx : Syntax) : CommandElabM Name := do let `($[$doc?:docComment]? $[ @[ $attrInstances:attrInstance,* ] ]? $attrKind:attrKind syntax%$tk $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $[$ps:stx]* : $catStx) := stx | throwUnsupportedSyntax - let cat := catStx.getId.eraseMacroScopes - if let some cat := Parser.getParserCategory? (← getEnv) cat then + withExporting (isExporting := !isLocalAttrKind attrKind) do + let catId := catStx.getId.eraseMacroScopes + if let some cat := Parser.getParserCategory? (← getEnv) catId then + if !(← hasConst cat.declName) && (← withoutExporting <| hasConst cat.declName) then + throwErrorAt catStx "unknown category `{catId}`, must be imported publicly" -- The category must be imported but is not directly referenced afterwards. recordExtraModUseFromDecl (isMeta := true) cat.declName else - throwErrorAt catStx "unknown category `{cat}`" - liftTermElabM <| Term.addCategoryInfo catStx cat + throwErrorAt catStx "unknown category `{catId}`" + liftTermElabM <| Term.addCategoryInfo catStx catId let syntaxParser := mkNullNode ps -- If the user did not provide an explicit precedence, we assign `maxPrec` to atom-like syntax and `leadPrec` otherwise. let precDefault := if isAtomLikeSyntax syntaxParser then Parser.maxPrec else Parser.leadPrec @@ -411,7 +418,7 @@ def elabSyntax (stx : Syntax) : CommandElabM Name := do let name ← match name? with | some name => pure name.getId | none => - let base ← liftMacroM <| mkNameFromParserSyntax cat syntaxParser + let base ← liftMacroM <| mkNameFromParserSyntax catId syntaxParser let mut name := base let mut i := 1 -- Avoid name conflicts, for which we have to check both public and private name @@ -427,8 +434,8 @@ def elabSyntax (stx : Syntax) : CommandElabM Name := do let mut stxNodeKind := (← getCurrNamespace) ++ name if attrKind matches `(attrKind| local) then stxNodeKind := mkPrivateName (← getEnv) stxNodeKind - let catParserId := mkIdentFrom idRef (cat.appendAfter "_parser") - let (val, lhsPrec?) ← runTermElabM fun _ => Term.toParserDescr syntaxParser cat + let catParserId := mkIdentFrom idRef (catId.appendAfter "_parser") + let (val, lhsPrec?) ← runTermElabM fun _ => Term.toParserDescr syntaxParser catId let declName := name?.getD (mkIdentFrom idRef name (canonical := true)) let attrInstance ← `(attrInstance| $attrKind:attrKind $catParserId:ident $(quote prio):num) let attrInstances := attrInstances.getD { elemsAndSeps := #[] } @@ -449,6 +456,10 @@ def elabSyntax (stx : Syntax) : CommandElabM Name := do @[builtin_command_elab «syntaxAbbrev»] def elabSyntaxAbbrev : CommandElab := fun stx => do let `($[$doc?:docComment]? $[$vis?:visibility]? syntax $declName:ident := $[$ps:stx]*) ← pure stx | throwUnsupportedSyntax + let sc ← getScope + withExporting (isExporting := match vis? with + | none => sc.isPublic + | some v => v matches `(Parser.Command.visibility| public)) do -- TODO: nonatomic names let (val, _) ← runTermElabM fun _ => Term.toParserDescr (mkNullNode ps) Name.anonymous let stxNodeKind := (← getCurrNamespace) ++ declName.getId diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 404cab01eb..58ca66e460 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -160,7 +160,7 @@ def ParserExtension.addEntryImpl (s : State) (e : Entry) : State := | Entry.token tk => match addTokenConfig s.tokens tk with | Except.ok tokens => { s with tokens } - | _ => unreachable! + | Except.error e => panic! s!"ParserExtension.addEntryImpl: {e}" | Entry.kind k => { s with kinds := s.kinds.insert k } | Entry.category catName declName behavior => @@ -170,7 +170,7 @@ def ParserExtension.addEntryImpl (s : State) (e : Entry) : State := | Entry.parser catName declName leading parser prio => match addParser s.categories catName declName leading parser prio with | Except.ok categories => { s with categories } - | _ => unreachable! + | Except.error e => panic! s!"ParserExtension.addEntryImpl: {e}" /-- Parser aliases for making `ParserDescr` extensible -/ inductive AliasValue (α : Type) where diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 4de8226289..17ca1957b4 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -772,20 +772,19 @@ protected def shake : CliM PUnit := do let mods := (← takeArgs).toArray.map (·.toName) -- Get default target modules from workspace if no modules specified let mods := if mods.isEmpty then ws.defaultTargetRoots else mods - if h : 0 < mods.size then - let args := {opts.shake with mods} - unless args.force do - let specs ← parseTargetSpecs ws [] - let upToDate ← ws.checkNoBuild (buildSpecs specs) - unless upToDate do - error "there are out of date oleans; run `lake build` or fetch them from a cache first" - -- Run shake with workspace search paths - Lean.searchPathRef.set ws.augmentedLeanPath - let exitCode ← Shake.run args h ws.augmentedLeanSrcPath - if exitCode != 0 then - exit exitCode - else + if mods.isEmpty then error "no modules specified and there are no applicable default targets" + let args := {opts.shake with mods} + unless args.force do + let specs ← parseTargetSpecs ws [] + let upToDate ← ws.checkNoBuild (buildSpecs specs) + unless upToDate do + error "there are out of date oleans; run `lake build` or fetch them from a cache first" + -- Run shake with workspace search paths + Lean.searchPathRef.set ws.augmentedLeanPath + let exitCode ← Shake.run args ws.augmentedLeanSrcPath + if exitCode != 0 then + exit exitCode protected def script : CliM PUnit := do if let some cmd ← takeArg? then diff --git a/src/lake/Lake/CLI/Shake.lean b/src/lake/Lake/CLI/Shake.lean index 8ef81b3bc2..326573ee5e 100644 --- a/src/lake/Lake/CLI/Shake.lean +++ b/src/lake/Lake/CLI/Shake.lean @@ -395,23 +395,24 @@ def decodeImport : TSyntax ``Parser.Module.import → Import /-- Analyze and report issues from module `i`. Arguments: -* `pkg`: the first component of the module name +* `pkgs`: the first components of the input modules * `srcSearchPath`: Used to find the path for error reporting purposes * `i`: the module index * `needs`: the module's calculated needs * `addOnly`: if true, only add missing imports, do not remove unused ones -/ -def visitModule (pkg : Name) (srcSearchPath : SearchPath) +def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath) (i : Nat) (needs : Needs) (headerStx : TSyntax ``Parser.Module.header) (args : Args) (addOnly := false) : StateT State IO Unit := do + let modName := (← get).modNames[i]! if isExtraRevModUse (← get).env i then modify fun s => { s with preserve := s.preserve.union (if args.addPublic then .pub else .priv) {i} } if args.trace then - IO.eprintln s!"Preserving `{(← get).modNames[i]!}` because of recorded extra rev use" + IO.eprintln s!"Preserving `{modName}` because of recorded extra rev use" - -- only process modules in the selected package + -- only process modules in the selected packages -- TODO: should be after `keep-downstream` but core headers are not found yet? - if !pkg.isPrefixOf (← get).modNames[i]! then + if !pkgs.any (·.isPrefixOf modName) then return let (module?, prelude?, imports) := decodeHeader headerStx @@ -429,7 +430,8 @@ def visitModule (pkg : Name) (srcSearchPath : SearchPath) let j := s.env.getModuleIdx? imp.module |>.get! let k := NeedsKind.ofImport imp if addOnly || - args.keepPublic && imp.isExported || + -- TODO: allow per-library configuration instead of hardcoding `Init` + args.keepPublic && imp.isExported && !(`Init).isPrefixOf modName || impStx.raw.getTrailing?.any (·.toString.contains "shake: keep") then deps := deps.union k {j} if args.trace then @@ -466,7 +468,7 @@ def visitModule (pkg : Name) (srcSearchPath : SearchPath) transDeps := addTransitiveImps transDeps imp j s.transDeps[j]! deps := deps.union k {j} -- skip folder-nested `public (meta)? import`s but remove `meta` - else if s.modNames[i]!.isPrefixOf imp.module then + else if modName.isPrefixOf imp.module then let imp := { imp with isMeta := false } let k := { k with isMeta := false } if args.trace then @@ -505,8 +507,8 @@ def visitModule (pkg : Name) (srcSearchPath : SearchPath) -- `j'` must be reachable from `i` (allow downgrading from `meta`) guard <| s.transDepsOrig[i]!.has k j' || s.transDepsOrig[i]!.has { k with isMeta := true } j' let j'transDeps := addTransitiveImps .empty p j' s.transDeps[j']! - -- `j` must be reachable from `j'` (now downgrading must be done in the other direction) - guard <| j'transDeps.has k j || j'transDeps.has { k with isMeta := false } j + -- `j` must be publicly reachable from `j'` (now downgrading must be done in the other direction) + guard <| j'transDeps.has { k with isExported := true } j || j'transDeps.has { k with isExported := true, isMeta := false } j return j') | _ => none if let some j' := tryPrefix imp.module then @@ -560,7 +562,7 @@ def visitModule (pkg : Name) (srcSearchPath : SearchPath) -- mark and report the removals modify fun s => { s with edits := toRemove.foldl (init := s.edits) fun edits imp => - edits.remove s.modNames[i]! imp } + edits.remove modName imp } if !toAdd.isEmpty || !toRemove.isEmpty || args.explain then if let some path ← srcSearchPath.findModuleWithExt "lean" s.modNames[i]! then @@ -634,13 +636,12 @@ Run the shake analysis with the given arguments. Assumes Lean's search path has already been properly configured. -/ -public def run (args : Args) (h : 0 < args.mods.size) - (srcSearchPath : SearchPath := {}) : IO UInt32 := do +public def run (args : Args) (srcSearchPath : SearchPath := {}) : IO UInt32 := do -- the list of root modules let mods := args.mods - -- Only submodules of `pkg` will be edited or have info reported on them - let pkg := mods[0].getRoot + -- Only submodules of `pkgs` will be edited or have info reported on them + let pkgs := mods.map (·.getRoot) -- Load all the modules let imps := mods.map ({ module := · }) @@ -663,7 +664,7 @@ public def run (args : Args) (h : 0 < args.mods.size) -- Parse headers in parallel let headers ← s.mods.mapIdxM fun i _ => - if !pkg.isPrefixOf s.modNames[i]! then + if !pkgs.any (·.isPrefixOf s.modNames[i]!) then pure <| Task.pure <| .ok ⟨default, default, default, default⟩ else BaseIO.asTask (parseHeader srcSearchPath s.modNames[i]! |>.toBaseIO) @@ -675,7 +676,7 @@ public def run (args : Args) (h : 0 < args.mods.size) for i in [0:s.mods.size], t in needs, header in headers do match header.get with | .ok ⟨_, _, stx, _⟩ => - visitModule pkg srcSearchPath i t.get stx args + visitModule pkgs srcSearchPath i t.get stx args | .error e => println! e.toString diff --git a/tests/lean/run/extraModUses.lean b/tests/lean/run/extraModUses.lean index 3111610f10..591d58c76a 100644 --- a/tests/lean/run/extraModUses.lean +++ b/tests/lean/run/extraModUses.lean @@ -82,7 +82,7 @@ Is rev mod use: false syntax "hi" : term /-- -info: Entries: [import Init.Notation] +info: Entries: [public import Init.Notation] Is rev mod use: false -/ #guard_msgs in #eval showExtraModUses @@ -171,7 +171,21 @@ References from `@[grind]` are tracked (here `List.append` from Init.Prelude) attribute [grind =] List.append /-- -info: Entries: [import Init.Grind.Attr, public import Init.Prelude, import Init.Prelude] +info: Entries: [import Init.Grind.Attr, public import Init.Prelude] +Is rev mod use: false +-/ +#guard_msgs in #eval showExtraModUses + +/-! +Local attribute applications are tracked as private. +-/ + +#eval resetExtraModUses + +attribute [local grind =] List.append + +/-- +info: Entries: [import Init.Grind.Attr, import Init.Prelude] Is rev mod use: false -/ #guard_msgs in #eval showExtraModUses @@ -231,13 +245,27 @@ The syntax node kind in `syntax` declarations get recorded as a `meta` dependenc syntax "test_me " Lean.Parser.Term.ident : term /-- -info: Entries: [meta import Lean.Parser.Term, import Init.Notation] +info: Entries: [public meta import Lean.Parser.Term, public import Init.Notation] Is rev mod use: false -/ #guard_msgs in #eval showExtraModUses /-! -The syntax node kind in quotations get recorded as a `meta` dependency. +The categories in `syntax` declarations get recorded as a `meta` dependency. +-/ + +#eval resetExtraModUses + +syntax "test_me " rcasesPat : term + +/-- +info: Entries: [public import Init.RCases, public import Init.Notation] +Is rev mod use: false +-/ +#guard_msgs in #eval showExtraModUses + +/-! +The quotation parser gets recorded as a `meta` dependency. -/ #eval resetExtraModUses