diff options
| author | Emilio Jesus Gallego Arias | 2019-04-01 19:09:59 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-26 16:09:49 -0500 |
| commit | 9d52407e9fccf27d02d952d40f3758dfe1898767 (patch) | |
| tree | 904f2a306b616e23c381cebc3e930da4bf1246fb /kernel | |
| parent | f97cb743386744e9da3ede4b6cf8c803c2f58fde (diff) | |
[native compiler] Allow to set the output directory for cmx objects
This is useful in order to implement native support in Dune for
example, which as of today as strict target rules.
Hopefully this option could go away; it is really internal, but I've
chosen to document it.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativelib.ml | 8 | ||||
| -rw-r--r-- | kernel/nativelib.mli | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index a62b51e8aa..60d4d84705 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -25,7 +25,7 @@ let open_header = ["Nativevalues"; let open_header = List.map mk_open open_header (* Directory where compiled files are stored *) -let output_dir = ".coq-native" +let output_dir = ref ".coq-native" (* Extension of generated ml files, stored for debugging purposes *) let source_ext = ".native" @@ -88,7 +88,7 @@ let error_native_compiler_failed e = let call_compiler ?profile:(profile=false) ml_filename = let load_path = !get_load_paths () in - let load_path = List.map (fun dn -> dn / output_dir) load_path in + let load_path = List.map (fun dn -> dn / !output_dir) load_path in let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in let f = Filename.chop_extension ml_filename in let link_filename = f ^ ".cmo" in @@ -139,7 +139,7 @@ let compile_library dir code fn = let fn = fn ^ source_ext in let basename = Filename.basename fn in let dirname = Filename.dirname fn in - let dirname = dirname / output_dir in + let dirname = dirname / !output_dir in let () = try Unix.mkdir dirname 0o755 with Unix.Unix_error (Unix.EEXIST, _, _) -> () @@ -181,5 +181,5 @@ let call_linker ?(fatal=true) env ~prefix f upds = match upds with Some upds -> update_locations upds | _ -> () let link_library env ~prefix ~dirname ~basename = - let f = dirname / output_dir / basename in + let f = dirname / !output_dir / basename in call_linker env ~fatal:false ~prefix f None diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 52d18acca6..4d95f822e7 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -13,7 +13,7 @@ open Nativecode used by the native compiler. *) (* Directory where compiled files are stored *) -val output_dir : string +val output_dir : CUnix.physical_path ref val get_load_paths : (unit -> string list) ref |