Skip to content

Commit 03a88ec

Browse files
KhaKha
committed
more
1 parent c874da0 commit 03a88ec

File tree

2 files changed

+85
-95
lines changed

2 files changed

+85
-95
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: 66 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -338,7 +338,7 @@ structure SetupImportsResult where
338338
register_builtin_option internal.minimalSnapshots : Bool := {
339339
defValue := false
340340
descr := "reduce information stored in snapshots to the minimum necessary for the cmdline \
341-
driver: diagnostics and environment per command"
341+
driver: diagnostics per command and final full snapshot"
342342
}
343343

344344
/--
@@ -369,16 +369,16 @@ where
369369
parseHeader (old? : Option HeaderParsedSnapshot) : LeanProcessingM HeaderParsedSnapshot := do
370370
let ctx ← read
371371
let ictx := ctx.toInputContext
372-
let unchanged old newParserState :=
372+
let unchanged old newStx newParserState :=
373373
-- when header syntax is unchanged, reuse import processing task as is and continue with
374374
-- parsing the first command, synchronously if possible
375-
-- NOTE: even if the syntax tree is functionally unchanged, the new parser state may still
376-
-- have changed because of trailing whitespace and comments etc., so it is passed separately
377-
-- from `old`
375+
-- NOTE: even if the syntax tree is functionally unchanged, its concrete structure and the new
376+
-- parser state may still have changed because of trailing whitespace and comments etc., so
377+
-- they are passed separately from `old`
378378
if let some oldSuccess := old.result? then
379379
return {
380380
ictx
381-
stx := old.stx
381+
stx := newStx
382382
diagnostics := old.diagnostics
383383
cancelTk? := ctx.newCancelTk
384384
result? := some { oldSuccess with
@@ -452,31 +452,47 @@ where
452452
let setup ← match (← setupImports stx) with
453453
| .ok setup => pure setup
454454
| .error snap => return snap
455+
456+
let startTime := (← IO.monoNanosNow).toFloat / 1000000000
455457
-- allows `headerEnv` to be leaked, which would live until the end of the process anyway
456458
let (headerEnv, msgLog) ← Elab.processHeader (leakEnv := true) stx setup.opts .empty
457459
ctx.toInputContext setup.trustLevel
460+
let stopTime := (← IO.monoNanosNow).toFloat / 1000000000
458461
let diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
459462
if msgLog.hasErrors then
460463
return { diagnostics, result? := none }
461464

462465
let headerEnv := headerEnv.setMainModule setup.mainModuleName
466+
let mut traceState := default
467+
if trace.profiler.output.get? setup.opts |>.isSome then
468+
traceState := {
469+
traces := #[{
470+
ref := .missing,
471+
msg := .trace { cls := `Import, startTime, stopTime }
472+
(.ofFormat "importing") #[]
473+
: TraceElem
474+
}].toPArray'
475+
}
463476
let cmdState := Elab.Command.mkState headerEnv msgLog setup.opts
464-
let cmdState := { cmdState with infoState := {
465-
enabled := true
466-
trees := #[Elab.InfoTree.context (.commandCtx {
467-
env := headerEnv
468-
fileMap := ctx.fileMap
469-
ngen := { namePrefix := `_import }
470-
}) (Elab.InfoTree.node
471-
(Elab.Info.ofCommandInfo { elaborator := `header, stx })
472-
(stx[1].getArgs.toList.map (fun importStx =>
473-
Elab.InfoTree.node (Elab.Info.ofCommandInfo {
474-
elaborator := `import
475-
stx := importStx
476-
}) #[].toPArray'
477-
)).toPArray'
478-
)].toPArray'
479-
}}
477+
let cmdState := { cmdState with
478+
infoState := {
479+
enabled := true
480+
trees := #[Elab.InfoTree.context (.commandCtx {
481+
env := headerEnv
482+
fileMap := ctx.fileMap
483+
ngen := { namePrefix := `_import }
484+
}) (Elab.InfoTree.node
485+
(Elab.Info.ofCommandInfo { elaborator := `header, stx })
486+
(stx[1].getArgs.toList.map (fun importStx =>
487+
Elab.InfoTree.node (Elab.Info.ofCommandInfo {
488+
elaborator := `import
489+
stx := importStx
490+
}) #[].toPArray'
491+
)).toPArray'
492+
)].toPArray'
493+
}
494+
traceState
495+
}
480496
let prom ← IO.Promise.new
481497
-- The speedup of these `markPersistent`s is negligible but they help in making unexpected
482498
-- `inc_ref_cold`s more visible
@@ -540,12 +556,16 @@ where
540556
env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace
541557
openDecls := scope.openDecls
542558
}
543-
let (stx, parserState, msgLog) := Parser.parseCommand ctx.toInputContext pmctx parserState
544-
.empty
559+
let (stx, parserState, msgLog) :=
560+
profileit "parsing" scope.opts fun _ =>
561+
Parser.parseCommand ctx.toInputContext pmctx parserState .empty
545562

546563
-- semi-fast path
547564
if let some old := old? then
548-
if (← isBeforeEditPos parserState.pos ctx) && old.data.stx == stx then
565+
-- NOTE: as `parserState.pos` includes trailing whitespace, this forces reprocessing even if
566+
-- only that whitespace changes, which is wasteful but still necessary because it may
567+
-- influence the range of error messages such as from a trailing `exact`
568+
if stx.eqWithInfo old.data.stx then
549569
-- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged`
550570
return (← unchanged old parserState)
551571
-- on first change, make sure to cancel old invocation
@@ -567,23 +587,27 @@ where
567587
let next? ← if Parser.isTerminalCommand stx then pure none
568588
-- for now, wait on "command finished" snapshot before parsing next command
569589
else some <$> IO.Promise.new
570-
prom.resolve <| .mk (nextCmdSnap? := next?.map ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) {
571-
diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
572-
stx := if minimalSnapshots then .missing else stx
573-
parserState := if minimalSnapshots then {} else parserState
590+
let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
591+
let data := if minimalSnapshots && !Parser.isTerminalCommand stx then {
592+
diagnostics
593+
stx := .missing
594+
parserState := {}
574595
elabSnap := { range? := stx.getRange?, task := elabPromise.result }
575-
finishedSnap := .pure <|
576-
if minimalSnapshots then
577-
{ finishedSnap with
578-
infoTree? := none
579-
cmdState := {
580-
env := Runtime.markPersistent (if Parser.isTerminalCommand stx then finishedSnap.cmdState.env else initEnv)
581-
maxRecDepth := 0
582-
}
583-
}
584-
else finishedSnap
596+
finishedSnap := .pure {
597+
diagnostics := finishedSnap.diagnostics
598+
infoTree? := none
599+
cmdState := {
600+
env := initEnv
601+
maxRecDepth := 0
602+
}
603+
}
585604
tacticCache
605+
} else {
606+
diagnostics, stx, parserState, tacticCache
607+
elabSnap := { range? := stx.getRange?, task := elabPromise.result }
608+
finishedSnap := .pure finishedSnap
586609
}
610+
prom.resolve <| .mk (nextCmdSnap? := next?.map ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data
587611
if let some next := next? then
588612
parseCmd none parserState finishedSnap.cmdState initEnv next ctx
589613

@@ -652,16 +676,15 @@ def processCommands (inputCtx : Parser.InputContext) (parserState : Parser.Modul
652676
|>.run { inputCtx with }
653677
return prom.result
654678

655-
656-
/-- Waits for and returns final environment, if importing was successful. -/
657-
partial def waitForFinalEnv? (snap : InitialSnapshot) : Option Environment := do
679+
/-- Waits for and returns final command state, if importing was successful. -/
680+
partial def waitForFinalCmdState? (snap : InitialSnapshot) : Option Command.State := do
658681
let snap ← snap.result?
659682
let snap ← snap.processedSnap.get.result?
660683
goCmd snap.firstCmdSnap.get
661684
where goCmd snap :=
662685
if let some next := snap.nextCmdSnap? then
663686
goCmd next.get
664687
else
665-
snap.data.finishedSnap.get.cmdState.env
688+
snap.data.finishedSnap.get.cmdState
666689

667690
end Lean

0 commit comments

Comments
 (0)