diff options
-rw-r--r-- | kernel/nativelib.mli | 3 | ||||
-rw-r--r-- | tools/coq_makefile.ml | 5 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 9 |
3 files changed, 14 insertions, 3 deletions
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index b4a3639f7..0941dc56c 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -10,6 +10,9 @@ open Nativecode (** This file provides facilities to access OCaml compiler and dynamic linker, used by the native compiler. *) +(* Directory where compiled files are stored *) +val output_dir : string + val get_load_paths : (unit -> string list) ref val load_obj : (string -> unit) ref diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 28b86ddc7..badaf280e 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -503,9 +503,14 @@ let parameters () = print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n"; print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n"; print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n"; + print "vo_to_obj = $(addsuffix .o,\\\n"; + print " $(filter-out Warning: Error:,\\\n"; + print " $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n" +(* print "vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),\\\n"; print " $(addprefix $(dir $(vo)),$(addprefix .coq-native/,$(filter-out Warning: Error:,$(firstword \\\n"; print " $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(vo))))))))\n\n" + *) let include_dirs (inc_ml,inc_i,inc_r) = let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 9f670c731..142f33867 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -375,9 +375,12 @@ let schedule_vio_compilation () = if !vio_files <> [] && not !vio_checking then Vio_checking.schedule_vio_compilation !vio_files_j !vio_files -let print_native_name s = +let get_native_name s = (* We ignore even critical errors because this mode has to be super silent *) - try print_endline (Library.native_name_from_filename s) with _ -> () + try + String.concat Filename.dir_sep [Filename.dirname s; + Nativelib.output_dir; Library.native_name_from_filename s] + with _ -> "" let parse_args arglist = let args = ref arglist in @@ -461,7 +464,7 @@ let parse_args arglist = |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ()) |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ()) |"-outputstate" -> set_outputstate (next ()) - |"-print-mod-uid" -> print_native_name (next ()); exit 0 + |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 |"-require" -> add_require (next ()) |"-top" -> set_toplevel_name (dirpath_of_string (next ())) |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) |