(
+ "$/coq/serverStatus"
+);
+
+// We should likely have one class per item, but not a big deal yet
+export class CoqLanguageStatus {
+ // Checking and what
+ status: LanguageStatusItem;
+ // Version info
+ version: LanguageStatusItem;
+ // Root: one or multiple, to be done soon
+ // root : LanguageStatusItem;
+
+ constructor(
+ version: CoqServerVersion,
+ status: CoqServerStatus,
+ lazy_mode: boolean
+ ) {
+ // Version info
+ this.version = languages.createLanguageStatusItem(
+ "coq.version",
+ CoqSelector.all
+ );
+ this.version.name = "Version";
+
+ // Server status
+ this.status = languages.createLanguageStatusItem(
+ "coq.status",
+ CoqSelector.all
+ );
+ this.status.name = "Running Status";
+
+ // this.status.command = "start continous toogle continous";
+ // root = languages.createLanguageStatusItem("coq.root", CoqSelector.all);
+
+ this.updateVersion(version);
+ this.updateStatus(status, lazy_mode);
+ }
+
+ updateVersion(version: CoqServerVersion) {
+ this.version.text = `coq-lsp ${version.coq_lsp}`;
+ this.version.detail = `Coq ${version.coq}, OCaml ${version.ocaml}`;
+ }
+
+ updateStatus(status: CoqServerStatus, lazy_mode: boolean) {
+ let command = lazy_mode
+ ? {
+ title: "Enable Continous Mode",
+ command: "coq-lsp.toggle_mode",
+ }
+ : {
+ title: "Enable On-Demand Mode",
+ command: "coq-lsp.toggle_mode",
+ args: true,
+ };
+
+ let status_name = lazy_mode ? "On-demand" : "Continous";
+
+ if (status.status == "Busy") {
+ this.status.busy = true;
+ this.status.text = `coq-lsp: Checking ${status.modname}`;
+ this.status.detail = `set mode`;
+ this.status.command = command;
+ this.status.severity = LanguageStatusSeverity.Information;
+ } else if (status.status == "Idle") {
+ // Idle
+ this.status.busy = false;
+ this.status.text = `coq-lsp: Idle (${status_name} |${status.mem})`;
+ this.status.detail = "";
+ this.status.command = command;
+ this.status.severity = LanguageStatusSeverity.Information;
+ } else if (status.status == "Stopped") {
+ this.status.busy = false;
+ this.status.text = `Stopped`;
+ this.status.detail = "";
+ this.status.command = { title: "Start Server", command: "coq-lsp.start" };
+ this.status.severity = LanguageStatusSeverity.Error;
+ }
+ }
+
+ dispose() {
+ this.status.dispose();
+ this.version.dispose();
+ // root.dispose();
+ }
+}
+
+export const defaultVersion: CoqServerVersion = {
+ coq: "N/A",
+ ocaml: "N/A",
+ coq_lsp: "N/A",
+};
+export const defaultStatus: CoqServerStatus = { status: "Idle", mem: "" };
diff --git a/editor/code/views/info/Goals.tsx b/editor/code/views/info/Goals.tsx
index 531b77da..1b479e69 100644
--- a/editor/code/views/info/Goals.tsx
+++ b/editor/code/views/info/Goals.tsx
@@ -61,16 +61,24 @@ function Goal({ goal, idx, open }: GoalP) {
}
});
+ // XXX: We want to add an option for this that can be set interactively
+ let show_goal_on_header = false;
+
+ let gtyp = (
+
+
+
+ );
+
return (
+ {show_goal_on_header ? "" : gtyp}
-
-
-
+ {show_goal_on_header ? gtyp : ""}
);
}
@@ -141,7 +149,7 @@ function StackGoals({ idx, stack }: StackSummaryP) {
diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md
index c3e303b4..8da3b04c 100644
--- a/etc/doc/PROTOCOL.md
+++ b/etc/doc/PROTOCOL.md
@@ -400,3 +400,45 @@ client.
#### Changelog
- v0.1.9: First public documentation.
+
+### Server Version Notification
+
+The server will send the `$/coq/serverVersion` notification to inform
+the client about `coq-lsp` version specific info.
+
+The parameters are:
+```typescript
+export interface CoqServerVersion {
+ coq: string;
+ ocaml: string;
+ coq_lsp: string;
+}
+```
+
+#### Changelog
+
+- v0.1.9: First public documentation.
+
+### Server Status Notification
+
+The server will send the `$/coq/serverStatus` notification to inform
+the client of checking status (start / end checking file)
+
+The parameters are:
+```typescript
+
+export interface CoqBusyStatus {
+ status: "Busy";
+ modname: string;
+}
+
+export interface CoqIdleStatus {
+ status: "Idle" | "Stopped";
+}
+
+export type CoqServerStatus = CoqBusyStatus | CoqIdleStatus;
+```
+
+#### Changelog
+
+- v0.1.9: First public documentation.
diff --git a/etc/doc/USER_MANUAL.md b/etc/doc/USER_MANUAL.md
index eeaa51e2..bed0f86d 100644
--- a/etc/doc/USER_MANUAL.md
+++ b/etc/doc/USER_MANUAL.md
@@ -39,10 +39,15 @@ facilities. In VSCode, these settings can be usually displayed in the
disables some useful features such as `documentSymbol` as they can
only be implemented by checking the full file.
- This mode provides the `check_on_scroll` option, which improves
+ This mode can use the `check_on_scroll` option, which improves
latency by telling `coq-lsp` to check eagerly what is on view on
user's screen.
+Users can change between on-demand/continuous mode by clicking on the
+"Coq language status" item in the bottom right corner for VSCode. We
+recommend pinning the language status item to see server status in
+real-time.
+
### Goal display
By default, `coq-lsp` will follow cursor and show goals at cursor
@@ -79,7 +84,24 @@ not fully completed. Also, you can work with bullets and `coq-lsp`
will automatically admit unfinished ones, so you can follow the
natural proof structure.
-## Settings
+### Server Status
+
+
+
+### Embedded Markdown and LaTeX documents
+
+`coq-lsp` supports checking of TeX and Markdown document with embedded
+Coq inside. As of today, to enable this feature you must:
+
+- **markdown**: open a file with `.mv` extension, `coq-lsp` will
+ recognize code blocks starting with ````coq`.
+- **TeX**: open a file with `.lv` extension, `coq-lsp` will recognize
+ code blocks delimited by `\begin{coq} ... \end{coq}`
+
+As of today, delimiters are expected at the beginning of the line,
+don't hesitate to request for further changes based on this feature.
+
+## Coq LSP Settings
### Goal display
@@ -91,7 +113,21 @@ A setting to have `coq-lsp` check documents continuously exists.
## Memory management
-## Advanced: Multiple workspaces
+You can tell the server to free up memory with the "Coq LSP: Free
+memory" command.
+
+## Advanced: Multiple Workspaces
+
+`coq-lsp` does support projects that combine multiple Coq project
+roots in a single workspace. That way, one can develop on several
+distinct Coq developments seamlessly.
+
+To enable this, use the "Add Folder" option in VSCode, where each root
+must be a folder containing a `_CoqProject` file.
+
+Check the example at
+[../../examples/multiple_workspaces/](../../examples/multiple_workspaces/)
+to see it in action!
## Interrupting coq-lsp
@@ -119,10 +155,13 @@ on Coq <= 8.19 do need to install a version of Coq with the backported
fixes. See the information about Coq upstream bugs in the README for
more information about available branches.
+`coq-lsp` will reject to enable the new interruption mode by default
+on Coq < 8.20 unless the `lsp` Coq branch version is detected.
+
## Advanced incremental tricks
You can use the `Reset $id` and `Back $steps` commands to isolate
-parts of the document from each others in terms of rechecking.
+parts of the document from each other in terms of rechecking.
For example, the command `Reset $id` will make the parts of the
document after it use the state before the node `id` was found. Thus,
diff --git a/etc/img/on_demand.gif b/etc/img/on_demand.gif
new file mode 100644
index 00000000..8ed14f48
Binary files /dev/null and b/etc/img/on_demand.gif differ
diff --git a/etc/release_notes/0.1.9.md b/etc/release_notes/0.1.9.md
new file mode 100644
index 00000000..694d7776
--- /dev/null
+++ b/etc/release_notes/0.1.9.md
@@ -0,0 +1,255 @@
+Dear all,
+
+We are happy to announce the 0.1.9 release of `coq-lsp`.
+
+This release brings many new features and fixes, in particular:
+
+- New on-demand checking mode: `coq-lsp` can now check files on
+ demand, either by following the goals requested, or by following the
+ current viewport of your editor. Combined with the new keybinding
+ `M-n/M-p` for moving between Coq sentences, this provides a mode
+ similar to the usual one in Proof General. Additionally, we now show
+ real-time server status and checking information in the VSCode
+ language status area.
+
+- New interruption support using `memprofs-limits` (only in OCaml
+ 4). This solves all known cases of the server hanging.
+ (By E. J. Gallego Arias, thanks to Guillaume Munch-Maccagnoni and
+ Alex Sanchez-Stern).
+
+- `petanque`: a new server built on top of Flèche specifically
+ targeted at high-throughput low-latency reinforcement learning
+ applications. A subset of `petanque` has been experimentally
+ embedded into LSP for profit of extensions. (By E. J. Gallego
+ Arias, Guillaume Baudart, and Laetitia Teodorescu; thanks to Alex
+ Sanchez-Stern).
+
+- New heatmap feature to detect execution time hotspots in your Coq
+ documents, by Ali Caglayan; plus many more improvements and fixes
+ w.r.t. performance monitoring.
+
+- Coq meta commands `Reset` / `Reset Inital` and `Back` are supported,
+ together with the incremental checking engine they do provide some
+ interesting document splitting and isolation features.
+
+- New user manual with some information on how to start with `coq-lsp`
+
+- `coq-lsp` will now recognize literate LaTeX Coq files that end in
+ `.v.tex` or `.lv` and allow interacting with the Coq code inside
+ `\begin{coq}/\end{coq}` blocks.
+
+- Improved support for VSCode Live Share; full support requires
+ approval from Microsoft, please see below if you are interested in
+ helping with this.
+
+- New `Free Memory` server command.
+
+- Server settings are now updated on the fly when edited in VSCode.
+
+- Locations are now stored in the server in protocol format, this
+ should solve some Unicode issues present in previous versions
+ (by E. J. Gallego Arias and Leo Stefanesco).
+
+- Many improvements to both client and server plugin API, including a
+ new client extension API by E. J. Gallego Arias and Bhakti Shah.
+
+This version should be quite usable for a large majority of users, we
+encourage you to test it!
+
+Please see the detailed Changelog below. We have added to the README a
+list of tools using `coq-lsp` that may be of your interest.
+
+We'd like to thank to all the contributors and bug reporters for their
+work. Contributions, bug reports, and feedback over `coq-lsp` are much
+welcome, get in touch with us at GitHub or Zulip if you have questions
+or comments.
+
+`coq-lsp` is compatible with Coq 8.17-8.20. The `fcc` compiler has
+been ported back to 8.11, for the benefit of some SerAPI users.
+
+## Live Share support
+
+If you are interesting in seeing VSCode Live Share support, please go
+to this issue and click the "Thumbs Up" icon at end of the first
+comment:
+
+https://github.com/microsoft/live-share/issues/5046
+
+This will help MS developers prioritizing support based on number of
+demands. Please, _don't comment_ on the issue as this would create
+load for MS developers, unless you have some feedback about the
+technical implementation points
+
+Full Changelog
+==============
+
+ - Added new heatmap feature allowing timing data to be seen in the
+ editor. Can be enabled with the `Coq LSP: Toggle heatmap`
+ comamnd. Can be configured to show memory usage. Colors and
+ granularity are configurable. (@Alizter and @ejgallego, #686,
+ grants #681).
+ - new option `show_loc_info_on_hover` that will display parsing debug
+ information on hover; previous flag was fixed in code, which is way
+ less flexible. This also fixes the option being on in 0.1.8 by
+ mistake (@ejgallego, #588)
+ - hover plugins can now access the full document, this is convenient
+ for many use cases (@ejgallego, #591)
+ - fix hover position computation on the presence of Utf characters
+ (@ejgallego, #597, thanks to Pierre Courtieu for the report and
+ example, closes #594)
+ - fix activation bug that prevented extension activation for `.mv`
+ files, see discussion in the issues about the upstream policy
+ (@ejgallego @r3m0t, #598, cc #596, reported by Théo Zimmerman)
+ - require VSCode >= 1.82 in package.json . Our VSCode extension uses
+ `vscode-languageclient` 9 which imposes this. (@ejgallego, #599,
+ thanks to Théo Zimmerman for the report)
+ - `proof/goals` request: new `mode` parameter, to specify goals
+ after/before sentence display; renamed `pretac` to `command`, as to
+ provide official support for speculative execution (@ejgallego, #600)
+ - fix some cases where interrupted computations where memoized
+ (@ejgallego, #603)
+ - [internal] Flèche [Doc.t] API will now absorb errors on document
+ update and creation into the document itself. Thus, a document that
+ failed to create or update is still valid, but in the right failed
+ state. This is a much needed API change for a lot of use cases
+ (@ejgallego, #604)
+ - support OCaml 5.1.x (@ejgallego, #606)
+ - update progress indicator correctly on End Of File (@ejgallego,
+ #605, fixes #445)
+ - [plugins] New `astdump` plugin to dump AST of files into JSON and
+ SEXP (@ejgallego, #607)
+ - errors on save where not properly caught (@ejgallego, #608)
+ - switch default of `goal_after_tactic` to `true` (@Alizter,
+ @ejgallego, cc: #614)
+ - error recovery: Recognize `Defined` and `Admitted` in lex recovery
+ (@ejgallego, #616)
+ - completion: correctly understand UTF-16 code points on completion
+ request (Léo Stefanesco, #613, fixes #531)
+ - don't trigger the goals window in general markdown buffer
+ (@ejgallego, #625, reported by Théo Zimmerman)
+ - allow not to postpone full document requests (#626, @ejgallego)
+ - new configuration value `check_only_on_request` which will delay
+ checking the document until a request has been made (#629, cc: #24,
+ @ejgallego)
+ - fix typo on package.json configuration section (@ejgallego, #645)
+ - be more resilient with invalid _CoqProject files (@ejgallego, #646)
+ - support for Coq 8.16 has been abandoned due to lack of dev
+ resources (@ejgallego, #649)
+ - new option `--no_vo` for `fcc`, which will skip the `.vo` saving
+ step. `.vo` saving is now an `fcc` plugins, but for now, it is
+ enabled by default (@ejgallego, #650)
+ - depend on `memprof-limits` on OCaml 4.x (@ejgallego, #660)
+ - bump minimal OCaml version to 4.12 due to `memprof-limits`
+ (@ejgallego, #660)
+ - monitor all Coq-level calls under an interruption token
+ (@ejgallego, #661)
+ - interpret require thru our own custom execution env-aware path
+ (@bhaktishh, @ejgallego, #642, #643, #644)
+ - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
+ goals from a document (@ejgallego @gbdrt, #619)
+ - new trim command (both in the server and in VSCode) to liberate
+ space used in the cache (@ejgallego, #662, fixes #367 cc: #253 #236
+ #348)
+ - fix Coq performance view display (@ejgallego, #663, regression in
+ #513)
+ - allow more than one input position in `selectionRange` LSP call
+ (@ejgallego, #667, fixes #663)
+ - new VSCode commands to allow to move one sentence backwards /
+ forward, this is particularly useful when combined with lazy
+ checking mode (@ejgallego, #671, fixes #263, fixes #580)
+ - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
+ are now bound by default to `Alt + N` / `Alt + P` keybindings
+ (@ejgallego, #718)
+ - change diagnostic `extra` field to `data`, so we now conform to the
+ LSP spec, include the data only when the `send_diags_extra_data`
+ server-side option is enabled (@ejgallego, #670)
+ - include range of full sentence in error diagnostic extra data
+ (@ejgallego, #670 , thanks to @driverag22 for the idea, cc: #663).
+ - The `coq-lsp.pp_type` VSCode client option now takes effect
+ immediately, no more need to restart the server to get different
+ goal display formats (@ejgallego, #675)
+ - new public VSCode extension API so other extensions can perform
+ actions when the user request the goals (@ejgallego, @bhaktishh,
+ #672, fixes #538)
+ - Support Visual Studio Live Share URIs better (`vsls://`), in
+ particular don't try to display goals if the URI is VSLS one
+ (@ejgallego, #676)
+ - New `InjectRequire` plugin API for plugins to be able to instrument
+ the default import list of files (@ejgallego @corwin-of-amber,
+ #679)
+ - Add `--max_errors=n` option to `fcc`, this way users can set
+ `--max_errors=0` to imitate `coqc` behavior (@ejgallego, #680)
+ - Fix `fcc` exit status when checking terminates with fatal errors
+ (@ejgallego, @Alizter, #680)
+ - Fix install to OPAM switches from `main` branch (@ejgallego, #683,
+ fixes #682, cc #479 #488, thanks to @Hazardouspeach for the report)
+ - New `--int_backend={Coq,Mp}` command line parameter to select the
+ interruption method for Coq (@ejgallego, #684)
+ - Update `package-lock.json` for latest bugfixes (@ejgallego, #687)
+ - Update Nix flake enviroment (@Alizter, #684 #688)
+ - Update `prettier` (@Alizter @ejgallego, #684 #688)
+ - Store original performance data in the cache, so we now display the
+ original timing and memory data even for cached commands (@ejgallego, #693)
+ - Fix type errors in the Performance Data Notifications (@ejgallego,
+ @Alizter, #689, #693)
+ - Send performance performance data for the full document
+ (@ejgallego, @Alizter, #689, #693)
+ - Better types `coq/perfData` call (@ejgallego @Alizter, #689)
+ - New server option to enable / disable `coq/perfData` (@ejgallego, #689)
+ - New client option to enable / disable `coq/perfData` (@ejgallego, #717)
+ - The `coq-lsp.document` VSCode command will now display the returned
+ JSON data in a new editor (@ejgallego, #701)
+ - Update server settings on the fly when tweaking them in VSCode.
+ Implement `workspace/didChangeConfiguration` (@ejgallego, #702)
+ - [Coq API] Add functions to retrieve list of declarations done in
+ .vo files (@ejallego, @eytans, #704)
+ - New `petanque` API to interact directly with Coq's proof
+ engine. (@ejgallego, @gbdrt, Laetitia Teodorescu #703, thanks to
+ Alex Sanchez-Stern for many insightful feedback and testing)
+ - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
+ to perform proof search and more (@ejgallego, @gbdrt, #705)
+ - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
+ #697)
+ - Always dispose UI elements. This should improve some strange
+ behaviors on extension restart (@ejgallego, #708)
+ - Support Coq meta-commands (Reset, Reset Initial, Back) They are
+ actually pretty useful to hint the incremental engine to ignore
+ changes in some part of the document (@ejgallego, #709)
+ - JSON-RPC library now supports all kind of incoming messages
+ (@ejgallego, #713)
+ - New `coq/viewRange` notification, from client to server, than hints
+ the scheduler for the visible area of the document; combined with
+ the new lazy checking mode, this provides checking on scroll, a
+ feature inspired from Isabelle IDE (@ejgallego, #717)
+ - Have VSCode wait for full LSP client shutdown on server
+ restart. This fixes some bugs on extension restart (finally!)
+ (@ejgallego, #719)
+ - Center the view if cursor goes out of scope in
+ `sentenceNext/sentencePrevious` (@ejgallego, #718)
+ - Switch Flèche range encoding to protocol native, this means UTF-16
+ code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620,
+ #621)
+ - Give `Goals` panel focus back if it has lost it (in case of
+ multiple panels in the second viewColumn of Vscode) whenever
+ user navigates proofs (@Alidra @ejgallego, #722, #725)
+ - `fcc`: new option `--diags_level` to control whether Coq's notice
+ and info messages appear as diagnostics
+ - Display the continous/on-request checking mode in the status bar,
+ allow to change it by clicking on it (@ejgallego, #721)
+ - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
+ #611)
+ - Don't show types of un-expanded goals. We should add an option for
+ this, but we don't have the cycles (@ejgallego, #730, workarounds
+ #525 #652)
+ - Support for `.lv / .v.tex` TeX files with embedded Coq code
+ (@ejgallego, #727)
+ - Don't expand bullet goals at previous levels by default
+ (@ejgallego, @Alizter, #731 cc #525)
+ - [petanque] Return basic goal information after `run_tac`, so we
+ avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
+ #733)
+ - [coq] Add support for reading glob files metadata (@ejgallego,
+ #735)
+ - [petanque] Return extra premise information: file name, position,
+ raw_text, using the above support for reading .glob files
+ (@ejgallego, #735)
diff --git a/examples/chicken.jpg b/examples/chicken.jpg
index 0028a92e..7488cd2f 100644
Binary files a/examples/chicken.jpg and b/examples/chicken.jpg differ
diff --git a/examples/goals.v b/examples/goals.v
index edc3834e..7ebb2d43 100644
--- a/examples/goals.v
+++ b/examples/goals.v
@@ -52,4 +52,16 @@ About baaar.
Lemma err_bullet: Type.
_.
_
-Qed.
\ No newline at end of file
+Qed.
+
+(* Case from https://github.com/ejgallego/coq-lsp/issues/525 *)
+Reset Initial.
+
+Inductive foo := a | b | c | d | e.
+
+Goal forall x y z w v : foo, Type.
+intros [].
+- intros [].
+ + intros [].
+ * intros [].
+ -- intros [].
\ No newline at end of file
diff --git a/examples/lists.lv b/examples/lists.lv
new file mode 100644
index 00000000..53b7d956
--- /dev/null
+++ b/examples/lists.lv
@@ -0,0 +1,82 @@
+\documentclass{article}
+
+\usepackage{listings}
+
+\lstdefinelanguage{Coq}
+ {morekeywords={Theorem, Definition}}
+
+\lstnewenvironment{coq}
+ {
+ \lstset{
+ language=Coq,
+ basicstyle=\ttfamily,
+ breaklines=true,
+ columns=fullflexible}
+ }
+ {
+ }
+
+\begin{document}
+
+\section{Welcome to Coq LSP}
+
+\begin{itemize}
+\item You can edit this document as you please
+\item Coq will recognize the code snippets as Coq
+\item You will be able to save the document and link to other documents soon
+\end{itemize}
+
+\begin{coq}
+From Coq Require Import List.
+Import ListNotations.
+\end{coq}
+
+\subsection{Here is a simple Proof about Lists}
+
+$$
+ \forall~x~l,
+ \mathsf{rev}(l \mathrel{++} [x]) = x \mathrel{::} (\mathsf{rev}~l)
+$$
+
+\begin{coq}
+Lemma rev_snoc_cons A :
+ forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l.
+Proof.
+ induction l.
+ - reflexivity.
+ - simpl. rewrite IHl. simpl. reflexivity.
+Qed.
+\end{coq}
+
+\subsection{Here is another proof depending on it}
+
+Try to update \emph{above} and \textbf{below}:
+
+\begin{coq}
+Theorem rev_rev A : forall (l : list A), rev (rev l) = l.
+Proof.
+ induction l.
+ - reflexivity.
+ - simpl. rewrite rev_snoc_cons. rewrite IHl.
+ reflexivity.
+Qed.
+\end{coq}
+
+Please edit your code here!
+
+\section{Here we do some lambda terms, because we can!}
+
+\begin{coq}
+Inductive term :=
+ | Var : nat -> term
+ | Abs : term -> term
+ | Lam : term -> term -> term.
+\end{coq}
+
+\end{document}
+
+
+%%% Local Variables:
+%%% mode: LaTeX
+%%% TeX-master: "lists"
+%%% End:
diff --git a/examples/lists.v.tex b/examples/lists.v.tex
new file mode 100644
index 00000000..53b7d956
--- /dev/null
+++ b/examples/lists.v.tex
@@ -0,0 +1,82 @@
+\documentclass{article}
+
+\usepackage{listings}
+
+\lstdefinelanguage{Coq}
+ {morekeywords={Theorem, Definition}}
+
+\lstnewenvironment{coq}
+ {
+ \lstset{
+ language=Coq,
+ basicstyle=\ttfamily,
+ breaklines=true,
+ columns=fullflexible}
+ }
+ {
+ }
+
+\begin{document}
+
+\section{Welcome to Coq LSP}
+
+\begin{itemize}
+\item You can edit this document as you please
+\item Coq will recognize the code snippets as Coq
+\item You will be able to save the document and link to other documents soon
+\end{itemize}
+
+\begin{coq}
+From Coq Require Import List.
+Import ListNotations.
+\end{coq}
+
+\subsection{Here is a simple Proof about Lists}
+
+$$
+ \forall~x~l,
+ \mathsf{rev}(l \mathrel{++} [x]) = x \mathrel{::} (\mathsf{rev}~l)
+$$
+
+\begin{coq}
+Lemma rev_snoc_cons A :
+ forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l.
+Proof.
+ induction l.
+ - reflexivity.
+ - simpl. rewrite IHl. simpl. reflexivity.
+Qed.
+\end{coq}
+
+\subsection{Here is another proof depending on it}
+
+Try to update \emph{above} and \textbf{below}:
+
+\begin{coq}
+Theorem rev_rev A : forall (l : list A), rev (rev l) = l.
+Proof.
+ induction l.
+ - reflexivity.
+ - simpl. rewrite rev_snoc_cons. rewrite IHl.
+ reflexivity.
+Qed.
+\end{coq}
+
+Please edit your code here!
+
+\section{Here we do some lambda terms, because we can!}
+
+\begin{coq}
+Inductive term :=
+ | Var : nat -> term
+ | Abs : term -> term
+ | Lam : term -> term -> term.
+\end{coq}
+
+\end{document}
+
+
+%%% Local Variables:
+%%% mode: LaTeX
+%%% TeX-master: "lists"
+%%% End:
diff --git a/examples/ltac2_simple.v b/examples/ltac2_simple.v
new file mode 100644
index 00000000..d8937f45
--- /dev/null
+++ b/examples/ltac2_simple.v
@@ -0,0 +1,6 @@
+From Ltac2 Require Import Ltac2.
+
+Goal True /\ True.
+ split; exact I.
+Qed.
+
diff --git a/examples/multiple_workspaces/README.md b/examples/multiple_workspaces/README.md
new file mode 100644
index 00000000..58ebebfc
--- /dev/null
+++ b/examples/multiple_workspaces/README.md
@@ -0,0 +1,42 @@
+# Multiple workspaces setup
+
+## How to run it:
+
+Try to load the `example.code-workspace` file in VSCode.
+
+You may need to compile the right `.vo` files for the imports to
+work. You can do that with the `Save VO command`; as of now, `coq-lsp`
+will require you do this before opening the depending files.
+
+`coq-lsp` will take care of this automatically in the next version,
+including the auto-update. You can also do:
+
+```sh
+$ coqc -R bar bar bar/barx.y
+$ coqc -R foo foo foo/foox.y
+```
+
+## `coq-lsp` workspace documentation
+
+One can add multiple folders or roots to a workspace — for instance
+via the "Add Folder to Workspace" command (or
+[alternatives](https://code.visualstudio.com/docs/editor/multi-root-workspaces#_adding-folders)).
+
+For each workspace added to a project, `coq-lsp` will try to configure
+it by searching for a `_CoqProject` file, then it will apply the
+options found there. In the near future, we will also detect
+`dune-project` files at the root too.
+
+`coq-lsp` does determine the workspace roots using the standard
+methods provided by the LSP protocol, in particular `wsFolders`,
+`rootURI`, and `rootPath` at initialiation, in this order; and by
+listening to the `workspace/didChangeWorkspaceFolders` notification
+after initialization.
+
+## Known problems
+
+When projects are using Coq plugins, `findlib` doesn't properly
+support having multiple roots in the same process. We are using a hack
+that seems to work (we reinitialize `findlib`), however the hack is
+very fragile; we should improve `findlib` upstream to support our use
+case.
diff --git a/examples/multiple_workspaces/bar/_CoqProject b/examples/multiple_workspaces/bar/_CoqProject
new file mode 100644
index 00000000..475f78d8
--- /dev/null
+++ b/examples/multiple_workspaces/bar/_CoqProject
@@ -0,0 +1 @@
+-R . bar
diff --git a/examples/multiple_workspaces/bar/barx.v b/examples/multiple_workspaces/bar/barx.v
new file mode 100644
index 00000000..5fcaa519
--- /dev/null
+++ b/examples/multiple_workspaces/bar/barx.v
@@ -0,0 +1,3 @@
+Definition x := 3.
+
+Print x.
diff --git a/examples/multiple_workspaces/bar/bary.v b/examples/multiple_workspaces/bar/bary.v
new file mode 100644
index 00000000..d2fabedf
--- /dev/null
+++ b/examples/multiple_workspaces/bar/bary.v
@@ -0,0 +1,3 @@
+From bar Require Import barx.
+
+Print x.
diff --git a/examples/multiple_workspaces/example.code-workspace b/examples/multiple_workspaces/example.code-workspace
new file mode 100644
index 00000000..e72e6f59
--- /dev/null
+++ b/examples/multiple_workspaces/example.code-workspace
@@ -0,0 +1,27 @@
+{
+ "folders": [
+ {
+ "path": "bar"
+ },
+ {
+ "path": "foo"
+ }
+ ],
+ "settings": {
+ "files.exclude": {
+ "**/*.vo": true,
+ "**/*.vok": true,
+ "**/*.vos": true,
+ "**/*.aux": true,
+ "**/*.glob": true,
+ "**/.git": true,
+ "**/.svn": true,
+ "**/.hg": true,
+ "**/CVS": true,
+ "**/.DS_Store": true,
+ "**/Thumbs.db": true,
+ "**/*.olean": true,
+ "out": false
+ }
+ }
+}
\ No newline at end of file
diff --git a/examples/multiple_workspaces/foo/_CoqProject b/examples/multiple_workspaces/foo/_CoqProject
new file mode 100644
index 00000000..35a0741d
--- /dev/null
+++ b/examples/multiple_workspaces/foo/_CoqProject
@@ -0,0 +1 @@
+-R . foo
diff --git a/examples/multiple_workspaces/foo/foox.v b/examples/multiple_workspaces/foo/foox.v
new file mode 100644
index 00000000..82ae5066
--- /dev/null
+++ b/examples/multiple_workspaces/foo/foox.v
@@ -0,0 +1,3 @@
+Definition x := 3.
+
+Print x.
\ No newline at end of file
diff --git a/examples/multiple_workspaces/foo/fooy.v b/examples/multiple_workspaces/foo/fooy.v
new file mode 100644
index 00000000..c80500f5
--- /dev/null
+++ b/examples/multiple_workspaces/foo/fooy.v
@@ -0,0 +1,3 @@
+From foo Require Import foox.
+
+Print x.
diff --git a/fleche/config.ml b/fleche/config.ml
index e8ee723e..2ad0b302 100644
--- a/fleche/config.ml
+++ b/fleche/config.ml
@@ -52,6 +52,8 @@ type t =
(** Experimental setting to check document lazily *)
; send_diags_extra_data : bool [@default false]
(** Send extra diagnostic data on the `data` diagnostic field. *)
+ ; send_serverStatus : bool [@default true]
+ (** Send server status client notification to the client *)
}
let default =
@@ -75,6 +77,7 @@ let default =
; send_diags = true
; check_only_on_request = false
; send_diags_extra_data = false
+ ; send_serverStatus = true
}
let v = ref default
diff --git a/fleche/contents.ml b/fleche/contents.ml
index f43687ac..bbd73b59 100644
--- a/fleche/contents.ml
+++ b/fleche/contents.ml
@@ -57,6 +57,24 @@ module Markdown = struct
String.concat "\n" lines
end
+module LaTeX = struct
+ let gen l = String.make (String.length l) ' '
+
+ let rec tex_map_lines coq l =
+ match l with
+ | [] -> []
+ | l :: ls ->
+ (* opening vs closing a markdown block *)
+ let code_marker = if coq then "\\end{coq}" else "\\begin{coq}" in
+ if String.equal code_marker l then gen l :: tex_map_lines (not coq) ls
+ else (if coq then l else gen l) :: tex_map_lines coq ls
+
+ let process text =
+ let lines = String.split_on_char '\n' text in
+ let lines = tex_map_lines false lines in
+ String.concat "\n" lines
+end
+
module WaterProof = struct
open Fleche_waterproof.Json
@@ -124,6 +142,7 @@ let process_contents ~uri ~raw =
let ext = Lang.LUri.File.extension uri in
match ext with
| ".v" -> R.Ok raw
+ | ".lv" | ".tex" -> R.Ok (LaTeX.process raw)
| ".mv" -> R.Ok (Markdown.process raw)
| ".wpn" -> WaterProof.process raw
| _ -> R.Error "unknown file format"
diff --git a/fleche/io.ml b/fleche/io.ml
index 0a4c34f1..1f376f2b 100644
--- a/fleche/io.ml
+++ b/fleche/io.ml
@@ -19,6 +19,8 @@ module CallBack = struct
; fileProgress :
uri:Lang.LUri.File.t -> version:int -> Progress.Info.t list -> unit
; perfData : uri:Lang.LUri.File.t -> version:int -> Perf.t -> unit
+ ; serverVersion : ServerInfo.Version.t -> unit
+ ; serverStatus : ServerInfo.Status.t -> unit
}
let default =
@@ -27,6 +29,8 @@ module CallBack = struct
; diagnostics = (fun ~uri:_ ~version:_ _ -> ())
; fileProgress = (fun ~uri:_ ~version:_ _ -> ())
; perfData = (fun ~uri:_ ~version:_ _ -> ())
+ ; serverVersion = (fun _ -> ())
+ ; serverStatus = (fun _ -> ())
}
let cb = ref default
@@ -52,4 +56,6 @@ module Report = struct
io.CallBack.fileProgress ~uri ~version d
let perfData ~io ~uri ~version pd = io.CallBack.perfData ~uri ~version pd
+ let serverVersion ~io vi = io.CallBack.serverVersion vi
+ let serverStatus ~io st = io.CallBack.serverStatus st
end
diff --git a/fleche/io.mli b/fleche/io.mli
index fefc30ee..822c3710 100644
--- a/fleche/io.mli
+++ b/fleche/io.mli
@@ -23,6 +23,8 @@ module CallBack : sig
; fileProgress :
uri:Lang.LUri.File.t -> version:int -> Progress.Info.t list -> unit
; perfData : uri:Lang.LUri.File.t -> version:int -> Perf.t -> unit
+ ; serverVersion : ServerInfo.Version.t -> unit
+ ; serverStatus : ServerInfo.Status.t -> unit
}
val set : t -> unit
@@ -56,4 +58,7 @@ module Report : sig
val perfData :
io:CallBack.t -> uri:Lang.LUri.File.t -> version:int -> Perf.t -> unit
+
+ val serverVersion : io:CallBack.t -> ServerInfo.Version.t -> unit
+ val serverStatus : io:CallBack.t -> ServerInfo.Status.t -> unit
end
diff --git a/fleche/serverInfo.ml b/fleche/serverInfo.ml
new file mode 100644
index 00000000..85c8b8c4
--- /dev/null
+++ b/fleche/serverInfo.ml
@@ -0,0 +1,21 @@
+(************************************************************************)
+(* Coq Language Server Protocol *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *)
+(* Copyright 2019-202r Inria -- Dual License LGPL 2.1 / GPL3+ *)
+(* Written by: Emilio J. Gallego Arias *)
+(************************************************************************)
+
+module Version = struct
+ type t =
+ { coq : string
+ ; ocaml : string
+ ; coq_lsp : string
+ }
+end
+
+module Status = struct
+ type t =
+ | Stopped
+ | Idle of string (* memory use *)
+ | Running of string (* modname *)
+end
diff --git a/fleche/theory.ml b/fleche/theory.ml
index 2c25f7ef..1c79e714 100644
--- a/fleche/theory.ml
+++ b/fleche/theory.ml
@@ -244,8 +244,17 @@ end = struct
pending := pend_pop !pending;
None
| (None | Some _) as tgt ->
+ let uri_short =
+ Lang.LUri.File.to_string_file uri |> Filename.basename
+ in
let target = Option.default Doc.Target.End tgt in
+ Io.Report.serverStatus ~io (ServerInfo.Status.Running uri_short);
let doc = Doc.check ~io ~token ~target ~doc:handle.doc () in
+ let mem =
+ Format.asprintf "%a" Stats.pp_words
+ (Gc.((quick_stat ()).heap_words) |> Float.of_int)
+ in
+ Io.Report.serverStatus ~io (ServerInfo.Status.Idle mem);
let requests = Handle.update_doc_info ~handle ~doc in
if Doc.Completion.is_completed doc.completed then
Register.Completed.fire ~io ~token ~doc;
diff --git a/fleche/version.ml b/fleche/version.ml
index d9c0dd8d..ece862fa 100644
--- a/fleche/version.ml
+++ b/fleche/version.ml
@@ -12,6 +12,6 @@ type t = string
(************************************************************************)
(* UPDATE VERSION HERE *)
-let server = "0.1.9-dev"
+let server = "0.1.9"
(* UPDATE VERSION HERE *)
(************************************************************************)
diff --git a/lsp/base.ml b/lsp/base.ml
index 6bb2e8b5..4a84481e 100644
--- a/lsp/base.ml
+++ b/lsp/base.ml
@@ -107,7 +107,7 @@ module Message = struct
Response.Ok { id; result }
| Some error ->
let error = U.to_assoc error in
- let code = int_field "message" error in
+ let code = int_field "code" error in
let message = string_field "message" error in
let data = None in
Error { id; code; message; data }
@@ -138,6 +138,9 @@ module Message = struct
| Notification n -> Notification.to_yojson n
| Request r -> Request.to_yojson r
| Response r -> Response.to_yojson r
+
+ let notification n = Notification n
+ let response r = Response r
end
module ProgressToken : sig
diff --git a/lsp/base.mli b/lsp/base.mli
index e8570f57..3643ac11 100644
--- a/lsp/base.mli
+++ b/lsp/base.mli
@@ -72,6 +72,9 @@ module Message : sig
| Request of Request.t
| Response of Response.t
[@@deriving yojson]
+
+ val notification : Notification.t -> t
+ val response : Response.t -> t
end
(** Build request *)
diff --git a/lsp/jFleche.ml b/lsp/jFleche.ml
index cb8bf70f..7df22a2f 100644
--- a/lsp/jFleche.ml
+++ b/lsp/jFleche.ml
@@ -64,7 +64,7 @@ let mk_progress ~uri ~version processing =
FileProgress.to_yojson { FileProgress.textDocument; processing }
|> Yojson.Safe.Util.to_assoc
in
- Base.Notification.(make ~method_:"$/coq/fileProgress" ~params () |> to_yojson)
+ Base.Notification.make ~method_:"$/coq/fileProgress" ~params ()
module Message = struct
type 'a t =
@@ -141,4 +141,22 @@ let mk_perf ~uri ~version perf =
DocumentPerfData.(
to_yojson { textDocument; summary; timings } |> Yojson.Safe.Util.to_assoc)
in
- Base.Notification.(make ~method_:"$/coq/filePerfData" ~params () |> to_yojson)
+ Base.Notification.make ~method_:"$/coq/filePerfData" ~params ()
+
+module ServerVersion = struct
+ type t = [%import: Fleche.ServerInfo.Version.t] [@@deriving yojson]
+end
+
+let mk_serverVersion vi =
+ let params = ServerVersion.to_yojson vi |> Yojson.Safe.Util.to_assoc in
+ Base.Notification.make ~method_:"$/coq/serverVersion" ~params ()
+
+let mk_serverStatus (st : Fleche.ServerInfo.Status.t) =
+ let params =
+ match st with
+ | Stopped -> [ ("status", `String "Stopped") ]
+ | Idle mem -> [ ("status", `String "Idle"); ("mem", `String mem) ]
+ | Running modname ->
+ [ ("status", `String "Busy"); ("modname", `String modname) ]
+ in
+ Base.Notification.make ~method_:"$/coq/serverStatus" ~params ()
diff --git a/lsp/jFleche.mli b/lsp/jFleche.mli
index ba99218a..57a5091b 100644
--- a/lsp/jFleche.mli
+++ b/lsp/jFleche.mli
@@ -28,7 +28,7 @@ val mk_progress :
uri:Lang.LUri.File.t
-> version:int
-> Fleche.Progress.Info.t list
- -> Yojson.Safe.t
+ -> Base.Notification.t
module FileProgress : sig
type t =
@@ -99,4 +99,8 @@ module DocumentPerfData : sig
end
val mk_perf :
- uri:Lang.LUri.File.t -> version:int -> Fleche.Perf.t -> Yojson.Safe.t
+ uri:Lang.LUri.File.t -> version:int -> Fleche.Perf.t -> Base.Notification.t
+
+(* Server status notifications *)
+val mk_serverVersion : Fleche.ServerInfo.Version.t -> Base.Notification.t
+val mk_serverStatus : Fleche.ServerInfo.Status.t -> Base.Notification.t
diff --git a/lsp/jLang.ml b/lsp/jLang.ml
index e7f7f3ca..304b8c66 100644
--- a/lsp/jLang.ml
+++ b/lsp/jLang.ml
@@ -89,7 +89,7 @@ module Diagnostic = struct
_t_to_yojson { range; severity; message; data }
end
-let mk_diagnostics ~uri ~version ld : Yojson.Safe.t =
+let mk_diagnostics ~uri ~version ld : Base.Notification.t =
let diags = List.map Diagnostic.to_yojson ld in
let uri = Lang.LUri.File.to_string_uri uri in
let params =
@@ -98,5 +98,4 @@ let mk_diagnostics ~uri ~version ld : Yojson.Safe.t =
; ("diagnostics", `List diags)
]
in
- Base.Notification.(
- make ~method_:"textDocument/publishDiagnostics" ~params () |> to_yojson)
+ Base.Notification.make ~method_:"textDocument/publishDiagnostics" ~params ()
diff --git a/lsp/jLang.mli b/lsp/jLang.mli
index 73f2df3a..9772fea7 100644
--- a/lsp/jLang.mli
+++ b/lsp/jLang.mli
@@ -40,4 +40,7 @@ module Diagnostic : sig
end
val mk_diagnostics :
- uri:Lang.LUri.File.t -> version:int -> Lang.Diagnostic.t list -> Yojson.Safe.t
+ uri:Lang.LUri.File.t
+ -> version:int
+ -> Lang.Diagnostic.t list
+ -> Base.Notification.t
diff --git a/petanque/README.md b/petanque/README.md
index 3ea91397..a7a85a6c 100644
--- a/petanque/README.md
+++ b/petanque/README.md
@@ -33,7 +33,7 @@ have three options:
See the contributing guide for instructions on how to perform the last
two.
-## Using `petanque`
+## Running `petanque` JSON shell
You can use `petanque` in 2 different ways:
@@ -84,3 +84,47 @@ Please use one line per json input. json input examples are:
Seems to work! (TM) (Famous last words)
+## Running `pet-server`
+
+After building Petanque, you can launch a TCP server with:
+```
+dune exec -- pet-server
+```
+
+Default address is 127.0.0.1 and default port is 8765.
+
+```
+❯ dune exec -- pet-server --help
+PET(1) Pet Manual PET(1)
+
+NAME
+ pet - Petanque Server
+
+SYNOPSIS
+ pet [--address=ADDRESS] [--backlog=BACKLOG] [--port=PORT] [OPTION]…
+
+DESCRIPTION
+ Launch a petanque server to interact with Coq
+
+USAGE
+ See the documentation on the project's webpage for more information
+
+OPTIONS
+ -a ADDRESS, --address=ADDRESS (absent=127.0.0.1)
+ address to listen to
+
+ -b BACKLOG, --backlog=BACKLOG (absent=10)
+ socket backlog
+
+ -p PORT, --port=PORT (absent=8765)
+ port to listen to
+
+COMMON OPTIONS
+ --help[=FMT] (default=auto)
+ Show this help in format FMT. The value FMT must be one of auto,
+ pager, groff or plain. With auto, the format is pager or plain
+ whenever the TERM env var is dumb or undefined.
+
+ --version
+ Show version information.
+```
diff --git a/petanque/agent.ml b/petanque/agent.ml
index b52fae34..dcb846a8 100644
--- a/petanque/agent.ml
+++ b/petanque/agent.ml
@@ -47,6 +47,12 @@ module R = struct
type 'a t = ('a, Error.t) Result.t
end
+module Run_result = struct
+ type 'a t =
+ | Proof_finished of 'a
+ | Current_state of 'a
+end
+
let init_coq ~debug =
let load_module = Dynlink.loadfile in
let load_plugin = Coq.Loader.plugin_handler None in
@@ -78,11 +84,21 @@ let io =
let diagnostics ~uri:_ ~version:_ _diags = () in
let fileProgress ~uri:_ ~version:_ _pinfo = () in
let perfData ~uri:_ ~version:_ _perf = () in
- { Fleche.Io.CallBack.trace; message; diagnostics; fileProgress; perfData }
+ let serverVersion _ = () in
+ let serverStatus _ = () in
+ { Fleche.Io.CallBack.trace
+ ; message
+ ; diagnostics
+ ; fileProgress
+ ; perfData
+ ; serverVersion
+ ; serverStatus
+ }
let read_raw ~uri =
let file = Lang.LUri.File.to_string_file uri in
- Fleche.Compat.Ocaml_414.In_channel.(with_open_text file input_all)
+ try Ok Coq.Compat.Ocaml_414.In_channel.(with_open_text file input_all)
+ with Sys_error err -> Error err
let find_thm ~(doc : Fleche.Doc.t) ~thm =
let { Fleche.Doc.toc; _ } = doc in
@@ -106,34 +122,46 @@ let init ~token ~debug ~root =
let init = init_coq ~debug in
Fleche.Io.CallBack.set io;
let dir = Lang.LUri.File.to_string_file root in
- (let open Fleche.Compat.Result.O in
+ (let open Coq.Compat.Result.O in
let+ workspace = Coq.Workspace.guess ~token ~debug ~cmdline ~dir in
let files = Coq.Files.make () in
Fleche.Doc.Env.make ~init ~workspace ~files)
|> Result.map_error (fun msg -> Error.Coq msg)
let start ~token ~env ~uri ~thm =
- let raw = read_raw ~uri in
- (* Format.eprintf "raw: @[%s@]%!" raw; *)
- let doc = Fleche.Doc.create ~token ~env ~uri ~version:0 ~raw in
- print_diags doc;
- let target = Fleche.Doc.Target.End in
- let doc = Fleche.Doc.check ~io ~token ~target ~doc () in
- find_thm ~doc ~thm
+ match read_raw ~uri with
+ | Ok raw ->
+ (* Format.eprintf "raw: @[%s@]%!" raw; *)
+ let doc = Fleche.Doc.create ~token ~env ~uri ~version:0 ~raw in
+ print_diags doc;
+ let target = Fleche.Doc.Target.End in
+ let doc = Fleche.Doc.check ~io ~token ~target ~doc () in
+ find_thm ~doc ~thm
+ | Error err ->
+ let msg = Format.asprintf "@[[read_raw] File not found %s@]" err in
+ Error (Error.Theorem_not_found msg)
let parse ~loc tac st =
let str = Gramlib.Stream.of_string tac in
let str = Coq.Parsing.Parsable.make ?loc str in
Coq.Parsing.parse ~st str
+let proof_finished { Coq.Goals.goals; stack; shelf; given_up; _ } =
+ List.for_all CList.is_empty [ goals; shelf; given_up ] && CList.is_empty stack
+
let parse_and_execute_in ~token ~loc tac st =
let open Coq.Protect.E.O in
let* ast = parse ~token ~loc tac st in
match ast with
- | Some ast -> Fleche.Memo.Interp.eval ~token (st, ast)
- (* On EOF we return the previous state, the command was the empty string or a
- comment *)
- | None -> Coq.Protect.E.ok st
+ | Some ast -> (
+ let open Coq.Protect.E.O in
+ let* st = Fleche.Memo.Interp.eval ~token (st, ast) in
+ let+ goals = Fleche.Info.Goals.goals ~token ~st in
+ match goals with
+ | None -> Run_result.Proof_finished st
+ | Some goals when proof_finished goals -> Run_result.Proof_finished st
+ | _ -> Run_result.Current_state st)
+ | None -> Coq.Protect.E.ok (Run_result.Current_state st)
let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
match r with
@@ -144,7 +172,7 @@ let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
Error (Error.Anomaly (Pp.string_of_ppcmds msg))
| { r = Completed (Ok r); feedback = _ } -> Ok r
-let run_tac ~token ~st ~tac : (Coq.State.t, Error.t) Result.t =
+let run_tac ~token ~st ~tac : (_ Run_result.t, Error.t) Result.t =
(* Improve with thm? *)
let loc = None in
Coq.State.in_stateM ~token ~st ~f:(parse_and_execute_in ~token ~loc tac) st
@@ -158,9 +186,81 @@ let goals ~token ~st =
in
Coq.Protect.E.map ~f (Fleche.Info.Goals.goals ~token ~st) |> protect_to_result
+module Premise = struct
+ type t =
+ { full_name : string
+ (* should be a Coq DirPath, but let's go step by step *)
+ ; file : string (* file (in FS format) where the premise is found *)
+ ; kind : (string, string) Result.t (* type of object *)
+ ; range : (Lang.Range.t, string) Result.t (* a range if known *)
+ ; offset : (int * int, string) Result.t
+ (* a offset in the file if known (from .glob files) *)
+ ; raw_text : (string, string) Result.t (* raw text of the premise *)
+ }
+end
+
+(* We need some caching here otherwise it is very expensive to re-parse the glob
+ files all the time.
+
+ XXX move this caching to Flèche. *)
+module Memo = struct
+ module H = Hashtbl.Make (CString)
+
+ let table_glob = H.create 1000
+
+ let open_file glob =
+ match H.find_opt table_glob glob with
+ | Some g -> g
+ | None ->
+ let g = Coq.Glob.open_file glob in
+ H.add table_glob glob g;
+ g
+
+ let table_source = H.create 1000
+
+ let input_source file =
+ match H.find_opt table_source file with
+ | Some res -> res
+ | None ->
+ if Sys.file_exists file then (
+ let res =
+ Ok Coq.Compat.Ocaml_414.In_channel.(with_open_text file input_all)
+ in
+ H.add table_source file res;
+ res)
+ else
+ let res = Error "source file is not available" in
+ H.add table_source file res;
+ res
+end
+
+let info_of ~glob ~name =
+ let open Coq.Compat.Result.O in
+ let* g = Memo.open_file glob in
+ let+ { Coq.Glob.Info.kind; offset } = Coq.Glob.get_info g name in
+ (kind, offset)
+
+let raw_of ~file ~offset =
+ match offset with
+ | Ok (bp, ep) ->
+ let open Coq.Compat.Result.O in
+ let* c = Memo.input_source file in
+ if String.length c < ep then Error "offset out of bounds"
+ else Ok (String.sub c bp (ep - bp + 1))
+ | Error err -> Error ("offset information is not available: " ^ err)
+
+let to_premise (p : Coq.Library_file.Entry.t) : Premise.t =
+ let { Coq.Library_file.Entry.name; typ = _; file } = p in
+ let file = Filename.(remove_extension file ^ ".v") in
+ let glob = Filename.(remove_extension file ^ ".glob") in
+ let range = Error "not implemented yet" in
+ let kind, offset = info_of ~glob ~name |> Coq.Compat.Result.split in
+ let raw_text = raw_of ~file ~offset in
+ { full_name = name; file; kind; range; offset; raw_text }
+
let premises ~token ~st =
(let open Coq.Protect.E.O in
let* all_libs = Coq.Library_file.loaded ~token ~st in
let+ all_premises = Coq.Library_file.toc ~token ~st all_libs in
- List.map fst all_premises)
+ List.map to_premise all_premises)
|> protect_to_result
diff --git a/petanque/agent.mli b/petanque/agent.mli
index 8f1a0cb1..18a3152d 100644
--- a/petanque/agent.mli
+++ b/petanque/agent.mli
@@ -37,6 +37,12 @@ module R : sig
type 'a t = ('a, Error.t) Result.t
end
+module Run_result : sig
+ type 'a t =
+ | Proof_finished of 'a
+ | Current_state of 'a
+end
+
(** I/O handling, by default, print to stderr *)
(** [trace header extra message] *)
@@ -61,7 +67,10 @@ val start :
(** [run_tac ~token ~st ~tac] tries to run [tac] over state [st] *)
val run_tac :
- token:Coq.Limits.Token.t -> st:State.t -> tac:string -> State.t R.t
+ token:Coq.Limits.Token.t
+ -> st:State.t
+ -> tac:string
+ -> State.t Run_result.t R.t
(** [goals ~token ~st] return the list of goals for a given [st] *)
val goals :
@@ -69,7 +78,20 @@ val goals :
-> st:State.t
-> string Coq.Goals.reified_pp option R.t
+module Premise : sig
+ type t =
+ { full_name : string
+ (* should be a Coq DirPath, but let's go step by step *)
+ ; file : string (* file (in FS format) where the premise is found *)
+ ; kind : (string, string) Result.t (* type of object *)
+ ; range : (Lang.Range.t, string) Result.t (* a range if known *)
+ ; offset : (int * int, string) Result.t
+ (* a offset in the file if known (from .glob files) *)
+ ; raw_text : (string, string) Result.t (* raw text of the premise *)
+ }
+end
+
(** Return the list of defined constants and inductives for a given state. For
now we just return their fully qualified name, but more options are of
course possible. *)
-val premises : token:Coq.Limits.Token.t -> st:State.t -> string list R.t
+val premises : token:Coq.Limits.Token.t -> st:State.t -> Premise.t list R.t
diff --git a/petanque/json_shell/client.ml b/petanque/json_shell/client.ml
index 787196c0..4535775d 100644
--- a/petanque/json_shell/client.ml
+++ b/petanque/json_shell/client.ml
@@ -48,7 +48,7 @@ let get_id () =
!id_counter
module Wrap (R : Protocol.Request.S) (C : Chans) : sig
- val call : R.Params_.t -> (R.Response_.t, string) Result.t
+ val call : R.Params.t -> (R.Response.t, string) Result.t
end = struct
let trace = C.trace
let message = C.message
@@ -56,14 +56,14 @@ end = struct
let call params =
let id = get_id () in
let method_ = R.method_ in
- let params = Yojson.Safe.Util.to_assoc (R.Params_.to_yojson params) in
+ let params = Yojson.Safe.Util.to_assoc (R.Params.to_yojson params) in
let request =
Lsp.Base.Request.(make ~id ~method_ ~params () |> to_yojson)
in
let () = Lsp.Io.send_json C.oc request in
read_response ~trace ~message C.ic |> fun r ->
Result.bind r (function
- | Ok { id = _; result } -> R.Response_.of_yojson result
+ | Ok { id = _; result } -> R.Response.of_yojson result
| Error { id = _; code = _; message; data = _ } -> Error message)
end
diff --git a/petanque/json_shell/client.mli b/petanque/json_shell/client.mli
index c7aa620a..83dcbefa 100644
--- a/petanque/json_shell/client.mli
+++ b/petanque/json_shell/client.mli
@@ -8,9 +8,9 @@ end
open Protocol
module S (C : Chans) : sig
- val init : Init.Params_.t -> (Init.Response_.t, string) result
- val start : Start.Params_.t -> (Start.Response_.t, string) result
- val run_tac : RunTac.Params_.t -> (RunTac.Response_.t, string) result
- val goals : Goals.Params_.t -> (Goals.Response_.t, string) result
- val premises : Premises.Params_.t -> (Premises.Response_.t, string) result
+ val init : Init.Params.t -> (Init.Response.t, string) result
+ val start : Start.Params.t -> (Start.Response.t, string) result
+ val run_tac : RunTac.Params.t -> (RunTac.Response.t, string) result
+ val goals : Goals.Params.t -> (Goals.Response.t, string) result
+ val premises : Premises.Params.t -> (Premises.Response.t, string) result
end
diff --git a/petanque/json_shell/dune b/petanque/json_shell/dune
index 97f28324..bd19ff96 100644
--- a/petanque/json_shell/dune
+++ b/petanque/json_shell/dune
@@ -1,7 +1,7 @@
(library
(name petanque_json)
(public_name coq-lsp.petanque.json)
- (modules :standard \ pet)
+ (modules :standard \ pet server)
(preprocess
(staged_pps ppx_import ppx_deriving_yojson))
(libraries cmdliner lsp petanque))
@@ -11,3 +11,10 @@
(public_name pet)
(modules pet)
(libraries petanque_json))
+
+(executable
+ (name server)
+ (public_name pet-server)
+ (modules server)
+ (optional)
+ (libraries logs.lwt lwt.unix petanque_json))
diff --git a/petanque/json_shell/interp.ml b/petanque/json_shell/interp.ml
index a9d6933b..38735748 100644
--- a/petanque/json_shell/interp.ml
+++ b/petanque/json_shell/interp.ml
@@ -2,11 +2,11 @@ open Protocol
module A = Petanque.Agent
let do_request ~token (module R : Request.S) ~id ~params =
- match R.Params.of_yojson (`Assoc params) with
+ match R.Handler.Params.of_yojson (`Assoc params) with
| Ok params -> (
- match R.handler ~token params with
+ match R.Handler.handler ~token params with
| Ok result ->
- let result = R.Response.to_yojson result in
+ let result = R.Handler.Response.to_yojson result in
Lsp.Base.Response.mk_ok ~id ~result
| Error err ->
let message = A.Error.to_string err in
diff --git a/petanque/json_shell/jAgent.ml b/petanque/json_shell/jAgent.ml
index 8f6f1a6a..d69ecb82 100644
--- a/petanque/json_shell/jAgent.ml
+++ b/petanque/json_shell/jAgent.ml
@@ -6,16 +6,26 @@ module Env = Obj_map.Make (Petanque.Agent.Env)
(* The typical protocol dance *)
-module Result = struct
- include Result
+module Stdlib = struct
+ module Result = struct
+ include Stdlib.Result
- type ('a, 'e) t = [%import: ('a, 'e) Result.t] [@@deriving yojson]
+ type ('a, 'e) t = [%import: ('a, 'e) Stdlib.Result.t] [@@deriving yojson]
+ end
end
+(* What a mess result stuff is, we need this in case result is installed, as
+ then the types below will be referenced as plain result ... *)
+module Result = Stdlib.Result
+
module Error = struct
type t = [%import: Petanque.Agent.Error.t] [@@deriving yojson]
end
+module Run_result = struct
+ type 'a t = [%import: 'a Petanque.Agent.Run_result.t] [@@deriving yojson]
+end
+
module R = struct
type 'a t = [%import: 'a Petanque.Agent.R.t] [@@deriving yojson]
end
@@ -23,3 +33,13 @@ end
module Goals = struct
type t = string Lsp.JCoq.Goals.reified_pp option [@@deriving yojson]
end
+
+module Lang = struct
+ module Range = struct
+ type t = Lsp.JLang.Range.t [@@deriving yojson]
+ end
+end
+
+module Premise = struct
+ type t = [%import: Petanque.Agent.Premise.t] [@@deriving yojson]
+end
diff --git a/petanque/json_shell/pet.ml b/petanque/json_shell/pet.ml
index 58d944b6..2b390fe4 100644
--- a/petanque/json_shell/pet.ml
+++ b/petanque/json_shell/pet.ml
@@ -40,11 +40,6 @@ let message_notification ~lvl ~message =
in
Lsp.Io.send_json Format.std_formatter notification
-(* XXX: Flèche LSP backend already handles the conversion at the protocol
- level *)
-let uri_of_string_exn uri =
- Lang.LUri.of_string uri |> Lang.LUri.File.of_uri |> Result.get_ok
-
let trace_enabled = true
let pet_main debug roots =
@@ -54,19 +49,7 @@ let pet_main debug roots =
Petanque.Agent.trace_ref := trace_notification;
Petanque.Agent.message_ref := message_notification);
let token = Coq.Limits.Token.create () in
- let () =
- match roots with
- | [] -> ()
- | [ root ] | root :: _ -> (
- let root = uri_of_string_exn root in
- match Petanque.Agent.init ~token ~debug ~root with
- | Ok env ->
- (* hack until we fix the stuff *)
- let _ : Yojson.Safe.t = JAgent.Env.to_yojson env in
- ()
- | Error err ->
- Format.eprintf "Error: %s@\n%!" (Petanque.Agent.Error.to_string err))
- in
+ let () = Utils.set_roots ~token ~debug ~roots in
loop ~token
open Cmdliner
diff --git a/petanque/json_shell/protocol.ml b/petanque/json_shell/protocol.ml
index 546a3eaa..a3c0defb 100644
--- a/petanque/json_shell/protocol.ml
+++ b/petanque/json_shell/protocol.ml
@@ -3,35 +3,38 @@ open Petanque
(* Serialization for agent types *)
open JAgent
+(* RPC-side server mappings, internal; we could split this in a different module
+ eventually as to make this clearer. *)
+module type Handler = sig
+ (* Server-side RPC specification *)
+ module Params : sig
+ type t [@@deriving of_yojson]
+ end
+
+ (* Server-side RPC specification *)
+ module Response : sig
+ type t [@@deriving to_yojson]
+ end
+
+ val handler : token:Coq.Limits.Token.t -> Params.t -> Response.t R.t
+end
+
(* Note that here we follow JSON-RPC / LSP capitalization conventions *)
module Request = struct
module type S = sig
val method_ : string
- (* Would be good to remove this duplicity, but that would complicate the
- server side setup which now is trivial. *)
-
- (* Server-side params specification *)
+ (* Protocol params specification *)
module Params : sig
- type t [@@deriving of_yojson]
- end
-
- (* Client-side params specification *)
- module Params_ : sig
- type t [@@deriving to_yojson]
+ type t [@@deriving yojson]
end
- (* Server-side response specification *)
+ (* Protocol response specification *)
module Response : sig
- type t [@@deriving to_yojson]
- end
-
- (* Client-side response specification *)
- module Response_ : sig
- type t [@@deriving of_yojson]
+ type t [@@deriving yojson]
end
- val handler : token:Coq.Limits.Token.t -> Params.t -> Response.t R.t
+ module Handler : Handler
end
end
@@ -47,17 +50,19 @@ module Init = struct
[@@deriving yojson]
end
- module Params_ = Params
-
module Response = struct
- type t = Env.t [@@deriving yojson]
- end
-
- module Response_ = struct
type t = int [@@deriving yojson]
end
- let handler ~token { Params.debug; root } = Agent.init ~token ~debug ~root
+ module Handler = struct
+ module Params = Params
+
+ module Response = struct
+ type t = Env.t [@@deriving yojson]
+ end
+
+ let handler ~token { Params.debug; root } = Agent.init ~token ~debug ~root
+ end
end
(* start RPC *)
@@ -65,15 +70,6 @@ module Start = struct
let method_ = "petanque/start"
module Params = struct
- type t =
- { env : Env.t
- ; uri : Lsp.JLang.LUri.File.t
- ; thm : string
- }
- [@@deriving yojson]
- end
-
- module Params_ = struct
type t =
{ env : int
; uri : Lsp.JLang.LUri.File.t
@@ -83,15 +79,26 @@ module Start = struct
end
module Response = struct
- type t = State.t [@@deriving yojson]
- end
-
- module Response_ = struct
type t = int [@@deriving yojson]
end
- let handler ~token { Params.env; uri; thm } =
- Agent.start ~token ~env ~uri ~thm
+ module Handler = struct
+ module Params = struct
+ type t =
+ { env : Env.t
+ ; uri : Lsp.JLang.LUri.File.t
+ ; thm : string
+ }
+ [@@deriving yojson]
+ end
+
+ module Response = struct
+ type t = State.t [@@deriving yojson]
+ end
+
+ let handler ~token { Params.env; uri; thm } =
+ Agent.start ~token ~env ~uri ~thm
+ end
end
(* run_tac RPC *)
@@ -99,14 +106,6 @@ module RunTac = struct
let method_ = "petanque/run"
module Params = struct
- type t =
- { st : State.t
- ; tac : string
- }
- [@@deriving yojson]
- end
-
- module Params_ = struct
type t =
{ st : int
; tac : string
@@ -115,14 +114,24 @@ module RunTac = struct
end
module Response = struct
- type t = State.t [@@deriving yojson]
+ type t = int Run_result.t [@@deriving yojson]
end
- module Response_ = struct
- type t = int [@@deriving yojson]
- end
+ module Handler = struct
+ module Params = struct
+ type t =
+ { st : State.t
+ ; tac : string
+ }
+ [@@deriving yojson]
+ end
+
+ module Response = struct
+ type t = State.t Run_result.t [@@deriving yojson]
+ end
- let handler ~token { Params.st; tac } = Agent.run_tac ~token ~st ~tac
+ let handler ~token { Params.st; tac } = Agent.run_tac ~token ~st ~tac
+ end
end
(* goals RPC *)
@@ -130,10 +139,6 @@ module Goals = struct
let method_ = "petanque/goals"
module Params = struct
- type t = { st : State.t } [@@deriving yojson]
- end
-
- module Params_ = struct
type t = { st : int } [@@deriving yojson]
end
@@ -141,9 +146,15 @@ module Goals = struct
type t = Goals.t [@@deriving yojson]
end
- module Response_ = Response
+ module Handler = struct
+ module Params = struct
+ type t = { st : State.t } [@@deriving yojson]
+ end
+
+ module Response = Response
- let handler ~token { Params.st } = Agent.goals ~token ~st
+ let handler ~token { Params.st } = Agent.goals ~token ~st
+ end
end
(* premises RPC *)
@@ -151,20 +162,22 @@ module Premises = struct
let method_ = "petanque/premises"
module Params = struct
- type t = { st : State.t } [@@deriving yojson]
- end
-
- module Params_ = struct
type t = { st : int } [@@deriving yojson]
end
module Response = struct
- type t = string list [@@deriving yojson]
+ type t = Premise.t list [@@deriving yojson]
end
- module Response_ = Response
+ module Handler = struct
+ module Params = struct
+ type t = { st : State.t } [@@deriving yojson]
+ end
+
+ module Response = Response
- let handler ~token { Params.st } = Agent.premises ~token ~st
+ let handler ~token { Params.st } = Agent.premises ~token ~st
+ end
end
(* Notifications don't get a reply *)
diff --git a/petanque/json_shell/server.ml b/petanque/json_shell/server.ml
new file mode 100644
index 00000000..1e536945
--- /dev/null
+++ b/petanque/json_shell/server.ml
@@ -0,0 +1,109 @@
+open Lwt
+open Lwt.Syntax
+open Petanque_json
+
+let rq_info (r : Lsp.Base.Message.t) =
+ match r with
+ | Notification { method_; _ } -> Format.asprintf "notification: %s" method_
+ | Request { method_; _ } -> Format.asprintf "request: %s" method_
+ | Response (Ok { id; _ } | Error { id; _ }) ->
+ Format.asprintf "response for: %d" id
+
+let rec handle_connection ~token ic oc () =
+ try
+ let* request = Lwt_io.read_line ic in
+ let request = Yojson.Safe.from_string request in
+ match Lsp.Base.Message.of_yojson request with
+ | Error err ->
+ (* error in Json message *)
+ let* () = Logs_lwt.info (fun m -> m "Error: %s" err) in
+ handle_connection ~token ic oc ()
+ | Ok request -> (
+ (* everything is fine up to JSON-RPC level *)
+ let* () = Logs_lwt.info (fun m -> m "Received: %s" (rq_info request)) in
+ (* request could be a notification, so maybe we don't have to do a
+ reply! *)
+ match Interp.interp ~token request with
+ | None -> handle_connection ~token ic oc ()
+ | Some reply ->
+ let* () = Logs_lwt.info (fun m -> m "Sent reply") in
+ let* () = Lwt_io.fprintl oc (Yojson.Safe.to_string reply) in
+ handle_connection ~token ic oc ())
+ with End_of_file -> return ()
+
+let accept_connection ~token conn =
+ let fd, _ = conn in
+ let ic = Lwt_io.of_fd ~mode:Lwt_io.Input fd in
+ let oc = Lwt_io.of_fd ~mode:Lwt_io.Output fd in
+ let* () = Logs_lwt.info (fun m -> m "New connection") in
+ Lwt.on_failure (handle_connection ~token ic oc ()) (fun e ->
+ Logs.err (fun m -> m "%s" (Printexc.to_string e)));
+ return ()
+
+let create_socket ~address ~port ~backlog =
+ let open Lwt_unix in
+ let sock = socket PF_INET SOCK_STREAM 0 in
+ ( bind sock @@ ADDR_INET (Unix.inet_addr_of_string address, port) |> fun x ->
+ ignore x );
+ listen sock backlog;
+ sock
+
+let create_server ~token sock =
+ let rec serve () =
+ let* conn = Lwt_unix.accept sock in
+ let* () = accept_connection ~token conn in
+ serve ()
+ in
+ serve
+
+let pet_main debug roots address port backlog =
+ Coq.Limits.start ();
+ let token = Coq.Limits.Token.create () in
+ let () = Logs.set_reporter (Logs.format_reporter ()) in
+ let () = Logs.set_level (Some Logs.Info) in
+ let sock = create_socket ~address ~port ~backlog in
+ let serve = create_server ~token sock in
+ let () = Utils.set_roots ~token ~debug ~roots in
+ Lwt_main.run @@ serve ()
+
+open Cmdliner
+
+let address =
+ let doc = "address to listen to" in
+ Arg.(
+ value & opt string "127.0.0.1"
+ & info [ "a"; "address" ] ~docv:"ADDRESS" ~doc)
+
+let port =
+ let doc = "port to listen to" in
+ Arg.(value & opt int 8765 & info [ "p"; "port" ] ~docv:"PORT" ~doc)
+
+let backlog =
+ let doc = "socket backlog" in
+ Arg.(value & opt int 10 & info [ "b"; "backlog" ] ~docv:"BACKLOG" ~doc)
+
+let pet_cmd : unit Cmd.t =
+ let doc = "Petanque Server" in
+ let man =
+ [ `S "DESCRIPTION"
+ ; `P "Launch a petanque server to interact with Coq"
+ ; `S "USAGE"
+ ; `P
+ "See\n\
+ \ the\n\
+ \ documentation on the project's webpage for more information"
+ ]
+ in
+ let version = Fleche.Version.server in
+ let pet_term =
+ Term.(
+ const pet_main $ Coq.Args.debug $ Coq.Args.roots $ address $ port
+ $ backlog)
+ in
+ Cmd.(v (Cmd.info "pet" ~version ~doc ~man) pet_term)
+
+let main () =
+ let ecode = Cmd.eval pet_cmd in
+ exit ecode
+
+let () = main ()
diff --git a/petanque/json_shell/utils.ml b/petanque/json_shell/utils.ml
new file mode 100644
index 00000000..84ebf089
--- /dev/null
+++ b/petanque/json_shell/utils.ml
@@ -0,0 +1,17 @@
+(* XXX: Flèche LSP backend already handles the conversion at the protocol
+ level *)
+let uri_of_string_exn uri =
+ Lang.LUri.of_string uri |> Lang.LUri.File.of_uri |> Result.get_ok
+
+let set_roots ~token ~debug ~roots =
+ match roots with
+ | [] -> ()
+ | [ root ] | root :: _ -> (
+ let root = uri_of_string_exn root in
+ match Petanque.Agent.init ~token ~debug ~root with
+ | Ok env ->
+ (* hack until we fix the stuff *)
+ let _ : Yojson.Safe.t = JAgent.Env.to_yojson env in
+ ()
+ | Error err ->
+ Format.eprintf "Error: %s@\n%!" (Petanque.Agent.Error.to_string err))
diff --git a/petanque/test/basic_api.ml b/petanque/test/basic_api.ml
index e8360520..19219ada 100644
--- a/petanque/test/basic_api.ml
+++ b/petanque/test/basic_api.ml
@@ -21,23 +21,31 @@ let start ~token =
Petanque.Agent.trace_ref := trace;
Petanque.Agent.message_ref := message;
(* Will this work on Windows? *)
- let open Fleche.Compat.Result.O in
+ let open Coq.Compat.Result.O in
let root, uri = prepare_paths () in
let* env = Agent.init ~token ~debug ~root in
Agent.start ~token ~env ~uri ~thm:"rev_snoc_cons"
+let extract_st (st : _ Agent.Run_result.t) =
+ match st with
+ | Proof_finished st | Current_state st -> st
+
let main () =
- let open Fleche.Compat.Result.O in
+ let open Coq.Compat.Result.O in
let token = Coq.Limits.create_atomic () in
+ let r ~st ~tac =
+ let st = extract_st st in
+ Agent.run_tac ~token ~st ~tac
+ in
let* st = start ~token in
let* _premises = Agent.premises ~token ~st in
let* st = Agent.run_tac ~token ~st ~tac:"induction l." in
- let* st = Agent.run_tac ~token ~st ~tac:"-" in
- let* st = Agent.run_tac ~token ~st ~tac:"reflexivity." in
- let* st = Agent.run_tac ~token ~st ~tac:"-" in
- let* st = Agent.run_tac ~token ~st ~tac:"now simpl; rewrite IHl." in
- let* st = Agent.run_tac ~token ~st ~tac:"Qed." in
- Agent.goals ~token ~st
+ let* st = r ~st ~tac:"-" in
+ let* st = r ~st ~tac:"reflexivity." in
+ let* st = r ~st ~tac:"-" in
+ let* st = r ~st ~tac:"now simpl; rewrite IHl." in
+ let* st = r ~st ~tac:"Qed." in
+ Agent.goals ~token ~st:(extract_st st)
let check_no_goals = function
| Error err ->
diff --git a/petanque/test/dune b/petanque/test/dune
index 4186be83..fe4c7a8e 100644
--- a/petanque/test/dune
+++ b/petanque/test/dune
@@ -11,3 +11,11 @@
(enabled_if
(<> %{os_type} "Win32"))
(libraries petanque petanque_json lsp))
+
+(test
+ (name json_api_failure)
+ (modules json_api_failure)
+ (deps test.v %{bin:pet})
+ (enabled_if
+ (<> %{os_type} "Win32"))
+ (libraries petanque petanque_json lsp))
diff --git a/petanque/test/json_api.ml b/petanque/test/json_api.ml
index bb6ef535..bbd5a53a 100644
--- a/petanque/test/json_api.ml
+++ b/petanque/test/json_api.ml
@@ -13,8 +13,32 @@ let trace ?verbose:_ msg = msgs := Format.asprintf "[trace] %s" msg :: !msgs
let message ~lvl:_ ~message = msgs := message :: !msgs
let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs)
+let extract_st (st : Protocol.RunTac.Response.t) =
+ match st with
+ | Proof_finished st | Current_state st -> st
+
+let pp_offset fmt (bp, ep) = Format.fprintf fmt "(%d,%d)" bp ep
+
+let pp_res_str =
+ Coq.Compat.Result.pp Format.pp_print_string Format.pp_print_string
+
+let pp_premise fmt
+ { Petanque.Agent.Premise.full_name
+ ; kind
+ ; file
+ ; range = _
+ ; offset
+ ; raw_text
+ } =
+ Format.(
+ fprintf fmt
+ "@[{ name = %s;@ file = %s;@ kind = %a;@ offset = %a;@ raw_text = %a}@]@\n"
+ full_name file pp_res_str kind
+ (Coq.Compat.Result.pp pp_offset pp_print_string)
+ offset pp_res_str raw_text)
+
let run (ic, oc) =
- let open Fleche.Compat.Result.O in
+ let open Coq.Compat.Result.O in
let debug = false in
let module S = Client.S (struct
let ic = ic
@@ -22,18 +46,23 @@ let run (ic, oc) =
let trace = trace
let message = message
end) in
+ let r ~st ~tac =
+ let st = extract_st st in
+ S.run_tac { st; tac }
+ in
(* Will this work on Windows? *)
let root, uri = prepare_paths () in
let* env = S.init { debug; root } in
let* st = S.start { env; uri; thm = "rev_snoc_cons" } in
let* _premises = S.premises { st } in
+ (* Format.(eprintf "@[%a@]@\n%!" (pp_print_list pp_premise) premises); *)
let* st = S.run_tac { st; tac = "induction l." } in
- let* st = S.run_tac { st; tac = "-" } in
- let* st = S.run_tac { st; tac = "reflexivity." } in
- let* st = S.run_tac { st; tac = "-" } in
- let* st = S.run_tac { st; tac = "now simpl; rewrite IHl." } in
- let* st = S.run_tac { st; tac = "Qed." } in
- S.goals { st }
+ let* st = r ~st ~tac:"-" in
+ let* st = r ~st ~tac:"reflexivity." in
+ let* st = r ~st ~tac:"-" in
+ let* st = r ~st ~tac:"now simpl; rewrite IHl." in
+ let* st = r ~st ~tac:"Qed." in
+ S.goals { st = extract_st st }
let main () =
let server_out, server_in = Unix.open_process "pet" in
diff --git a/petanque/test/json_api_failure.ml b/petanque/test/json_api_failure.ml
new file mode 100644
index 00000000..71bce482
--- /dev/null
+++ b/petanque/test/json_api_failure.ml
@@ -0,0 +1,68 @@
+open Petanque_json
+
+let prepare_paths () =
+ let to_uri file =
+ Lang.LUri.of_string file |> Lang.LUri.File.of_uri |> Result.get_ok
+ in
+ let cwd = Sys.getcwd () in
+ let file = Filename.concat cwd "test.v" in
+ (to_uri cwd, to_uri file)
+
+let msgs = ref []
+let trace ?verbose:_ msg = msgs := Format.asprintf "[trace] %s" msg :: !msgs
+let message ~lvl:_ ~message = msgs := message :: !msgs
+let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs)
+
+let extract_st (st : Protocol.RunTac.Response.t) =
+ match st with
+ | Proof_finished st | Current_state st -> st
+
+let run (ic, oc) =
+ let open Coq.Compat.Result.O in
+ let debug = false in
+ let module S = Client.S (struct
+ let ic = ic
+ let oc = oc
+ let trace = trace
+ let message = message
+ end) in
+ let r ~st ~tac =
+ let st = extract_st st in
+ S.run_tac { st; tac }
+ in
+ (* Will this work on Windows? *)
+ let root, uri = prepare_paths () in
+ let* env = S.init { debug; root } in
+ let* st = S.start { env; uri; thm = "rev_snoc_cons" } in
+ let* _premises = S.premises { st } in
+ let* st = S.run_tac { st; tac = "induction l." } in
+ let* st = r ~st ~tac:"-" in
+ (* Introduce an error *)
+ (* let* st = r ~st ~tac:"reflexivity." in *)
+ let* st = r ~st ~tac:"-" in
+ let* st = r ~st ~tac:"now simpl; rewrite IHl." in
+ let* st = r ~st ~tac:"Qed." in
+ S.goals { st = extract_st st }
+
+let main () =
+ let server_out, server_in = Unix.open_process "pet" in
+ run (server_out, Format.formatter_of_out_channel server_in)
+
+let check_no_goals = function
+ | Error _err ->
+ (* errored as expected! *)
+ 0
+ | Ok None ->
+ dump_msgs ();
+ Format.eprintf "error: we did succeded when we should not@\n%!";
+ 1
+ | Ok (Some _goals) ->
+ dump_msgs ();
+ Format.eprintf "error: goals remaining@\n%!";
+ 1
+
+let () =
+ let result = main () in
+ (* Need to kill the sever... *)
+ (* let () = Unix.kill server 9 in *)
+ check_no_goals result |> exit
diff --git a/test/compiler/basic/run.t b/test/compiler/basic/run.t
index 7a63f22c..ac7db57b 100644
--- a/test/compiler/basic/run.t
+++ b/test/compiler/basic/run.t
@@ -113,38 +113,63 @@ Compile a dependent file without the dep being built
b.v
b.vo
$ cat proj1/a.diags
+ $ cat proj1/b.diags
{
"range": {
"start": { "line": 0, "character": 0 },
- "end": { "line": 0, "character": 19 }
+ "end": { "line": 0, "character": 10 }
},
- "severity": 4,
- "message": "aa is defined"
+ "severity": 1,
+ "message": "Cannot find a physical path bound to logical path a."
}
{
"range": {
- "start": { "line": 6, "character": 0 },
- "end": { "line": 6, "character": 4 }
+ "start": { "line": 1, "character": 17 },
+ "end": { "line": 1, "character": 21 }
},
- "severity": 4,
- "message": "foo is defined"
+ "severity": 1,
+ "message": "The reference a.aa was not found in the current environment."
}
- $ cat proj1/b.diags
+
+Compile a file with all messages:
+ $ rm -f proj1/a.{diags,vo}
+ $ fcc --root proj1 --diags_level=1 proj1/a.v
+ [message] Configuration loaded from Command-line arguments
+ - coqlib is at: [TEST_PATH]
+ + coqcorelib is at: [TEST_PATH]
+ - Modules [Coq.Init.Prelude] will be loaded by default
+ - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope
+ - ocamlpath wasn't overriden
+ + findlib config: [TEST_PATH]
+ + findlib default location: [TEST_PATH]
+ [message] compiling file proj1/a.v
+ $ cat proj1/a.diags
+ $ fcc --root proj1 --diags_level=2 proj1/a.v
+ [message] Configuration loaded from Command-line arguments
+ - coqlib is at: [TEST_PATH]
+ + coqcorelib is at: [TEST_PATH]
+ - Modules [Coq.Init.Prelude] will be loaded by default
+ - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope
+ - ocamlpath wasn't overriden
+ + findlib config: [TEST_PATH]
+ + findlib default location: [TEST_PATH]
+ [message] compiling file proj1/a.v
+ $ cat proj1/a.diags
{
"range": {
"start": { "line": 0, "character": 0 },
- "end": { "line": 0, "character": 10 }
+ "end": { "line": 0, "character": 19 }
},
- "severity": 1,
- "message": "Cannot find a physical path bound to logical path a."
+ "severity": 4,
+ "message": "aa is defined"
}
{
"range": {
- "start": { "line": 1, "character": 17 },
- "end": { "line": 1, "character": 21 }
+ "start": { "line": 6, "character": 0 },
+ "end": { "line": 6, "character": 4 }
},
- "severity": 1,
- "message": "The reference a.aa was not found in the current environment."
+ "severity": 4,
+ "message": "foo is defined"
}
Use two workspaces
diff --git a/test/compiler/exit_code/run.t b/test/compiler/exit_code/run.t
index 5d38e9a2..3d2af0e4 100644
--- a/test/compiler/exit_code/run.t
+++ b/test/compiler/exit_code/run.t
@@ -18,14 +18,6 @@ Compile normally, even with errors, we exit 0:
$ echo $?
0
$ cat Demo.diags
- {
- "range": {
- "start": { "line": 8, "character": 0 },
- "end": { "line": 8, "character": 4 }
- },
- "severity": 4,
- "message": "add_0_r is defined"
- }
{
"range": {
"start": { "line": 11, "character": 8 },
+
### 🧠 Smart, Cache-Aware Error Recovery
`coq-lsp` won't stop checking on errors, but supports (and encourages) working
@@ -307,6 +319,17 @@ guide](./CONTRIBUTING.md)
- Interact programmatically with Coq files by using the [Python `coq-lsp` client](https://github.com/sr-lab/coq-lsp-pyclient)
by Pedro Carrott and Nuno Saavedra.
+## ⇨ `coq-lsp` users and extensions
+
+The below projects are using `coq-lsp`, we recommend you try them!
+
+- [CoqPilot uses Large Language Models to generate multiple potential proofs and then uses coq-lsp to typecheck them](https://github.com/JetBrains-Research/coqpilot).
+- [jsCoq: use Coq from your browser](https://github.com/jscoq/jscoq)
+- [Pytanque: a Python library implementing RL Environments](https://github.com/LLM4Coq/pytanque)
+- [ViZX: A Visualizer for the ZX Calculus](https://github.com/inQWIRE/ViZX).
+- [The Waterproof vscode extension helps students learn how to write mathematical proofs](https://github.com/impermeable/waterproof-vscode).
+- [Yade: Support for the YADE diagram editor in VSCode](https://github.com/amblafont/vscode-yade-example).
+
## 🗣️ Discussion Channel
`coq-lsp` discussion channel it at [Coq's
@@ -332,7 +355,7 @@ recommend that if you are installing via opam, you use the following branches
that have some fixes backported:
- For 8.20: No known problems
-- For 8.19: No known problems
+- For 8.19: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.19+lsp`
- For 8.18: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.18+lsp`
- For 8.17: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.17+lsp`
- For 8.16: `opam pin add coq https://github.com/ejgallego/coq.git#v8.16+lsp`
diff --git a/compiler/args.ml b/compiler/args.ml
index ede34c06..b6de9e98 100644
--- a/compiler/args.ml
+++ b/compiler/args.ml
@@ -14,6 +14,8 @@ type t =
; plugins : string list (** Flèche plugins to load *)
; max_errors : int option
(** Maximum erros before aborting the compilation *)
+ ; coq_diags_level : int
+ (** Whether to include feedback messages in the diagnostics *)
}
let compute_default_plugins ~no_vo ~plugins =
diff --git a/compiler/compile.ml b/compiler/compile.ml
index 9bbfa342..263817d0 100644
--- a/compiler/compile.ml
+++ b/compiler/compile.ml
@@ -22,7 +22,7 @@ let save_diags_file ~(doc : Fleche.Doc.t) =
let file = Lang.LUri.File.to_string_file doc.uri in
let file = Filename.remove_extension file ^ ".diags" in
let diags = Fleche.Doc.diags doc in
- Fleche.Compat.format_to_file ~file ~f:Output.pp_diags diags
+ Coq.Compat.format_to_file ~file ~f:Output.pp_diags diags
(** Return: exit status for file:
@@ -47,9 +47,7 @@ let compile_file ~cc file : int =
let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in
let files = Coq.Files.make () in
let env = Doc.Env.make ~init:root_state ~workspace ~files in
- let raw =
- Fleche.Compat.Ocaml_414.In_channel.(with_open_bin file input_all)
- in
+ let raw = Coq.Compat.Ocaml_414.In_channel.(with_open_bin file input_all) in
let () = Theory.create ~io ~token ~env ~uri ~raw ~version:1 in
match Theory.Check.maybe_check ~io ~token with
| None -> 102
diff --git a/compiler/driver.ml b/compiler/driver.ml
index ccb4b139..20814cc6 100644
--- a/compiler/driver.ml
+++ b/compiler/driver.ml
@@ -36,12 +36,20 @@ let apply_config ~max_errors =
max_errors
let go ~int_backend args =
- let { Args.cmdline; roots; display; debug; files; plugins; max_errors } =
+ let { Args.cmdline
+ ; roots
+ ; display
+ ; debug
+ ; files
+ ; plugins
+ ; max_errors
+ ; coq_diags_level
+ } =
args
in
(* Initialize event callbacks, in testing don't do perfData *)
let perfData = Option.is_empty fcc_test in
- let io = Output.init display ~perfData in
+ let io = Output.init ~display ~perfData ~coq_diags_level in
(* Initialize Coq *)
let debug = debug || Fleche.Debug.backtraces || !Fleche.Config.v.debug in
let root_state = coq_init ~debug in
diff --git a/compiler/fcc.ml b/compiler/fcc.ml
index 57930519..dd990ad3 100644
--- a/compiler/fcc.ml
+++ b/compiler/fcc.ml
@@ -3,7 +3,8 @@ open Cmdliner
open Fcc_lib
let fcc_main int_backend roots display debug plugins files coqlib coqcorelib
- ocamlpath rload_path load_path require_libraries no_vo max_errors =
+ ocamlpath rload_path load_path require_libraries no_vo max_errors
+ coq_diags_level =
let vo_load_path = rload_path @ load_path in
let ml_include_path = [] in
let args = [] in
@@ -19,7 +20,16 @@ let fcc_main int_backend roots display debug plugins files coqlib coqcorelib
in
let plugins = Args.compute_default_plugins ~no_vo ~plugins in
let args =
- Args.{ cmdline; roots; display; files; debug; plugins; max_errors }
+ Args.
+ { cmdline
+ ; roots
+ ; display
+ ; files
+ ; debug
+ ; plugins
+ ; max_errors
+ ; coq_diags_level
+ }
in
Driver.go ~int_backend args
@@ -91,7 +101,7 @@ let fcc_cmd : int Cmd.t =
Term.(
const fcc_main $ int_backend $ roots $ display $ debug $ plugins $ file
$ coqlib $ coqcorelib $ ocamlpath $ rload_paths $ qload_paths $ ri_from
- $ no_vo $ max_errors)
+ $ no_vo $ max_errors $ coq_diags_level)
in
let exits = Exit_codes.[ fatal; stopped; scheduled; uri_failed ] in
Cmd.(v (Cmd.info "fcc" ~exits ~version ~doc ~man) fcc_term)
diff --git a/compiler/output.ml b/compiler/output.ml
index f9f13f4d..bbf66a2a 100644
--- a/compiler/output.ml
+++ b/compiler/output.ml
@@ -9,7 +9,6 @@ let pp_diags fmt dl =
(* We will use this when we set eager diagnotics to true *)
let diagnostics ~uri:_ ~version:_ _diags = ()
let fileProgress ~uri:_ ~version:_ _progress = ()
-let perfData ~uri:_ ~version:_ _perf = ()
(* We print trace and messages, and perfData summary *)
module Fcc_verbose = struct
@@ -24,26 +23,30 @@ module Fcc_verbose = struct
let perfData ~uri:_ ~version:_ { Fleche.Perf.summary; _ } =
Format.(eprintf "[perfdata]@\n@[%s@]@\n%!" summary)
+ let serverVersion _ = ()
+ let serverStatus _ = ()
+
let cb =
- Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData }
+ Fleche.Io.CallBack.
+ { trace
+ ; message
+ ; diagnostics
+ ; fileProgress
+ ; perfData
+ ; serverVersion
+ ; serverStatus
+ }
end
(* We print trace, messages *)
module Fcc_normal = struct
let trace _ ?extra:_ _ = ()
- let message = Fcc_verbose.message
- let perfData = Fcc_verbose.perfData
-
- let cb =
- Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData }
+ let cb = { Fcc_verbose.cb with trace }
end
module Fcc_quiet = struct
- let trace _ ?extra:_ _ = ()
let message ~lvl:_ ~message:_ = ()
-
- let cb =
- Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData }
+ let cb = { Fcc_normal.cb with message }
end
let set_callbacks (display : Args.Display.t) =
@@ -56,16 +59,18 @@ let set_callbacks (display : Args.Display.t) =
Fleche.Io.CallBack.set cb;
cb
-let set_config ~perfData =
+let set_config ~perfData ~coq_diags_level =
+ let show_coq_info_messages = coq_diags_level > 1 in
+ let show_notices_as_diagnostics = coq_diags_level > 0 in
Fleche.Config.(
v :=
{ !v with
send_perf_data = perfData
; eager_diagnostics = false
- ; show_coq_info_messages = true
- ; show_notices_as_diagnostics = true
+ ; show_coq_info_messages
+ ; show_notices_as_diagnostics
})
-let init display ~perfData =
- set_config ~perfData;
+let init ~display ~coq_diags_level ~perfData =
+ set_config ~perfData ~coq_diags_level;
set_callbacks display
diff --git a/compiler/output.mli b/compiler/output.mli
index 7e643bc0..a4699ef7 100644
--- a/compiler/output.mli
+++ b/compiler/output.mli
@@ -1,5 +1,9 @@
(** Initialize Console Output System *)
-val init : Args.Display.t -> perfData:bool -> Fleche.Io.CallBack.t
+val init :
+ display:Args.Display.t
+ -> coq_diags_level:int
+ -> perfData:bool
+ -> Fleche.Io.CallBack.t
(** Report progress on file compilation *)
(* val report : unit -> unit *)
diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
index dff2d0c9..25caf87d 100644
--- a/controller/coq_lsp.ml
+++ b/controller/coq_lsp.ml
@@ -49,35 +49,52 @@ let rec process_queue ~delay ~io ~ofn ~state : unit =
| Some (Cont state) -> process_queue ~delay ~io ~ofn ~state
let concise_cb ofn =
+ let send_notification nt =
+ Lsp.Base.Message.(Notification nt |> to_yojson) |> ofn
+ in
+ let diagnostics ~uri ~version diags =
+ if List.length diags > 0 then
+ Lsp.JLang.mk_diagnostics ~uri ~version diags |> send_notification
+ in
Fleche.Io.CallBack.
{ trace = (fun _hdr ?extra:_ _msg -> ())
; message = (fun ~lvl:_ ~message:_ -> ())
- ; diagnostics =
- (fun ~uri ~version diags ->
- if List.length diags > 0 then
- Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn)
+ ; diagnostics
; fileProgress = (fun ~uri:_ ~version:_ _progress -> ())
; perfData = (fun ~uri:_ ~version:_ _perf -> ())
+ ; serverVersion = (fun _ -> ())
+ ; serverStatus = (fun _ -> ())
}
(* Main loop *)
let lsp_cb ofn =
+ let send_notification nt =
+ Lsp.Base.Message.(Notification nt |> to_yojson) |> ofn
+ in
+ let trace = LIO.trace in
let message ~lvl ~message =
let lvl = Fleche.Io.Level.to_int lvl in
LIO.logMessageInt ~lvl ~message
in
+ let diagnostics ~uri ~version diags =
+ Lsp.JLang.mk_diagnostics ~uri ~version diags |> send_notification
+ in
+ let fileProgress ~uri ~version progress =
+ Lsp.JFleche.mk_progress ~uri ~version progress |> send_notification
+ in
+ let perfData ~uri ~version perf =
+ Lsp.JFleche.mk_perf ~uri ~version perf |> send_notification
+ in
+ let serverVersion vi = Lsp.JFleche.mk_serverVersion vi |> send_notification in
+ let serverStatus st = Lsp.JFleche.mk_serverStatus st |> send_notification in
Fleche.Io.CallBack.
- { trace = LIO.trace
+ { trace
; message
- ; diagnostics =
- (fun ~uri ~version diags ->
- Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn)
- ; fileProgress =
- (fun ~uri ~version progress ->
- Lsp.JFleche.mk_progress ~uri ~version progress |> ofn)
- ; perfData =
- (fun ~uri ~version perf ->
- Lsp.JFleche.mk_perf ~uri ~version perf |> ofn)
+ ; diagnostics
+ ; fileProgress
+ ; perfData
+ ; serverVersion
+ ; serverStatus
}
let coq_init ~debug =
@@ -116,7 +133,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
let json_fn = LIO.send_json Format.std_formatter in
let ofn response =
- let response = Lsp.Base.Response.to_yojson response in
+ let response = Lsp.Base.Message.to_yojson response in
LIO.send_json Format.std_formatter response
in
diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml
index aa593abb..abc0c48c 100644
--- a/controller/lsp_core.ml
+++ b/controller/lsp_core.ml
@@ -164,28 +164,28 @@ module Rq : sig
end
val serve :
- ofn:(LSP.Response.t -> unit)
+ ofn_rq:(LSP.Response.t -> unit)
-> token:Coq.Limits.Token.t
-> id:int
-> Action.t
-> unit
val cancel :
- ofn:(LSP.Response.t -> unit) -> code:int -> message:string -> int -> unit
+ ofn_rq:(LSP.Response.t -> unit) -> code:int -> message:string -> int -> unit
val serve_postponed :
- ofn:(LSP.Response.t -> unit)
+ ofn_rq:(LSP.Response.t -> unit)
-> token:Coq.Limits.Token.t
-> doc:Fleche.Doc.t
-> Int.Set.t
-> unit
end = struct
(* Answer a request, private *)
- let answer ~ofn ~id result =
+ let answer ~ofn_rq ~id result =
(match result with
| Result.Ok result -> LSP.Response.mk_ok ~id ~result
| Error (code, message) -> LSP.Response.mk_error ~id ~code ~message)
- |> ofn
+ |> ofn_rq
(* private to the Rq module, just used not to retrigger canceled requests *)
let _rtable : (int, Request.Data.t) Hashtbl.t = Hashtbl.create 673
@@ -196,16 +196,16 @@ end = struct
Hashtbl.add _rtable id pr
(* Consumes a request, if alive, it answers mandatorily *)
- let consume_ ~ofn ~f id =
+ let consume_ ~ofn_rq ~f id =
match Hashtbl.find_opt _rtable id with
| Some pr ->
Hashtbl.remove _rtable id;
- f pr |> answer ~ofn ~id
+ f pr |> answer ~ofn_rq ~id
| None ->
LIO.trace "can't consume cancelled request: " (string_of_int id);
()
- let cancel ~ofn ~code ~message id : unit =
+ let cancel ~ofn_rq ~code ~message id : unit =
(* fail the request, do cleanup first *)
let f pr =
let () =
@@ -214,30 +214,30 @@ end = struct
in
Error (code, message)
in
- consume_ ~ofn ~f id
+ consume_ ~ofn_rq ~f id
let debug_serve id pr =
if Fleche.Debug.request_delay then
LIO.trace "serving"
(Format.asprintf "rq: %d | %a" id Request.Data.data pr)
- let serve_postponed ~ofn ~token ~doc id =
+ let serve_postponed ~ofn_rq ~token ~doc id =
let f pr =
debug_serve id pr;
Request.Data.serve ~token ~doc pr
in
- consume_ ~ofn ~f id
+ consume_ ~ofn_rq ~f id
- let query ~ofn ~token ~id (pr : Request.Data.t) =
+ let query ~ofn_rq ~token ~id (pr : Request.Data.t) =
let uri, postpone, request = Request.Data.dm_request pr in
match Fleche.Theory.Request.add { id; uri; postpone; request } with
| Cancel ->
let code = -32802 in
let message = "Document is not ready" in
- Error (code, message) |> answer ~ofn ~id
+ Error (code, message) |> answer ~ofn_rq ~id
| Now doc ->
debug_serve id pr;
- Request.Data.serve ~token ~doc pr |> answer ~ofn ~id
+ Request.Data.serve ~token ~doc pr |> answer ~ofn_rq ~id
| Postpone -> postpone_ ~id pr
module Action = struct
@@ -249,13 +249,13 @@ end = struct
let error (code, msg) = now (Error (code, msg))
end
- let serve ~ofn ~token ~id action =
+ let serve ~ofn_rq ~token ~id action =
match action with
- | Action.Immediate r -> answer ~ofn ~id r
- | Action.Data p -> query ~ofn ~token ~id p
+ | Action.Immediate r -> answer ~ofn_rq ~id r
+ | Action.Data p -> query ~ofn_rq ~token ~id p
- let serve_postponed ~ofn ~token ~doc rl =
- Int.Set.iter (serve_postponed ~ofn ~token ~doc) rl
+ let serve_postponed ~ofn_rq ~token ~doc rl =
+ Int.Set.iter (serve_postponed ~ofn_rq ~token ~doc) rl
end
(***********************************************************************)
@@ -272,7 +272,7 @@ let do_open ~io ~token ~(state : State.t) params =
let env = Fleche.Doc.Env.make ~init ~workspace ~files in
Fleche.Theory.create ~io ~token ~env ~uri ~raw:text ~version
-let do_change ~ofn ~io ~token params =
+let do_change ~ofn_rq ~io ~token params =
let uri, version = Helpers.get_uri_version params in
let changes = List.map U.to_assoc @@ list_field "contentChanges" params in
match changes with
@@ -288,7 +288,7 @@ let do_change ~ofn ~io ~token params =
let invalid_rq = Fleche.Theory.change ~io ~token ~uri ~version ~raw in
let code = -32802 in
let message = "Request got old in server" in
- Int.Set.iter (Rq.cancel ~ofn ~code ~message) invalid_rq
+ Int.Set.iter (Rq.cancel ~ofn_rq ~code ~message) invalid_rq
let do_close ~ofn:_ params =
let uri = Helpers.get_uri params in
@@ -403,11 +403,11 @@ let do_document = do_document_request_maybe ~handler:Rq_document.request
let do_save_vo = do_document_request_maybe ~handler:Rq_save.request
let do_lens = do_document_request_maybe ~handler:Rq_lens.request
-let do_cancel ~ofn ~params =
+let do_cancel ~ofn_rq ~params =
let id = int_field "id" params in
let code = -32800 in
let message = "Cancelled by client" in
- Rq.cancel ~ofn ~code ~message id
+ Rq.cancel ~ofn_rq ~code ~message id
let do_cache_trim () = Nt_cache_trim.notification ()
@@ -456,6 +456,7 @@ module Init_effect = struct
end
let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t =
+ let ofn_rq r = Lsp.Base.Message.response r |> ofn in
match msg with
| LSP.Message.Request { method_ = "initialize"; id; params } ->
(* At this point logging is allowed per LSP spec *)
@@ -465,7 +466,14 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t =
LIO.logMessage ~lvl:Info ~message;
let token = Coq.Limits.Token.create () in
let result, dirs = Rq_init.do_initialize ~params in
- Rq.Action.now (Ok result) |> Rq.serve ~ofn ~token ~id;
+ Rq.Action.now (Ok result) |> Rq.serve ~ofn_rq ~token ~id;
+ let vi =
+ let coq = Coq_config.version in
+ let ocaml = Sys.ocaml_version in
+ let coq_lsp = Fleche.Version.server in
+ Fleche.ServerInfo.Version.{ coq; ocaml; coq_lsp }
+ in
+ Lsp.JFleche.mk_serverVersion vi |> Lsp.Base.Message.notification |> ofn;
let message =
Format.asprintf "Server initializing (int_backend: %s)"
(Coq.Limits.name ())
@@ -483,7 +491,7 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t =
| LSP.Message.Request { id; _ } ->
(* per spec *)
LSP.Response.mk_error ~id ~code:(-32002) ~message:"server not initialized"
- |> ofn;
+ |> ofn_rq;
Loop
| LSP.Message.Notification { method_ = "exit"; params = _ } -> Exit
| LSP.Message.Notification _ ->
@@ -495,6 +503,7 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t =
(** Dispatching *)
let dispatch_notification ~io ~ofn ~token ~state ~method_ ~params : unit =
+ let ofn_rq r = Lsp.Base.Message.response r |> ofn in
match method_ with
(* Lifecycle *)
| "exit" -> raise Lsp_exit
@@ -503,14 +512,14 @@ let dispatch_notification ~io ~ofn ~token ~state ~method_ ~params : unit =
| "workspace/didChangeConfiguration" -> do_changeConfiguration params
(* Document lifetime *)
| "textDocument/didOpen" -> do_open ~io ~token ~state params
- | "textDocument/didChange" -> do_change ~io ~ofn ~token params
+ | "textDocument/didChange" -> do_change ~io ~ofn_rq ~token params
| "textDocument/didClose" -> do_close ~ofn params
| "textDocument/didSave" -> Cache.save_to_disk ()
(* Specific to coq-lsp *)
| "coq/viewRange" -> do_viewRange params
| "coq/trimCaches" -> do_cache_trim ()
(* Cancel Request *)
- | "$/cancelRequest" -> do_cancel ~ofn ~params
+ | "$/cancelRequest" -> do_cancel ~ofn_rq ~params
(* NOOPs *)
| "initialized" -> ()
(* Generic handler *)
@@ -552,17 +561,18 @@ let dispatch_request ~method_ ~params : Rq.Action.t =
LIO.trace "no_handler" msg;
Rq.Action.error (-32601, "method not found")
-let dispatch_request ~ofn ~token ~id ~method_ ~params =
- dispatch_request ~method_ ~params |> Rq.serve ~ofn ~token ~id
+let dispatch_request ~ofn_rq ~token ~id ~method_ ~params =
+ dispatch_request ~method_ ~params |> Rq.serve ~ofn_rq ~token ~id
let dispatch_message ~io ~ofn ~token ~state (com : LSP.Message.t) : State.t =
+ let ofn_rq r = Lsp.Base.Message.response r |> ofn in
match com with
| Notification { method_; params } ->
LIO.trace "process_queue" ("Serving notification: " ^ method_);
dispatch_state_notification ~io ~ofn ~token ~state ~method_ ~params
| Request { id; method_; params } ->
LIO.trace "process_queue" ("Serving Request: " ^ method_);
- dispatch_request ~ofn ~token ~id ~method_ ~params;
+ dispatch_request ~ofn_rq ~token ~id ~method_ ~params;
state
| Response r ->
LIO.trace "process_queue"
@@ -597,10 +607,11 @@ type 'a cont =
| Yield of 'a
let check_or_yield ~io ~ofn ~token ~state =
+ let ofn_rq r = Lsp.Base.Message.response r |> ofn in
match Fleche.Theory.Check.maybe_check ~io ~token with
| None -> Yield state
| Some (ready, doc) ->
- let () = Rq.serve_postponed ~ofn ~token ~doc ready in
+ let () = Rq.serve_postponed ~ofn_rq ~token ~doc ready in
Cont state
module LspQueue : sig
diff --git a/controller/lsp_core.mli b/controller/lsp_core.mli
index e05be395..8581e189 100644
--- a/controller/lsp_core.mli
+++ b/controller/lsp_core.mli
@@ -41,7 +41,7 @@ module Init_effect : sig
end
val lsp_init_process :
- ofn:(Lsp.Base.Response.t -> unit)
+ ofn:(Lsp.Base.Message.t -> unit)
-> cmdline:Coq.Workspace.CmdLine.t
-> debug:bool
-> Lsp.Base.Message.t
@@ -56,7 +56,7 @@ type 'a cont =
wake up pending requests *)
val dispatch_or_resume_check :
io:Fleche.Io.CallBack.t
- -> ofn:(Lsp.Base.Response.t -> unit)
+ -> ofn:(Lsp.Base.Message.t -> unit)
-> state:State.t
-> State.t cont option
diff --git a/coq-lsp.opam b/coq-lsp.opam
index 529414d3..c10c53ce 100644
--- a/coq-lsp.opam
+++ b/coq-lsp.opam
@@ -40,6 +40,8 @@ depends: [
"coq-serapi" { >= "8.18.0+0.18.2" < "8.19" }
]
+depopts: ["lwt" "logs"]
+
build: [
[ "rm" "-rf" "vendor" ]
[ "dune" "build" "-p" name "-j" jobs ]
diff --git a/coq/args.ml b/coq/args.ml
index 83922a01..d9d5a56a 100644
--- a/coq/args.ml
+++ b/coq/args.ml
@@ -96,3 +96,10 @@ let int_backend =
let roots : string list Term.t =
let doc = "Workspace(s) root(s)" in
Arg.(value & opt_all string [] & info [ "root" ] ~docv:"ROOTS" ~doc)
+
+let coq_diags_level : int Term.t =
+ let doc =
+ "Controsl whether Coq Info and Notice message appear in diagnostics.\n\
+ \ 0 = None; 1 = Notices, 2 = Notices and Info"
+ in
+ Arg.(value & opt int 0 & info [ "diags_level" ] ~docv:"DIAGS_LEVEL" ~doc)
diff --git a/coq/args.mli b/coq/args.mli
index 119978e6..0181d2e8 100644
--- a/coq/args.mli
+++ b/coq/args.mli
@@ -18,3 +18,4 @@ val ml_include_path : string list Term.t
val ri_from : (string option * string) list Term.t
val int_backend : Limits.backend option Term.t
val roots : string list Term.t
+val coq_diags_level : int Term.t
diff --git a/fleche/compat.ml b/coq/compat.ml
similarity index 93%
rename from fleche/compat.ml
rename to coq/compat.ml
index d20d7f0b..ea4561c3 100644
--- a/fleche/compat.ml
+++ b/coq/compat.ml
@@ -105,6 +105,14 @@ module Result = struct
let ( let+ ) r f = map f r
let ( let* ) r f = bind r f
end
+
+ let split = function
+ | Ok (x1, x2) -> (Ok x1, Ok x2)
+ | Error err -> (Error err, Error err)
+
+ let pp pp_r pp_e fmt = function
+ | Ok r -> Format.fprintf fmt "@[Ok: @[%a@]@]" pp_r r
+ | Error e -> Format.fprintf fmt "@[Error: @[%a@]@]" pp_e e
end
let format_to_file ~file ~f x =
diff --git a/fleche/compat.mli b/coq/compat.mli
similarity index 79%
rename from fleche/compat.mli
rename to coq/compat.mli
index fa1a01a0..fc56a00c 100644
--- a/fleche/compat.mli
+++ b/coq/compat.mli
@@ -25,4 +25,13 @@ module Result : sig
val ( let+ ) : ('a, 'l) t -> ('a -> 'b) -> ('b, 'l) t
val ( let* ) : ('a, 'l) t -> ('a -> ('b, 'l) t) -> ('b, 'l) t
end
+
+ val split : ('a * 'b, 'e) t -> ('a, 'e) t * ('b, 'e) t
+
+ val pp :
+ (Format.formatter -> 'r -> unit)
+ -> (Format.formatter -> 'e -> unit)
+ -> Format.formatter
+ -> ('r, 'e) Result.t
+ -> unit
end
diff --git a/coq/glob.ml b/coq/glob.ml
new file mode 100644
index 00000000..6c9eb714
--- /dev/null
+++ b/coq/glob.ml
@@ -0,0 +1,190 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(*