search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
143 stars 31 forks source link

[limits] Allow to select interruption backend at startup. #685

Closed ejgallego closed 4 months ago

ejgallego commented 4 months ago

New command-line parameter to coq-lsp and fcc --int_backend={Coq,Mp} that allows to select the interruption backend between client-side polling (Coq) and memprof-limits (Mp).

We also avoid to document initialization, for what usually are read-queries.

Taken from #509 .