max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: shake: keep-downstream and import privacy (#11634)

Browse source
This commit is contained in:
Sebastian Ullrich 2025-12-12 15:09:50 +01:00 • committed by GitHub
parent 9be007ad70
commit 7f5e28ac89
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
script/Shake.lean
View file

@ -466,7 +466,7 @@ def visitModule (pkg : Name) (srcSearchPath : SearchPath)
let (module?, prelude?, imports) := decodeHeader headerStx
if module?.any (·.raw.getTrailing?.any (·.toString.contains "shake: keep-downstream")) then
modify fun s => { s with preserve := s.preserve.union .pub {i} }
modify fun s => { s with preserve := s.preserve.union (if args.addPublic then .pub else .priv) {i} }
let s ← get
@ -486,9 +486,12 @@ def visitModule (pkg : Name) (srcSearchPath : SearchPath)
IO.eprintln s!"Adding `{imp}` as additional dependency"
for j in [0:s.mods.size] do
for k in NeedsKind.all do
-- remove `meta` while preserving, no use-case for preserving `meta` so far
if s.transDepsOrig[i]!.has k j && s.preserve.has { k with isMeta := false } j then
deps := deps.union { k with isMeta := false } {j}
-- Remove `meta` while preserving, no use-case for preserving `meta` so far.
-- Downgrade to private unless `--add-public` is used.
if s.transDepsOrig[i]!.has k j &&
(s.preserve.has { k with isMeta := false, isExported := false } j ||
s.preserve.has { k with isMeta := false, isExported := true } j) then
deps := deps.union { k with isMeta := false, isExported := k.isExported && args.addPublic } {j}
-- Do transitive reduction of `needs` in `deps`.
if !addOnly then
@ -793,16 +796,16 @@ public def main (args : List String) : IO UInt32 := do
for stx in imports do
let mod := decodeImport stx
if remove.contains mod || seen.contains mod then
out := out ++ pos.extract (text.pos! stx.raw.getPos?.get!)
out := out ++ text.extract pos (text.pos! stx.raw.getPos?.get!)
-- We use the end position of the syntax, but include whitespace up to the first newline
pos := text.pos! stx.raw.getTailPos?.get! |>.find '\n' |>.next!
seen := seen.insert mod
out := out ++ pos.extract insertion
out := out ++ text.extract pos insertion
for mod in add do
if !seen.contains mod then
seen := seen.insert mod
out := out ++ s!"{mod}\n"
out := out ++ insertion.extract text.endPos
out := out ++ text.extract insertion text.endPos
IO.FS.writeFile path out
count := count + 1