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
      @[reducible, inline]
      Equations
        Instances For
          @[reducible, inline]
          Equations
            Instances For
              @[reducible, inline]
              Equations
                Instances For

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

                  • imports : ImportMap

                    For every open file, the files that it imports.

                  • importedBy : ImportMap

                    For every open file, the files that it is imported by.

                  Instances For

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

                    Equations
                      Instances For

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

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

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

                                                    Equations
                                                      Instances For

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

                                                        Equations
                                                          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

                                                                  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
                                                                    Instances For
                                                                      Equations
                                                                        Instances For
                                                                          def Lean.Server.Watchdog.parseParams (paramType : Type) [FromJson paramType] (params : Json) :
                                                                          IO paramType
                                                                          Equations
                                                                            Instances For
                                                                              Equations
                                                                                Instances For
                                                                                  Equations
                                                                                    Instances For
                                                                                      Equations
                                                                                        Instances For
                                                                                          Equations
                                                                                            Instances For
                                                                                              Equations
                                                                                                Instances For
                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      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
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                              Instances For
                                                                                                                @[export lean_server_watchdog_main]
                                                                                                                Equations
                                                                                                                  Instances For