Skip to content

Commit 1bb6ca5

Browse files
KhaKha
committed
more
1 parent 69f10eb commit 1bb6ca5

File tree

2 files changed

+79
-92
lines changed

2 files changed

+79
-92
lines changed

‎src/Lean/Elab/Frontend.lean

Lines changed: 19 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -81,23 +81,17 @@ end Frontend
8181

8282
open Frontend
8383

84-
def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) (commandState : Command.State) : IO State := do
85-
let (_, s) ← (Frontend.processCommands.run { inputCtx := inputCtx }).run { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
86-
pure s
87-
8884
structure IncrementalState extends State where
8985
inputCtx : Parser.InputContext
9086
initialSnap : Language.Lean.CommandParsedSnapshot
9187
deriving Nonempty
9288

9389
open Language in
9490
/--
95-
Variant of `IO.processCommands` that uses the new Lean language processor implementation for
96-
potential incremental reuse. Pass in result of a previous invocation done with the same state
97-
(but usually different input context) to allow for reuse.
91+
Variant of `IO.processCommands` that allows for potential incremental reuse. Pass in result of a
92+
previous invocation done with the same state (but usually different input context) to allow for
93+
reuse.
9894
-/
99-
-- `IO.processCommands` can be reimplemented on top of this as soon as the additional tasks speed up
100-
-- things instead of slowing them down
10195
partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext)
10296
(parserState : Parser.ModuleParserState) (commandState : Command.State)
10397
(old? : Option IncrementalState) :
@@ -126,6 +120,11 @@ where
126120
inputCtx, initialSnap, commands
127121
}
128122

