Documentation

Lean.Server.FileWorker

For general server architecture, see README.md. For details of IPC communication, see Watchdog.lean. This module implements per-file worker processes.

File processing and requests+notifications against a file should be concurrent for two reasons:

To achieve these goals, elaboration is executed in a chain of tasks, where each task corresponds to the elaboration of one command. When the elaboration of one command is done, the next task is spawned. On didChange notifications, we search for the task in which the change occured. If we stumble across a task that has not yet finished before finding the task we're looking for, we terminate it and start the elaboration there, otherwise we start the elaboration at the task where the change occured.

Requests iterate over tasks until they find the command that they need to answer the request. In order to not block the main thread, this is done in a request task. If a task that the request task waits for is terminated, a change occured somewhere before the command that the request is looking for and the request sends a "content changed" error.

Asynchronous snapshot elaboration #

Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into hOut.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Instances For

      Use lake print-paths to compile dependencies on the fly and add them to LEAN_PATH. Compilation progress is reported to hOut via LSP notifications. Return the search path for source files.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        partial def Lean.Server.FileWorker.lakeSetupSearchPath.processStderr (lakePath : Lake.FilePath) (m : Lean.Server.DocumentMeta) (hOut : IO.FS.Stream) (args : Array String) (lakeProc : IO.Process.Child { toStdioConfig := { stdin := IO.Process.Stdio.null, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped }, cmd := lakePath.toString, args := args, cwd := none, env := #[], setsid := false }.toStdioConfig) (acc : String) :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Given the new document, updates editable doc state.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Requests here are handled synchronously rather than in the asynchronous RequestM.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[export lean_server_worker_main]
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For