diff options
| author | Enrico Tassi | 2016-05-19 07:41:09 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-05-19 07:41:09 +0200 |
| commit | 802366bdf00adf3849499f43ba07ee726da0668a (patch) | |
| tree | a5d0c160d98a9f414dc670df47ac5840b86506ea /lib | |
| parent | f7fb1918619fcef384d4aa84938246de67c707fa (diff) | |
coqc: support -o option to specify output file name
The -o option lets one put .vo or .vio files in a directory of choice,
i.e. decouple the location of the sources and the compiled files.
This ease the integration of Coq in already existing IDEs that handle
the build process automatically (eg Eclipse) and also enables one to
compile/run at the same time 2 versions of Coq on the same sources.
Example: b.v depending on a.v
coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo
coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo
coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo
coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/aux_file.ml | 6 | ||||
| -rw-r--r-- | lib/aux_file.mli | 3 | ||||
| -rw-r--r-- | lib/flags.ml | 1 | ||||
| -rw-r--r-- | lib/flags.mli | 1 |
4 files changed, 7 insertions, 4 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml index f7bd81f85d..c814438dd7 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -25,9 +25,9 @@ let mk_absolute vfile = if Filename.is_relative vfile then CUnix.correct_path vfile (Sys.getcwd ()) else vfile -let start_aux_file_for vfile = - let vfile = mk_absolute vfile in - oc := Some (open_out (aux_file_name_for vfile)); +let start_aux_file ~aux_file:output_file ~v_file = + let vfile = mk_absolute v_file in + oc := Some (open_out output_file); Printf.fprintf (Option.get !oc) "COQAUX%d %s %s\n" version (Digest.to_hex (Digest.file vfile)) vfile diff --git a/lib/aux_file.mli b/lib/aux_file.mli index 127827ab6a..86e322b71d 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -17,7 +17,8 @@ module H : Map.S with type key = int * int module M : Map.S with type key = string val contents : aux_file -> string M.t H.t -val start_aux_file_for : string -> unit +val aux_file_name_for : string -> string +val start_aux_file : aux_file:string -> v_file:string -> unit val stop_aux_file : unit -> unit val recording : unit -> bool diff --git a/lib/flags.ml b/lib/flags.ml index c1ec9738ca..9a209a2b3e 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -47,6 +47,7 @@ let batch_mode = ref false type compilation_mode = BuildVo | BuildVio | Vio2Vo let compilation_mode = ref BuildVo +let compilation_output_name = ref None let test_mode = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 24780f0dcc..f52a14a303 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -14,6 +14,7 @@ val load_init : bool ref val batch_mode : bool ref type compilation_mode = BuildVo | BuildVio | Vio2Vo val compilation_mode : compilation_mode ref +val compilation_output_name : string option ref val test_mode : bool ref |