From 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 10 Jun 2017 04:57:03 +0200 Subject: [stm] [flags] Move document mode flags to the STM. We move toplevel/STM flags from `Flags` to their proper components; this ensures that low-level code doesn't depend on them, which was incorrect and source of many problems wrt the interfaces. Lower-level components should not be aware whether they are running in batch or interactive mode, but instead provide a functional interface. In particular: == Added flags == - `Safe_typing.allow_delayed_constants` Allow delayed constants in the kernel. - `Flags.record_aux_file` Output `Proof using` information from the kernel. - `System.trust_file_cache` Assume that the file system won't change during our run. == Deleted flags == - `Flags.compilation_mode` - `Flags.batch_mode` Additionally, we modify the STM entry point and `coqtop` to account for the needed state. Note that testing may be necessary and the number of combinations possible exceeds what the test-suite / regular use does. The next step is to fix the initialization problems [c.f. Bugzilla], which will require a larger rework of the STM interface. --- toplevel/coqinit.ml | 4 +- toplevel/coqtop.ml | 193 ++++++++++++++++++++++++++++++++-------------------- toplevel/coqtop.mli | 1 - toplevel/vernac.ml | 52 +++++++------- toplevel/vernac.mli | 6 +- 5 files changed, 151 insertions(+), 105 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 1d5406770..8f676c656 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -32,7 +32,7 @@ let load_rcfile sid = try if !rcfile_specified then if CUnix.file_readable_p !rcfile then - Vernac.load_vernac false sid !rcfile + Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true sid !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) else try @@ -43,7 +43,7 @@ let load_rcfile sid = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac false sid inferedrc + Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true sid inferedrc with Not_found -> sid (* Flags.if_verbose diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c159a1c6a..0624c9bed 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -9,7 +9,6 @@ open Pp open CErrors open Libnames -open Coqinit let () = at_exit flush_all @@ -121,6 +120,14 @@ let print_memory_stat () = let _ = at_exit print_memory_stat +(******************************************************************************) +(* Deprecated *) +(******************************************************************************) +let _remove_top_ml () = Mltop.remove () + +(******************************************************************************) +(* Engagement *) +(******************************************************************************) let impredicative_set = ref Declarations.PredicativeSet let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet let set_type_in_type () = @@ -129,14 +136,18 @@ let set_type_in_type () = let engage () = Global.set_engagement !impredicative_set -let set_batch_mode () = Flags.batch_mode := true - +(******************************************************************************) +(* Interactive toplevel name *) +(******************************************************************************) let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"]) let toplevel_name = ref toplevel_default_name let set_toplevel_name dir = if Names.DirPath.is_empty dir then user_err Pp.(str "Need a non empty toplevel module name"); toplevel_name := dir +(******************************************************************************) +(* Input/Output State *) +(******************************************************************************) let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> strbrk "The inputstate option is deprecated and discouraged.") @@ -164,21 +175,22 @@ let outputstate () = let fname = CUnix.make_suffix !outputstate ".coq" in States.extern_state fname -let set_include d p implicit = - let p = dirpath_of_string p in - push_include d p implicit - +(******************************************************************************) +(* Interactive Load File Simulation *) +(******************************************************************************) let load_vernacular_list = ref ([] : (string * bool) list) + let add_load_vernacular verb s = load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list + let load_vernacular sid = List.fold_left - (fun sid (s,v) -> - let s = Loadpath.locate_file s in + (fun sid (f_in, verbosely) -> + let s = Loadpath.locate_file f_in in if !Flags.beautify then - Flags.(with_option beautify_file (Vernac.load_vernac v sid) s) + Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true sid) f_in else - Vernac.load_vernac v sid s) + Vernac.load_vernac ~verbosely ~interactive:false ~check:true sid s) sid (List.rev !load_vernacular_list) let load_vernacular_obj = ref ([] : string list) @@ -187,6 +199,13 @@ let load_vernac_obj () = let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj) +(******************************************************************************) +(* Required Modules *) +(******************************************************************************) +let set_include d p implicit = + let p = dirpath_of_string p in + Coqinit.push_include d p implicit + let require_prelude () = let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in let vio = Envars.coqlib () / "theories/Init/Prelude.vio" in @@ -209,10 +228,23 @@ let add_compat_require v = | Flags.V8_7 -> add_require "Coq.Compat.Coq87" | Flags.VOld | Flags.Current -> () -let compile_list = ref ([] : (bool * string) list) +(******************************************************************************) +(* File Compilation *) +(******************************************************************************) let glob_opt = ref false +let compile_list = ref ([] : (bool * string) list) +let _compilation_list : Stm.stm_doc_type list ref = ref [] + +let compilation_mode = ref Vernac.BuildVo +let compilation_output_name = ref None + +let batch_mode = ref false +let set_batch_mode () = + System.trust_file_cache := false; + batch_mode := true + let add_compile verbose s = set_batch_mode (); Flags.quiet := true; @@ -226,21 +258,66 @@ let add_compile verbose s = in compile_list := (verbose,s) :: !compile_list -let compile_file (v,f) = +let compile_file mode (verbosely,f_in) = if !Flags.beautify then - Flags.(with_option beautify_file (Vernac.compile v) f) + Flags.with_option Flags.beautify_file (fun f_in -> Vernac.compile ~verbosely ~mode ~f_in ~f_out:None) f_in else - Vernac.compile v f + Vernac.compile ~verbosely ~mode ~f_in ~f_out:None let compile_files () = if !compile_list == [] then () else let init_state = States.freeze ~marshallable:`No in + let mode = !compilation_mode in List.iter (fun vf -> States.unfreeze init_state; - compile_file vf) + compile_file mode vf) (List.rev !compile_list) +(******************************************************************************) +(* VIO Dispatching *) +(******************************************************************************) + +let vio_tasks = ref [] +let add_vio_task f = + set_batch_mode (); + Flags.quiet := true; + vio_tasks := f :: !vio_tasks +let check_vio_tasks () = + let rc = + List.fold_left (fun acc t -> Vio_checking.check_vio t && acc) + true (List.rev !vio_tasks) in + if not rc then exit 1 + +(* vio files *) +let vio_files = ref [] +let vio_files_j = ref 0 +let vio_checking = ref false +let add_vio_file f = + set_batch_mode (); + Flags.quiet := true; + vio_files := f :: !vio_files + +let set_vio_checking_j opt j = + try vio_files_j := int_of_string j + with Failure _ -> + prerr_endline ("The first argument of " ^ opt ^ " must the number"); + prerr_endline "of concurrent workers to be used (a positive integer)."; + prerr_endline "Makefiles generated by coq_makefile should be called"; + prerr_endline "setting the J variable like in 'make vio2vo J=3'"; + exit 1 + +let schedule_vio_checking () = + if !vio_files <> [] && !vio_checking then + Vio_checking.schedule_vio_checking !vio_files_j !vio_files + +let schedule_vio_compilation () = + if !vio_files <> [] && not !vio_checking then + Vio_checking.schedule_vio_compilation !vio_files_j !vio_files + +(******************************************************************************) +(* UI Options *) +(******************************************************************************) (** Options for proof general *) let set_emacs () = @@ -296,14 +373,15 @@ let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesy (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned") exception NoCoqLib -let usage () = + +let usage batch = begin try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib); - init_load_path (); + Coqinit.init_load_path (); with NoCoqLib -> usage_no_coqlib () end; - if !Flags.batch_mode then Usage.print_usage_coqc () + if batch then Usage.print_usage_coqc () else begin Mltop.load_ml_objects_raw_rex (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$")); @@ -389,47 +467,10 @@ let get_error_resilience opt = function let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) -let vio_tasks = ref [] - -let add_vio_task f = - set_batch_mode (); - Flags.quiet := true; - vio_tasks := f :: !vio_tasks - -let check_vio_tasks () = - let rc = - List.fold_left (fun acc t -> Vio_checking.check_vio t && acc) - true (List.rev !vio_tasks) in - if not rc then exit 1 - -let vio_files = ref [] -let vio_files_j = ref 0 -let vio_checking = ref false -let add_vio_file f = - set_batch_mode (); - Flags.quiet := true; - vio_files := f :: !vio_files - -let set_vio_checking_j opt j = - try vio_files_j := int_of_string j - with Failure _ -> - prerr_endline ("The first argument of " ^ opt ^ " must the number"); - prerr_endline "of concurrent workers to be used (a positive integer)."; - prerr_endline "Makefiles generated by coq_makefile should be called"; - prerr_endline "setting the J variable like in 'make vio2vo J=3'"; - exit 1 - let is_not_dash_option = function | Some f when String.length f > 0 && f.[0] <> '-' -> true | _ -> false -let schedule_vio_checking () = - if !vio_files <> [] && !vio_checking then - Vio_checking.schedule_vio_checking !vio_files_j !vio_files -let schedule_vio_compilation () = - if !vio_files <> [] && not !vio_checking then - Vio_checking.schedule_vio_compilation !vio_files_j !vio_files - let get_native_name s = (* We ignore even critical errors because this mode has to be super silent *) try @@ -464,7 +505,7 @@ let parse_args arglist = (* Complex options with many args *) |"-I"|"-include" -> begin match rem with - | d :: rem -> push_ml_include d; args := rem + | d :: rem -> Coqinit.push_ml_include d; args := rem | [] -> error_missing_arg opt end |"-Q" -> @@ -522,7 +563,7 @@ let parse_args arglist = |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true |"-feedback-glob" -> Dumpglob.feedback_glob () |"-exclude-dir" -> System.exclude_directory (next ()) - |"-init-file" -> set_rcfile (next ()) + |"-init-file" -> Coqinit.set_rcfile (next ()) |"-inputstate"|"-is" -> set_inputstate (next ()) |"-load-ml-object" -> Mltop.dir_ml_load (next ()) |"-load-ml-source" -> Mltop.dir_ml_use (next ()) @@ -537,7 +578,9 @@ let parse_args arglist = |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) - |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Flags.Vio2Vo + |"-vio2vo" -> + add_compile false (next ()); + compilation_mode := Vernac.Vio2Vo |"-toploop" -> set_toploop (next ()) |"-w" | "-W" -> let w = next () in @@ -545,7 +588,7 @@ let parse_args arglist = else let w = CWarnings.get_flags () ^ "," ^ w in CWarnings.set_flags (CWarnings.normalize_flags_string w) - |"-o" -> Flags.compilation_output_name := Some (next()) + |"-o" -> compilation_output_name := Some (next()) (* Options with zero arg *) |"-async-queries-always-delegate" @@ -557,15 +600,15 @@ let parse_args arglist = |"-batch" -> set_batch_mode () |"-test-mode" -> Flags.test_mode := true |"-beautify" -> Flags.beautify := true - |"-boot" -> Flags.boot := true; no_load_rc () + |"-boot" -> Flags.boot := true; Coqinit.no_load_rc () |"-bt" -> Backtrace.record_backtrace true |"-color" -> set_color (next ()) |"-config"|"--config" -> print_config := true - |"-debug" -> set_debug () + |"-debug" -> Coqinit.set_debug () |"-stm-debug" -> Flags.stm_debug := true |"-emacs" -> set_emacs () |"-filteropts" -> filter_opts := true - |"-h"|"-H"|"-?"|"-help"|"--help" -> usage () + |"-h"|"-H"|"-?"|"-help"|"--help" -> usage !batch_mode |"-ideslave" -> set_ideslave () |"-impredicative-set" -> set_impredicative_set () |"-indices-matter" -> Indtypes.enforce_indices_matter () @@ -578,9 +621,11 @@ let parse_args arglist = else Flags.native_compiler := true |"-output-context" -> output_context := true |"-profile-ltac" -> Flags.profile_ltac := true - |"-q" -> no_load_rc () + |"-q" -> Coqinit.no_load_rc () |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false - |"-quick" -> Flags.compilation_mode := Flags.BuildVio + |"-quick" -> + Safe_typing.allow_delayed_constants := true; + compilation_mode := Vernac.BuildVio |"-list-tags" -> print_tags := true |"-time" -> Flags.time := true |"-type-in-type" -> set_type_in_type () @@ -615,7 +660,7 @@ let init_toplevel arglist = if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ())); if !print_tags then (print_style_tags (); exit (exitcode ())); if !filter_opts then (print_string (String.concat "\n" extras); exit 0); - init_load_path (); + Coqinit.init_load_path (); Option.iter Mltop.load_ml_object_raw !toploop; let extras = !toploop_init extras in if not (CList.is_empty extras) then begin @@ -627,19 +672,19 @@ let init_toplevel arglist = inputstate (); Mltop.init_known_plugins (); engage (); - if (not !Flags.batch_mode || CList.is_empty !compile_list) + if (not !batch_mode || CList.is_empty !compile_list) && Global.env_is_initial () then Declaremods.start_library !toplevel_name; load_vernac_obj (); require (); - (* XXX: This is incorrect in batch mode, as we will initialize - the STM before having done Declaremods.start_library, thus - state 1 is invalid. This bug was present in 8.5/8.6. *) - Stm.init (); - let sid = load_rcfile (Stm.get_current_state ()) in + Stm.(init { doc_type = Interactive Names.DirPath.empty }); + let sid = Coqinit.load_rcfile (Stm.get_current_state ()) in (* XXX: We ignore this for now, but should be threaded to the toplevels *) let _sid = load_vernacular sid in compile_files (); + (* All these tasks use coqtop as a driver to invoke more coqtop, + * they should be really orthogonal to coqtop. + *) schedule_vio_checking (); schedule_vio_compilation (); check_vio_tasks (); @@ -647,13 +692,13 @@ let init_toplevel arglist = with any -> flush_all(); let extra = - if !Flags.batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) + if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) then None else Some (str "Error during initialization: ") in fatal_error ?extra any end; - if !Flags.batch_mode then begin + if !batch_mode then begin flush_all(); if !output_context then Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 892d64d91..ac2be7e16 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -15,7 +15,6 @@ val init_toplevel : string list -> unit val start : unit -> unit - (* For other toploops *) val toploop_init : (string list -> string list) ref val toploop_run : (unit -> unit) ref diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 1b020bc87..cb89dc8ff 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -113,13 +113,13 @@ let vernac_error msg = (* Stm.End_of_input -> true *) (* | _ -> false *) -let rec interp_vernac sid (loc,com) = +let rec interp_vernac ~check ~interactive sid (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in - load_vernac verbosely sid f + load_vernac ~verbosely ~check ~interactive sid f | v -> (* XXX: We need to run this before add as the classification is @@ -142,17 +142,16 @@ let rec interp_vernac sid (loc,com) = (* Main STM interaction *) if ntip <> `NewTip then anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!"); + (* Due to bug #5363 we cannot use observe here as we should, it otherwise reveals bugs *) (* Stm.observe nsid; *) - - let check_proof = Flags.(!compilation_mode = BuildVo || not !batch_mode) in - if check_proof then Stm.finish (); + if check then Stm.finish (); (* We could use a more refined criteria that depends on the vernac. For now we imitate the old approach and rely on the classification. *) - let print_goals = not !Flags.batch_mode && not !Flags.quiet && + let print_goals = interactive && not !Flags.quiet && is_proof_step && Proof_global.there_are_pending_proofs () in if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); @@ -167,7 +166,7 @@ let rec interp_vernac sid (loc,com) = with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) - if not !Flags.batch_mode then ignore(Stm.edit_at sid); + if interactive then ignore(Stm.edit_at sid); let (reraise, info) = CErrors.push reraise in let info = begin match Loc.get_loc info with @@ -176,7 +175,7 @@ let rec interp_vernac sid (loc,com) = end in iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -and load_vernac verbosely sid file = +and load_vernac ~verbosely ~check ~interactive sid file = let ft_beautify, close_beautify = if !Flags.beautify_file then let chan_beautify = open_out (file^beautify_suffix) in @@ -217,7 +216,7 @@ and load_vernac verbosely sid file = Option.iter (vernac_echo ?loc) in_echo; checknav_simple (loc, ast); - let nsid = Flags.silently (interp_vernac !rsid) (loc, ast) in + let nsid = Flags.silently (interp_vernac ~check ~interactive !rsid) (loc, ast) in rsid := nsid done; !rsid @@ -245,7 +244,7 @@ and load_vernac verbosely sid file = let process_expr sid loc_ast = checknav_deep loc_ast; - interp_vernac sid loc_ast + interp_vernac ~interactive:true ~check:true sid loc_ast let warn_file_no_extension = CWarnings.create ~name:"file-no-extension" ~category:"filesystem" @@ -282,8 +281,10 @@ let ensure_exists f = if not (Sys.file_exists f) then vernac_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) +type compilation_mode = BuildVo | BuildVio | Vio2Vo + (* Compile a vernac file *) -let compile verbosely f = +let compile ~verbosely ~mode ~f_in ~f_out= let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in if not (List.is_empty pfs) then @@ -293,12 +294,12 @@ let compile verbosely f = |> prlist_with_sep pr_comma Names.Id.print) ++ str ".") in - match !Flags.compilation_mode with - | Flags.BuildVo -> - let long_f_dot_v = ensure_v f in + match mode with + | BuildVo -> + let long_f_dot_v = ensure_v f_in in ensure_exists long_f_dot_v; let long_f_dot_vo = - match !Flags.compilation_output_name with + match f_out 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 @@ -309,7 +310,7 @@ let compile verbosely f = Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); let wall_clock1 = Unix.gettimeofday () in - let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in + let _ = load_vernac ~verbosely ~check:true ~interactive:false (Stm.get_current_state ()) long_f_dot_v in Stm.join (); let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -318,32 +319,31 @@ let compile verbosely f = (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); Dumpglob.end_dump_glob () - | Flags.BuildVio -> - let long_f_dot_v = ensure_v f in + | BuildVio -> + let long_f_dot_v = ensure_v f_in in ensure_exists long_f_dot_v; let long_f_dot_vio = - match !Flags.compilation_output_name with + match f_out 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_vio; - let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in + let _ = load_vernac ~verbosely ~check:false ~interactive:false (Stm.get_current_state ()) long_f_dot_v in Stm.finish (); check_pending_proofs (); Stm.snapshot_vio ldir long_f_dot_vio; Stm.reset_task_queue () - | Flags.Vio2Vo -> + | Vio2Vo -> let open Filename in - let open Library in Dumpglob.noglob (); - let f = if check_suffix f ".vio" then chop_extension f else f in - let lfdv, sum, lib, univs, disch, tasks, proofs = load_library_todo f in + let f = if check_suffix f_in ".vio" then chop_extension f_in else f_in in + let lfdv, sum, lib, univs, disch, tasks, proofs = Library.load_library_todo f in Stm.set_compilation_hints lfdv; let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv sum lib univs proofs -let compile v f = +let compile ~verbosely ~mode ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile v f; + compile ~verbosely ~mode ~f_in ~f_out; CoqworkmgrApi.giveback 1 diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index bccf560e1..410dcf0d4 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -17,7 +17,9 @@ val process_expr : Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stateid.t (** [load_vernac echo sid file] Loads [file] on top of [sid], will echo the commands if [echo] is set. Callers are expected to handle and print errors in form of exceptions. *) -val load_vernac : bool -> Stateid.t -> string -> Stateid.t +val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stateid.t -> string -> Stateid.t + +type compilation_mode = BuildVo | BuildVio | Vio2Vo (** Compile a vernac file, (f is assumed without .v suffix) *) -val compile : bool -> string -> unit +val compile : verbosely:bool -> mode:compilation_mode -> f_in:string -> f_out:string option -> unit -- cgit v1.2.3