diff options
35 files changed, 176 insertions, 255 deletions
diff --git a/API/API.mli b/API/API.mli index 901ed3528b..50fbee5298 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3676,7 +3676,7 @@ sig | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * Feedback.route_id - | VtStm of vernac_control * vernac_part_of_script + | VtBack of vernac_part_of_script * Stateid.t | VtUnknown and vernac_qed_type = | VtKeep @@ -3685,10 +3685,6 @@ sig and vernac_start = string * opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and vernac_part_of_script = bool - and vernac_control = - | VtWait - | VtJoinDocument - | VtBack of Stateid.t and opacity_guarantee = | GuaranteesOpacity | Doesn'tGuaranteeOpacity @@ -3770,7 +3766,6 @@ sig type option_value type showable type bullet - type stm_vernac type comment type register_kind type locatable @@ -3922,7 +3917,6 @@ sig | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list - | VernacStm of stm_vernac | VernacGoal of Constrexpr.constr_expr | VernacAbort of lident option | VernacAbortAll diff --git a/checker/checker.ml b/checker/checker.ml index 7a69700d28..247a98e63e 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open System -open Flags open Names open Check @@ -74,7 +73,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Id.of_string d with CErrors.UserError _ -> - if_verbose Feedback.msg_warning + Flags.if_verbose Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit @@ -342,7 +341,7 @@ let parse_args argv = | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - | "-boot" :: rem -> boot := true; parse rem + | "-boot" :: rem -> Flags.boot := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem @@ -366,15 +365,53 @@ let parse_args argv = (* To prevent from doing the initialization twice *) let initialized = ref false +(* XXX: At some point we need to either port the checker to use the + feedback system or to remove its use completely. *) +let init_feedback_listener () = + let open Format in + let pp_lvl fmt lvl = let open Feedback in match lvl with + | Error -> fprintf fmt "Error: " + | Info -> fprintf fmt "Info: " + | Debug -> fprintf fmt "Debug: " + | Warning -> fprintf fmt "Warning: " + | Notice -> fprintf fmt "" + in + let pp_loc fmt loc = let open Loc in match loc with + | None -> fprintf fmt "" + | Some loc -> + let where = + match loc.fname with InFile f -> f | ToplevelInput -> "Toplevel input" in + fprintf fmt "\"%s\", line %d, characters %d-%d:@\n" + where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in + let checker_feed (fb : Feedback.feedback) = let open Feedback in + match fb.contents with + | Processed -> () + | Incomplete -> () + | Complete -> () + | ProcessingIn _ -> () + | InProgress _ -> () + | WorkerStatus (_,_) -> () + | AddedAxiom -> () + | GlobRef (_,_,_,_,_) -> () + | GlobDef (_,_,_,_) -> () + | FileDependency (_,_) -> () + | FileLoaded (_,_) -> () + | Custom (_,_,_) -> () + (* Re-enable when we switch back to feedback-based error printing *) + | Message (lvl,loc,msg) -> + Format.eprintf "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg + in ignore(Feedback.add_feeder checker_feed) + let init_with_argv argv = if not !initialized then begin initialized := true; Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) + init_feedback_listener (); try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); - if_verbose print_header (); + Flags.if_verbose print_header (); init_load_path (); engage (); with e -> diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 3c9e1cac54..63e28448f9 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -25,7 +25,7 @@ let refresh_arity ar = | _ -> ar, Univ.ContextSet.empty let check_constant_declaration env kn cb = - Feedback.msg_notice (str " checking cst:" ++ prcon kn); + Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn); (** [env'] contains De Bruijn universe variables *) let env' = match cb.const_universes with diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index a420b5d8bb..f91b301b8c 100644 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -328,12 +328,6 @@ ECHO ========== INSTALL CYGWIN ========== REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES. REM Otherwise chmod won't work and e.g. the ocaml build will fail. REM Cygwin setup does not touch the ACLs of existing folders. -REM => Create the setup log in a temporary location and move it later. - -REM Get Unique temporary file name -:logfileloop -SET LOGFILE=%TEMP%\CygwinSetUp%RANDOM%-%RANDOM%-%RANDOM%-%RANDOM%.log -if exist "%LOGFILE%" GOTO logfileloop REM Run Cygwin Setup @@ -348,6 +342,12 @@ IF "%COQREGTESTING%" == "Y" ( SET RUNSETUP=Y ) +SET "EXTRAPACKAGES= " + +IF NOT "%APPVEYOR%" == "True" ( + SET EXTRAPACKAGES="-P wget,curl,git,gcc-core,gcc-g++,automake1.5" +) + IF "%RUNSETUP%"=="Y" ( %SETUP% ^ --proxy "%PROXY%" ^ @@ -356,10 +356,9 @@ IF "%RUNSETUP%"=="Y" ( --local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^ --no-shortcuts ^ %CYGWIN_OPT% ^ - -P wget,curl,git,make,unzip ^ - -P gcc-core,gcc-g++ ^ + -P make,unzip ^ -P gdb,liblzma5 ^ - -P patch,automake1.14,automake1.15 ^ + -P patch,automake1.14 ^ -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^ -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^ -P libiconv-devel,libunistring-devel,libncurses-devel ^ @@ -369,12 +368,11 @@ IF "%RUNSETUP%"=="Y" ( -P gtk-update-icon-cache ^ -P libtool,automake ^ -P intltool ^ - > "%LOGFILE%" ^ + %EXTRAPACKAGES% ^ || GOTO ErrorExit MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build" MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs" - MOVE "%LOGFILE%" "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs\cygwinsetup.log" || GOTO ErrorExit ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 358f527f9e..1bfdf7dfbe 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -5,6 +5,7 @@ set -xe if [ -n "${GITLAB_CI}" ]; then export COQBIN=`pwd`/_install_ci/bin + export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME" else export COQBIN=`pwd`/bin fi diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 127b4a6d2d..cf7d205d8b 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -291,7 +291,10 @@ Pseudocode for listing all of the goals in order: `rev (flat_map fst background) ### <a name="command-status">**Status(force: bool)**</a> -CoqIDE typically sets `force` to `false`. +Returns information about the current proofs. CoqIDE typically sends this +message with `force = false` after each sentence, and with `force = true` if +the user wants to force the checking of all proofs (wheels button). In terms of +the STM API, `force` triggers a `Join`. ```html <call val="Status"><bool val="${force}"/></call> ``` diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 7b879a8031..a54c082979 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -566,7 +566,6 @@ let compare_constr sigma cmp c1 c2 = let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr c2) -(** TODO: factorize with universes.ml *) let test_constr_universes sigma leq m n = let open Universes in let kind c = kind_upto sigma c in @@ -574,14 +573,20 @@ let test_constr_universes sigma leq m n = else let cstrs = ref Constraints.empty in let eq_universes strict l l' = + let l = EInstance.kind sigma (EInstance.make l) in + let l' = EInstance.kind sigma (EInstance.make l') in cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in let eq_sorts s1 s2 = + let s1 = ESorts.kind sigma (ESorts.make s1) in + let s2 = ESorts.kind sigma (ESorts.make s2) in if Sorts.equal s1 s2 then true else (cstrs := Constraints.add (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; true) in let leq_sorts s1 s2 = + let s1 = ESorts.kind sigma (ESorts.make s1) in + let s2 = ESorts.kind sigma (ESorts.make s2) in if Sorts.equal s1 s2 then true else (cstrs := Constraints.add diff --git a/engine/universes.ml b/engine/universes.ml index 719af43edf..686411e7d5 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -131,47 +131,6 @@ let to_constraints g s = "to_constraints: non-trivial algebraic constraint between universes") in Constraints.fold tr s Constraint.empty -let test_constr_univs_infer leq univs fold m n accu = - if m == n then Some accu - else - let cstrs = ref accu in - let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with - | None -> false - | Some accu -> cstrs := accu; true - in - let leq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with - | None -> false - | Some accu -> cstrs := accu; true - in - let rec eq_constr' m n = - m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n - in - let res = - if leq then - let rec compare_leq m n = - Constr.compare_head_gen_leq eq_universes leq_sorts - eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - compare_leq m n - else Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n - in - if res then Some !cstrs else None - -let eq_constr_univs_infer univs fold m n accu = - test_constr_univs_infer false univs fold m n accu - -let leq_constr_univs_infer univs fold m n accu = - test_constr_univs_infer true univs fold m n accu - (** Variant of [eq_constr_univs_infer] taking kind-of-term functions, to expose subterms of [m] and [n], arguments. *) let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = @@ -197,42 +156,6 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in if res then Some !cstrs else None -let test_constr_universes leq m n = - if m == n then Some Constraints.empty - else - let cstrs = ref Constraints.empty in - let eq_universes strict l l' = - cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else (cstrs := Constraints.add - (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; - true) - in - let leq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - (cstrs := Constraints.add - (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; - true) - in - let rec eq_constr' m n = - m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n - in - let res = - if leq then - let rec compare_leq m n = - Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - compare_leq m n - else - Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n - in - if res then Some !cstrs else None - -let eq_constr_universes m n = test_constr_universes false m n -let leq_constr_universes m n = test_constr_universes true m n - let compare_head_gen_proj env equ eqs eqc' m n = match kind_of_term m, kind_of_term n with | Proj (p, c), App (f, args) diff --git a/engine/universes.mli b/engine/universes.mli index fe40f82385..8b2217d446 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -67,11 +67,6 @@ val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_f val to_constraints : UGraph.t -> universe_constraints -> constraints -(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts, - application grouping, the universe constraints in [u] and additional constraints [c]. *) -val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> - constr -> constr -> 'a -> 'a option - (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of {!eq_constr_univs_infer} taking kind-of-term functions, to expose subterms of [m] and [n], arguments. *) @@ -80,20 +75,6 @@ val eq_constr_univs_infer_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option -(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] - modulo alpha, casts, application grouping, the universe constraints - in [u] and additional constraints [c]. *) -val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> - constr -> constr -> 'a -> 'a option - -(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and the universe constraints in [c]. *) -val eq_constr_universes : constr -> constr -> universe_constraints option - -(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe constraints in [c]. *) -val leq_constr_universes : constr -> constr -> universe_constraints option - (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [c]. *) val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index b11a11606f..f00b1e1421 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -413,6 +413,7 @@ let eval_call c = Interface.quit = (fun () -> quit := true); Interface.init = interruptible init; Interface.about = interruptible about; + Interface.wait = interruptible Stm.wait; Interface.interp = interruptible interp; Interface.handle_exn = handle_exn; Interface.stop_worker = Stm.stop_worker; diff --git a/ide/interface.mli b/ide/interface.mli index 1939a8427c..a5d98946f3 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -229,6 +229,9 @@ type print_ast_rty = Xml_datatype.xml type annotate_sty = string type annotate_rty = Xml_datatype.xml +type wait_sty = unit +type wait_rty = unit + type handler = { add : add_sty -> add_rty; edit_at : edit_at_sty -> edit_at_rty; @@ -248,6 +251,8 @@ type handler = { handle_exn : handle_exn_sty -> handle_exn_rty; init : init_sty -> init_rty; quit : quit_sty -> quit_rty; + (* for internal use (fake_id) only, do not use *) + wait : wait_sty -> wait_rty; (* Retrocompatibility stuff *) interp : interp_sty -> interp_rty; } diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 4b521a9682..b452b0a13f 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -531,6 +531,7 @@ let set_options_sty_t : set_options_sty val_t = list_t (pair_t (list_t string_t) option_value_t) let mkcases_sty_t : mkcases_sty val_t = string_t let quit_sty_t : quit_sty val_t = unit_t +let wait_sty_t : wait_sty val_t = unit_t let about_sty_t : about_sty val_t = unit_t let init_sty_t : init_sty val_t = option_t string_t let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t @@ -555,6 +556,7 @@ let get_options_rty_t : get_options_rty val_t = let set_options_rty_t : set_options_rty val_t = unit_t let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t) let quit_rty_t : quit_rty val_t = unit_t +let wait_rty_t : wait_rty val_t = unit_t let about_rty_t : about_rty val_t = coq_info_t let init_rty_t : init_rty val_t = state_id_t let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string_t) @@ -576,6 +578,7 @@ let calls = [| "SetOptions", ($)set_options_sty_t, ($)set_options_rty_t; "MkCases", ($)mkcases_sty_t, ($)mkcases_rty_t; "Quit", ($)quit_sty_t, ($)quit_rty_t; + "Wait", ($)wait_sty_t, ($)wait_rty_t; "About", ($)about_sty_t, ($)about_rty_t; "Init", ($)init_sty_t, ($)init_rty_t; "Interp", ($)interp_sty_t, ($)interp_rty_t; @@ -600,6 +603,8 @@ type 'a call = | About : about_sty -> about_rty call | Init : init_sty -> init_rty call | StopWorker : stop_worker_sty -> stop_worker_rty call + (* internal use (fake_ide) only, do not use *) + | Wait : wait_sty -> wait_rty call (* retrocompatibility *) | Interp : interp_sty -> interp_rty call | PrintAst : print_ast_sty -> print_ast_rty call @@ -618,12 +623,13 @@ let id_of_call : type a. a call -> int = function | SetOptions _ -> 9 | MkCases _ -> 10 | Quit _ -> 11 - | About _ -> 12 - | Init _ -> 13 - | Interp _ -> 14 - | StopWorker _ -> 15 - | PrintAst _ -> 16 - | Annotate _ -> 17 + | Wait _ -> 12 + | About _ -> 13 + | Init _ -> 14 + | Interp _ -> 15 + | StopWorker _ -> 16 + | PrintAst _ -> 17 + | Annotate _ -> 18 let str_of_call c = pi1 calls.(id_of_call c) @@ -643,6 +649,7 @@ let mkcases x : mkcases_rty call = MkCases x let search x : search_rty call = Search x let quit x : quit_rty call = Quit x let init x : init_rty call = Init x +let wait x : wait_rty call = Wait x let interp x : interp_rty call = Interp x let stop_worker x : stop_worker_rty call = StopWorker x let print_ast x : print_ast_rty call = PrintAst x @@ -664,6 +671,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> | SetOptions x -> mkGood (handler.set_options x) | MkCases x -> mkGood (handler.mkcases x) | Quit x -> mkGood (handler.quit x) + | Wait x -> mkGood (handler.wait x) | About x -> mkGood (handler.about x) | Init x -> mkGood (handler.init x) | Interp x -> mkGood (handler.interp x) @@ -688,6 +696,7 @@ let of_answer : type a. a call -> a value -> xml = function | SetOptions _ -> of_value (of_value_type set_options_rty_t) | MkCases _ -> of_value (of_value_type mkcases_rty_t ) | Quit _ -> of_value (of_value_type quit_rty_t ) + | Wait _ -> of_value (of_value_type wait_rty_t ) | About _ -> of_value (of_value_type about_rty_t ) | Init _ -> of_value (of_value_type init_rty_t ) | Interp _ -> of_value (of_value_type interp_rty_t ) @@ -711,6 +720,7 @@ let to_answer : type a. a call -> xml -> a value = function | SetOptions _ -> to_value (to_value_type set_options_rty_t) | MkCases _ -> to_value (to_value_type mkcases_rty_t ) | Quit _ -> to_value (to_value_type quit_rty_t ) + | Wait _ -> to_value (to_value_type wait_rty_t ) | About _ -> to_value (to_value_type about_rty_t ) | Init _ -> to_value (to_value_type init_rty_t ) | Interp _ -> to_value (to_value_type interp_rty_t ) @@ -733,6 +743,7 @@ let of_call : type a. a call -> xml = fun q -> | SetOptions x -> mkCall (of_value_type set_options_sty_t x) | MkCases x -> mkCall (of_value_type mkcases_sty_t x) | Quit x -> mkCall (of_value_type quit_sty_t x) + | Wait x -> mkCall (of_value_type wait_sty_t x) | About x -> mkCall (of_value_type about_sty_t x) | Init x -> mkCall (of_value_type init_sty_t x) | Interp x -> mkCall (of_value_type interp_sty_t x) @@ -756,6 +767,7 @@ let to_call : xml -> unknown_call = | "SetOptions" -> Unknown (SetOptions (mkCallArg set_options_sty_t a)) | "MkCases" -> Unknown (MkCases (mkCallArg mkcases_sty_t a)) | "Quit" -> Unknown (Quit (mkCallArg quit_sty_t a)) + | "Wait" -> Unknown (Wait (mkCallArg wait_sty_t a)) | "About" -> Unknown (About (mkCallArg about_sty_t a)) | "Init" -> Unknown (Init (mkCallArg init_sty_t a)) | "Interp" -> Unknown (Interp (mkCallArg interp_sty_t a)) @@ -786,6 +798,7 @@ let pr_full_value : type a. a call -> a value -> string = fun call value -> matc | SetOptions _ -> pr_value_gen (print set_options_rty_t) value | MkCases _ -> pr_value_gen (print mkcases_rty_t ) value | Quit _ -> pr_value_gen (print quit_rty_t ) value + | Wait _ -> pr_value_gen (print wait_rty_t ) value | About _ -> pr_value_gen (print about_rty_t ) value | Init _ -> pr_value_gen (print init_rty_t ) value | Interp _ -> pr_value_gen (print interp_rty_t ) value @@ -807,6 +820,7 @@ let pr_call : type a. a call -> string = fun call -> | SetOptions x -> return set_options_sty_t x | MkCases x -> return mkcases_sty_t x | Quit x -> return quit_sty_t x + | Wait x -> return wait_sty_t x | About x -> return about_sty_t x | Init x -> return init_sty_t x | Interp x -> return interp_sty_t x diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index d1c678b90f..22117e35c0 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -29,6 +29,8 @@ val set_options : set_options_sty -> set_options_rty call val quit : quit_sty -> quit_rty call val init : init_sty -> init_rty call val stop_worker : stop_worker_sty -> stop_worker_rty call +(* internal use (fake_ide) only, do not use *) +val wait : wait_sty -> wait_rty call (* retrocompatibility *) val interp : interp_sty -> interp_rty call val print_ast : print_ast_sty -> print_ast_rty call diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 94e166f920..fb713d3524 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -280,11 +280,6 @@ type bullet = | Star of int | Plus of int -(** {6 Types concerning Stm} *) -type stm_vernac = - | JoinDocument - | Wait - (** {6 Types concerning the module layer} *) (** Rigid / flexible module signature *) @@ -450,10 +445,6 @@ type vernac_expr = | VernacRegister of lident * register_kind | VernacComments of comment list - (* Stm backdoor: used in fake_id, will be removed when fake_ide - becomes aware of feedback about completed jobs. *) - | VernacStm of stm_vernac - (* Proof management *) | VernacGoal of constr_expr | VernacAbort of lident option @@ -504,16 +495,12 @@ type vernac_type = | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * Feedback.route_id - | VtStm of vernac_control * vernac_part_of_script + | VtBack of vernac_part_of_script * Stateid.t | VtUnknown and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Id.t list and vernac_sideff_type = Id.t list and vernac_part_of_script = bool -and vernac_control = - | VtWait - | VtJoinDocument - | VtBack of Stateid.t and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index de98415cd6..0da22fd71c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -75,10 +75,6 @@ GEXTEND Gram | IDENT "Local"; v = vernac_poly -> VernacLocal (true, v) | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v) - (* Stm backdoor *) - | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument - | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait - | v = vernac_poly -> v ] ] ; diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 1cc072a2a2..260cd04446 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -9,7 +9,6 @@ open CErrors open Util open Pp -open Flags open Names open Libnames open Globnames @@ -387,7 +386,7 @@ let add_coercion_in_graph (ic,source,target) = old_inheritance_graph end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in - if is_ambig && not !quiet then + if is_ambig && not !Flags.quiet then Feedback.msg_info (message_ambig !ambig_paths) type coercion = { diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 1eb22cdb81..5e14307418 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -460,8 +460,11 @@ and detype_r d flags avoid env sigma t = in GVar (Id.of_string s)) | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) - (* using numbers to be unparsable *) - GEvar (Id.of_string ("M" ^ string_of_int n), []) + if n = Constr_matching.special_meta then + (* Using a dash to be unparsable *) + GEvar (Id.of_string_soft "CONTEXT-HOLE", []) + else + GEvar (Id.of_string_soft ("INTERNAL#" ^ string_of_int n), []) | Var id -> (try let _ = Global.lookup_named id in GRef (VarRef id, None) with Not_found -> GVar id) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3563235434..2aa2f90131 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1438,17 +1438,13 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) - let open Universes in - let x = EConstr.Unsafe.to_constr x in - let y = EConstr.Unsafe.to_constr y in try - let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in let b, sigma = let ans = if pb == Reduction.CUMUL then - Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty + EConstr.leq_constr_universes sigma x y else - Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty + EConstr.eq_constr_universes sigma x y in let ans = match ans with | None -> None @@ -1462,6 +1458,8 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) in if b then sigma, true else + let x = EConstr.Unsafe.to_constr x in + let y = EConstr.Unsafe.to_constr y in let sigma' = conv_fun pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y in diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5e57f5de03..51c3eb2129 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -524,12 +524,6 @@ open Decl_kinds | VernacLocal (local, v) -> return (pr_locality local ++ spc() ++ pr_vernac_body v) - (* Stm *) - | VernacStm JoinDocument -> - return (keyword "Stm JoinDocument") - | VernacStm Wait -> - return (keyword "Stm Wait") - (* Proof management *) | VernacAbortAll -> return (keyword "Abort All") diff --git a/stm/stm.ml b/stm/stm.ml index 3386044f26..e0064df9bb 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1049,7 +1049,7 @@ end = struct (* {{{ *) try match v with | VernacResetInitial -> - VtStm (VtBack Stateid.initial, true), VtNow + VtBack (true, Stateid.initial), VtNow | VernacResetName (_,name) -> let id = VCS.get_branch_pos (VCS.current_branch ()) in (try @@ -1057,20 +1057,20 @@ end = struct (* {{{ *) fold_until (fun b (id,_,label,_,_) -> if b then `Stop id else `Cont (List.mem name label)) false id in - VtStm (VtBack oid, true), VtNow + VtBack (true, oid), VtNow with Not_found -> - VtStm (VtBack id, true), VtNow) + VtBack (true, id), VtNow) | VernacBack n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - VtStm (VtBack oid, true), VtNow + VtBack (true, oid), VtNow | VernacUndo n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_,tactic,undo) -> let value = (if tactic then 1 else 0) - undo in if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in - VtStm (VtBack oid, true), VtLater + VtBack (true, oid), VtLater | VernacUndoTo _ | VernacRestart as e -> let m = match e with VernacUndoTo m -> m | _ -> 0 in @@ -1087,16 +1087,16 @@ end = struct (* {{{ *) 0 id in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in - VtStm (VtBack oid, true), VtLater + VtBack (true, oid), VtLater | VernacAbortAll -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun () (id,vcs,_,_,_) -> match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in - VtStm (VtBack oid, true), VtLater + VtBack (true, oid), VtLater | VernacBacktrack (id,_,_) | VernacBackTo id -> - VtStm (VtBack (Stateid.of_int id), not !Flags.batch_mode), VtNow + VtBack (not !Flags.batch_mode, Stateid.of_int id), VtNow | _ -> VtUnknown, VtNow with | Not_found -> @@ -2373,6 +2373,7 @@ let finish () = | _ -> () let wait () = + finish (); Slaves.wait_all_done (); VCS.print () @@ -2386,7 +2387,6 @@ let rec join_admitted_proofs id = | _ -> join_admitted_proofs view.next let join () = - finish (); wait (); stm_prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); @@ -2484,14 +2484,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) stm_prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with - (* Joining various parts of the document *) - | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok - | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok - | VtStm ((VtJoinDocument|VtWait),_), VtLater -> - anomaly(str"classifier: join actions cannot be classified as VtLater.") - (* Back *) - | VtStm (VtBack oid, true), w -> + | VtBack (true, oid), w -> let id = VCS.new_node ~id:newtip () in let { mine; others } = Backtrack.branches_of oid in let valid = VCS.get_branch_pos head in @@ -2510,12 +2504,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) VCS.checkout_shallowest_proof_branch (); VCS.commit id (Alias (oid,x)); Backtrack.record (); if w == VtNow then finish (); `Ok - | VtStm (VtBack id, false), VtNow -> + | VtBack (false, id), VtNow -> stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); Backtrack.backto id; VCS.checkout_shallowest_proof_branch (); Reach.known_state ~cache:(interactive ()) id; `Ok - | VtStm (VtBack id, false), VtLater -> + | VtBack (false, id), VtLater -> anomaly(str"classifier: VtBack + VtLater must imply part_of_script.") (* Query *) @@ -2779,8 +2773,8 @@ let query ~at ~route s = let clas = classify_vernac ast in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in match clas with - | VtStm (w,_), _ -> - ignore(process_transaction aast (VtStm (w,false), VtNow)) + | VtBack (_,id), _ -> (* TODO: can this still happen ? *) + ignore(process_transaction aast (VtBack (false,id), VtNow)) | _ -> ignore(process_transaction aast (VtQuery (false, route), VtNow))) s diff --git a/stm/stm.mli b/stm/stm.mli index 188b176bab..3f01fca013 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -51,6 +51,9 @@ val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ] (* Evaluates the tip of the current branch *) val finish : unit -> unit +(* Internal use (fake_ide) only, do not use *) +val wait : unit -> unit + val observe : Stateid.t -> unit val stop_worker : string -> unit diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index c2ebea961f..158ad90846 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -31,8 +31,7 @@ let string_of_vernac_type = function Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route - | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b - | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b + | VtBack (b, _) -> "Stm Back " ^ string_of_in_script b let string_of_vernac_when = function | VtLater -> "Later" @@ -64,9 +63,6 @@ let rec classify_vernac e = * look at the entire dag to detect this option. *) | VernacSetOption (["Universe"; "Polymorphism"],_) | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow - (* Stm *) - | VernacStm Wait -> VtStm (VtWait, true), VtNow - | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow (* Nested vernac exprs *) | VernacProgram e -> classify_vernac e | VernacLocal (_,e) -> classify_vernac e @@ -79,7 +75,7 @@ let rec classify_vernac e = | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ - | VtStm _ | VtProofMode _ ), _ as x -> x + | VtBack _ | VtProofMode _ ), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtNow diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2b06e1133e..f1dd61358c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -74,7 +74,7 @@ let _ = let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "trigger bugged context matching compatibility"; optkey = ["Tactic";"Compat";"Context"]; optread = (fun () -> !Flags.tactic_context_compat) ; diff --git a/test-suite/bugs/closed/5750.v b/test-suite/bugs/closed/5750.v new file mode 100644 index 0000000000..6d0e21f5d0 --- /dev/null +++ b/test-suite/bugs/closed/5750.v @@ -0,0 +1,3 @@ +(* Check printability of the hole of the context *) +Goal 0 = 0. +match goal with |- context c [0] => idtac c end. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 56e12a1e06..afe8e62ee3 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -500,7 +500,7 @@ uninstall:: instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ rm -f "$$instf" &&\ echo RM "$$instf" &&\ - (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" || true); \ + (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \ done .PHONY: uninstall diff --git a/tools/coqc.ml b/tools/coqc.ml index 862225d3d1..b381c5ba42 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -93,7 +93,7 @@ let parse_args () = | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" - |"-q"|"-profile"|"-just-parsing"|"-echo" |"-quiet" + |"-q"|"-profile"|"-echo" |"-quiet" |"-silent"|"-m"|"-beautify"|"-strict-implicit" |"-impredicative-set"|"-vm"|"-native-compiler" |"-indices-matter"|"-quick"|"-type-in-type" diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index a9da27ba23..79723431cf 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -252,11 +252,9 @@ let eval_print l coq = let to_id, _ = get_id id in eval_call (query (0,(phrase, to_id))) coq | [ Tok(_,"WAIT") ] -> - let phrase = "Stm Wait." in - eval_call (query (0,(phrase,tip_id()))) coq + eval_call (wait ()) coq | [ Tok(_,"JOIN") ] -> - let phrase = "Stm JoinDocument." in - eval_call (query (0,(phrase,tip_id()))) coq + eval_call (status true) coq | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> let to_id, _ = get_id id in if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0f8524e923..c1cdaa5a34 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -8,7 +8,6 @@ open Pp open CErrors -open Flags open Libnames open Coqinit @@ -31,7 +30,7 @@ let print_header () = Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); flush_all () -let warning s = with_option Flags.warn Feedback.msg_warning (strbrk s) +let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) let toploop = ref None @@ -87,7 +86,7 @@ let console_toploop_run () = (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in if Dumpglob.dump () then begin - if_verbose warning "Dumpglob cannot be used in interactive mode."; + Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; Coqloop.loop(); @@ -130,7 +129,7 @@ let set_type_in_type () = let engage () = Global.set_engagement !impredicative_set -let set_batch_mode () = batch_mode := true +let set_batch_mode () = Flags.batch_mode := true let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"]) let toplevel_name = ref toplevel_default_name @@ -177,7 +176,7 @@ let load_vernacular sid = (fun sid (s,v) -> let s = Loadpath.locate_file s in if !Flags.beautify then - with_option beautify_file (Vernac.load_vernac v sid) s + Flags.(with_option beautify_file (Vernac.load_vernac v sid) s) else Vernac.load_vernac v sid s) sid (List.rev !load_vernacular_list) @@ -199,7 +198,7 @@ let require_prelude () = let require_list = ref ([] : string list) let add_require s = require_list := s :: !require_list let require () = - let () = if !load_init then silently require_prelude () in + let () = if !Flags.load_init then Flags.silently require_prelude () in let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list) @@ -229,7 +228,7 @@ let add_compile verbose s = let compile_file (v,f) = if !Flags.beautify then - with_option beautify_file (Vernac.compile v) f + Flags.(with_option beautify_file (Vernac.compile v) f) else Vernac.compile v f @@ -304,7 +303,7 @@ let usage () = init_load_path (); with NoCoqLib -> usage_no_coqlib () end; - if !batch_mode then Usage.print_usage_coqc () + if !Flags.batch_mode 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$")); @@ -538,7 +537,7 @@ 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 := Vio2Vo + |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Flags.Vio2Vo |"-toploop" -> set_toploop (next ()) |"-w" | "-W" -> CWarnings.set_flags (CWarnings.normalize_flags_string (next ())) |"-o" -> Flags.compilation_output_name := Some (next()) @@ -551,9 +550,9 @@ let parse_args arglist = |"-async-proofs-never-reopen-branch" -> Flags.async_proofs_never_reopen_branch := true; |"-batch" -> set_batch_mode () - |"-test-mode" -> test_mode := true - |"-beautify" -> beautify := true - |"-boot" -> boot := true; no_load_rc () + |"-test-mode" -> Flags.test_mode := true + |"-beautify" -> Flags.beautify := true + |"-boot" -> Flags.boot := true; no_load_rc () |"-bt" -> Backtrace.record_backtrace true |"-color" -> set_color (next ()) |"-config"|"--config" -> print_config := true @@ -565,19 +564,18 @@ let parse_args arglist = |"-ideslave" -> set_ideslave () |"-impredicative-set" -> set_impredicative_set () |"-indices-matter" -> Indtypes.enforce_indices_matter () - |"-just-parsing" -> warning "-just-parsing option has been removed in 8.6" |"-m"|"--memory" -> memory_stat := true - |"-noinit"|"-nois" -> load_init := false + |"-noinit"|"-nois" -> Flags.load_init := false |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true |"-native-compiler" -> if Coq_config.no_native_compiler then warning "Native compilation was disabled at configure time." - else native_compiler := true + else Flags.native_compiler := true |"-output-context" -> output_context := true |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> no_load_rc () |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false - |"-quick" -> Flags.compilation_mode := BuildVio + |"-quick" -> Flags.compilation_mode := Flags.BuildVio |"-list-tags" -> print_tags := true |"-time" -> Flags.time := true |"-type-in-type" -> set_type_in_type () @@ -620,11 +618,11 @@ let init_toplevel arglist = prerr_endline "See -help for the list of supported options"; exit 1 end; - if_verbose print_header (); + Flags.if_verbose print_header (); inputstate (); Mltop.init_known_plugins (); engage (); - if (not !batch_mode || CList.is_empty !compile_list) + if (not !Flags.batch_mode || CList.is_empty !compile_list) && Global.env_is_initial () then Declaremods.start_library !toplevel_name; init_library_roots (); @@ -645,16 +643,16 @@ let init_toplevel arglist = with any -> flush_all(); let extra = - if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) + if !Flags.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 !batch_mode then begin + if !Flags.batch_mode then begin flush_all(); if !output_context then - Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); + Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); Profile.print_profile (); exit 0 end; diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 1602f9c683..4b97ee0dde 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -11,7 +11,6 @@ open Pp open CErrors open Util -open Flags open Vernacexpr open Vernacprop @@ -53,7 +52,7 @@ let set_formatter_translator ch = let pr_new_syntax_in_context ?loc chan_beautify ocom = let loc = Option.cata Loc.unloc (0,0) loc in - if !beautify_file then set_formatter_translator chan_beautify; + if !Flags.beautify_file then set_formatter_translator chan_beautify; let fs = States.freeze ~marshallable:`No in (* The content of this is not supposed to fail, but if ever *) try @@ -63,7 +62,7 @@ let pr_new_syntax_in_context ?loc chan_beautify ocom = | Some com -> Ppvernac.pr_vernac com | None -> mt() in let after = comment (CLexer.extract_comments (snd loc)) in - if !beautify_file then + if !Flags.beautify_file then (Pp.pp_with !Topfmt.std_ft (hov 0 (before ++ com ++ after)); Format.pp_print_flush !Topfmt.std_ft ()) else @@ -134,7 +133,7 @@ let rec interp_vernac sid (loc,com) = document. Hopefully this is fixed when VtBack can be removed and Undo etc... are just interpreted regularly. *) let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with - | VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _ -> true + | VtProofStep _ | VtBack (_, _) | VtStartProof _ -> true | _ -> false in @@ -209,7 +208,7 @@ and load_vernac verbosely sid file = *) in (* Printing of vernacs *) - if !beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast); + if !Flags.beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast); Option.iter (vernac_echo ?loc) in_echo; checknav_simple (loc, ast); @@ -224,7 +223,7 @@ and load_vernac verbosely sid file = match e with | Stm.End_of_input -> (* Is this called so comments at EOF are printed? *) - if !beautify then + if !Flags.beautify then pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa chan_beautify None; if !Flags.beautify_file then close_out chan_beautify; !rsid @@ -290,7 +289,7 @@ let compile verbosely f = ++ str ".") in match !Flags.compilation_mode with - | BuildVo -> + | Flags.BuildVo -> let long_f_dot_v = ensure_v f in ensure_exists long_f_dot_v; let long_f_dot_vo = @@ -314,7 +313,7 @@ let compile verbosely f = (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); Dumpglob.end_dump_glob () - | BuildVio -> + | Flags.BuildVio -> let long_f_dot_v = ensure_v f in ensure_exists long_f_dot_v; let long_f_dot_vio = @@ -329,7 +328,7 @@ let compile verbosely f = check_pending_proofs (); Stm.snapshot_vio ldir long_f_dot_vio; Stm.reset_task_queue () - | Vio2Vo -> + | Flags.Vio2Vo -> let open Filename in let open Library in Dumpglob.noglob (); diff --git a/vernac/command.ml b/vernac/command.ml index 32ab5401a0..b611edc41d 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -9,7 +9,6 @@ open Pp open CErrors open Util -open Flags open Term open Vars open Termops @@ -692,7 +691,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls = constrimpls) impls; let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in - if_verbose Feedback.msg_info (minductive_message warn_prim names); + Flags.if_verbose Feedback.msg_info (minductive_message warn_prim names); if mie.mind_entry_private == None then declare_default_schemes mind; mind diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 645320c603..590fa62134 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -11,7 +11,6 @@ open CErrors open Util -open Flags open Pp open Names open Term @@ -137,7 +136,7 @@ let find_mutually_recursive_statements thms = assert (List.is_empty rest); (* One occ. of common coind ccls and no common inductive hyps *) if not (List.is_empty common_same_indhyp) then - if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements."); + Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements."); flush_all (); indccl, true, [] | [], _::_ -> @@ -145,7 +144,7 @@ let find_mutually_recursive_statements thms = | ind :: _ -> if List.distinct_f ind_ord (List.map pi1 ind) then - if_verbose Feedback.msg_info + Flags.if_verbose Feedback.msg_info (strbrk ("Coinductive statements do not follow the order of "^ "definition, assuming the proof to be by induction.")); diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index c424b1d501..7b0d59812c 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Flags open CErrors open Util open Names @@ -794,7 +793,7 @@ type notation_modifier = { (* common to syn_data below *) only_parsing : bool; only_printing : bool; - compat : compat_version option; + compat : Flags.compat_version option; format : string Loc.located option; extra : (string * string) list; } @@ -1073,7 +1072,7 @@ module SynData = struct (* Fields coming from the vernac-level modifiers *) only_parsing : bool; only_printing : bool; - compat : compat_version option; + compat : Flags.compat_version option; format : string Loc.located option; extra : (string * string) list; @@ -1389,7 +1388,7 @@ let add_notation_interpretation ((loc,df),c,sc) = let set_notation_for_interpretation impls ((_,df),c,sc) = (try ignore - (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); + (Flags.silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); with NoSyntaxRule -> user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc diff --git a/vernac/mltop.ml b/vernac/mltop.ml index e8a0ba3dda..1edbd1a850 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -9,7 +9,6 @@ open CErrors open Util open Pp -open Flags open Libobject open System @@ -365,7 +364,7 @@ let trigger_ml_object verb cache reinit ?path name = else begin let file = file_of_name (Option.default name path) in let path = - if_verbose_load (verb && not !quiet) load_ml_object name ?path file in + if_verbose_load (verb && not !Flags.quiet) load_ml_object name ?path file in add_loaded_module name (Some path); if cache then perform_cache_obj name end diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4fd08b42d4..c7b8def0e0 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -11,7 +11,6 @@ open Pp open CErrors open Util -open Flags open Names open Nameops open Term @@ -657,7 +656,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = id binders_ast (Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; - if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared"); + Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared"); Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = @@ -678,7 +677,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = export id binders_ast mty_ast_o in Dumpglob.dump_moddef ?loc mp "mod"; - if_verbose Feedback.msg_info + Flags.if_verbose Feedback.msg_info (str "Interactive Module " ++ pr_id id ++ str " started"); List.iter (fun (export,id) -> @@ -696,7 +695,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = id binders_ast mty_ast_o mexpr_ast_l in Dumpglob.dump_moddef ?loc mp "mod"; - if_verbose Feedback.msg_info + Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export @@ -704,7 +703,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = let vernac_end_module export (loc,id as lid) = let mp = Declaremods.end_module () in Dumpglob.dump_modref ?loc mp "mod"; - if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined"); + Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident lid]) export let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = @@ -725,7 +724,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = id binders_ast mty_sign in Dumpglob.dump_moddef ?loc mp "modtype"; - if_verbose Feedback.msg_info + Flags.if_verbose Feedback.msg_info (str "Interactive Module Type " ++ pr_id id ++ str " started"); List.iter (fun (export,id) -> @@ -744,13 +743,13 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = id binders_ast mty_sign mty_ast_l in Dumpglob.dump_moddef ?loc mp "modtype"; - if_verbose Feedback.msg_info + Flags.if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined") let vernac_end_modtype (loc,id) = let mp = Declaremods.end_modtype () in Dumpglob.dump_modref ?loc mp "modtype"; - if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined") let vernac_include l = Declaremods.declare_include Modintern.interp_module_ast l @@ -818,7 +817,7 @@ let vernac_coercion locality poly local ref qids qidt = let source = cl_of_qualid qids in let ref' = smart_global ref in Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target; - if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion") + Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion") let vernac_identity_coercion locality poly local id qids qidt = let local = enforce_locality locality local in @@ -920,7 +919,7 @@ let vernac_chdir = function so we make it an error. *) user_err Pp.(str ("Cd failed: " ^ err)) end; - if_verbose Feedback.msg_info (str (Sys.getcwd())) + Flags.if_verbose Feedback.msg_info (str (Sys.getcwd())) (********************) @@ -1302,7 +1301,7 @@ let _ = optname = "automatic introduction of variables"; optkey = ["Automatic";"Introduction"]; optread = Flags.is_auto_intros; - optwrite = make_auto_intros } + optwrite = Flags.make_auto_intros } let _ = declare_bool_option @@ -1924,7 +1923,6 @@ let interp ?proof ?loc locality poly c = | VernacTime _ -> assert false | VernacRedirect _ -> assert false | VernacTimeout _ -> assert false - | VernacStm _ -> assert false (* The STM should handle that, but LOAD bypasses the STM... *) | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command") @@ -2050,7 +2048,7 @@ let interp ?proof ?loc locality poly c = | VernacSearch (s,g,r) -> vernac_search ?loc s g r | VernacLocate l -> vernac_locate l | VernacRegister (id, r) -> vernac_register id r - | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n") + | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n") (* Proof management *) | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)] @@ -2176,7 +2174,7 @@ let with_fail b f = | HasNotFailed -> user_err ~hdr:"Fail" (str "The command has not failed!") | HasFailed msg -> - if not !Flags.quiet || !test_mode || !ide_slave then Feedback.msg_info + if not !Flags.quiet || !Flags.test_mode || !Flags.ide_slave then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end @@ -2185,10 +2183,6 @@ let interp ?(verbosely=true) ?proof (loc,c) = let orig_program_mode = Flags.is_program_mode () in let rec aux ?locality ?polymorphism isprogcmd = function - (* This assert case will be removed when fake_ide can understand - completion feedback *) - | VernacStm _ -> assert false (* Done by Stm *) - | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c | VernacProgram _ -> user_err Pp.(str "Program mode specified twice") | VernacLocal (b, c) when Option.is_empty locality -> diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index fc11bcf4a0..3cff1f14c0 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -17,8 +17,7 @@ let rec is_navigation_vernac = function | VernacResetName _ | VernacBacktrack _ | VernacBackTo _ - | VernacBack _ - | VernacStm _ -> true + | VernacBack _ -> true | VernacRedirect (_, (_,c)) | VernacTime (_,c) -> is_navigation_vernac c (* Time Back* is harmless *) |