123+
def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
124+
(commandState : Command.State) : IO State := do
125+
let st ← IO.processCommandsIncrementally inputCtx parserState commandState none
126+
return st.toState
127+
129128
def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do
130129
let fileName := fileName.getD "<input>"
131130
let inputCtx := Parser.mkInputContext input fileName
@@ -144,63 +143,31 @@ def runFrontend
144143
: IO (Environment × Bool) := do
145144
let startTime := (← IO.monoNanosNow).toFloat / 1000000000
146145
let inputCtx := Parser.mkInputContext input fileName
147-
if false then
148-
-- Temporarily keep alive old cmdline driver for the Lean language so that we don't pay the
149-
-- overhead of passing the environment between snapshots until we actually make good use of it
150-
-- outside the server
151-
let (header, parserState, messages) ← Parser.parseHeader inputCtx
152-
-- allow `env` to be leaked, which would live until the end of the process anyway
153-
let (env, messages) ← processHeader (leakEnv := true) header opts messages inputCtx trustLevel
154-
let env := env.setMainModule mainModuleName
155-
let mut commandState := Command.mkState env messages opts
156-
let elabStartTime := (← IO.monoNanosNow).toFloat / 1000000000
157-
158-
if ileanFileName?.isSome then
159-
-- Collect InfoTrees so we can later extract and export their info to the ilean file
160-
commandState := { commandState with infoState.enabled := true }
161-
162-
let s ← IO.processCommands inputCtx parserState commandState
163-
Language.reportMessages s.commandState.messages opts jsonOutput
164-
165-
if let some ileanFileName := ileanFileName? then
166-
let trees := s.commandState.infoState.trees.toArray
167-
let references ←
168-
Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false) |>.toLspModuleRefs
169-
let ilean := { module := mainModuleName, references : Lean.Server.Ilean }
170-
IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
171-
172-
if let some out := trace.profiler.output.get? opts then
173-
let traceState := s.commandState.traceState
174-
-- importing does not happen in an elaboration monad, add now
175-
let traceState := { traceState with
176-
traces := #[{
177-
ref := .missing,
178-
msg := .trace { cls := `Import, startTime, stopTime := elabStartTime }
179-
(.ofFormat "importing") #[]
180-
}].toPArray' ++ traceState.traces
181-
}
182-
let profile ← Firefox.Profile.export mainModuleName.toString startTime traceState opts
183-
IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile
184-
185-
return (s.commandState.env, !s.commandState.messages.hasErrors)
186-
187146
let opts := Language.Lean.internal.minimalSnapshots.set opts true
188147
let ctx := { inputCtx with }
189148
let processor := Language.Lean.process
190149
let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel }) none ctx
191150
let snaps := Language.toSnapshotTree snap
192151
snaps.runAndReport opts jsonOutput
152+
193153
if let some ileanFileName := ileanFileName? then
194154
let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
195155
let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
196156
let ilean := { module := mainModuleName, references := ← references.toLspModuleRefs : Lean.Server.Ilean }
197157
IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
198158

199-
let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
200159
-- TODO: remove default when reworking cmdline interface in Lean; currently the only case
201160
-- where we use the environment despite errors in the file is `--stats`
202-
let env := Language.Lean.waitForFinalEnv? snap |>.getD (← mkEmptyEnvironment)
203-
pure (env, !hasErrors)
161+
let some cmdState := Language.Lean.waitForFinalCmdState? snap
162+
| return (← mkEmptyEnvironment, false)
163+
164+
if let some out := trace.profiler.output.get? opts then
165+
let traceState := cmdState.traceState
166+
let profile ← Firefox.Profile.export mainModuleName.toString startTime traceState opts
167+
IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile
168+
169+
let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
170+
pure (cmdState.env, !hasErrors)
204171

205172

206173
end Lean.Elab

‎src/Lean/Language/Lean.lean

Lines changed: 60 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -238,7 +238,7 @@ structure SetupImportsResult where
238238
register_builtin_option internal.minimalSnapshots : Bool := {
239239
defValue := false
240240
descr := "reduce information stored in snapshots to the minimum necessary for the cmdline \
241-
driver: diagnostics and environment per command"
241+
driver: diagnostics per command and final full snapshot"
242242
}
243243

244244
/--
@@ -352,31 +352,47 @@ where
352352
let setup ← match (← setupImports stx) with
353353
| .ok setup => pure setup
354354
| .error snap => return snap
355+
356+
let startTime := (← IO.monoNanosNow).toFloat / 1000000000
355357
-- allows `headerEnv` to be leaked, which would live until the end of the process anyway
356358
let (headerEnv, msgLog) ← Elab.processHeader (leakEnv := true) stx setup.opts .empty
357359
ctx.toInputContext setup.trustLevel
360+
let stopTime := (← IO.monoNanosNow).toFloat / 1000000000
358361
let diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
359362
if msgLog.hasErrors then
360363
return { diagnostics, result? := none }
361364

362365
let headerEnv := headerEnv.setMainModule setup.mainModuleName
366+
let mut traceState := default
367+
if trace.profiler.output.get? setup.opts |>.isSome then
368+
traceState := {
369+
traces := #[{
370+
ref := .missing,
371+
msg := .trace { cls := `Import, startTime, stopTime }
372+
(.ofFormat "importing") #[]
373+
: TraceElem
374+
}].toPArray'
375+
}
363376
let cmdState := Elab.Command.mkState headerEnv msgLog setup.opts
364-
let cmdState := { cmdState with infoState := {
365-
enabled := true
366-
trees := #[Elab.InfoTree.context (.commandCtx {
367-
env := headerEnv
368-
fileMap := ctx.fileMap
369-
ngen := { namePrefix := `_import }
370-
}) (Elab.InfoTree.node
371-
(Elab.Info.ofCommandInfo { elaborator := `header, stx })
372-
(stx[1].getArgs.toList.map (fun importStx =>
373-
Elab.InfoTree.node (Elab.Info.ofCommandInfo {
374-
elaborator := `import
375-
stx := importStx
376-
}) #[].toPArray'
377-
)).toPArray'
378-
)].toPArray'
379-
}}
377+
let cmdState := { cmdState with
378+
infoState := {
379+
enabled := true
380+
trees := #[Elab.InfoTree.context (.commandCtx {
381+
env := headerEnv
382+
fileMap := ctx.fileMap
383+
ngen := { namePrefix := `_import }
384+
}) (Elab.InfoTree.node
385+
(Elab.Info.ofCommandInfo { elaborator := `header, stx })
386+
(stx[1].getArgs.toList.map (fun importStx =>
387+
Elab.InfoTree.node (Elab.Info.ofCommandInfo {
388+
elaborator := `import
389+
stx := importStx
390+
}) #[].toPArray'
391+
)).toPArray'
392+
)].toPArray'
393+
}
394+
traceState
395+
}
380396
let prom ← IO.Promise.new
381397
-- The speedup of these `markPersistent`s is negligible but they help in making unexpected
382398
-- `inc_ref_cold`s more visible
@@ -440,15 +456,16 @@ where
440456
env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace
441457
openDecls := scope.openDecls
442458
}
443-
let (stx, parserState, msgLog) := Parser.parseCommand ctx.toInputContext pmctx parserState
444-
.empty
459+
let (stx, parserState, msgLog) :=
460+
profileit "parsing" scope.opts fun _ =>
461+
Parser.parseCommand ctx.toInputContext pmctx parserState .empty
445462

