From 3c785936a0b56623f7c3512fa861a7a9823ad495 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 3 Apr 2019 18:38:10 +0200 Subject: Better error message when OCaml compiler not found for native compute Fixes #6699 --- kernel/nativelib.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/nativelib.mli') diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 25adcf224b..d8557e667f 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -21,9 +21,9 @@ val load_obj : (string -> unit) ref val get_ml_filename : unit -> string * string -val compile : string -> global list -> profile:bool -> bool * string +val compile : string -> global list -> profile:bool -> string -val compile_library : Names.DirPath.t -> global list -> string -> bool +val compile_library : Names.DirPath.t -> global list -> string -> unit val call_linker : ?fatal:bool -> string -> string -> code_location_updates option -> unit -- cgit v1.2.3 From 8af91e636038cb113bbd16f7f8225196190bb2d4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 16 Apr 2019 19:56:38 +0200 Subject: [doc] [kernel] Add docstrings for native interface functions. --- kernel/nativelib.mli | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'kernel/nativelib.mli') diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index d8557e667f..e113350368 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -21,8 +21,13 @@ val load_obj : (string -> unit) ref val get_ml_filename : unit -> string * string +(** [compile file code ~profile] will compile native [code] to [file], + and return the name of the object file; this name depends on + whether are in byte mode or not; file is expected to be .ml file *) val compile : string -> global list -> profile:bool -> string +(** [compile_library lib code file] is similar to [compile file code] + but will perform some extra tweaks to handle [code] as a Coq lib. *) val compile_library : Names.DirPath.t -> global list -> string -> unit val call_linker : -- cgit v1.2.3