Merge pull request #1077 from ejgallego/vof

[fcc] Allow to save a Fleche cache .vof file

Author: ejgallego

CHANGES.md

@@ -81,6 +81,9 @@
  - [fcc] New option `--trace-file` that will generate trace data for
    visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert,
    #1076)
+ - [fcc] New options `--save_vof` and `--load_vof` that can save a
+   Fleche version of a document to a `.vof` file, thus avoiding
+   `.vo` recompilation for example when calling `fcc --plugin=...` for a given file (@ejgallego, Alexj, #, )
 
 # coq-lsp 0.2.4: (W)Activation
 ------------------------------

compiler/args.ml

@@ -28,6 +28,8 @@ type t =
   ; coq_diags_level : int
         (** Whether to include feedback messages in the diagnostics *)
   ; record_comments : bool  (** Record comments (experimental) *)
+  ; save_vof : bool  (** Save a vof file *)
+  ; load_vof : bool  (** Load a vof file instead of compiling *)
   }
 
 let compute_default_plugins ~no_vo ~plugins =

compiler/cc.ml

@@ -5,4 +5,5 @@ type t =
   ; default : Coq.Workspace.t
   ; io : Fleche.Io.CallBack.t
   ; token : Coq.Limits.Token.t
+  ; save_vof : bool
   }

compiler/compile.ml

@@ -49,8 +49,22 @@ let guess_languageId file =
   | ".v.tex" -> "latex"
   | _ -> "rocq"
 
+let do_save_vof ~io ~token ~doc =
+  match Doc.save_vof ~token ~doc with
+  | Coq.Protect.E.{ r = Coq.Protect.R.Completed (Ok ()); feedback } ->
+    Io.Log.feedback "vof safe" feedback;
+    Io.Report.msg ~io ~lvl:Info "vof file saved"
+  | Coq.Protect.E.{ r = Completed (Error (User msg)); feedback }
+  | Coq.Protect.E.{ r = Completed (Error (Anomaly msg)); feedback } ->
+    Io.Log.feedback "vof safe" feedback;
+    Io.Report.msg ~io ~lvl:Error "error saving vof file %a" Coq.Pp_t.pp_with
+      msg.msg
+  | Coq.Protect.E.{ r = Interrupted; feedback } ->
+    Io.Log.feedback "vof safe" feedback;
+    Io.Report.msg ~io ~lvl:Error "saving vof file interrupted"
+
 let compile_file ~cc file : int =
-  let { Cc.io; root_state; workspaces; default; token } = cc in
+  let { Cc.io; root_state; workspaces; default; token; save_vof } = cc in
   Io.Report.msg ~io ~lvl:Info "compiling file %s" file;
   match Lang.LUri.(File.of_uri (of_string file)) with
   | Error _ -> 222
@@ -67,6 +81,7 @@ let compile_file ~cc file : int =
       save_diags_file ~doc;
       (* Vo file saving is now done by a plugin *)
       Theory.close ~uri;
+      if save_vof then do_save_vof ~io ~token ~doc;
       status_of_doc doc)
 
 let compile_file ~cc file : int =

compiler/driver.ml

@@ -47,6 +47,8 @@ let go ~int_backend args =
       ; max_errors
       ; coq_diags_level
       ; record_comments
+      ; save_vof
+      ; load_vof = _
       } =
     args
   in
@@ -65,7 +67,44 @@ let go ~int_backend args =
   let workspaces = List.map make_ws roots in
   List.iter (log_workspace ~io) workspaces;
   let () = apply_config ~max_errors in
-  let cc = Cc.{ root_state; workspaces; default; io; token } in
+  let cc = Cc.{ root_state; workspaces; default; io; token; save_vof } in
   (* Initialize plugins *)
   plugin_init plugins;
   Compile.compile ~cc ~trace_file files
+
+let go_vof args =
+  let { Args.cmdline = _
+      ; roots = _
+      ; display
+      ; debug = _
+      ; files
+      ; plugins
+      ; trace_file = _
+      ; max_errors = _
+      ; coq_diags_level
+      ; record_comments = _
+      ; save_vof = _
+      ; load_vof = _
+      } =
+    args
+  in
+  let open Fleche in
+  (* Initialize logging; we skip Rocq's init *)
+  let fb_handler = Coq.Init.mk_fb_handler Coq.Protect.fb_queue in
+  ignore (Feedback.add_feeder fb_handler);
+  plugin_init plugins;
+  let perfData = Option.is_empty fcc_test in
+  let io = Output.init ~display ~perfData ~coq_diags_level in
+  let in_file = List.nth files 0 in
+  let in_vof = Filename.(remove_extension in_file) ^ ".vof" in
+  let doc = Doc.doc_of_disk ~in_file:in_vof in
+  Io.Report.msg ~io ~lvl:Info "vof file loaded";
+  Io.Report.msg ~io ~lvl:Info "document has %d nodes" (List.length doc.nodes);
+  Io.Report.msg ~io ~lvl:Info "calling plugins for [Theory.Register.Completed]";
+  (* Call plugins for the .vof file *)
+  let token = Coq.Limits.Token.create () in
+  Theory.Register.Completed.fire ~io ~token ~doc;
+  0
+
+let go ~int_backend (args : Args.t) =
+  if args.load_vof then go_vof args else go ~int_backend args

compiler/fcc.ml

@@ -4,7 +4,7 @@ open Fcc_lib
 
 let fcc_main int_backend roots display debug plugins trace_file files coqlib
     findlib_config ocamlpath rload_path load_path require_libraries no_vo
-    max_errors coq_diags_level record_comments =
+    max_errors coq_diags_level record_comments save_vof load_vof =
   let vo_load_path = rload_path @ load_path in
   let args = [] in
   let cmdline =
@@ -29,6 +29,8 @@ let fcc_main int_backend roots display debug plugins trace_file files coqlib
       ; max_errors
       ; coq_diags_level
       ; record_comments
+      ; save_vof
+      ; load_vof
       }
   in
   Driver.go ~int_backend args
