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 occurred. 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 occurred.

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 occurred somewhere before the command that the request is looking for and the request sends a "content changed" error.

  • lastRefreshTimestamp : Nat
  • successiveRefreshAttempts : Nat
Instances For
    Instances For
      Instances For
        Equations
          Instances For

            Asynchronous snapshot elaboration #

            Type of state stored in Snapshot.Diagnostics.cacheRef?.

            See also section "Communication" in Lean/Server/README.md.

            Instances For
              @[reducible, inline]
              Equations
                Instances For
                  Instances For
                    Instances For
                      @[reducible, inline]
                      Equations
                        Instances For

                          Callback from Lean language processor after parsing imports that requests necessary information from Lake for processing imports.

                          Equations
                            Instances For

                              Creates an LSP message output channel along with a reader that sends out read messages on the output FS stream after discarding outdated notifications. This is the only component of the worker with access to the output stream, so we can synchronize messages from parallel elaboration tasks here.

                              Equations
                                Instances For
                                  def Lean.Server.FileWorker.sendServerRequest (paramType : Type u_1) [ToJson paramType] (responseType : Type) [FromJson responseType] [Inhabited responseType] (ctx : WorkerContext) (method : String) (param : paramType) :
                                  Equations
                                    Instances For

                                      Given the new document, updates editable doc state.

                                      Equations
                                        Instances For

                                          Received from the watchdog when a dependency of this file is detected as being stale. Issues a sticky diagnostic to the client that it should run "Restart File".

                                          Equations
                                            Instances For

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

                                              def Lean.Server.FileWorker.parseParams (paramType : Type) [FromJson paramType] (params : Json) :
                                              WorkerM paramType
                                              Equations
                                                Instances For
                                                  Equations
                                                    Instances For
                                                      Equations
                                                        Instances For
                                                          Equations
                                                            Instances For
                                                              Equations
                                                                Instances For
                                                                  Equations
                                                                    Instances For
                                                                      @[export lean_server_worker_main]
                                                                      Equations
                                                                        Instances For