446463
-- semi-fast path
447464
if let some old := old? then
448465
-- NOTE: as `parserState.pos` includes trailing whitespace, this forces reprocessing even if
449-
-- only that whitespace changes, which is wasteful but still necessary because it may
450-
-- influence the range of error messages such as from a trailing `exact`
451-
if stx.eqWithInfo old.data.stx then
466+
-- only that whitespace changes, which is wasteful but still necessary because it may
467+
-- influence the range of error messages such as from a trailing `exact`
468+
if stx.eqWithInfo old.data.stx then
452469
-- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged`
453470
return (← unchanged old parserState)
454471
-- on first change, make sure to cancel old invocation
@@ -470,23 +487,27 @@ where
470487
let next? ← if Parser.isTerminalCommand stx then pure none
471488
-- for now, wait on "command finished" snapshot before parsing next command
472489
else some <$> IO.Promise.new
473-
prom.resolve <| .mk (nextCmdSnap? := next?.map ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) {
474-
diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
475-
stx := if minimalSnapshots then .missing else stx
476-
parserState := if minimalSnapshots then {} else parserState
490+
let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
491+
let data := if minimalSnapshots && !Parser.isTerminalCommand stx then {
492+
diagnostics
493+
stx := .missing
494+
parserState := {}
477495
elabSnap := { range? := stx.getRange?, task := elabPromise.result }
478-
finishedSnap := .pure <|
479-
if minimalSnapshots then
480-
{ finishedSnap with
481-
infoTree? := none
482-
cmdState := {
483-
env := Runtime.markPersistent (if Parser.isTerminalCommand stx then finishedSnap.cmdState.env else initEnv)
484-
maxRecDepth := 0
485-
}
486-
}
487-
else finishedSnap
496+
finishedSnap := .pure {
497+
diagnostics := finishedSnap.diagnostics
498+
infoTree? := none
499+
cmdState := {
500+
env := initEnv
501+
maxRecDepth := 0
502+
}
503+
}
488504
tacticCache
505+
} else {
506+
diagnostics, stx, parserState, tacticCache
507+
elabSnap := { range? := stx.getRange?, task := elabPromise.result }
508+
finishedSnap := .pure finishedSnap
489509
}
510+
prom.resolve <| .mk (nextCmdSnap? := next?.map ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data
490511
if let some next := next? then
491512
parseCmd none parserState finishedSnap.cmdState initEnv next ctx
492513

@@ -555,16 +576,15 @@ def processCommands (inputCtx : Parser.InputContext) (parserState : Parser.Modul
555576
|>.run { inputCtx with }
556577
return prom.result
557578

558-
559-
/-- Waits for and returns final environment, if importing was successful. -/
560-
partial def waitForFinalEnv? (snap : InitialSnapshot) : Option Environment := do
579+
/-- Waits for and returns final command state, if importing was successful. -/
580+
partial def waitForFinalCmdState? (snap : InitialSnapshot) : Option Command.State := do
561581
let snap ← snap.result?
562582
let snap ← snap.processedSnap.get.result?
563583
goCmd snap.firstCmdSnap.get
564584
where goCmd snap :=
565585
if let some next := snap.nextCmdSnap? then
566586
goCmd next.get
567587
else
568-
snap.data.finishedSnap.get.cmdState.env
588+
snap.data.finishedSnap.get.cmdState
569589

570590
end Lean

0 commit comments

Comments
 (0)