From ed2e352802af525fdcc70c6188d37d65894b9254 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 19 Oct 2023 17:18:53 +0200
Subject: [PATCH] [workspace] Support `-rifrom` option.

Both in command line, `CoqProject`, and `fcc`.

Fixes: #579

Thanks to Lasse Blaauwbroek for the report.
---
 CHANGES.md                  |  3 +++
 compiler/fcc.ml             | 14 ++++++++++++--
 controller/coq_lsp.ml       | 15 +++++++++++++--
 coq/workspace.ml            | 31 ++++++++++++++++++++-----------
 coq/workspace.mli           |  1 +
 examples/lists.mv           | 17 ++++++++++++++++-
 test/CoqProject/_CoqProject |  1 +
 test/CoqProject/test.v      |  2 ++
 8 files changed, 68 insertions(+), 16 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 6e8c18b62..4ee537b62 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -39,6 +39,9 @@
  - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
    @CohenCyril, #572, via
    https://github.com/coq-community/coq-nix-toolbox/pull/164 )
+ - Support for `-rifrom` in `_CoqProject` and in command line
+   (`--rifrom`). Thanks to Lasse Blaauwbroek for the report.
+   (@ejgallego, #581, fixes #579)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------
diff --git a/compiler/fcc.ml b/compiler/fcc.ml
index af22182cb..a5905da11 100644
--- a/compiler/fcc.ml
+++ b/compiler/fcc.ml
@@ -3,7 +3,7 @@ open Cmdliner
 open Fcc_lib
 
 let fcc_main roots display debug plugins files coqlib coqcorelib ocamlpath
-    rload_path load_path =
+    rload_path load_path require_libraries =
   let vo_load_path = rload_path @ load_path in
   let ml_include_path = [] in
   let args = [] in
@@ -14,6 +14,7 @@ let fcc_main roots display debug plugins files coqlib coqcorelib ocamlpath
     ; vo_load_path
     ; ml_include_path
     ; args
+    ; require_libraries
     }
   in
   let args = Args.{ cmdline; roots; display; files; debug; plugins } in
@@ -98,6 +99,15 @@ let plugins : string list Term.t =
   let doc = "Compiler plugins to load" in
   Arg.(value & opt_all string [] & info [ "plugin" ] ~docv:"PLUGINS" ~doc)
 
+let rifrom : string list Term.t =
+  let doc =
+    "Require Import Coq LIBRARY before creating the document, à la \
+     Coq.Init.Prelude"
+  in
+  Arg.(
+    value & opt_all dir []
+    & info [ "rifrom"; "require-import-from" ] ~docv:"LIBRARY" ~doc)
+
 let fcc_cmd : unit Cmd.t =
   let doc = "Flèche Coq Compiler" in
   let man =
@@ -111,7 +121,7 @@ let fcc_cmd : unit Cmd.t =
   let fcc_term =
     Term.(
       const fcc_main $ roots $ display $ debug $ plugins $ file $ coqlib
-      $ coqcorelib $ ocamlpath $ rload_path $ load_path)
+      $ coqcorelib $ ocamlpath $ rload_path $ load_path $ rifrom)
   in
   Cmd.(v (Cmd.info "fcc" ~version ~doc ~man) fcc_term)
 
diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
index d241ae05a..2d0cabd25 100644
--- a/controller/coq_lsp.ml
+++ b/controller/coq_lsp.ml
@@ -89,7 +89,8 @@ let rec lsp_init_loop ~ifn ~ofn ~cmdline ~debug =
     | Init_effect.Loop -> lsp_init_loop ~ifn ~ofn ~cmdline ~debug
     | Init_effect.Success w -> w)
 
-let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path delay =
+let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
+    require_libraries delay =
   (* Try to be sane w.r.t. \r\n in Windows *)
   Stdlib.set_binary_mode_in stdin true;
   Stdlib.set_binary_mode_out stdout true;
@@ -116,6 +117,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path delay =
     ; vo_load_path
     ; ml_include_path
     ; args = []
+    ; require_libraries
     }
   in
 
@@ -231,6 +233,15 @@ let ml_include_path : string list Term.t =
   Arg.(
     value & opt_all dir [] & info [ "I"; "ml-include-path" ] ~docv:"DIR" ~doc)
 
+let rifrom : string list Term.t =
+  let doc =
+    "Require Import Coq LIBRARY before creating the document, à la \
+     Coq.Init.Prelude"
+  in
+  Arg.(
+    value & opt_all dir []
+    & info [ "rifrom"; "require-import-from" ] ~docv:"LIBRARY" ~doc)
+
 let delay : float Term.t =
   let doc = "Delay value in seconds when server is idle" in
   Arg.(value & opt float 0.1 & info [ "D"; "idle-delay" ] ~docv:"DELAY" ~doc)
@@ -253,7 +264,7 @@ let lsp_cmd : unit Cmd.t =
       (Cmd.info "coq-lsp" ~version:Fleche.Version.server ~doc ~man)
       Term.(
         const lsp_main $ bt $ coqcorelib $ coqlib $ ocamlpath $ vo_load_path
-        $ ml_include_path $ delay))
+        $ ml_include_path $ rifrom $ delay))
 
 let main () =
   let ecode = Cmd.eval lsp_cmd in
diff --git a/coq/workspace.ml b/coq/workspace.ml
index f6f7a715f..8aa20682d 100644
--- a/coq/workspace.ml
+++ b/coq/workspace.ml
@@ -80,21 +80,22 @@ let mk_userlib unix_path =
 
 let getenv var else_ = try Sys.getenv var with Not_found -> else_
 
