[fleche] Support .tex literate documents

Similarly to `.mv` files, we recognize `.lv` files to be LaTeX files
with embedded Coq snippets, delimited by `begin/end` pairs.

To have some Coq code recognized inside a `.lv` file do:

```LaTeX
\begin{coq}
\end{coq}
```

Some tweaks to this scheme will be likely needed, for example I'm
unsure the `.lv` extension will work in practice; suggestions welcome!

CHANGES.md

@@ -155,6 +155,8 @@
    allow to change it by clicking on it (@ejgallego, #721)
  - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
    #611)
+ - Support for `.lv / .v.tex` TeX files with embedded Coq code
+   (@ejgallego, #727)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

README.md

@@ -20,6 +20,8 @@ document checking, advanced error recovery, hybrid Coq/markdown document
 support, multiple workspace support, positional goals and information panel,
 performance data, extensible command-line compiler, plugin system, and more.
 
+See the [coq-lsp User Manual](./etc/doc/USER_MANUAL.md) for more information.
+
 `coq-lsp` aims to provide a seamless, modern interactive theorem proving
 experience, as well as to serve as a maintainable platform for research and UI
 integration with other projects.

coq/workspace.ml

@@ -272,6 +272,11 @@ let load_objs libs =
   in
   List.(iter rq_file (rev libs))
 
+let fleche_chop_extension basename =
+  match Filename.chop_suffix_opt ~suffix:".v.tex" basename with
+  | Some file -> file
+  | None -> Filename.chop_extension basename
+
 (* We need to compute this with the right load path *)
 let dirpath_of_uri ~uri =
   let f = Lang.LUri.File.to_string_file uri in
@@ -282,7 +287,7 @@ let dirpath_of_uri ~uri =
     with Not_found -> Libnames.default_root_prefix
   in
   let f =
-    try Filename.chop_extension (Filename.basename f)
+    try fleche_chop_extension (Filename.basename f)
     with Invalid_argument _ -> f
   in
   let id = Names.Id.of_string f in

editor/code/package.json

@@ -29,7 +29,8 @@
     "url": "https://github.com/ejgallego/coq-lsp"
   },
   "activationEvents": [
-    "onLanguage:markdown"
+    "onLanguage:markdown",
+    "onLanguage:latex"
   ],
   "contributes": {
     "languages": [
@@ -54,6 +55,15 @@
         "extensions": [
           ".mv"
         ]
+      },
+      {
+        "id": "latex",
+        "aliases": [
+          "LaTeX"
+        ],
+        "extensions": [
+          ".lv"
+        ]
       }
     ],
     "grammars": [

editor/code/src/config.ts

@@ -81,6 +81,8 @@ export namespace CoqSelector {
   export const all: TextDocumentFilter[] = [
     { language: "coq" },
     { language: "markdown", pattern: "**/*.mv" },
+    { language: "latex", pattern: "**/*.lv" },
+    { language: "latex", pattern: "**/*.v.tex" },
   ];
 
   // Local Coq files, suitable for interaction with a local server

etc/doc/USER_MANUAL.md

@@ -79,9 +79,22 @@ 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.
 
+### 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
 

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:

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:

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"