[fleche] Prepare for caching / sharing of .vo contents

For now we just update the types to get ready for coq/coq#17393 , we
will add the cache in the next commit.

Based on work from #641

coq/init.ml

@@ -85,19 +85,19 @@ let coq_init opts =
 (**************************************************************************)
 
 (* Inits the context for a document *)
-let doc_init ~root_state ~workspace ~uri () =
+let doc_init ~intern ~root_state ~workspace ~uri () =
   (* Lsp.Io.log_error "init" "starting"; *)
   Vernacstate.unfreeze_full_state (State.to_coq root_state);
 
   (* Set load paths from workspace info. *Important*, this has to happen before
      we declare the library below as [Declaremods/Library] will infer the module
      name by looking at the load path! *)
-  Workspace.apply ~uri workspace;
+  Workspace.apply ~intern ~uri workspace;
 
   (* We return the state at this point! *)
   Vernacstate.freeze_full_state () |> State.of_coq
 
-let doc_init ~token:_ ~root_state ~workspace ~uri =
+let doc_init ~token:_ ~intern ~root_state ~workspace ~uri =
   (* Don't interrupt document creation. *)
   let token = Limits.create_atomic () in
-  Protect.eval ~token ~f:(doc_init ~root_state ~workspace ~uri) ()
+  Protect.eval ~token ~f:(doc_init ~intern ~root_state ~workspace ~uri) ()

coq/init.mli

@@ -29,6 +29,7 @@ val coq_init : coq_opts -> State.t
 
 val doc_init :
      token:Limits.Token.t
+  -> intern:Library.Intern.t
   -> root_state:State.t
   -> workspace:Workspace.t
   -> uri:Lang.LUri.File.t

coq/interp.ml

@@ -15,20 +15,21 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-let coq_interp ~st cmd =
+let coq_interp ~intern ~st cmd =
   let st = State.to_coq st in
   let cmd = Ast.to_coq cmd in
-  Vernacinterp.interp ~st cmd |> State.of_coq
+  Vernacinterp.interp ~intern ~st cmd |> State.of_coq
 
-let interp ~token ~st cmd = Protect.eval ~token cmd ~f:(coq_interp ~st)
+let interp ~token ~intern ~st cmd =
+  Protect.eval ~token cmd ~f:(coq_interp ~intern ~st)
 
 module Require = struct
   (* We could improve this Coq upstream by making the API a bit more
      orthogonal *)
-  let interp ~st _files
+  let interp ~intern ~st _files
       { Ast.Require.from; export; mods; loc = _; attrs; control } =
     let () = Vernacstate.unfreeze_full_state (State.to_coq st) in
-    let fn () = Vernacentries.vernac_require from export mods in
+    let fn () = Vernacentries.vernac_require ~intern from export mods in
     (* Check generic attributes *)
     let fn () =
       Synterp.with_generic_atts ~check:true attrs (fun ~atts ->
@@ -40,6 +41,6 @@ module Require = struct
     let () = Utils.with_control ~fn ~control ~st in
     Vernacstate.freeze_full_state () |> State.of_coq
 
-  let interp ~token ~st files cmd =
-    Protect.eval ~token ~f:(interp ~st files) cmd
+  let interp ~token ~intern ~st files cmd =
+    Protect.eval ~token ~f:(interp ~intern ~st files) cmd
 end

coq/interp.mli

@@ -19,7 +19,11 @@
     assumed not to interact with the file-system, etc... Note these commands
     will be memoized. *)
 val interp :
-  token:Limits.Token.t -> st:State.t -> Ast.t -> (State.t, Loc.t) Protect.E.t
+     token:Limits.Token.t
+  -> intern:Library.Intern.t
+  -> st:State.t
+  -> Ast.t
+  -> (State.t, Loc.t) Protect.E.t
 
 (** Interpretation of "require". We wrap this function for two reasons:
 
@@ -28,6 +32,7 @@ val interp :
 module Require : sig
   val interp :
        token:Limits.Token.t
+    -> intern:Library.Intern.t
     -> st:State.t
     -> Files.t
     -> Ast.Require.t

coq/workspace.ml

@@ -262,12 +262,12 @@ let describe_guess = function
   | Error msg -> (msg, "")
 
 (* Require a set of libraries *)
-let load_objs libs =
+let load_objs ~intern libs =
   let rq_file { Require.library; from; flags } =
     let mp = Libnames.qualid_of_string library in
     let mfrom = Option.map Libnames.qualid_of_string from in
     Flags_.silently
-      (Vernacentries.vernac_require mfrom flags)
+      (Vernacentries.vernac_require ~intern mfrom flags)
       [ (mp, Vernacexpr.ImportAll) ]
   in
   List.(iter rq_file (rev libs))
@@ -295,7 +295,7 @@ let dirpath_of_uri ~uri =
   ldir
 
 (* NOTE: Use exhaustive match below to avoid bugs by skipping fields *)
-let apply ~uri
+let apply ~intern ~uri
     { coqlib = _
     ; coqcorelib = _
     ; ocamlpath
@@ -314,7 +314,7 @@ let apply ~uri
   findlib_init ~ml_include_path ~ocamlpath;
   List.iter Loadpath.add_vo_path vo_load_path;
   Declaremods.start_library (dirpath_of_uri ~uri);
-  load_objs require_libs
+  load_objs ~intern require_libs
 
 (* This can raise, and will do in incorrect CoqProject files *)
 let dirpath_of_string_exn coq_path = Libnames.dirpath_of_string coq_path

coq/workspace.mli

@@ -94,7 +94,7 @@ val guess :
 val default : debug:bool -> cmdline:CmdLine.t -> t
 
 (** [apply libname w] will prepare Coq for a new file [libname] on workspace [w] *)
-val apply : uri:Lang.LUri.File.t -> t -> unit
+val apply : intern:Library.Intern.t -> uri:Lang.LUri.File.t -> t -> unit
 
 (** *)
 val dirpath_of_uri : uri:Lang.LUri.File.t -> Names.DirPath.t

fleche/doc.ml

@@ -656,7 +656,10 @@ end = struct
       ->
       Io.Log.trace "recovery" "bullet";
       Coq.State.admit_goal ~token ~st
-      |> Coq.Protect.E.bind ~f:(fun st -> Coq.Interp.interp ~token ~st v)
+      |> Coq.Protect.E.bind ~f:(fun st ->
+             (* We skip the cache here, but likely we don't want to do that. *)
+             let intern = Vernacinterp.fs_intern in
+             Coq.Interp.interp ~token ~intern ~st v)
     | _ ->
       (* Fallback to qed special lex case *)
       lex_recovery_heuristic ~token last_tok contents nodes st

fleche/memo.ml

@@ -287,7 +287,9 @@ module VernacEval = struct
 
   type output = Coq.State.t
 
-  let eval ~token (st, stm) = Coq.Interp.interp ~token ~st stm
+  let eval ~token (st, stm) =
+    let intern = Vernacinterp.fs_intern in
+    Coq.Interp.interp ~token ~intern ~st stm
 end
 
 module Interp = CEval (VernacEval)
@@ -316,7 +318,8 @@ module RequireEval = struct
   type output = Coq.State.t
 
   let eval ~token (st, files, stm) =
-    Coq.Interp.Require.interp ~token ~st files stm
+    let intern = Vernacinterp.fs_intern in
+    Coq.Interp.Require.interp ~token ~intern ~st files stm
 end
 
 module Require = CEval (RequireEval)
@@ -347,7 +350,8 @@ module InitEval = struct
   type output = Coq.State.t
 
   let eval ~token (root_state, workspace, uri) =
-    Coq.Init.doc_init ~token ~root_state ~workspace ~uri
+    let intern = Vernacinterp.fs_intern in
+    Coq.Init.doc_init ~token ~intern ~root_state ~workspace ~uri
 
   let input_info (st, ws, file) =
     Format.asprintf "st %d | ws %d | file %s" (Hashtbl.hash st)

test/serlib/genarg/dune

@@ -1,4 +1,5 @@
 ; Eventually we should use the "put binaries in scope feature of Dune"
+
 (rule
  (targets test_roundtrip)
  (deps