From 4acfffe7fb7b8e7f802587d5609dc548239d8939 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 20 Jun 2023 22:15:34 +0200 Subject: [PATCH] =?UTF-8?q?[compiler]=20Fl=C3=A8che-based=20command=20line?= =?UTF-8?q?=20compiler.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- .github/workflows/build.yml | 4 + CHANGES.md | 17 ++-- Makefile | 4 + README.md | 11 +++ compiler/args.ml | 14 +++ compiler/cc.ml | 6 ++ compiler/compile.ml | 42 +++++++++ compiler/driver.ml | 48 +++++++++++ compiler/dune | 10 +++ compiler/fcc.ml | 54 ++++++++++++ compiler/fcc.mli | 1 + compiler/output.ml | 60 +++++++++++++ compiler/output.mli | 8 ++ compiler/util.ml | 106 +++++++++++++++++++++++ compiler/util.mli | 4 + controller/coq_lsp.ml | 2 +- controller/lsp_core.ml | 4 +- controller/rq_init.ml | 7 +- dune-project | 2 + fleche/doc.ml | 5 +- fleche/doc.mli | 3 + fleche/theory.mli | 9 ++ {controller => fleche}/version.ml | 0 {controller => fleche}/version.mli | 0 plugins/simple/dune | 4 + plugins/simple/main.ml | 6 ++ test/compiler/_CoqProject | 4 + test/compiler/dune | 5 ++ test/compiler/proj1/a.v | 1 + test/compiler/proj1/b.v | 2 + test/compiler/run.t | 132 +++++++++++++++++++++++++++++ 31 files changed, 559 insertions(+), 16 deletions(-) create mode 100644 compiler/args.ml create mode 100644 compiler/cc.ml create mode 100644 compiler/compile.ml create mode 100644 compiler/driver.ml create mode 100644 compiler/dune create mode 100644 compiler/fcc.ml create mode 100644 compiler/fcc.mli create mode 100644 compiler/output.ml create mode 100644 compiler/output.mli create mode 100644 compiler/util.ml create mode 100644 compiler/util.mli rename {controller => fleche}/version.ml (100%) rename {controller => fleche}/version.mli (100%) create mode 100644 plugins/simple/dune create mode 100644 plugins/simple/main.ml create mode 100644 test/compiler/_CoqProject create mode 100644 test/compiler/dune create mode 100644 test/compiler/proj1/a.v create mode 100644 test/compiler/proj1/b.v create mode 100644 test/compiler/run.t diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index e1ee9375..68d83d1e 100644 --- a/.github/workflows/build.yml +++ b/.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: diff --git a/CHANGES.md b/CHANGES.md index 80a2b700..ee6fa48a 100644 --- a/CHANGES.md +++ b/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 --------------------- diff --git a/Makefile b/Makefile index 4dbb9aec..ca8192cd 100644 --- a/Makefile +++ b/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) diff --git a/README.md b/README.md index fe3ef4a5..79ec1a57 100644 --- a/README.md +++ b/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. Configuration screen +### 🖵 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 diff --git a/compiler/args.ml b/compiler/args.ml new file mode 100644 index 00000000..b358214b --- /dev/null +++ b/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 *) + } diff --git a/compiler/cc.ml b/compiler/cc.ml new file mode 100644 index 00000000..82091f3a --- /dev/null +++ b/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 + } diff --git a/compiler/compile.ml b/compiler/compile.ml new file mode 100644 index 00000000..2623d56e --- /dev/null +++ b/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) diff --git a/compiler/driver.ml b/compiler/driver.ml new file mode 100644 index 00000000..d10e0ff1 --- /dev/null +++ b/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 diff --git a/compiler/dune b/compiler/dune new file mode 100644 index 00000000..a03c0122 --- /dev/null +++ b/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)) diff --git a/compiler/fcc.ml b/compiler/fcc.ml new file mode 100644 index 00000000..e3ad2ba0 --- /dev/null +++ b/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 () diff --git a/compiler/fcc.mli b/compiler/fcc.mli new file mode 100644 index 00000000..e6c353a3 --- /dev/null +++ b/compiler/fcc.mli @@ -0,0 +1 @@ +(* Flèche Coq compiler *) diff --git a/compiler/output.ml b/compiler/output.ml new file mode 100644 index 00000000..5d899cf5 --- /dev/null +++ b/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 diff --git a/compiler/output.mli b/compiler/output.mli new file mode 100644 index 00000000..30f0e24c --- /dev/null +++ b/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 diff --git a/compiler/util.ml b/compiler/util.ml new file mode 100644 index 00000000..31745eb1 --- /dev/null +++ b/compiler/util.ml @@ -0,0 +1,106 @@ +module Ocaml_414 = struct + module In_channel = struct + (* 4.14 can do this: In_channel.with_open_bin file In_channel.input_all, so + we better copy the code XD *) + + let with_open openfun s f = + let ic = openfun s in + Fun.protect ~finally:(fun () -> Stdlib.close_in_noerr ic) (fun () -> f ic) + + let with_open_bin s f = with_open Stdlib.open_in_bin s f + + (* Read up to [len] bytes into [buf], starting at [ofs]. Return total bytes + read. *) + let read_upto ic buf ofs len = + let rec loop ofs len = + if len = 0 then ofs + else + let r = Stdlib.input ic buf ofs len in + if r = 0 then ofs else loop (ofs + r) (len - r) + in + loop ofs len - ofs + + let ensure buf ofs n = + let len = Bytes.length buf in + if len >= ofs + n then buf + else + let new_len = ref len in + while !new_len < ofs + n do + new_len := (2 * !new_len) + 1 + done; + let new_len = !new_len in + let new_len = + if new_len <= Sys.max_string_length then new_len + else if ofs < Sys.max_string_length then Sys.max_string_length + else + failwith + "In_channel.input_all: channel content is larger than maximum \ + string length" + in + let new_buf = Bytes.create new_len in + Bytes.blit buf 0 new_buf 0 ofs; + new_buf + + let input_all ic = + let chunk_size = 65536 in + (* IO_BUFFER_SIZE *) + let initial_size = + try Stdlib.in_channel_length ic - Stdlib.pos_in ic + with Sys_error _ -> -1 + in + let initial_size = + if initial_size < 0 then chunk_size else initial_size + in + let initial_size = + if initial_size <= Sys.max_string_length then initial_size + else Sys.max_string_length + in + let buf = Bytes.create initial_size in + let nread = read_upto ic buf 0 initial_size in + if nread < initial_size then + (* EOF reached, buffer partially filled *) + Bytes.sub_string buf 0 nread + else + (* nread = initial_size, maybe EOF reached *) + match Stdlib.input_char ic with + | exception End_of_file -> + (* EOF reached, buffer is completely filled *) + Bytes.unsafe_to_string buf + | c -> + (* EOF not reached *) + let rec loop buf ofs = + let buf = ensure buf ofs chunk_size in + let rem = Bytes.length buf - ofs in + (* [rem] can be < [chunk_size] if buffer size close to + [Sys.max_string_length] *) + let r = read_upto ic buf ofs rem in + if r < rem then (* EOF reached *) + Bytes.sub_string buf 0 (ofs + r) + else (* r = rem *) + loop buf (ofs + rem) + in + let buf = ensure buf nread (chunk_size + 1) in + Bytes.set buf nread c; + loop buf (nread + 1) + end + + module Out_channel = struct + let with_open openfun s f = + let oc = openfun s in + Fun.protect + ~finally:(fun () -> Stdlib.close_out_noerr oc) + (fun () -> f oc) + + let with_open_bin s f = with_open Stdlib.open_out_bin s f + end +end + +let input_all file = + let open Ocaml_414 in + In_channel.with_open_bin file In_channel.input_all + +let format_to_file ~file ~f x = + let open Ocaml_414 in + Out_channel.with_open_bin file (fun oc -> + let of_fmt = Format.formatter_of_out_channel oc in + Format.fprintf of_fmt "@[%a@]%!" f x) diff --git a/compiler/util.mli b/compiler/util.mli new file mode 100644 index 00000000..b9eaaf94 --- /dev/null +++ b/compiler/util.mli @@ -0,0 +1,4 @@ +val input_all : string -> string + +val format_to_file : + file:string -> f:(Format.formatter -> 'a -> unit) -> 'a -> unit diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 1b6bbbb7..d241ae05 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -250,7 +250,7 @@ let lsp_cmd : unit Cmd.t = let vo_load_path = term_append [ rload_path; load_path ] in Cmd.( v - (Cmd.info "coq-lsp" ~version:Version.server ~doc ~man) + (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)) diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 2f95cf9d..d8dc66e2 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -330,8 +330,8 @@ let version () = | None -> "N/A" | Some bi -> Build_info.V1.Version.to_string bi in - Format.asprintf "version %s, dev: %s, Coq version: %s, OS: %s" Version.server - dev_version Coq_config.version Sys.os_type + Format.asprintf "version %s, dev: %s, Coq version: %s, OS: %s" + Fleche.Version.server dev_version Coq_config.version Sys.os_type module Init_effect = struct type t = diff --git a/controller/rq_init.ml b/controller/rq_init.ml index d23603d6..abc534f4 100644 --- a/controller/rq_init.ml +++ b/controller/rq_init.ml @@ -32,13 +32,14 @@ let do_client_options coq_lsp_options : unit = | Error msg -> LIO.trace "CoqLspOption.of_yojson error: " msg let check_client_version client_version : unit = + let server_version = Fleche.Version.server in LIO.trace "client_version" client_version; - if String.(equal client_version "any" || equal client_version Version.server) + if String.(equal client_version "any" || equal client_version server_version) then () (* Version OK *) else let message = Format.asprintf "Incorrect client version: %s , expected %s." - client_version Version.server + client_version server_version in LIO.logMessage ~lvl:1 ~message @@ -142,7 +143,7 @@ let do_initialize ~params = ; ( "serverInfo" , `Assoc [ ("name", `String "coq-lsp (C) Inria 2022-2023") - ; ("version", `String Version.server) + ; ("version", `String Fleche.Version.server) ] ) ] , dir ) diff --git a/dune-project b/dune-project index 50b68b8e..1f3c77ef 100644 --- a/dune-project +++ b/dune-project @@ -1,6 +1,8 @@ (lang dune 3.2) ; Can't bump to dune > 3.2 due to https://github.com/ocaml/dune/issues/6644 +(cram enable) + (using menhir 2.1) (name coq-lsp) diff --git a/fleche/doc.ml b/fleche/doc.ml index ac149148..bdcb1746 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -217,6 +217,7 @@ type t = (* Flatten the list of document asts *) let asts doc = List.filter_map Node.ast doc.nodes +let diags doc = List.concat_map (fun node -> node.Node.diags) doc.nodes (* TOC handling *) let rec add_toc_info toc { Lang.Ast.Info.name; range; children; _ } = @@ -379,14 +380,12 @@ let add_node ~node doc = let toc = update_toc_node doc.toc node in { doc with nodes = node :: doc.nodes; toc; diags_dirty } -let concat_diags doc = List.concat_map (fun node -> node.Node.diags) doc.nodes - let send_eager_diagnostics ~io ~uri ~version ~doc = (* this is too noisy *) (* let proc_diag = mk_diag loc 3 (Pp.str "Processing") in *) (* Io.Report.diagnostics ~uri ~version (proc_diag :: doc.diags)); *) if doc.diags_dirty && !Config.v.eager_diagnostics then ( - let diags = concat_diags doc in + let diags = diags doc in Io.Report.diagnostics ~io ~uri ~version diags; { doc with diags_dirty = false }) else doc diff --git a/fleche/doc.mli b/fleche/doc.mli index f43fe791..88711422 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -75,6 +75,9 @@ type t = private (** Return the list of all asts in the doc *) val asts : t -> Node.Ast.t list +(** Return the list of all diags in the doc *) +val diags : t -> Lang.Diagnostic.t list + (** Create a new Coq document, this is cached! *) val create : state:Coq.State.t diff --git a/fleche/theory.mli b/fleche/theory.mli index 42755496..1ec98508 100644 --- a/fleche/theory.mli +++ b/fleche/theory.mli @@ -70,3 +70,12 @@ module Request : sig (** Removes the request from the list of things to wake up *) val remove : t -> unit end + +(* Experimental plugin API, not stable yet *) +module Register : sig + module Completed : sig + type t = io:Io.CallBack.t -> doc:Doc.t -> unit + end + + val add : Completed.t -> unit +end diff --git a/controller/version.ml b/fleche/version.ml similarity index 100% rename from controller/version.ml rename to fleche/version.ml diff --git a/controller/version.mli b/fleche/version.mli similarity index 100% rename from controller/version.mli rename to fleche/version.mli diff --git a/plugins/simple/dune b/plugins/simple/dune new file mode 100644 index 00000000..4354b18a --- /dev/null +++ b/plugins/simple/dune @@ -0,0 +1,4 @@ +(library + (name Example_plugin) + (public_name coq-lsp.plugin.example) + (libraries coq-lsp.fleche)) diff --git a/plugins/simple/main.ml b/plugins/simple/main.ml new file mode 100644 index 00000000..6dd38f04 --- /dev/null +++ b/plugins/simple/main.ml @@ -0,0 +1,6 @@ +let simple_action ~io:_ ~doc = + let uri = Lang.LUri.File.to_string_uri doc.Fleche.Doc.uri in + Format.eprintf "[example plugin] file checking for %s was completed@\n%!" uri + +let main () = Fleche.Theory.Register.add simple_action +let () = main () diff --git a/test/compiler/_CoqProject b/test/compiler/_CoqProject new file mode 100644 index 00000000..77011d3b --- /dev/null +++ b/test/compiler/_CoqProject @@ -0,0 +1,4 @@ +-R proj1 . + +a.v +b.v diff --git a/test/compiler/dune b/test/compiler/dune new file mode 100644 index 00000000..7a63250c --- /dev/null +++ b/test/compiler/dune @@ -0,0 +1,5 @@ +(cram + (deps + (source_tree proj1) + (source_tree proj2) + %{bin:fcc})) diff --git a/test/compiler/proj1/a.v b/test/compiler/proj1/a.v new file mode 100644 index 00000000..cb1e5b1b --- /dev/null +++ b/test/compiler/proj1/a.v @@ -0,0 +1 @@ +Definition aa := 3. diff --git a/test/compiler/proj1/b.v b/test/compiler/proj1/b.v new file mode 100644 index 00000000..bb7730cb --- /dev/null +++ b/test/compiler/proj1/b.v @@ -0,0 +1,2 @@ +Require a. +Definition bb := a.aa. diff --git a/test/compiler/run.t b/test/compiler/run.t new file mode 100644 index 00000000..a445e664 --- /dev/null +++ b/test/compiler/run.t @@ -0,0 +1,132 @@ +General tests for the Flèche Compiler + +Describe the project + $ fcc --root proj1 + [message] Configuration loaded from Command-line arguments + - coqlib is at: [TEST_PATH] + - Modules [Coq.Init.Prelude] will be loaded by default + - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope + +Compile a single file + $ fcc --root proj1 proj1/a.v + [message] Configuration loaded from Command-line arguments + - coqlib is at: [TEST_PATH] + - Modules [Coq.Init.Prelude] will be loaded by default + - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope + [message] compiling file proj1/a.v + + $ ls proj1 + a.diags + a.v + a.vo + b.v + +Compile a single file, silent + $ fcc --display=quiet --root proj1 proj1/a.v + +Compile a dependent file + $ fcc --root proj1 proj1/b.v + [message] Configuration loaded from Command-line arguments + - coqlib is at: [TEST_PATH] + - Modules [Coq.Init.Prelude] will be loaded by default + - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope + [message] compiling file proj1/b.v + + $ ls proj1 + a.diags + a.v + a.vo + b.diags + b.v + b.vo + +Compile both files + $ rm proj1/*.vo + $ fcc --root proj1 proj1/a.v proj1/b.v + [message] Configuration loaded from Command-line arguments + - coqlib is at: [TEST_PATH] + - Modules [Coq.Init.Prelude] will be loaded by default + - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope + [message] compiling file proj1/a.v + + [message] compiling file proj1/b.v + + $ ls proj1 + a.diags + a.v + a.vo + b.diags + b.v + b.vo + +Compile a dependent file without the dep being built + $ rm proj1/*.vo + $ fcc --root proj1 proj1/b.v + [message] Configuration loaded from Command-line arguments + - coqlib is at: [TEST_PATH] + - Modules [Coq.Init.Prelude] will be loaded by default + - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope + [message] compiling file proj1/b.v + + $ ls proj1 + a.diags + a.v + b.diags + b.v + b.vo + $ cat proj1/a.diags + { + "range": { + "start": { "line": 0, "character": 0 }, + "end": { "line": 0, "character": 19 } + }, + "severity": 4, + "message": "aa is defined" + } + $ cat proj1/b.diags + { + "range": { + "start": { "line": 0, "character": 0 }, + "end": { "line": 0, "character": 10 } + }, + "severity": 1, + "message": "Cannot find a physical path bound to logical path a." + } + { + "range": { + "start": { "line": 1, "character": 17 }, + "end": { "line": 1, "character": 21 } + }, + "severity": 1, + "message": "The reference a.aa was not found in the current environment." + } + +Use two workspaces + $ rm proj1/*.vo + $ fcc --root proj1 --root proj2 proj1/a.v proj2/b.v + [message] Configuration loaded from Command-line arguments + - coqlib is at: [TEST_PATH] + - Modules [Coq.Init.Prelude] will be loaded by default + - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope + [message] Configuration loaded from Command-line arguments + - coqlib is at: [TEST_PATH] + - Modules [Coq.Init.Prelude] will be loaded by default + - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope + [message] compiling file proj1/a.v + + [message] compiling file proj2/b.v + + fcc: internal error, uncaught exception: + Sys_error("proj2/b.v: No such file or directory") + + [125] + +Load the example plugin + $ fcc --plugin=coq-lsp.plugin.example --root proj1 proj1/a.v + [message] Configuration loaded from Command-line arguments + - coqlib is at: [TEST_PATH] + - Modules [Coq.Init.Prelude] will be loaded by default + - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope + [message] compiling file proj1/a.v + + [example plugin] file checking for proj1/a.v was completed