Merge pull request #507 from ejgallego/compiler

[compiler] Flèche-based command line compiler.

.github/workflows/build.yml

@@ -66,6 +66,10 @@ jobs:
         if: matrix.os != 'windows-latest'
         run: opam exec -- make test
 
+      - name: 🐛 Test fcc
+        if: matrix.os != 'windows-latest'
+        run: opam exec -- make test-compiler
+
   build-nix:
     name: Nix
     strategy:

CHANGES.md

@@ -1,14 +1,18 @@
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------
 
+ - New command line compiler `fcc`. `fcc` allows to access most
+   features of `coq-lsp` without the need for a command line client,
+   and it has been designed to be extensible and machine-friendly
+   (@ejgallego, #507, fixes #472)
+ - Enable web extension support. For now this will not try to start
+   the coq-lsp worker as it is not yet built. (@ejgallego, #430, fixes
+   #234)
  - Improvements and clenaups on hover display, in particular we don't
    print repeated `Notation` strings (@ejgallego, #422)
  - Don't fail on missing serlib plugins, they are indeed an
    optimization; this mostly impacts 8.16 by lowering the SerAPI
    requirements (@ejgallego, #421)
- - Enable web extension support. For now this will not try to start
-   the coq-lsp worker as it is not yet built. (@ejgallego, #430, fixes
-   #234)
  - Fix bug that prevented "Goal after tactic" from working properly
    (@ejgallego, #438, reported by David Ilcinkas)
  - Message about workspace detection was printing the wrong file,
@@ -38,10 +42,9 @@
    reported by Gijs Pennings)
  - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, #511)
  - More granular options `send_perf_data` `send_diags`, `verbosity`
-   will set them now (@ejgallego, #)
- - `.mv` files for Coq Markdown now have markdown as their base mode,
-   this works better and exposes all the usual Markdown commands such
-   as preview to users (@4ever2, #519, fixes #456)
+   will set them now (@ejgallego, #517)
+ - Preliminary plugin API for completion events (@ejgallego, #518,
+   fixes #506)
 
 # coq-lsp 0.1.6: Peek
 ---------------------

Makefile

@@ -29,6 +29,10 @@ test/server/node_modules: test/server/package.json
 test: build test/server/node_modules
 	cd test/server && npm test
 
+.PHONY: test-compiler
+test-compiler: build
+	OCAMLPATH=_build/install/default/lib:$$OCAMLPATH FCC_TEST=true dune runtest
+
 .PHONY: fmt format
 fmt format:
 	dune fmt $(DUNEOPT)

README.md

@@ -38,6 +38,7 @@ and web native usage, providing quite a few extra features from vanilla Coq.
   - [💾 `.vo` file saving](#-vo-file-saving)
   - [⏱️ Detailed Timing and Memory Statistics](#️-detailed-timing-and-memory-statistics)
   - [🔧 Client-Side Configuration Options](#-client-side-configuration-options)
+  - [🖵 Extensible, Machine-friendly Command Line Compiler](#️-extensive-machine-friendly-command-line-compiler)
   - [♻️ Reusability, Standards, Modularity](#️-reusability-standards-modularity)
   - [🌐 Web Native!](#-web-native)
   - [🔎 A Platform for Research!](#-a-platform-for-research)
@@ -161,6 +162,16 @@ See the `coq-lsp` extension configuration in VSCode for options available.
 
 <img alt="Configuration screen" height="286px" src="etc/img/lsp-config.png"/>
 
+### 🖵 Extensible, Machine-friendly Command Line Compiler
+
+`coq-lsp` includes the `fcc` "Flèche Coq Compiler" which allows the access to
+almost all the features of Flèche / `coq-lsp` without the need to spawn a
+fully-fledged LSP client.
+
+`fcc` has been designed to be machine-friendly and extensible, so you can easily
+add your pre/post processing passes, for example to analyze or serialize parts
+of Coq files.
+
 ### ♻️ Reusability, Standards, Modularity
 
 The incremental document checking library of `coq-lsp` has been designed to be

compiler/args.ml

@@ -0,0 +1,14 @@
+module Display = struct
+  type t =
+    | Verbose
+    | Normal
+    | Quiet
+end
+
+type t =
+  { roots : string list  (** workspace root(s) *)
+  ; files : string list  (** files to compile *)
+  ; debug : bool  (** run in debug mode *)
+  ; display : Display.t  (** display level *)
+  ; plugins : string list  (** Flèche plugins to load *)
+  }

compiler/cc.ml

@@ -0,0 +1,6 @@
+(* Compiler context *)
+type t =
+  { root_state : Coq.State.t
+  ; workspaces : (string * Coq.Workspace.t) list
+  ; io : Fleche.Io.CallBack.t
+  }

compiler/compile.ml

@@ -0,0 +1,42 @@
+open Fleche
+
+let is_in_dir ~dir ~file = CString.is_prefix dir file
+
+let workspace_of_uri ~io ~uri ~workspaces =
+  let file = Lang.LUri.File.to_string_file uri in
+  match List.find_opt (fun (dir, _) -> is_in_dir ~dir ~file) workspaces with
+  | None ->
+    Io.Report.message ~io ~lvl:1 ~message:("file not in workspace: " ^ file);
+    snd (List.hd workspaces)
+  | Some (_, workspace) -> workspace
+
+(* Improve errors *)
+let save_vo_file ~doc =
+  match Fleche.Doc.save ~doc with
+  | { r = Completed (Ok ()); feedback = _ } -> ()
+  | { r = Completed (Error _); feedback = _ } -> ()
+  | { r = Interrupted; feedback = _ } -> ()
+
+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
+  Util.format_to_file ~file ~f:Output.pp_diags diags
+
+let compile_file ~cc file =
+  let { Cc.io; root_state; workspaces } = cc in
+  io.message ~lvl:3 ~message:(Format.asprintf "compiling file %s@\n%!" file);
+  match Lang.LUri.(File.of_uri (of_string file)) with
+  | Error _ -> ()
+  | Ok uri -> (
+    let workspace = workspace_of_uri ~io ~workspaces ~uri in
+    let raw = Util.input_all file in
+    let () = Theory.create ~io ~root_state ~workspace ~uri ~raw ~version:1 in
+    match Theory.Check.maybe_check ~io with
+    | None -> ()
+    | Some (_, doc) ->
+      save_vo_file ~doc;
+      save_diags_file ~doc;
+      Theory.close ~uri)
+
+let compile ~cc = List.iter (compile_file ~cc)

compiler/driver.ml

@@ -0,0 +1,48 @@
+(* Duplicated with coq_lsp *)
+let coq_init ~debug =
+  let load_module = Dynlink.loadfile in
+  let load_plugin = Coq.Loader.plugin_handler None in
+  Coq.Init.(coq_init { debug; load_module; load_plugin })
+
+let sanitize_paths message =
+  match Sys.getenv_opt "FCC_TEST" with
+  | None -> message
+  | Some _ ->
+    let home_re = Str.regexp "coqlib is at: .*$" in
+    Str.global_replace home_re "coqlib is at: [TEST_PATH]" message
+
+let log_workspace ~io (dir, w) =
+  let message, extra = Coq.Workspace.describe w in
+  Fleche.Io.Log.trace "workspace" ("initialized " ^ dir) ~extra;
+  let message = sanitize_paths message in
+  Fleche.Io.Report.message ~io ~lvl:3 ~message
+
+let load_plugin plugin_name = Fl_dynload.load_packages [ plugin_name ]
+let plugin_init = List.iter load_plugin
+
+let go args =
+  let { Args.roots; display; debug; files; plugins } = args in
+  (* Initialize event callbacks *)
+  let io = Output.init display in
+  (* Initialize Coq *)
+  let debug = debug || Fleche.Debug.backtraces || !Fleche.Config.v.debug in
+  let root_state = coq_init ~debug in
+  let cmdline =
+    { Coq.Workspace.CmdLine.coqcorelib =
+        Filename.concat Coq_config.coqlib "../coq-core/"
+    ; coqlib = Coq_config.coqlib
+    ; ocamlpath = None
+    ; vo_load_path = []
+    ; ml_include_path = []
+    ; args = []
+    }
+  in
+  let roots = if List.length roots < 1 then [ Sys.getcwd () ] else roots in
+  let workspaces =
+    List.map (fun dir -> (dir, Coq.Workspace.guess ~cmdline ~debug ~dir)) roots
+  in
+  List.iter (log_workspace ~io) workspaces;
+  let cc = Cc.{ root_state; workspaces; io } in
+  (* Initialize plugins *)
+  plugin_init plugins;
+  Compile.compile ~cc files

compiler/dune

@@ -0,0 +1,10 @@
+(library
+ (name fcc_lib)
+ (modules :standard \ fcc)
+ ; LSP is used to print diagnostics, etc...
+ (libraries fleche lsp))
+
+(executable
+ (public_name fcc)
+ (modules fcc)
+ (libraries cmdliner fcc_lib))

compiler/fcc.ml

@@ -0,0 +1,54 @@
+(* Flèche Coq compiler *)
+open Cmdliner
+open Fcc_lib
+
+let fcc_main roots display debug plugins files =
+  let args = Args.{ roots; display; files; debug; plugins } in
+  Driver.go args
+
+let roots : string list Term.t =
+  let doc = "Workspace(s) root(s)" in
+  Arg.(value & opt_all string [] & info [ "root" ] ~docv:"ROOTS" ~doc)
+
+let display : Args.Display.t Term.t =
+  let doc = "Verbosity display settings" in
+  let dparse =
+    Args.Display.[ ("verbose", Verbose); ("normal", Normal); ("quiet", Quiet) ]
+  in
+  Arg.(
+    value
+    & opt (enum dparse) Args.Display.Normal
+    & info [ "display" ] ~docv:"DISPLAY" ~doc)
+
+let debug : bool Term.t =
+  let doc = "Enable debug mode" in
+  Arg.(value & flag & info [ "debug" ] ~docv:"DISPLAY" ~doc)
+
+let file : string list Term.t =
+  let doc = "File(s) to compile" in
+  Arg.(value & pos_all string [] & info [] ~docv:"FILES" ~doc)
+
+let plugins : string list Term.t =
+  let doc = "Compiler plugins to load" in
+  Arg.(value & opt_all string [] & info [ "plugin" ] ~docv:"PLUGINS" ~doc)
+
+let fcc_cmd : unit Cmd.t =
+  let doc = "Flèche Coq Compiler" in
+  let man =
+    [ `S "DESCRIPTION"
+    ; `P "Flèche Coq Compiler"
+    ; `S "USAGE"
+    ; `P "See the documentation on the project's webpage for more information"
+    ]
+  in
+  let version = Fleche.Version.server in
+  let fcc_term =
+    Term.(const fcc_main $ roots $ display $ debug $ plugins $ file)
+  in
+  Cmd.(v (Cmd.info "fcc" ~version ~doc ~man) fcc_term)
+
+let main () =
+  let ecode = Cmd.eval fcc_cmd in
+  exit ecode
+
+let () = main ()

compiler/fcc.mli

@@ -0,0 +1 @@
+(* Flèche Coq compiler *)

compiler/output.ml

@@ -0,0 +1,60 @@
+let pp_diag fmt (d : Lang.Diagnostic.t) =
+  Format.fprintf fmt "@[%a@]"
+    (Yojson.Safe.pretty_print ~std:true)
+    (Lsp.JLang.Diagnostic.to_yojson d)
+
+let pp_diags fmt dl =
+  Format.fprintf fmt "@[%a@]" (Format.pp_print_list pp_diag) dl
+
+(* We will use this when we set eager diagnotics to true *)
+let diagnostics ~uri:_ ~version:_ _diags = ()
+let fileProgress ~uri:_ ~version:_ _progress = ()
+
+(* We print trace and messages *)
+module Fcc_verbose = struct
+  let trace hdr ?extra message =
+    Format.(
+      eprintf "[trace] {%s} %s %a@\n%!" hdr message
+        (pp_print_option pp_print_string)
+        extra)
+
+  let message ~lvl:_ ~message = Format.(eprintf "[message] %s@\n%!" message)
+  let cb = Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress }
+end
+
+(* We print trace and messages *)
+module Fcc_normal = struct
+  let trace _ ?extra:_ _ = ()
+  let message = Fcc_verbose.message
+  let cb = Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress }
+end
+
+module Fcc_quiet = struct
+  let trace _ ?extra:_ _ = ()
+  let message ~lvl:_ ~message:_ = ()
+  let cb = Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress }
+end
+
+let set_callbacks (display : Args.Display.t) =
+  let cb =
+    match display with
+    | Verbose -> Fcc_verbose.cb
+    | Normal -> Fcc_normal.cb
+    | Quiet -> Fcc_quiet.cb
+  in
+  Fleche.Io.CallBack.set cb;
+  cb
+
+let set_config () =
+  Fleche.Config.(
+    v :=
+      { !v with
+        send_perf_data = false
+      ; eager_diagnostics = false
+      ; show_coq_info_messages = true
+      ; show_notices_as_diagnostics = true
+      })
+
+let init display =
+  set_config ();
+  set_callbacks display

compiler/output.mli

@@ -0,0 +1,8 @@
+(** Initialize Console Output System *)
+val init : Args.Display.t -> Fleche.Io.CallBack.t
+
+(** Report progress on file compilation *)
+(* val report : unit -> unit *)
+
+(** Output diagnostics *)
+val pp_diags : Format.formatter -> Lang.Diagnostic.t list -> unit