diff --git a/coq/workspace.ml b/coq/workspace.ml index 175550e4..11010987 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -56,6 +56,18 @@ module Require = struct } end +module Module : sig + type t + + val make : string -> t +end = struct + type t = string + + (* XXX: A lot more work needs to happen here, in particular we must understand + -Q -R flags and loadpath bindings *) + let make x = x +end + type t = { coqlib : string ; coqcorelib : string @@ -65,6 +77,7 @@ type t = ; require_libs : Require.t list ; flags : Flags.t ; warnings : Warning.t list + ; modules : Module.t list ; kind : string ; debug : bool } @@ -124,7 +137,7 @@ let mk_require_from (from, library) = let flags = Some (Lib.Import, None) in { Require.library; from; flags } -let make ~cmdline ~implicit ~kind ~debug = +let make ~cmdline ~implicit ~kind ~debug ~modules = let { CmdLine.coqcorelib ; coqlib ; ocamlpath @@ -171,6 +184,7 @@ let make ~cmdline ~implicit ~kind ~debug = ; require_libs ; flags ; warnings + ; modules ; kind ; debug } @@ -203,6 +217,7 @@ let describe ; vo_load_path ; ml_include_path ; require_libs + ; modules ; flags = _ ; warnings = _ ; debug = _ @@ -211,6 +226,7 @@ let describe String.concat " " (List.map (fun { Require.library; _ } -> library) require_libs) in + let n_mod = List.length modules in let n_vo = List.length vo_load_path in let n_ml = List.length ml_include_path in let ocamlpath_msg = @@ -249,12 +265,13 @@ let describe \ - coqlib is at: %s@\n\ \ + coqcorelib is at: %s@\n\ \ - Modules [%s] will be loaded by default@\n\ + \ - %d Coq modules (.v files) known@\n\ \ - %d Coq path directory bindings in scope; %d Coq plugin directory \ bindings in scope@\n\ \ - ocamlpath %s@\n\ \ + findlib config: %s@\n\ \ + findlib default location: %s@]" kind coqlib coqcorelib require_msg - n_vo n_ml ocamlpath_msg fl_config fl_location + n_mod n_vo n_ml ocamlpath_msg fl_config fl_location , extra ) let describe_guess = function @@ -304,6 +321,7 @@ let apply ~intern ~uri ; require_libs ; flags ; warnings + ; modules = _ ; kind = _ ; debug } = @@ -319,6 +337,11 @@ let apply ~intern ~uri (* This can raise, and will do in incorrect CoqProject files *) let dirpath_of_string_exn coq_path = Libnames.dirpath_of_string coq_path +let module_from_coqproject { CoqProject_file.thing = file; _ } = + match Filename.extension file with + | ".v" -> Some (Module.make file) + | _ -> None + let workspace_from_coqproject ~cmdline ~debug cp_file : t = (* Io.Log.error "init" "Parsing _CoqProject"; *) let open CoqProject_file in @@ -336,7 +359,7 @@ let workspace_from_coqproject ~cmdline ~debug cp_file : t = in (* XXX: [read_project_file] will do [exit 1] on parsing error! Please someone fix upstream!! *) - let { r_includes; q_includes; ml_includes; extra_args; _ } = + let { r_includes; q_includes; ml_includes; extra_args; files; _ } = read_project_file ~warning_fn:(fun _ -> ()) cp_file in let ml_include_path = List.map (fun f -> f.thing.path) ml_includes in @@ -354,20 +377,21 @@ let workspace_from_coqproject ~cmdline ~debug cp_file : t = ; ml_include_path = cmdline.ml_include_path @ ml_include_path } in + let modules = List.filter_map module_from_coqproject files in let implicit = true in let kind = cp_file in - make ~cmdline ~implicit ~kind ~debug + make ~cmdline ~implicit ~kind ~debug ~modules -let workspace_from_cmdline ~debug ~cmdline = +let workspace_from_cmdline ~debug ~cmdline ~modules = let kind = "Command-line arguments" in let implicit = true in - make ~cmdline ~implicit ~kind ~debug + make ~cmdline ~implicit ~kind ~debug ~modules let guess ~debug ~cmdline ~dir () = let cp_file = Filename.concat dir "_CoqProject" in if Sys.file_exists cp_file then workspace_from_coqproject ~cmdline ~debug cp_file - else workspace_from_cmdline ~debug ~cmdline + else workspace_from_cmdline ~debug ~cmdline ~modules:[] let guess ~token ~debug ~cmdline ~dir = let { Protect.E.r; feedback } = @@ -381,4 +405,4 @@ let guess ~token ~debug ~cmdline ~dir = Error (Format.asprintf "Workspace Scanning Errored: %a" Pp.pp_with msg) | Protect.R.Completed (Ok workspace) -> Ok workspace -let default ~debug ~cmdline = workspace_from_cmdline ~debug ~cmdline +let default ~debug ~cmdline = workspace_from_cmdline ~debug ~cmdline ~modules:[] diff --git a/coq/workspace.mli b/coq/workspace.mli index fb5b461f..4aea1518 100644 --- a/coq/workspace.mli +++ b/coq/workspace.mli @@ -40,6 +40,10 @@ module Require : sig } end +module Module : sig + type t +end + type t = private { coqlib : string ; coqcorelib : string @@ -53,6 +57,7 @@ type t = private (** Modules to preload, usually Coq.Init.Prelude *) ; flags : Flags.t (** Coq-specific flags *) ; warnings : Warning.t list + ; modules : Module.t list ; kind : string (** How the workspace was built *) ; debug : bool (** Enable backtraces *) } diff --git a/test/CoqProject/_CoqProject b/test/CoqProject/_CoqProject index 3bf09db5..8bf3321e 100644 --- a/test/CoqProject/_CoqProject +++ b/test/CoqProject/_CoqProject @@ -6,3 +6,5 @@ -arg -rifrom -arg Coq.Lists -arg List test.v +rest.ml +jest.v diff --git a/test/CoqProject/jest.v b/test/CoqProject/jest.v new file mode 100644 index 00000000..61785add --- /dev/null +++ b/test/CoqProject/jest.v @@ -0,0 +1 @@ +Definition jest := 0. diff --git a/test/CoqProject/rest.ml b/test/CoqProject/rest.ml new file mode 100644 index 00000000..306831a0 --- /dev/null +++ b/test/CoqProject/rest.ml @@ -0,0 +1 @@ +let () = () diff --git a/test/compiler/basic/run.t b/test/compiler/basic/run.t index 7454f38b..fde855d0 100644 --- a/test/compiler/basic/run.t +++ b/test/compiler/basic/run.t @@ -7,6 +7,7 @@ Describe the project - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -18,6 +19,7 @@ Compile a single file, don't generate a `.vo` file: - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -34,6 +36,7 @@ Compile a single file, generate a .vo file - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -54,6 +57,7 @@ Compile a dependent file - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -74,6 +78,7 @@ Compile both files - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -95,6 +100,7 @@ Compile a dependent file without the dep being built - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -132,6 +138,7 @@ Compile a file with all messages: - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -143,6 +150,7 @@ Compile a file with all messages: - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -173,6 +181,7 @@ Use two workspaces - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -181,6 +190,7 @@ Use two workspaces - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -198,6 +208,7 @@ Load the example plugin - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -211,6 +222,7 @@ Load the astdump plugin - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -236,6 +248,7 @@ We do the same for the goaldump plugin: - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] diff --git a/test/compiler/exit_code/run.t b/test/compiler/exit_code/run.t index a3167dc8..c5fda5af 100644 --- a/test/compiler/exit_code/run.t +++ b/test/compiler/exit_code/run.t @@ -8,6 +8,7 @@ Describe the environment: - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 1 Coq modules (.v files) known - 3 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] diff --git a/test/compiler/long_file/run.t b/test/compiler/long_file/run.t index c0450de9..23b30bac 100644 --- a/test/compiler/long_file/run.t +++ b/test/compiler/long_file/run.t @@ -11,6 +11,7 @@ We now compile the challenging file: - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default + - 0 Coq modules (.v files) known - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH]