aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/aux_file.ml6
-rw-r--r--lib/aux_file.mli3
-rw-r--r--lib/flags.ml1
-rw-r--r--lib/flags.mli1
-rw-r--r--library/library.ml16
-rw-r--r--library/library.mli6
-rw-r--r--stm/stm.ml4
-rw-r--r--tools/coqc.ml1
-rw-r--r--toplevel/coqtop.ml1
-rw-r--r--toplevel/usage.ml1
-rw-r--r--toplevel/vernac.ml57
11 files changed, 68 insertions, 29 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index f7bd81f85..c814438dd 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 127827ab6..86e322b71 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 c1ec9738c..9a209a2b3 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 24780f0dc..f52a14a30 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
diff --git a/library/library.ml b/library/library.ml
index 8e2402dda..34dbdfeba 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -628,17 +628,14 @@ let check_module_name s =
done
| c -> err c
-let start_library f =
- let () = if not (Sys.file_exists f) then
- errorlabstrm "" (hov 0 (str "Can't find file" ++ spc () ++ str f))
- in
+let start_library fo =
let ldir0 =
try
- let lp = Loadpath.find_load_path (Filename.dirname f) in
+ let lp = Loadpath.find_load_path (Filename.dirname fo) in
Loadpath.logical lp
with Not_found -> Nameops.default_root_prefix
in
- let file = Filename.chop_extension (Filename.basename f) in
+ let file = Filename.chop_extension (Filename.basename fo) in
let id = Id.of_string file in
check_module_name file;
check_coq_overwriting ldir0 id;
@@ -693,12 +690,13 @@ let error_recursively_dependent_library dir =
writing the content and computing the checksum... *)
let save_library_to ?todo dir f otab =
- let f, except = match todo with
+ let except = match todo with
| None ->
assert(!Flags.compilation_mode = Flags.BuildVo);
- f ^ "o", Future.UUIDSet.empty
+ assert(Filename.check_suffix f ".vo");
+ Future.UUIDSet.empty
| Some (l,_) ->
- f ^ "io",
+ assert(Filename.check_suffix f ".vio");
List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
Future.UUIDSet.empty l in
let cenv, seg, ast = Declaremods.end_library ~except dir in
diff --git a/library/library.mli b/library/library.mli
index 8f5b775d8..b9044b60d 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -37,9 +37,9 @@ type seg_proofs = Term.constr Future.computation array
an export otherwise just a simple import *)
val import_module : bool -> qualid located list -> unit
-(** Start the compilation of a file as a library. The argument must be an
- existing file on the system, and the returned path is the associated
- absolute logical path of the library. *)
+(** Start the compilation of a file as a library. The first argument must be
+ output file, and the
+ returned path is the associated absolute logical path of the library. *)
val start_library : CUnix.physical_path -> DirPath.t
(** End the compilation of a library and save it to a ".vo" file *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 8f11875b6..ebafed8d3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2108,11 +2108,11 @@ let handle_failure (e, info) vcs tty =
VCS.print ();
iraise (e, info)
-let snapshot_vio ldir long_f_dot_v =
+let snapshot_vio ldir long_f_dot_vo =
finish ();
if List.length (VCS.branches ()) > 1 then
Errors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
- Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v
+ Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
(Global.opaque_tables ())
let reset_task_queue = Slaves.reset_task_queue
diff --git a/tools/coqc.ml b/tools/coqc.ml
index f957200ab..d4f1447b1 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -107,6 +107,7 @@ let parse_args () =
|"-load-ml-source"|"-require"|"-load-ml-object"
|"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
|"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
+ |"-o"
as o) :: rem ->
begin
match rem with
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c4222b330..379a96b89 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -514,6 +514,7 @@ let parse_args arglist =
|"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
|"-toploop" -> set_toploop (next ())
|"-w" -> set_warning (next ())
+ |"-o" -> Flags.compilation_output_name := Some (next())
(* Options with zero arg *)
|"-async-queries-always-delegate"
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index f855c096e..aa27b952f 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -45,6 +45,7 @@ let print_usage_channel co command =
\n -require path load Coq library path and import it (Require Import path.)\
\n -compile f.v compile Coq file f.v (implies -batch)\
\n -compile-verbose f.v verbosely compile Coq file f.v (implies -batch)\
+\n -o f.vo use f.vo as the output file name\
\n -quick quickly compile .v files to .vio files (skip proofs)\
\n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\
\n into fi.vo\
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 64225a644..c47fde788 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -291,12 +291,35 @@ let load_vernac verb file =
if !Flags.beautify_file then close_out !chan_beautify;
raise_with_file file (disable_drop e, info)
-let ensure_v f =
- if Filename.check_suffix f ".v" then f
+let ensure_ext ext f =
+ if Filename.check_suffix f ext then f
else begin
msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
- expanded to \"" ++ str f ++ str ".v\"");
- f ^ ".v"
+ expanded to \"" ++ str f ++ str ext ++ str "\"");
+ f ^ ext
+ end
+
+let ensure_bname src tgt =
+ let src, tgt = Filename.basename src, Filename.basename tgt in
+ let src, tgt = Filename.chop_extension src, Filename.chop_extension tgt in
+ if src <> tgt then begin
+ msg_error (str "Source and target file names must coincide, directories can differ");
+ msg_error (str "Source: " ++ str src);
+ msg_error (str "Target: " ++ str tgt);
+ flush_all ();
+ exit 1
+ end
+
+let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt
+
+let ensure_v v = ensure ".v" v v
+let ensure_vo v vo = ensure ".vo" v vo
+let ensure_vio v vio = ensure ".vio" v vio
+
+let ensure_exists f =
+ if not (Sys.file_exists f) then begin
+ msg_error (hov 0 (str "Can't find file" ++ spc () ++ str f));
+ exit 1
end
(* Compile a vernac file *)
@@ -308,9 +331,16 @@ let compile verbosely f =
match !Flags.compilation_mode with
| BuildVo ->
let long_f_dot_v = ensure_v f in
- let ldir = Flags.verbosely Library.start_library long_f_dot_v in
- Stm.set_compilation_hints long_f_dot_v;
- Aux_file.start_aux_file_for long_f_dot_v;
+ ensure_exists long_f_dot_v;
+ let long_f_dot_vo =
+ match !Flags.compilation_output_name with
+ | None -> long_f_dot_v ^ "o"
+ | Some f -> ensure_vo long_f_dot_v f in
+ let ldir = Flags.verbosely Library.start_library long_f_dot_vo in
+ Stm.set_compilation_hints long_f_dot_vo;
+ Aux_file.(start_aux_file
+ ~aux_file:(aux_file_name_for long_f_dot_vo)
+ ~v_file:long_f_dot_v);
Dumpglob.start_dump_glob long_f_dot_v;
Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
if !Flags.xml_export then Hook.get f_xml_start_library ();
@@ -319,7 +349,7 @@ let compile verbosely f =
Stm.join ();
let wall_clock2 = Unix.gettimeofday () in
check_pending_proofs ();
- Library.save_library_to ldir long_f_dot_v (Global.opaque_tables ());
+ Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ());
Aux_file.record_in_aux_at Loc.ghost "vo_compile_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
Aux_file.stop_aux_file ();
@@ -327,13 +357,18 @@ let compile verbosely f =
Dumpglob.end_dump_glob ()
| BuildVio ->
let long_f_dot_v = ensure_v f in
- let ldir = Flags.verbosely Library.start_library long_f_dot_v in
+ ensure_exists long_f_dot_v;
+ let long_f_dot_vio =
+ match !Flags.compilation_output_name with
+ | None -> long_f_dot_v ^ "io"
+ | Some f -> ensure_vio long_f_dot_v f in
+ let ldir = Flags.verbosely Library.start_library long_f_dot_vio in
Dumpglob.noglob ();
- Stm.set_compilation_hints long_f_dot_v;
+ Stm.set_compilation_hints long_f_dot_vio;
let _ = load_vernac verbosely long_f_dot_v in
Stm.finish ();
check_pending_proofs ();
- Stm.snapshot_vio ldir long_f_dot_v;
+ Stm.snapshot_vio ldir long_f_dot_vio;
Stm.reset_task_queue ()
| Vio2Vo ->
let open Filename in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 01:29:08 +0000