Skip to content

Commit ed34ee0

Browse files
KhaKha
authored
chore: make declMetaExt persistent for shake (#11201)
1 parent 8ef7426 commit ed34ee0

File tree

15 files changed

+80
-72
lines changed

15 files changed

+80
-72
lines changed

‎src/Lean/Attributes.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -156,7 +156,7 @@ def ensureAttrDeclIsPublic (attrName declName : Name) (attrKind : AttributeKind)
156156
throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` must be public"
157157

158158
def ensureAttrDeclIsMeta (attrName declName : Name) (attrKind : AttributeKind) : AttrM Unit := do
159-
if (← getEnv).header.isModule && !isMeta (← getEnv) declName then
159+
if (← getEnv).header.isModule && !isMarkedMeta (← getEnv) declName then
160160
throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` must be marked as `meta`"
161161
-- Make sure attributed decls can't refer to private meta imports, which is already checked for
162162
-- public decls.

‎src/Lean/Compiler/IR/CompilerM.lean‎

Lines changed: 0 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -77,40 +77,6 @@ private abbrev findAtSorted? (decls : Array Decl) (declName : Name) : Option Dec
7777
let tmpDecl := Decl.extern declName #[] default default
7878
decls.binSearch tmpDecl declLt
7979

80-
/-- Meta status of local declarations, not persisted. -/
81-
private builtin_initialize declMetaExt : EnvExtension (List Name × NameSet) ←
82-
registerEnvExtension
83-
(mkInitial := pure ([], {}))
84-
(asyncMode := .sync)
85-
(replay? := some <| fun oldState newState _ s =>
86-
let newEntries := newState.1.take (newState.1.length - oldState.1.length)
87-
newEntries.foldl (init := s) fun s n =>
88-
if s.1.contains n then
89-
s
90-
else
91-
(n :: s.1, s.2.insert n))
92-
93-
/-- Whether a declaration should be exported for interpretation. -/
94-
def isDeclMeta (env : Environment) (declName : Name) : Bool :=
95-
if !env.header.isModule then
96-
true
97-
else
98-
-- The interpreter may call the boxed variant even if the IR does not directly reference it, so
99-
-- use same visibility as base decl.
100-
-- Note that boxed decls are created after the `inferVisibility` pass.
101-
let inferFor := match declName with
102-
| .str n "_boxed" => n
103-
| n => n
104-
declMetaExt.getState env |>.2.contains inferFor
105-
106-
/-- Marks a declaration to be exported for interpretation. -/
107-
def setDeclMeta (env : Environment) (declName : Name) : Environment :=
108-
if isDeclMeta env declName then
109-
env
110-
else
111-
declMetaExt.modifyState env fun s =>
112-
(declName :: s.1, s.2.insert declName)
113-
11480
builtin_initialize declMapExt : SimplePersistentEnvExtension Decl DeclMap ←
11581
registerSimplePersistentEnvExtension {
11682
addImportedFn := fun _ => {}

‎src/Lean/Compiler/IR/Meta.lean‎

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ partial def inferMeta (decls : Array Decl) : CompilerM Unit := do
4343
if !(← getEnv).header.isModule then
4444
return
4545
for decl in decls do
46-
if isMeta (← getEnv) decl.name then
46+
if isMarkedMeta (← getEnv) decl.name then
4747
trace[compiler.ir.inferMeta] m!"Marking {decl.name} as meta because it is tagged with `meta`"
4848
modifyEnv (setDeclMeta · decl.name)
4949
setClosureMeta decl
@@ -59,18 +59,18 @@ private partial def evalCheckMeta (env : Environment) (declName : Name) : Except
5959
return
6060
go declName |>.run' {}
6161
where go (ref : Name) : StateT NameSet (Except String) Unit := do
62-
if (← get).contains ref then
63-
return
64-
modify (·.insert ref)
65-
if let some localDecl := declMapExt.getState env |>.find? ref then
66-
for ref in collectUsedFDecls localDecl do
67-
go ref
68-
else
69-
-- NOTE: We do not use `getIRPhases` here as it's intended for env decls, nor IR decls. We do
70-
-- not set `includeServer` as we want this check to be independent of server mode. Server-only
71-
-- users disable this check instead.
72-
if findEnvDecl env ref |>.isNone then
73-
throw s!"Cannot evaluate constant `{declName}` as it uses `{ref}` which is neither marked nor imported as `meta`"
62+
if (← get).contains ref then
63+
return
64+
modify (·.insert ref)
65+
if let some localDecl := declMapExt.getState env |>.find? ref then
66+
for ref in collectUsedFDecls localDecl do
67+
go ref
68+
else
69+
-- NOTE: We do not use `getIRPhases` here as it's intended for env decls, nor IR decls. We do
70+
-- not set `includeServer` as we want this check to be independent of server mode. Server-only
71+
-- users disable this check instead.
72+
if findEnvDecl env ref |>.isNone then
73+
throw s!"Cannot evaluate constant `{declName}` as it uses `{ref}` which is neither marked nor imported as `meta`"
7474

7575
builtin_initialize
7676
registerTraceClass `compiler.ir.inferMeta

‎src/Lean/Compiler/InitAttr.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) (ref
6969
-- TODO: The interpreter currently depends on `[builtin_init]` to be exported for
7070
-- `prefer_native` handling but this is incorrect with private imports anyway and should be
7171
-- replaced by consulting a builtin list.
72-
!runAfterImport || isMeta env declName
72+
!runAfterImport || isMarkedMeta env declName
7373
}
7474

7575
@[implemented_by registerInitAttrUnsafe]

‎src/Lean/Compiler/LCNF/Visibility.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ where go (isMeta isPublic : Bool) (decl : Decl) : StateT NameSet CompilerM Unit
7777
let env ← getEnv
7878
if isMeta && isPublic then
7979
if let some modIdx := env.getModuleIdxFor? ref then
80-
if Lean.isMeta env ref then
80+
if isMarkedMeta env ref then
8181
if env.header.modules[modIdx]?.any (!·.isExported) then
8282
throwError "Invalid public `meta` definition `{.ofConstName origDecl.name}`, \
8383
`{.ofConstName ref}` is not accessible here; consider adding \
@@ -101,7 +101,7 @@ where go (isMeta isPublic : Bool) (decl : Decl) : StateT NameSet CompilerM Unit
101101
`{.ofConstName ref}` not marked `meta`"
102102
| .comptime, false =>
103103
if let some modIdx := env.getModuleIdxFor? ref then
104-
if !Lean.isMeta env ref then
104+
if !isMarkedMeta env ref then
105105
throwError "Invalid definition `{.ofConstName origDecl.name}`, may not access \
106106
declaration `{.ofConstName ref}` imported as `meta`; consider adding \
107107
`import {env.header.moduleNames[modIdx]!}`"
@@ -131,7 +131,7 @@ partial def checkTemplateVisibility : Pass where
131131
-- A private template-like decl cannot directly be used by a different module. If it could be used
132132
-- indirectly via a public template-like, we do a recursive check when checking the latter.
133133
if !isPrivateName decl.name && (← decl.isTemplateLike) then
134-
let isMeta := isMeta (← getEnv) decl.name
134+
let isMeta := isMarkedMeta (← getEnv) decl.name
135135
go decl decl |>.run' {}
136136
return decls
137137
where go (origDecl decl : Decl) : StateT NameSet CompilerM Unit := do

‎src/Lean/Compiler/MetaAttr.lean‎

Lines changed: 47 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -29,23 +29,65 @@ private builtin_initialize notMetaExt : EnvExtension NameSet ←
2929
(replay? := some fun _ _ newEntries s => newEntries.foldl (·.insert) s)
3030

3131
/-- Marks in the environment extension that the given declaration has been declared by the user as `meta`. -/
32-
def addMeta (env : Environment) (declName : Name) : Environment :=
32+
def markMeta (env : Environment) (declName : Name) : Environment :=
3333
metaExt.tag env declName
3434

3535
/--
3636
Marks the given declaration as not being annotated with `meta` even if it could have been by the
3737
user.
3838
-/
39-
def addNotMeta (env : Environment) (declName : Name) : Environment :=
39+
def markNotMeta (env : Environment) (declName : Name) : Environment :=
4040
if declName.isAnonymous then -- avoid panic from `modifyState` on partial input
4141
env
4242
else
4343
notMetaExt.modifyState (asyncDecl := declName) env (·.insert declName)
4444

4545
/-- Returns true iff the user has declared the given declaration as `meta`. -/
46-
def isMeta (env : Environment) (declName : Name) : Bool :=
46+
def isMarkedMeta (env : Environment) (declName : Name) : Bool :=
4747
metaExt.isTagged env declName
4848

49+
/--
50+
Set of IR decls that should be made available to any importer. This is a superset of `metaExt`,
51+
which is managed by the elaborator and has a different async mode. More precisely, it contains the
52+
closure of `metaExt` as well as further derived decls such as `_boxed` versions. We store this set
53+
primarily to filter exports in `declMapExt`; we persist it in `.olean.private` for the benefit of
54+
`shake`.
55+
-/
56+
private builtin_initialize declMetaExt : SimplePersistentEnvExtension Name NameSet ←
57+
registerSimplePersistentEnvExtension {
58+
addImportedFn := fun _ => {}
59+
addEntryFn := fun s n => s.insert n
60+
asyncMode := .sync
61+
replay? := some <| SimplePersistentEnvExtension.replayOfFilter (!·.contains ·) (·.insert ·)
62+
exportEntriesFnEx? := some fun env s entries => fun
63+
| .private =>
64+
let decls := entries.foldl (init := #[]) fun decls decl => decls.push decl
65+
decls.qsort Name.quickLt
66+
| _ => #[]
67+
}
68+
69+
/-- Whether a declaration should be exported for interpretation. -/
70+
def isDeclMeta (env : Environment) (declName : Name) : Bool :=
71+
if !env.header.isModule then
72+
true
73+
else
74+
-- The interpreter may call the boxed variant even if the IR does not directly reference it, so
75+
-- use same visibility as base decl.
76+
-- Note that boxed decls are created after the `inferVisibility` pass.
77+
let inferFor := match declName with
78+
| .str n "_boxed" => n
79+
| n => n
80+
match env.getModuleIdxFor? declName with
81+
| some idx => declMetaExt.getModuleEntries env idx |>.binSearchContains inferFor Name.quickLt
82+
| none => declMetaExt.getState env |>.contains inferFor
83+
84+
/-- Marks a declaration to be exported for interpretation. -/
85+
def setDeclMeta (env : Environment) (declName : Name) : Environment :=
86+
if isDeclMeta env declName then
87+
env
88+
else
89+
declMetaExt.addEntry env declName
90+
4991
/--
5092
Returns the IR phases of the given declaration that should be considered accessible. Does not take
5193
additional IR loaded for language server purposes into account.
@@ -55,12 +97,12 @@ def getIRPhases (env : Environment) (declName : Name) : IRPhases := Id.run do
5597
return .all
5698
match env.getModuleIdxFor? declName with
5799
| some idx =>
58-
if isMeta env declName then
100+
if isMarkedMeta env declName then
59101
.comptime
60102
else
61103
env.header.modules[idx]?.map (·.irPhases) |>.get!
62104
| none =>
63-
if isMeta env declName then
105+
if isMarkedMeta env declName then
64106
.comptime
65107
else if notMetaExt.getState env |>.contains declName then
66108
.runtime

‎src/Lean/Elab/Binders.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -99,7 +99,7 @@ def declareTacticSyntax (tactic : Syntax) (name? : Option Name := none) : TermEl
9999
let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := .opaque,
100100
safety := DefinitionSafety.safe }
101101
addDecl decl
102-
modifyEnv (addMeta · name)
102+
modifyEnv (markMeta · name)
103103
compileDecl decl
104104
return name
105105

‎src/Lean/Elab/Deriving/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -262,7 +262,7 @@ def getOptDerivingClasses (optDeriving : Syntax) : CoreM (Array DerivingClassVie
262262

263263
def DerivingClassView.applyHandlers (view : DerivingClassView) (declNames : Array Name) : CommandElabM Unit := do
264264
let env ← getEnv
265-
withScope (fun sc => { sc with isMeta := sc.isMeta || declNames.all (isMeta env) }) do
265+
withScope (fun sc => { sc with isMeta := sc.isMeta || declNames.all (isMarkedMeta env) }) do
266266
withRef view.ref do
267267
applyDerivingHandlers (setExpose := view.hasExpose) (← liftCoreM <| view.getClassName) declNames
268268

‎src/Lean/Elab/Inductive.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoi
3030
let declId := decl[1]
3131
let ⟨name, declName, levelNames, docString?⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
3232
if modifiers.isMeta then
33-
modifyEnv (addMeta · declName)
33+
modifyEnv (markMeta · declName)
3434
addDeclarationRangesForBuiltin declName modifiers.stx decl
3535
/-
3636
Relates to issue
@@ -74,7 +74,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoi
7474
let (binders, type?) := expandOptDeclSig ctor[4]
7575
addDeclarationRangesFromSyntax ctorName ctor ctor[3]
7676
if modifiers.isMeta then
77-
modifyEnv (addMeta · ctorName)
77+
modifyEnv (markMeta · ctorName)
7878
return { ref := ctor, declId := ctor[3], modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
7979
let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
8080
return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }

‎src/Lean/Elab/MutualDef.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1192,7 +1192,7 @@ where
11921192
for view in views, declId in expandedDeclIds do
11931193
-- Add tags early so elaboration can access them
11941194
match view.modifiers.computeKind with
1195-
| .meta => modifyEnv (addMeta · declId.declName)
1195+
| .meta => modifyEnv (markMeta · declId.declName)
11961196
| .noncomputable => modifyEnv (addNoncomputable · declId.declName)
11971197
| .regular => pure ()
11981198
withExporting (isExporting :=

0 commit comments

Comments
 (0)