Skip to content

Commit

Permalink
[compiler] Flèche-based command line compiler.
Browse files Browse the repository at this point in the history
We expose Flèche compilation capabilities to the command line,
avoiding the need to use LSP for batch compiling.

The `fcc` Flèche Coq Compiler shares many of the features of the
Flèche-based LSP server, in particular, advanced error recovery,
markdown support, _CoqProject detection, caching (which is not yet
very exploited), and the possibility to access all metadata Flèche
knows about.

This PR is for now just a base to experiment, however it should work
fine for most files and use cases.
  • Loading branch information
ejgallego committed Jun 29, 2023
1 parent 4731a66 commit d4df7f3
Show file tree
Hide file tree
Showing 31 changed files with 551 additions and 13 deletions.
4 changes: 4 additions & 0 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
14 changes: 10 additions & 4 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -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,
Expand Down Expand Up @@ -38,7 +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, #)
will set them now (@ejgallego, #517)
- Preliminary plugin API for completion events (@ejgallego, #518,
fixes #506)

# coq-lsp 0.1.6: Peek
---------------------
Expand Down
4 changes: 4 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 dune runtest

.PHONY: fmt format
fmt format:
dune fmt $(DUNEOPT)
Expand Down
11 changes: 11 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down
14 changes: 14 additions & 0 deletions compiler/args.ml
Original file line number Diff line number Diff line change
@@ -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 *)
}
6 changes: 6 additions & 0 deletions compiler/cc.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
(* Compiler context *)
type t =
{ root_state : Coq.State.t
; workspaces : (string * Coq.Workspace.t) list
; io : Fleche.Io.CallBack.t
}
42 changes: 42 additions & 0 deletions compiler/compile.ml
Original file line number Diff line number Diff line change
@@ -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)
40 changes: 40 additions & 0 deletions compiler/driver.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
(* 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 log_workspace ~io (dir, w) =
let message, extra = Coq.Workspace.describe w in
Fleche.Io.Log.trace "workspace" ("initialized " ^ dir) ~extra;
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
10 changes: 10 additions & 0 deletions compiler/dune
Original file line number Diff line number Diff line change
@@ -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))
54 changes: 54 additions & 0 deletions compiler/fcc.ml
Original file line number Diff line number Diff line change
@@ -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 ()
1 change: 1 addition & 0 deletions compiler/fcc.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(* Flèche Coq compiler *)
60 changes: 60 additions & 0 deletions compiler/output.ml
Original file line number Diff line number Diff line change
@@ -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
8 changes: 8 additions & 0 deletions compiler/output.mli
Original file line number Diff line number Diff line change
@@ -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
Loading

0 comments on commit d4df7f3

Please sign in to comment.