-let rec parse_args args init boot f w =
+let rec parse_args args init boot libs f w =
   match args with
-  | [] -> (init, boot, f, List.rev w)
+  | [] -> (init, boot, List.rev libs, f, List.rev w)
+  | "-rifrom" :: lib :: rest -> parse_args rest init boot (lib :: libs) f w
   | "-indices-matter" :: rest ->
-    parse_args rest init boot { f with Flags.indices_matter = true } w
+    parse_args rest init boot libs { f with Flags.indices_matter = true } w
   | "-impredicative-set" :: rest ->
-    parse_args rest init boot { f with Flags.impredicative_set = true } w
-  | "-noinit" :: rest -> parse_args rest false boot f w
-  | "-boot" :: rest -> parse_args rest init true f w
+    parse_args rest init boot libs { f with Flags.impredicative_set = true } w
+  | "-noinit" :: rest -> parse_args rest false boot libs f w
+  | "-boot" :: rest -> parse_args rest init true libs f w
   | "-w" :: warn :: rest ->
     let warn = Warning.make warn in
-    parse_args rest init boot f (warn :: w)
+    parse_args rest init boot libs f (warn :: w)
   | _ :: rest ->
     (* emit warning? *)
-    parse_args rest init boot f w
+    parse_args rest init boot libs f w
 
 module CmdLine = struct
   type t =
@@ -104,9 +105,12 @@ module CmdLine = struct
     ; vo_load_path : Loadpath.vo_path list
     ; ml_include_path : string list
     ; args : string list
+    ; require_libraries : string list
     }
 end
 
+let mk_require_from lib = (lib, None, Some (Lib.Import, None))
+
 let make ~cmdline ~implicit ~kind ~debug =
   let { CmdLine.coqcorelib
       ; coqlib
@@ -114,14 +118,15 @@ let make ~cmdline ~implicit ~kind ~debug =
       ; args
       ; ml_include_path
       ; vo_load_path
+      ; require_libraries
       } =
     cmdline
   in
   let coqcorelib = getenv "COQCORELIB" coqcorelib in
   let coqlib = getenv "COQLIB" coqlib in
   let mk_path_coqlib prefix = coqlib ^ "/" ^ prefix in
-  let init, boot, flags, warnings =
-    parse_args args true false Flags.default []
+  let init, boot, libs, flags, warnings =
+    parse_args args true false [] Flags.default []
   in
   (* Setup ml_include for the core plugins *)
   let dft_ml_include_path, dft_vo_load_path =
@@ -137,7 +142,11 @@ let make ~cmdline ~implicit ~kind ~debug =
         stdlib_vo_path :: user_vo_path )
   in
   let require_libs =
-    if init then [ ("Coq.Init.Prelude", None, Some (Lib.Import, None)) ] else []
+    let rq_list =
+      if init then ("Coq.Init.Prelude" :: require_libraries) @ libs
+      else require_libraries @ libs
+    in
+    List.map mk_require_from rq_list
   in
   let vo_load_path = dft_vo_load_path @ vo_load_path in
   let ml_include_path = dft_ml_include_path @ ml_include_path in
diff --git a/coq/workspace.mli b/coq/workspace.mli
index f64948563..1f2d539a1 100644
--- a/coq/workspace.mli
+++ b/coq/workspace.mli
@@ -63,6 +63,7 @@ module CmdLine : sig
     ; vo_load_path : Loadpath.vo_path list
     ; ml_include_path : string list
     ; args : string list
+    ; require_libraries : string list
     }
 end
 
diff --git a/examples/lists.mv b/examples/lists.mv
index 659bbc591..543b16b8c 100644
--- a/examples/lists.mv
+++ b/examples/lists.mv
@@ -1,4 +1,4 @@
-### Welcome to Coq LSP
+## Welcome to Coq LSP
 
 - You can edit this document as you please
 - Coq will recognize the code snippets as Coq
@@ -9,6 +9,11 @@ From Coq Require Import List.
 Import ListNotations.
 ```
 
+### Here is a simple Proof about Lists
+$$
+  \forall~x~l,
+    \mathsf{rev}(l \mathrel{++} [x]) = x \mathrel{::} (\mathsf{rev}~l)
+$$
 ```coq
 Lemma rev_snoc_cons A :
   forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l.
@@ -19,6 +24,7 @@ Proof.
 Qed.
 ```
 
+### Here is another proof depending on it
 Try to update _above_ and **below**:
 ```coq
 Theorem rev_rev A : forall (l : list A), rev (rev l) = l.
@@ -31,3 +37,12 @@ Qed.
 ```
 
 Please edit your code here!
+
+### Here we do some lambda terms, because we can!
+
+```coq
+Inductive term :=
+  | Var : nat -> term
+  | Abs : term -> term
+  | Lam : term -> term -> term.
+```
diff --git a/test/CoqProject/_CoqProject b/test/CoqProject/_CoqProject
index da0de778b..bda18f5ef 100644
--- a/test/CoqProject/_CoqProject
+++ b/test/CoqProject/_CoqProject
@@ -3,5 +3,6 @@
 
 -arg -w -arg -local-declaration
 -arg -w -arg +non-primitive-record
+-arg -rifrom -arg Coq.Lists.List
 
 test.v
diff --git a/test/CoqProject/test.v b/test/CoqProject/test.v
index ea6b2bcfa..e7cd74d89 100644
--- a/test/CoqProject/test.v
+++ b/test/CoqProject/test.v
@@ -1,3 +1,5 @@
+Search _ list.
+
 Variable (A : nat).
 
 Set Primitive Projections.