diff options
42 files changed, 222 insertions, 316 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c3e59a6d89..73b979c6a3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -749,6 +749,9 @@ plugin:plugin-tutorial: plugin:ci-quickchick: extends: .ci-template-flambda +plugin:ci-reduction_effects: + extends: .ci-template + plugin:ci-relation_algebra: extends: .ci-template diff --git a/Makefile.ci b/Makefile.ci index 8315c16c64..4fc0e69748 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -38,6 +38,7 @@ CI_TARGETS= \ ci-paramcoq \ ci-perennial \ ci-quickchick \ + ci-reduction_effects \ ci-relation_algebra \ ci-rewriter \ ci-sf \ diff --git a/clib/backtrace.ml b/clib/backtrace.ml deleted file mode 100644 index 81803a81a5..0000000000 --- a/clib/backtrace.ml +++ /dev/null @@ -1,119 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -[@@@ocaml.warning "-37"] - -type raw_frame = -| Known_location of bool (* is_raise *) - * string (* filename *) - * int (* line number *) - * int (* start char *) - * int (* end char *) -| Unknown_location of bool (*is_raise*) - -type location = { - loc_filename : string; - loc_line : int; - loc_start : int; - loc_end : int; -} - -type frame = { frame_location : location option; frame_raised : bool; } - -external get_exception_backtrace: unit -> raw_frame array option - = "caml_get_exception_backtrace" - -type t = raw_frame array list -(** List of partial raw stack frames, in reverse order *) - -let empty = [] - -let of_raw = function -| Unknown_location r -> - { frame_location = None; frame_raised = r; } -| Known_location (r, file, line, st, en) -> - let loc = { - loc_filename = file; - loc_line = line; - loc_start = st; - loc_end = en; - } in - { frame_location = Some loc; frame_raised = r; } - -let rec repr_aux accu = function -| [] -> accu -| fragment :: stack -> - let len = Array.length fragment in - let rec append accu i = - if i = len then accu - else append (of_raw fragment.(i) :: accu) (succ i) - in - repr_aux (append accu 0) stack - -let repr bt = repr_aux [] (List.rev bt) - -let push stack = match get_exception_backtrace () with -| None -> [] -| Some frames -> frames :: stack - -(** Utilities *) - -let print_frame frame = - let raise = if frame.frame_raised then "raise" else "frame" in - match frame.frame_location with - | None -> Printf.sprintf "%s @ unknown" raise - | Some loc -> - Printf.sprintf "%s @ file \"%s\", line %d, characters %d-%d" - raise loc.loc_filename loc.loc_line loc.loc_start loc.loc_end - -(** Exception manipulation *) - -let backtrace : t Exninfo.t = Exninfo.make () - -let is_recording = ref false - -let record_backtrace b = - let () = Printexc.record_backtrace b in - is_recording := b - -let get_backtrace e = - Exninfo.get e backtrace - -let add_backtrace e = - if !is_recording then - (* This must be the first function call, otherwise the stack may be - destroyed *) - let current = get_exception_backtrace () in - let info = Exninfo.info e in - begin match current with - | None -> (e, info) - | Some fragment -> - let bt = match get_backtrace info with - | None -> [] - | Some bt -> bt - in - let bt = fragment :: bt in - (e, Exninfo.add info backtrace bt) - end - else - let info = Exninfo.info e in - (e, info) - -let app_backtrace ~src ~dst = - if !is_recording then - match get_backtrace src with - | None -> dst - | Some bt -> - match get_backtrace dst with - | None -> - Exninfo.add dst backtrace bt - | Some nbt -> - let bt = bt @ nbt in - Exninfo.add dst backtrace bt - else dst diff --git a/clib/backtrace.mli b/clib/backtrace.mli deleted file mode 100644 index 55c60e5483..0000000000 --- a/clib/backtrace.mli +++ /dev/null @@ -1,98 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** * Low-level management of OCaml backtraces. - - Currently, OCaml manages its backtraces in a very imperative way. That is to - say, it only keeps track of the stack destroyed by the last raised exception. - So we have to be very careful when using this module not to do silly things. - - Basically, you need to manually handle the reraising of exceptions. In order - to do so, each time the backtrace is lost, you must [push] the stack fragment. - This essentially occurs whenever a [with] handler is crossed. - -*) - -(** {5 Backtrace information} *) - -type location = { - loc_filename : string; - loc_line : int; - loc_start : int; - loc_end : int; -} -(** OCaml debugging information for function calls. *) - -type frame = { frame_location : location option; frame_raised : bool; } -(** A frame contains two informations: its optional physical location, and - whether it raised the exception or let it pass through. *) - -type t -(** Type of backtraces. They're essentially stack of frames. *) - -val empty : t -(** Empty frame stack. *) - -val push : t -> t -(** Add the current backtrace information to a given backtrace. *) - -val repr : t -> frame list -(** Represent a backtrace as a list of frames. Leftmost element is the outermost - call. *) - -(** {5 Utilities} *) - -val print_frame : frame -> string -(** Represent a frame. *) - -(** {5 Exception handling} *) - -val record_backtrace : bool -> unit -(** Whether to activate the backtrace recording mechanism. Note that it will - only work whenever the program was compiled with the [debug] flag. *) - -val get_backtrace : Exninfo.info -> t option -(** Retrieve the optional backtrace coming with the exception. *) - -val add_backtrace : exn -> Exninfo.iexn -(** Add the current backtrace information to the given exception. - - The intended use case is of the form: {[ - - try foo - with - | Bar -> bar - | err -> let err = add_backtrace err in baz - - ]} - - WARNING: any intermediate code between the [with] and the handler may - modify the backtrace. Yes, that includes [when] clauses. Ideally, what you - should do is something like: {[ - - try foo - with err -> - let err = add_backtrace err in - match err with - | Bar -> bar - | err -> baz - - ]} - - I admit that's a bit heavy, but there is not much to do... - -*) - -val app_backtrace : src:Exninfo.info -> dst:Exninfo.info -> Exninfo.info -(** Append the backtrace from [src] to [dst]. The returned exception is [dst] - except for its backtrace information. This is targeted at container - exceptions, that is, exceptions that contain exceptions. This way, one can - transfer the backtrace from the container to the underlying exception, as if - the latter was the one originally raised. *) diff --git a/clib/cArray.ml b/clib/cArray.ml index be59ae57d0..0f57204cc1 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -392,18 +392,30 @@ let iter2_i f v1 v2 = let () = if not (Int.equal len2 len1) then invalid_arg "Array.iter2" in for i = 0 to len1 - 1 do f i (uget v1 i) (uget v2 i) done -let pure_functional = false +let map_right f a = + let l = length a in + if l = 0 then [||] else begin + let r = Array.make l (f (unsafe_get a (l-1))) in + for i = l-2 downto 0 do + unsafe_set r i (f (unsafe_get a i)) + done; + r + end + +let map2_right f a b = + let l = length a in + if l <> length b then invalid_arg "CArray.map2_right: length mismatch"; + if l = 0 then [||] else begin + let r = Array.make l (f (unsafe_get a (l-1)) (unsafe_get b (l-1))) in + for i = l-2 downto 0 do + unsafe_set r i (f (unsafe_get a i) (unsafe_get b i)) + done; + r + end let fold_right_map f v e = -if pure_functional then - let (l,e) = - Array.fold_right - (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) - v ([],e) in - (Array.of_list l,e) -else let e' = ref e in - let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in + let v' = map_right (fun x -> let (y,e) = f x !e' in e' := e; y) v in (v',!e') let fold_left_map f e v = @@ -414,7 +426,7 @@ let fold_left_map f e v = let fold_right2_map f v1 v2 e = let e' = ref e in let v' = - map2 (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2 + map2_right (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2 in (v',!e') diff --git a/clib/cArray.mli b/clib/cArray.mli index f94af26515..94390a369f 100644 --- a/clib/cArray.mli +++ b/clib/cArray.mli @@ -107,7 +107,7 @@ sig (** Same than [fold_left2_map] but passing the index of the array *) val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c - (** Same with two arrays, folding on the left *) + (** Same with two arrays, folding on the right *) val distinct : 'a array -> bool (** Return [true] if every element of the array is unique (for default diff --git a/clib/exninfo.ml b/clib/exninfo.ml index 34f76a2edd..ee998c2f17 100644 --- a/clib/exninfo.ml +++ b/clib/exninfo.ml @@ -57,12 +57,29 @@ let rec find_and_remove_assoc (i : int) = function if rem == ans then (r, l) else (r, (j, v) :: ans) -let iraise e = +type backtrace = Printexc.raw_backtrace +let backtrace_to_string = Printexc.raw_backtrace_to_string + +let backtrace_info : backtrace t = make () + +let is_recording = ref false + +let record_backtrace b = + let () = Printexc.record_backtrace b in + is_recording := b + +let get_backtrace e = get e backtrace_info + +let iraise (e,i) = let () = Mutex.lock lock in let id = Thread.id (Thread.self ()) in - let () = current := (id, e) :: remove_assoc id !current in + let () = current := (id, (e,i)) :: remove_assoc id !current in let () = Mutex.unlock lock in - raise (fst e) + match get i backtrace_info with + | None -> + raise e + | Some bt -> + Printexc.raise_with_backtrace e bt let raise ?info e = match info with | None -> @@ -72,11 +89,7 @@ let raise ?info e = match info with let () = Mutex.unlock lock in raise e | Some i -> - let () = Mutex.lock lock in - let id = Thread.id (Thread.self ()) in - let () = current := (id, (e, i)) :: remove_assoc id !current in - let () = Mutex.unlock lock in - raise e + iraise (e,i) let find_and_remove () = let () = Mutex.lock lock in @@ -104,3 +117,13 @@ let info e = (* Mismatch: the raised exception is not the one stored, either because the previous raise was not instrumented, or because something went wrong. *) Store.empty + +let capture e = + if !is_recording then + (* This must be the first function call, otherwise the stack may be + destroyed *) + let bt = Printexc.get_raw_backtrace () in + let info = info e in + e, add info backtrace_info bt + else + e, info e diff --git a/clib/exninfo.mli b/clib/exninfo.mli index 30803e3e6a..36cc44cf82 100644 --- a/clib/exninfo.mli +++ b/clib/exninfo.mli @@ -34,6 +34,49 @@ val get : info -> 'a t -> 'a option val info : exn -> info (** Retrieve the information of the last exception raised. *) +type backtrace + +val get_backtrace : info -> backtrace option +(** [get_backtrace info] does get the backtrace associated to info *) + +val backtrace_to_string : backtrace -> string +(** [backtrace_to_string info] does get the backtrace associated to info *) + +val record_backtrace : bool -> unit + +val capture : exn -> iexn +(** Add the current backtrace information to the given exception. + + The intended use case is of the form: {[ + + try foo + with + | Bar -> bar + | exn -> + let exn = Exninfo.capture err in + baz + + ]} + + where [baz] should re-raise using [iraise] below. + + WARNING: any intermediate code between the [with] and the handler may + modify the backtrace. Yes, that includes [when] clauses. Ideally, what you + should do is something like: {[ + + try foo + with exn -> + let exn = Exninfo.capture exn in + match err with + | Bar -> bar + | err -> baz + + ]} + + I admit that's a bit heavy, but there is not much to do... + +*) + val iraise : iexn -> 'a (** Raise the given enriched exception. *) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 9e9e3b4cfa..7342bc72e7 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -259,6 +259,13 @@ : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" ######################################################################## +# reduction-effects +######################################################################## +: "${reduction_effects_CI_REF:=master}" +: "${reduction_effects_CI_GITURL:=https://github.com/coq-community/reduction-effects}" +: "${reduction_effects_CI_ARCHIVEURL:=${reduction_effects_CI_GITURL}/archive}" + +######################################################################## # menhirlib ######################################################################## : "${menhirlib_CI_REF:=master}" diff --git a/dev/ci/ci-reduction_effects.sh b/dev/ci/ci-reduction_effects.sh new file mode 100755 index 0000000000..6b6de3fa2f --- /dev/null +++ b/dev/ci/ci-reduction_effects.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download reduction_effects + +( cd "${CI_BUILD_DIR}/reduction_effects" && make && make test && make install) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 04b20c6889..3bc92e6aee 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,13 @@ ### ML API +Exception handling: + +- Coq's custom `Backtrace` module has been removed in favor of OCaml's + native backtrace implementation. Please use the functions in + `Exninfo.capture` and `iraise` when re-raising inside an exception + handler. + Printers: - Functions such as Printer.pr_lconstr_goal_style_env have been diff --git a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst new file mode 100644 index 0000000000..cb92945b8b --- /dev/null +++ b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst @@ -0,0 +1,4 @@ +- **Removed:** + Removed the "Revert all buffers" command from CoqIDE which had been broken for a long time + (`#11415 <https://github.com/coq/coq/pull/11415>`_, + by Pierre-Marie Pédrot). diff --git a/engine/evd.ml b/engine/evd.ml index 8e7d942c37..70f58163fd 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -902,14 +902,14 @@ let make_nonalgebraic_variable evd u = let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s = with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s) -let fresh_constant_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c) +let fresh_constant_instance ?loc ?(rigid=univ_flexible) env evd c = + with_context_set ?loc rigid evd (UnivGen.fresh_constant_instance env c) -let fresh_inductive_instance ?loc env evd i = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i) +let fresh_inductive_instance ?loc ?(rigid=univ_flexible) env evd i = + with_context_set ?loc rigid evd (UnivGen.fresh_inductive_instance env i) -let fresh_constructor_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c) +let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c = + with_context_set ?loc rigid evd (UnivGen.fresh_constructor_instance env c) let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr) diff --git a/engine/evd.mli b/engine/evd.mli index 8843adc853..82e1003a65 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -653,10 +653,14 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t -val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant -val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive -val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid + -> evar_map -> Sorts.family -> evar_map * Sorts.t +val fresh_constant_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> Constant.t -> evar_map * pconstant +val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> inductive -> evar_map * pinductive +val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> constructor -> evar_map * pconstructor val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> GlobRef.t -> evar_map * econstr diff --git a/engine/univGen.ml b/engine/univGen.ml index 1fe09270ba..b270f9dc0b 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -48,8 +48,6 @@ let fresh_instance_from ?loc ctx = function (** Fresh universe polymorphic construction *) -open Globnames - let fresh_global_instance ?loc ?names env gr = let auctx = Environ.universes_of_global env gr in let u, ctx = fresh_instance_from ?loc auctx names in @@ -78,10 +76,6 @@ let constr_of_monomorphic_global gr = Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ str " would forget universes.") -let fresh_global_or_constr_instance env = function - | IsConstr c -> c, ContextSet.empty - | IsGlobal gr -> fresh_global_instance env gr - let fresh_sort_in_family = function | InSProp -> Sorts.sprop, ContextSet.empty | InProp -> Sorts.prop, ContextSet.empty diff --git a/engine/univGen.mli b/engine/univGen.mli index 1b351c61c4..bbde9d4e30 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -46,9 +46,6 @@ val fresh_constructor_instance : env -> constructor -> val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t -> constr in_universe_context_set -val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> - constr in_universe_context_set - (** Get fresh variables for the universe context. Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) val fresh_universe_context_set_instance : ContextSet.t -> diff --git a/ide/coqide.ml b/ide/coqide.ml index 918c196968..e0347d3c5f 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -996,8 +996,6 @@ let build_ui () = item "Save" ~callback:(File.save ~parent:w) ~stock:`SAVE ~tooltip:"Save current buffer"; item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:(File.saveas ~parent:w); item "Save all" ~label:"Sa_ve all" ~callback:File.saveall; - item "Revert all buffers" ~label:"_Revert all buffers" - ~callback:(File.revert_all ~parent:w) ~stock:`REVERT_TO_SAVED; item "Close buffer" ~label:"_Close buffer" ~stock:`CLOSE ~callback:(File.close_buffer ~parent:w) ~tooltip:"Close current buffer"; item "Print..." ~label:"_Print..." @@ -1368,7 +1366,7 @@ let read_coqide_args argv = |"-debug"::args -> Minilib.debug := true; Flags.debug := true; - Backtrace.record_backtrace true; + Exninfo.record_backtrace true; filter_coqtop coqtop project_files bindings_files ("-debug"::out) args |"-coqtop-flags" :: flags :: args-> Coq.ideslave_coqtop_flags := Some flags; diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index f056af6703..59dd9c0e4c 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -36,7 +36,6 @@ let init () = \n <menuitem action='Save' />\ \n <menuitem action='Save as' />\ \n <menuitem action='Save all' />\ -\n <menuitem action='Revert all buffers' />\ \n <menuitem action='Close buffer' />\ \n <menuitem action='Print...' />\ \n <menu action='Export to'>\ diff --git a/lib/cErrors.ml b/lib/cErrors.ml index b9735d0579..9f496f5845 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -12,7 +12,7 @@ open Pp (** Aliases *) -let push = Backtrace.add_backtrace +let push = Exninfo.capture (* Errors *) @@ -51,12 +51,10 @@ let raw_anomaly e = match e with | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." -let print_backtrace e = match Backtrace.get_backtrace e with +let print_backtrace e = match Exninfo.get_backtrace e with | None -> mt () | Some bt -> - let bt = Backtrace.repr bt in - let pr_frame f = str (Backtrace.print_frame f) in - let bt = prlist_with_sep fnl pr_frame bt in + let bt = str (Exninfo.backtrace_to_string bt) in fnl () ++ hov 0 bt let print_anomaly askreport e = diff --git a/lib/control.ml b/lib/control.ml index 7d54838df8..e67e88ee95 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -38,7 +38,7 @@ let unix_timeout n f x e = restore_timeout (); res with e -> - let e = Backtrace.add_backtrace e in + let e = Exninfo.capture e in restore_timeout (); Exninfo.iraise e @@ -76,7 +76,7 @@ let windows_timeout n f x e = else raise e | e -> let () = killed := true in - let e = Backtrace.add_backtrace e in + let e = Exninfo.capture e in Exninfo.iraise e type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } @@ -102,7 +102,7 @@ let protect_sigalrm f x = | true, Sys.Signal_handle f -> f Sys.sigalrm; res | _, _ -> res with e -> - let e = Backtrace.add_backtrace e in + let e = Exninfo.capture e in Sys.set_signal Sys.sigalrm old_handler; Exninfo.iraise e with Invalid_argument _ -> (* This happens on Windows, as handling SIGALRM does not seem supported *) diff --git a/lib/flags.ml b/lib/flags.ml index b87ba46634..ad48024761 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -19,7 +19,7 @@ let with_modified_ref ?(restore=true) r nf f x = if restore || pre == !r then r := old_ref; res with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in r := old_ref; Exninfo.iraise reraise @@ -37,7 +37,7 @@ let with_options ol f x = let r = f x in let () = List.iter2 (:=) ol vl in r with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise @@ -203,7 +203,7 @@ let pp_with ft pp = in try pp_cmd pp with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in let () = Format.pp_print_flush ft () in Exninfo.iraise reraise diff --git a/library/globnames.ml b/library/globnames.ml index acb05f9ac0..63cb2c69bd 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -123,7 +123,3 @@ module ExtRefOrdered = struct | SynDef kn -> combinesmall 2 (KerName.hash kn) end - -type global_reference_or_constr = - | IsGlobal of GlobRef.t - | IsConstr of constr diff --git a/library/globnames.mli b/library/globnames.mli index 48cbb11b66..d61cdd2b64 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -59,7 +59,3 @@ module ExtRefOrdered : sig val equal : t -> t -> bool val hash : t -> int end - -type global_reference_or_constr = - | IsGlobal of GlobRef.t - | IsConstr of constr diff --git a/library/lib.ml b/library/lib.ml index 9cce9b92ad..7f96adeecf 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -500,7 +500,7 @@ let close_section () = type frozen = lib_state -let freeze ~marshallable = !lib_state +let freeze () = !lib_state let unfreeze st = lib_state := st diff --git a/library/lib.mli b/library/lib.mli index 0d03046dc2..1fe72389f6 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -151,7 +151,7 @@ val close_section : unit -> unit type frozen -val freeze : marshallable:bool -> frozen +val freeze : unit -> frozen val unfreeze : frozen -> unit (** Keep only the libobject structure, not the objects themselves *) diff --git a/library/states.ml b/library/states.ml index 0be153d96a..90303a2a5c 100644 --- a/library/states.ml +++ b/library/states.ml @@ -18,7 +18,7 @@ let replace_summary (lib,_) st = lib, st let replace_lib (_,st) lib = lib, st let freeze ~marshallable = - (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable) + (Lib.freeze (), Summary.freeze_summaries ~marshallable) let unfreeze (fl,fs) = Lib.unfreeze fl; diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 70c1077106..f6fbdaa958 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -164,7 +164,7 @@ let rawnum_of_r c = match DAst.get c with let s, i = if is_pos_or_zero i then SPlus, i else SMinus, neg i in let i = Bigint.to_string i in let se = if is_gr md glob_Rdiv then "-" else "" in - let e = se ^ Bigint.to_string e in + let e = "e" ^ se ^ Bigint.to_string e in s, { NumTok.int = i; frac = ""; exp = e } | _ -> raise Non_closed_number end diff --git a/stm/stm.ml b/stm/stm.ml index eff2403eca..4c539684e3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2362,7 +2362,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in - st, Lib.freeze ~marshallable:false in + st, Lib.freeze () in let inject_non_pstate (s,l) = Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env () diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index d6fda00ad8..6cdb24965d 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -49,14 +49,14 @@ let optimize_non_type_induction_scheme kind dep sort ind = let sigma = Evd.minimize_universes sigma in (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma) else - let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in (c, Evd.evar_universe_context sigma) let build_induction_scheme_in_type dep sort ind = let env = Global.env () in let sigma = Evd.from_env env in - let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in c, Evd.evar_universe_context sigma diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out new file mode 100644 index 0000000000..6bc04f1cef --- /dev/null +++ b/test-suite/output/QArithSyntax.out @@ -0,0 +1,14 @@ +eq_refl : 102e-2 = 102e-2 + : 102e-2 = 102e-2 +eq_refl : 102e-1 = 102e-1 + : 102e-1 = 102e-1 +eq_refl : 1020 = 1020 + : 1020 = 1020 +eq_refl : 102 = 102 + : 102 = 102 +eq_refl : 102e-2 = 102e-2 + : 102e-2 = 102e-2 +eq_refl : -1e-4 = -1e-4 + : -1e-4 = -1e-4 +eq_refl : -50e-2 = -50e-2 + : -50e-2 = -50e-2 diff --git a/test-suite/success/QArithSyntax.v b/test-suite/output/QArithSyntax.v index 2f2ee0134a..2f2ee0134a 100644 --- a/test-suite/success/QArithSyntax.v +++ b/test-suite/output/QArithSyntax.v diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index e6f7556d96..2d877bd813 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -2,3 +2,17 @@ : R (-31)%R : R +eq_refl : 102e-2 = 102e-2 + : 102e-2 = 102e-2 +eq_refl : 102e-1 = 102e-1 + : 102e-1 = 102e-1 +eq_refl : 102e1 = 102e1 + : 102e1 = 102e1 +eq_refl : 102 = 102 + : 102 = 102 +eq_refl : 102e-2 = 102e-2 + : 102e-2 = 102e-2 +eq_refl : -1e-4 = -1e-4 + : -1e-4 = -1e-4 +eq_refl : -50e-2 = -50e-2 + : -50e-2 = -50e-2 diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index 44e8c7a50c..cb3bce70d4 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -1,3 +1,25 @@ Require Import Reals.Rdefinitions. Check 32%R. Check (-31)%R. + +Open Scope R_scope. + +Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). +Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)). +Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)). +Check (eq_refl : 1.02e+02 = IZR 102). +Check (eq_refl : 10.2e-1 = 1.02). +Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)). +Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)). + +Require Import Reals. + +Goal 254e3 = 2540 * 10 ^ 2. +ring. +Qed. + +Require Import Psatz. + +Goal 254e3 = 2540 * 10 ^ 2. +lra. +Qed. diff --git a/test-suite/success/RealSyntax.v b/test-suite/success/RealSyntax.v deleted file mode 100644 index 2765200991..0000000000 --- a/test-suite/success/RealSyntax.v +++ /dev/null @@ -1,19 +0,0 @@ -Require Import Reals. -Open Scope R_scope. -Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). -Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)). -Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)). -Check (eq_refl : 1.02e+02 = IZR 102). -Check (eq_refl : 10.2e-1 = 1.02). -Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)). -Check (eq_refl : -0.5 = IZR (-5) / IZR (Z.pow_pos 10 1)). - -Goal 254e3 = 2540 * 10 ^ 2. -ring. -Qed. - -Require Import Psatz. - -Goal 254e3 = 2540 * 10 ^ 2. -lra. -Qed. diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v index 855f26698c..4b928007cf 100644 --- a/test-suite/success/Scheme.v +++ b/test-suite/success/Scheme.v @@ -25,3 +25,8 @@ Check myeq_rew_fwd_r_dep. Set Rewriting Schemes. Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true. Unset Rewriting Schemes. + +(* check that the scheme doesn't minimize itself into something non general *) +Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= . +Lemma bla@{u v|u < v} : foo@{u v} -> False. +Proof. induction 1. Qed. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 56a6312b61..52e2562ae8 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -513,7 +513,7 @@ let parse_args ~help ~init arglist : t * string list = }}} |"-test-mode" -> Vernacinterp.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval - |"-bt" -> Backtrace.record_backtrace true; oval + |"-bt" -> Exninfo.record_backtrace true; oval |"-color" -> set_color oval (next ()) |"-config"|"--config" -> set_query oval PrintConfig |"-debug" -> Coqinit.set_debug (); oval diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index ae37e40101..ac348b9646 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -14,7 +14,7 @@ open Pp let ( / ) s1 s2 = Filename.concat s1 s2 let set_debug () = - let () = Backtrace.record_backtrace true in + let () = Exninfo.record_backtrace true in Flags.debug := true (* Loading of the resource file. diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index bca6b48499..adcce67b0d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -69,10 +69,10 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () [@ocaml.warning "-3"] in { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> + let (reraise, info) = CErrors.push reraise in (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) if interactive then ignore(Stm.edit_at ~doc:state.doc state.sid); - let (reraise, info) = CErrors.push reraise in let info = begin match Loc.get_loc info with | None -> Option.cata (Loc.add_loc info) info loc diff --git a/vernac/classes.ml b/vernac/classes.ml index c9b5144299..77bc4e4f8a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -42,13 +42,10 @@ let () = Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state let add_instance_hint inst path local info poly = - let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) - | IsGlobal gr -> Hints.IsGlobRef gr - in Flags.silently (fun () -> Hints.add_hints ~local [typeclasses_db] (Hints.HintsResolveEntry - [info, poly, false, Hints.PathHints path, inst'])) () + [info, poly, false, Hints.PathHints path, inst])) () let is_local_for_hint i = match i.is_global with @@ -61,9 +58,9 @@ let is_local_for_hint i = let add_instance check inst = let poly = Global.is_polymorphic inst.is_impl in let local = is_local_for_hint inst in - add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local + add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local inst.is_info poly; - List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path + List.iter (fun (path, pri, c) -> add_instance_hint (Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)) path local pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 222e9eb825..05e23164b1 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1346,7 +1346,7 @@ let inNotation : notation_obj -> obj = (**********************************************************************) let with_lib_stk_protection f x = - let fs = Lib.freeze ~marshallable:false in + let fs = Lib.freeze () in try let a = f x in Lib.unfreeze fs; a with reraise -> let reraise = CErrors.push reraise in diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 45f40b1258..de02f7ecfb 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -359,7 +359,7 @@ let in_phase ~phase f x = default_phase := op; res with exn -> - let iexn = Backtrace.add_backtrace exn in + let iexn = Exninfo.capture exn in default_phase := op; Util.iraise iexn @@ -415,7 +415,7 @@ let with_output_to_file fname func input = close_out channel; output with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in std_ft := Util.pi1 old_fmt; err_ft := Util.pi2 old_fmt; deep_ft := Util.pi3 old_fmt; |