#+TITLE: Tooling

* About

This document describes the developer tooling around Sol: the
language server, the Emacs mode, and the REPL. The tooling reuses
the pipeline instead of imitating it; the checker the editor runs is
the checker the runtime runs.

* The language server

=sol lsp= speaks the Language Server Protocol over stdio. It has one
capability, the load bearing one: diagnostics. On every open and
every change the document goes through the same parse and the same
admission the loader performs, so a recursive rule without a
decrease witness, a fact violating its schema, an unknown relation
or a failed membership criterion appears in the editor at typing
time, with the same message the runtime would give. Parse errors
carry line and column; admission errors anchor at the top of the
file until the loader learns source locations.

The server is hand rolled JSON-RPC on yojson, in =bin/lsp.ml=. It
answers =initialize=, tracks documents through full-content sync,
publishes diagnostics, clears them on close, and answers unsupported
requests with method-not-found instead of silence.

* The Emacs mode

=editors/emacs/sol-mode.el= provides:

- highlighting per token category under the delimiter law:
  directives, combinators, structural and generic labels, relation
  heads, variables, references (=#Name=), literals;
- =%= line comments, bracket pairing for =[]= ={}= =()=, prettify
  of =:and= =:or= =:not= into their logical glyphs;
- imenu over Relations, Rules and Queries, and defun navigation
  across top level forms;
- =run-sol= (C-c C-z), an inferior REPL through comint;
  =sol-send-line= (C-c C-l) sends the statement at point;
  =sol-run-buffer= (C-c C-k) runs the file and shows answers in a
  compilation buffer;
- eglot wiring: with eglot enabled, =sol lsp= starts automatically
  for =sol-mode= buffers.

Install by adding the directory to =load-path= and requiring
=sol-mode=; =.sol= files open in the mode automatically.

* The REPL

=sol= with no arguments reads one statement per line. Declarations
and facts accumulate; =Query expression: ...= runs against
everything accumulated so far. A rejected statement reports its
error and changes nothing. The prompt flushes eagerly so the REPL
works under comint and pipes.