@@ -61,6 +63,14 @@ let no_vo : bool Term.t =
   let doc = "Don't generate .vo files at the end of compilation" in
   Arg.(value & flag & info [ "no_vo" ] ~doc)
 
+let save_vof : bool Term.t =
+  let doc = "Save a .vof file with Fleche-specific metadata" in
+  Arg.(value & flag & info [ "vof" ] ~doc)
+
+let load_vof : bool Term.t =
+  let doc = "Save a .vof file with Fleche-specific metadata" in
+  Arg.(value & flag & info [ "load_vof" ] ~doc)
+
 let max_errors : int option Term.t =
   let doc = "Maximum errors in files before aborting" in
   Arg.(
@@ -106,7 +116,7 @@ let fcc_cmd : int Cmd.t =
       const fcc_main $ int_backend $ roots $ display $ debug $ plugins
       $ trace_file $ file $ coqlib $ findlib_config $ ocamlpath $ rload_paths
       $ qload_paths $ ri_from $ no_vo $ max_errors $ coq_diags_level
-      $ record_comments)
+      $ record_comments $ save_vof $ load_vof)
   in
   let exits = Exit_codes.[ fatal; stopped; scheduled; uri_failed ] in
   Cmd.(v (Cmd.info "fcc" ~exits ~version ~doc ~man) fcc_term)

coq/init.mli

@@ -37,3 +37,6 @@ val doc_init :
   -> workspace:Workspace.t
   -> uri:Lang.LUri.File.t
   -> (State.t, Loc.t) Protect.E.t
+
+val mk_fb_handler :
+  (int * Loc.t Message.Payload.t) list ref -> Feedback.feedback -> unit

fleche/doc.ml

@@ -1212,6 +1212,28 @@ let save ~token ~doc =
     let error = Coq.Pp_t.(str "Can't save document that failed to check") in
     Coq.Protect.E.error error
 
+let doc_to_disk ~doc ~in_file : unit =
+  let out_vof = Filename.(remove_extension in_file) ^ ".vof" in
+  Coq.Compat.Ocaml_414.Out_channel.with_open_bin out_vof (fun oc ->
+      Marshal.to_channel oc doc [])
+
+let doc_of_disk ~in_file : t =
+  let out_vof = Filename.(remove_extension in_file) ^ ".vof" in
+  Stdlib.In_channel.with_open_bin out_vof (fun ic -> Marshal.from_channel ic)
+
+let save_vof ~token ~doc =
+  match doc.completed with
+  | Yes _ ->
+    let st =
+      Util.last doc.nodes |> Stdlib.Option.fold ~some:Node.state ~none:doc.root
+    in
+    let uri = doc.uri in
+    let in_file = Lang.LUri.File.to_string_file uri in
+    Coq.State.in_state ~token ~st ~f:(fun () -> doc_to_disk ~doc ~in_file) ()
+  | _ ->
+    let error = Coq.Pp_t.(str "Can't save document that failed to check") in
+    Coq.Protect.E.error error
+
 (* run api, experimental *)
 
 (* Adaptor, should be supported in memo directly *)

fleche/doc.mli

@@ -170,6 +170,13 @@ val check :
 val save :
   token:Coq.Limits.Token.t -> doc:t -> (unit, Coq.Loc_t.t) Coq.Protect.E.t
 
+(** [save_vof ~doc ... *)
+val save_vof :
+  token:Coq.Limits.Token.t -> doc:t -> (unit, Coq.Loc_t.t) Coq.Protect.E.t
+
+(** Pass .v file *)
+val doc_of_disk : in_file:string -> t
+
 (** [run ~token ?loc ?memo ~st cmds] run commands [cmds] starting on state [st],
     without commiting changes to the document. [loc] can be used to seed an
     initial location if desired, if not the locations will be considered

fleche/theory.mli

@@ -92,5 +92,6 @@ module Register : sig
     type t = io:Io.CallBack.t -> token:Coq.Limits.Token.t -> doc:Doc.t -> unit
 
     val add : t -> unit
+    val fire : io:Io.CallBack.t -> token:Coq.Limits.Token.t -> doc:Doc.t -> unit
   end
 end