language server over stdio, emacs mode with repl and eglot wiring

1 files changed, 54 insertions, 0 deletions

diff --git a/docs/tooling.org b/docs/tooling.org
new file mode 100644
index 0000000..7fb0e8c
--- /dev/null
+++ b/docs/tooling.org
@@ -0,0 +1,54 @@
+#+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.