Skip to content

Commit

Permalink
feat: new snapshot architecture on the cmdline (#3106)
Browse files Browse the repository at this point in the history 
This is #3014 with cad5cce reverted for testing.
  • Loading branch information
@Kha
Kha authored Aug 5, 2024
1 parent 87d41e6 commit a3d144a
Show file tree
Hide file tree
Showing 16 changed files with 265 additions and 238 deletions.
117 changes: 21 additions & 96 deletions src/Lean/Elab/Frontend.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,23 +81,17 @@ end Frontend

open Frontend

def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) (commandState : Command.State) : IO State := do
let (_, s) ← (Frontend.processCommands.run { inputCtx := inputCtx }).run { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
pure s

structure IncrementalState extends State where
inputCtx : Parser.InputContext
initialSnap : Language.Lean.CommandParsedSnapshot
deriving Nonempty

open Language in
/--
Variant of `IO.processCommands` that uses the new Lean language processor implementation for
potential incremental reuse. Pass in result of a previous invocation done with the same state
(but usually different input context) to allow for reuse.
Variant of `IO.processCommands` that allows for potential incremental reuse. Pass in the result of a
previous invocation done with the same state (but usually different input context) to allow for
reuse.
-/
-- `IO.processCommands` can be reimplemented on top of this as soon as the additional tasks speed up
-- things instead of slowing them down
partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext)
(parserState : Parser.ModuleParserState) (commandState : Command.State)
(old? : Option IncrementalState) :
Expand All @@ -110,7 +104,7 @@ where
let snap := t.get
let commands := commands.push snap.data.stx
if let some next := snap.nextCmdSnap? then
go initialSnap next commands
go initialSnap next.task commands
else
-- Opting into reuse also enables incremental reporting, so make sure to collect messages from
-- all snapshots
Expand All @@ -126,53 +120,17 @@ where
inputCtx, initialSnap, commands
}

def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
(commandState : Command.State) : IO State := do
let st ← IO.processCommandsIncrementally inputCtx parserState commandState none
return st.toState

def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do
let fileName := fileName.getD "<input>"
let inputCtx := Parser.mkInputContext input fileName
let s ← IO.processCommands inputCtx { : Parser.ModuleParserState } (Command.mkState env {} opts)
pure (s.commandState.env, s.commandState.messages)

/--
Parses values of options registered during import and left by the C++ frontend as strings, fails if
any option names remain unknown.
-/
def reparseOptions (opts : Options) : IO Options := do
let mut opts := opts
let decls ← getOptionDecls
for (name, val) in opts do
let .ofString val := val
| continue -- Already parsed by C++
-- Options can be prefixed with `weak` in order to turn off the error when the option is not
-- defined
let weak := name.getRoot == `weak
if weak then
opts := opts.erase name
let name := name.replacePrefix `weak Name.anonymous
let some decl := decls.find? name
| unless weak do
throw <| .userError s!"invalid -D parameter, unknown configuration option '{name}'
If the option is defined in this library, use '-D{`weak ++ name}' to set it conditionally"

match decl.defValue with
| .ofBool _ =>
match val with
| "true" => opts := opts.insert name true
| "false" => opts := opts.insert name false
| _ =>
throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
it must be true/false"
| .ofNat _ =>
let some val := val.toNat?
| throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
it must be a natural number"
opts := opts.insert name val
| .ofString _ => opts := opts.insert name val
| _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
cannot be set in the command line, use set_option command"

return opts

@[export lean_run_frontend]
def runFrontend
(input : String)
Expand All @@ -185,64 +143,31 @@ def runFrontend
: IO (Environment × Bool) := do
let startTime := (← IO.monoNanosNow).toFloat / 1000000000
let inputCtx := Parser.mkInputContext input fileName
if true then
-- Temporarily keep alive old cmdline driver for the Lean language so that we don't pay the
-- overhead of passing the environment between snapshots until we actually make good use of it
-- outside the server
let (header, parserState, messages) ← Parser.parseHeader inputCtx
-- allow `env` to be leaked, which would live until the end of the process anyway
let (env, messages) ← processHeader (leakEnv := true) header opts messages inputCtx trustLevel
-- now that imports have been loaded, check options again
let opts ← reparseOptions opts
let env := env.setMainModule mainModuleName
let mut commandState := Command.mkState env messages opts
let elabStartTime := (← IO.monoNanosNow).toFloat / 1000000000

if ileanFileName?.isSome then
-- Collect InfoTrees so we can later extract and export their info to the ilean file
commandState := { commandState with infoState.enabled := true }

let s ← IO.processCommands inputCtx parserState commandState
Language.reportMessages s.commandState.messages opts jsonOutput

if let some ileanFileName := ileanFileName? then
let trees := s.commandState.infoState.trees.toArray
let references ←
Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false) |>.toLspModuleRefs
let ilean := { module := mainModuleName, references : Lean.Server.Ilean }
IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean

if let some out := trace.profiler.output.get? opts then
let traceState := s.commandState.traceState
-- importing does not happen in an elaboration monad, add now
let traceState := { traceState with
traces := #[{
ref := .missing,
msg := .trace { cls := `Import, startTime, stopTime := elabStartTime }
(.ofFormat "importing") #[]
}].toPArray' ++ traceState.traces
}
let profile ← Firefox.Profile.export mainModuleName.toString startTime traceState opts
IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile

return (s.commandState.env, !s.commandState.messages.hasErrors)

let opts := Language.Lean.internal.minimalSnapshots.set opts true
let ctx := { inputCtx with }
let processor := Language.Lean.process
let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel }) none ctx
let snaps := Language.toSnapshotTree snap
snaps.runAndReport opts jsonOutput

if let some ileanFileName := ileanFileName? then
let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
let ilean := { module := mainModuleName, references := ← references.toLspModuleRefs : Lean.Server.Ilean }
IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean

let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
-- TODO: remove default when reworking cmdline interface in Lean; currently the only case
-- where we use the environment despite errors in the file is `--stats`
let env := Language.Lean.waitForFinalEnv? snap |>.getD (← mkEmptyEnvironment)
pure (env, !hasErrors)
let some cmdState := Language.Lean.waitForFinalCmdState? snap
| return (← mkEmptyEnvironment, false)

if let some out := trace.profiler.output.get? opts then
let traceState := cmdState.traceState
let profile ← Firefox.Profile.export mainModuleName.toString startTime traceState opts
IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile

let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
pure (cmdState.env, !hasErrors)


end Lean.Elab
Loading

0 comments on commit a3d144a

Please sign in to comment.