Documentation

Lean.Server.Watchdog

For general server architecture, see README.md. This module implements the watchdog process.

Watchdog state #

Most LSP clients only send us file diffs, so to facilitate sending entire file contents to freshly restarted workers, the watchdog needs to maintain the current state of each file. It can also use this state to detect changes to the header and thus restart the corresponding worker, freeing its imports.

TODO(WN): We may eventually want to keep track of approximately (since this isn't knowable exactly) where in the file a worker crashed. Then on restart, we tell said worker to only parse up to that point and query the user about how to proceed (continue OR allow the user to fix the bug and then continue OR ..). Without this, if the crash is deterministic, users may be confused about why the server seemingly stopped working for a single file.

Watchdog <-> worker communication #

The watchdog process and its file worker processes communicate via LSP. If the necessity arises, we might add non-standard commands similarly based on JSON-RPC. Most requests and notifications are forwarded to the corresponding file worker process, with the exception of these notifications:

Moreover, we don't implement the full protocol at this level:

Watchdog <-> client communication #

The watchdog itself should implement the LSP standard as closely as possible. However we reserve the right to add non-standard extensions in case they're needed, for example to communicate tactic state.

Events that worker-specific tasks signal to the main thread.

Instances For
    Instances For
      • crashed: Array Lean.JsonRpc.MessageLean.Server.Watchdog.CrashOriginLean.Server.Watchdog.WorkerState

        The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker and when reading a request reply. In the latter case, the forwarding task terminates and delegates a crashed event to the main task. Then, in both cases, the file worker has its state set to crashed and requests that are in-flight are errored. Upon receiving the next packet for that file worker, the file worker is restarted and the packet is forwarded to it. If the crash was detected while writing a packet, we queue that packet until the next packet for the file worker arrives.

      • running: Lean.Server.Watchdog.WorkerState
      Instances For
        Instances For
          Equations
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Global import data for all open files managed by this watchdog.

              Instances For

                Updates d with the new set of imports for the file uri.

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

                  Sets the imports of uri in d to the empty set.

                  Equations
                  • d.eraseImportsOf uri = d.update uri
                  Instances For
                    Instances For
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              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

                                    Updates the global import data with the import closure provided by the file worker after it successfully processed its header.

                                    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

                                              Tries to write a message, sets the state of the FileWorker to crashed if it does not succeed and restarts the file worker if the crashed flag was already set. Just logs an error if there is no FileWorker at this uri. Messages that couldn't be sent can be queued up via the queueFailedMessage flag and will be discharged after the FileWorker is restarted.

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

                                                Sends a notification to the file worker identified by uri that its dependency staleDependency is out-of-date.

                                                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

                                                      Used in CallHierarchyItem.data? to retain all the data needed to quickly re-identify the call hierarchy item.

                                                      Instances For

                                                        Extracts the CallHierarchyItemData from item.data? and returns none if this is not possible.

                                                        Equations
                                                        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
                                                                  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

                                                                          When a file is saved, notifies all file workers for files that depend on this file that this specific import is now stale so that the file worker can issue a diagnostic asking users to restart the file.

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

                                                                                                    Starts loading .ileans present in the search path asynchronously in an IO task. This ensures that server startup is not blocked by loading the .ileans. In return, while the .ileans are being loaded, users will only get incomplete results in requests that need references.

                                                                                                    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_watchdog_main]
                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For