aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checker.ml37
-rw-r--r--dev/ci/ci-basic-overlay.sh2
-rw-r--r--doc/refman/RefMan-ltac.tex4
-rw-r--r--lib/feedback.ml38
-rw-r--r--lib/feedback.mli8
-rw-r--r--pretyping/pretyping.ml7
-rw-r--r--pretyping/unification.ml4
-rw-r--r--test-suite/success/destruct.v6
-rw-r--r--test-suite/success/refine.v10
9 files changed, 77 insertions, 39 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index 247a98e63e..e960a55fd2 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -367,46 +367,11 @@ 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 ();
+ let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
try
parse_args argv;
if !Flags.debug then Printexc.record_backtrace true;
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5c37b3133e..59a71b6086 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -80,7 +80,7 @@
# VST
########################################################################
: ${VST_CI_BRANCH:=master}
-: ${VST_CI_GITURL:=https://github.com/Zimmi48/VST.git}
+: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
########################################################################
# fiat_parsers
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 574591185c..5fb4585884 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -547,7 +547,7 @@ Yet another way of branching without backtracking is the following structure:
$v_2$ which must be tactic values. The tactic value $v_1$ is applied in each
subgoal independently and if it fails \emph{to progress} then $v_2$ is
applied. {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ is equivalent to {\tt
- first [} {\tt progress} {\tacexpr}$_1$ {\tt |} {\tt progress}
+ first [} {\tt progress} {\tacexpr}$_1$ {\tt |}
{\tacexpr}$_2$ {\tt ]} (except that if it fails, it fails like
$v_2$). Branching is left-associative.
@@ -561,7 +561,7 @@ The tactic
is a generalization of the biased-branching tactics above. The
expression {\tacexpr}$_1$ is evaluated to $v_1$, which is then applied
to each subgoal independently. For each goal where $v_1$ succeeds at
-least once, {tacexpr}$_2$ is evaluated to $v_2$ which is then applied
+least once, {\tacexpr}$_2$ is evaluated to $v_2$ which is then applied
collectively to the generated subgoals. The $v_2$ tactic can trigger
backtracking points in $v_1$: where $v_1$ succeeds at least once, {\tt
tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 7a126363cc..1007582e08 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -63,6 +63,7 @@ let set_id_for_feedback ?(route=default_route) d i =
span_id := i;
feedback_route := route
+let warn_no_listeners = ref true
let feedback ?did ?id ?route what =
let m = {
contents = what;
@@ -70,6 +71,8 @@ let feedback ?did ?id ?route what =
doc_id = Option.default !doc_id did;
span_id = Option.default !span_id id;
} in
+ if !warn_no_listeners && Hashtbl.length feeders = 0 then
+ Format.eprintf "Warning, feedback message received but no listener to handle it!@\n%!";
Hashtbl.iter (fun _ f -> f m) feeders
(* Logging messages *)
@@ -81,3 +84,38 @@ let msg_notice ?loc x = feedback_logger ?loc Notice x
let msg_warning ?loc x = feedback_logger ?loc Warning x
let msg_error ?loc x = feedback_logger ?loc Error x
let msg_debug ?loc x = feedback_logger ?loc Debug x
+
+(* Helper for tools willing to understand only the messages *)
+let console_feedback_listener fmt =
+ let open Format in
+ let pp_lvl fmt lvl = 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) =
+ match fb.contents with
+ | Processed -> ()
+ | Incomplete -> ()
+ | Complete -> ()
+ | ProcessingIn _ -> ()
+ | InProgress _ -> ()
+ | WorkerStatus (_,_) -> ()
+ | AddedAxiom -> ()
+ | GlobRef (_,_,_,_,_) -> ()
+ | GlobDef (_,_,_,_) -> ()
+ | FileDependency (_,_) -> ()
+ | FileLoaded (_,_) -> ()
+ | Custom (_,_,_) -> ()
+ | Message (lvl,loc,msg) ->
+ fprintf fmt "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg
+ in checker_feed
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 73b84614f1..62b909516f 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -99,3 +99,11 @@ val msg_error : ?loc:Loc.t -> Pp.t -> unit
val msg_debug : ?loc:Loc.t -> Pp.t -> unit
(** For debugging purposes *)
+
+val console_feedback_listener : Format.formatter -> feedback -> unit
+(** Helper for tools willing to print to the feedback system *)
+
+val warn_no_listeners : bool ref
+(** The library will print a warning to the console if no listener is
+ available by default; ML-clients willing to use Coq without a
+ feedback handler should set this to false. *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a69caecabe..b2b583ba74 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -888,6 +888,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| [], [] -> []
| _ -> assert false
in aux 1 1 (List.rev nal) cs.cs_args, true in
+ let fsign = if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
+ then Context.Rel.map (whd_betaiota !evdref) fsign
+ else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in
let obj ind p v f =
if not record then
let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
@@ -997,6 +1000,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let pi = lift n pred in (* liftn n 2 pred ? *)
let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
+ let cs_args =
+ if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
+ then Context.Rel.map (whd_betaiota !evdref) cs_args
+ else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in
let csgn =
List.map (set_name Anonymous) cs_args
in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e8f7e2bbaf..86ebc1f01f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -194,6 +194,10 @@ let pose_all_metas_as_evars env evd t =
let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
let ty = EConstr.of_constr ty in
let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
+ let ty =
+ if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
+ then nf_betaiota evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
+ else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
let src = Evd.evar_source_of_meta mv !evdref in
let ev = Evarutil.e_new_evar env evdref ~src ty in
evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref;
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 0219c3bfdf..6fbe61a9be 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -430,3 +430,9 @@ eexists ?[x].
destruct (S _).
change (0 = ?x).
Abort.
+
+Goal (forall P, P 0 -> True/\True) -> True.
+intro H.
+destruct (H (fun x => True)).
+match goal with |- True => idtac end.
+Abort.
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index b8a8ff7561..22fb4d7576 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -122,3 +122,13 @@ Abort.
Goal (forall A : Prop, A -> ~~A).
Proof. refine(fun A a f => _).
+
+(* Checking beta-iota normalization of hypotheses in created evars *)
+
+Goal {x|x=0} -> True.
+refine (fun y => let (x,a) := y in _).
+match goal with a:_=0 |- _ => idtac end.
+
+Goal (forall P, {P 0}+{P 1}) -> True.
+refine (fun H => if H (fun x => x=x) then _ else _).
+match goal with _:0=0 |- _ => idtac end.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 18:06:50 +0000