feat: basic `#lang`

[Kha]

Makes the entire Lean frontend substitutable with a custom implementation, directly inspired by Racket #lang.

This is an early proof of concept; as a basis for design discussions, it shows what changes are necessary but not necessarily yet the best way to do them. The best place to look at right now probably is the minimal example Hello. TODO: more extensive examples. Actually providing a nice API for implementing languages is an important but separate topic that should be looked at after these foundations have been nailed!

Includes:

• #3014

Major design changes that should be reviewed, and other unclear points:

• [ ] Handling of module dependencies. We need this information both in a language processor itself in order to do the import as well as in the build system in order to construct the build graph.
  • current status: in the build system (via Lean.parseImports'), we only respect dependencies of the form

  (#lang dep1)?
  import dep2
  import dep3
  ...
  

  i.e. only Lean-like headers. This might be okay for a first version. In the #lang processor, we do not actually run lake setup-file for dep1 yet so it only works if the #lang is already built.
  • general solution: not completely clear to me yet. Lake should first parse the #lang directive and make sure that the #lang is already built, then it could run a #lang-aware lean --deps on the file to retrieve further dependencies. The overhead can be avoided by special-casing built-in #langs and/or caching.
• [ ] #lang LSP request handling. Each language has custom types (and logic) for handling request so I have parameterized RequestM by the type of the root snapshot (parameterizing by the full Language would also work but seemed unnecessary). There is a new abbrev LeanRequestM replacing the old type.
  • Moved handleWaitForDiagnostics to the file worker as it is a very special request handler, the only one that wants access to the reporter task.
  • The registry of request handlers cannot be a global IO.Ref anymore with this change, so there is e.g. a new leanLspRequestHandlers IO.Ref that is explicitly passed to e.g. registerLspRequestHandler.
  • The watchdog uses the registry of request handlers in order to invoke RequestHandler.fileSource for routing requests to the correct worker. It now explicitly uses the registry of Lean handlers for this, which should be fine in practice, but it would be nicer to separate the concerns of translating a request to a file path, which is #lang-agnostic, and handling the request in the worker.
  • TODO: find a nicer module structure for generic and Lean-specific request handling
  • TODO: Should srcSearchPath remain in the generic RequestContext? Its handling also affects how the only missing request handler handleImportCompletionRequest should be reimplemented as it's the only Lean request that must not wait on the search path. I believe these concerns should be moved into LeanRequestM and import completion should be a regular handler.
  • TODO: code actions and widgets are currently limited to the Lean language, would require similar generalization
• [ ] TODO: Currently the inner language has to parse and skip the #lang directive itself as it is only given a ParserInputContext. It should be provided with a parsing start position as well. /cc @david-christiansen
• [ ] TODO: Should there be #lang shortcuts? E.g. #lang Lean.CS automatically resolves to #lang Lean.Lang.Lean.CS

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-20 16:42:29)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. (2024-01-29 16:59:11)

[david-christiansen]

I found when testing this branch that the language module isn't automatically rebuilt. That is, if I change the definition of the #lang in one buffer, save the file, then go back to the client file's buffer and say "restart file", the changed language definition is not used. Running lake build fixes it.