-
Notifications
You must be signed in to change notification settings - Fork 30
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
77 changed files
with
2,199 additions
and
421 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 *) | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 () |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| (* Flèche Coq compiler *) |
Oops, something went wrong.