diff options
| author | Hugo Herbelin | 2019-05-08 21:28:25 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-14 11:15:15 +0200 |
| commit | 63a953ddc0db1ec1bf101ed6afdf9262d0d9f355 (patch) | |
| tree | b8b12986afa3c31115c57c66e69429047ce6667f /library | |
| parent | d452f359566ec6593aad564acb281f5a49dd931a (diff) | |
Ensuring suffix of file to compile also for -vio2vo checking.
We do it by consistently using variants of the "ensure_exists" policy
in compilation modes: vo (default), vio (-quick), vio2vo (-vio2vo) and
parallel vio2vo (schedule-vio2vo), vio checking (-check-vio-tasks) and
parallel vio checking (schedule-vio-checking).
For instance, coqc -vio2vo dir/file.vio now works, while before,
dir/file was expected.
Incidentally, this avoids the non-recommended Loadpath.locate_file.
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 19 | ||||
| -rw-r--r-- | library/library.mli | 2 |
2 files changed, 9 insertions, 12 deletions
diff --git a/library/library.ml b/library/library.ml index 04e38296d9..500e77f89b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -612,8 +612,6 @@ let import_module export modl = (*s Initializing the compilation of a library. *) let load_library_todo f = - let longf = Loadpath.locate_file (f^".v") in - let f = longf^"io" in let ch = raw_intern_library f in let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in @@ -626,7 +624,7 @@ let load_library_todo f = if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); if s3 = None then user_err ~hdr:"restart" (str"not a .vio file"); if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); - longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 + s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 (************************************************************************) (*s [save_library dir] ends library [dir] and save it to the disk. *) @@ -727,14 +725,13 @@ let save_library_to ?todo ~output_native_objects dir f otab = iraise reraise let save_library_raw f sum lib univs proofs = - let f' = f^"o" in - let ch = raw_extern_library f' in - System.marshal_out_segment f' ch (sum : seg_sum); - System.marshal_out_segment f' ch (lib : seg_lib); - System.marshal_out_segment f' ch (Some univs : seg_univ option); - System.marshal_out_segment f' ch (None : seg_discharge option); - System.marshal_out_segment f' ch (None : 'tasks option); - System.marshal_out_segment f' ch (proofs : seg_proofs); + let ch = raw_extern_library f in + System.marshal_out_segment f ch (sum : seg_sum); + System.marshal_out_segment f ch (lib : seg_lib); + System.marshal_out_segment f ch (Some univs : seg_univ option); + System.marshal_out_segment f ch (None : seg_discharge option); + System.marshal_out_segment f ch (None : 'tasks option); + System.marshal_out_segment f ch (proofs : seg_proofs); close_out ch module StringOrd = struct type t = string let compare = String.compare end diff --git a/library/library.mli b/library/library.mli index a976be0184..390299bf56 100644 --- a/library/library.mli +++ b/library/library.mli @@ -46,7 +46,7 @@ val save_library_to : DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : - string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs + string -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit (** {6 Interrogate the status of libraries } *) |