aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2015-06-22 11:49:58 +0200
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2015-06-22 11:49:58 +0200
commit6bec099f8487b9d3ec5c44079cf69d3474c73b91 (patch)
treeb23d8983fa887cc7e7255df455c64d5d54130787
parent07e8eede6670a256a81d9d70133ebbeb64f45fe3 (diff)
parent949d027ce8fa94b5c62f938b58c3f85d015b177b (diff)
Merge remote-tracking branch 'forge/v8.5'
-rw-r--r--checker/votour.ml50
-rwxr-xr-xdev/make-installer-win64.sh26
-rw-r--r--doc/refman/AsyncProofs.tex10
-rw-r--r--ide/coq-ssreflect.lang1
-rw-r--r--ide/coq.lang1
-rw-r--r--ide/coqOps.ml2
-rw-r--r--ide/wg_ProofView.ml16
-rw-r--r--kernel/byterun/coq_gc.h13
-rw-r--r--kernel/nativecode.ml8
-rw-r--r--kernel/nativelib.ml21
-rw-r--r--library/universes.ml50
-rw-r--r--parsing/g_vernac.ml43
-rw-r--r--pretyping/nativenorm.ml2
-rw-r--r--printing/printer.ml10
-rw-r--r--proofs/proof_global.ml5
-rw-r--r--proofs/proof_global.mli3
-rw-r--r--stm/lemmas.ml17
-rw-r--r--stm/stm.ml22
-rw-r--r--test-suite/bugs/closed/3446.v47
-rw-r--r--test-suite/bugs/closed/4057.v210
-rw-r--r--test-suite/ide/bug4246.fake14
-rw-r--r--test-suite/ide/bug4249.fake16
-rw-r--r--theories/Program/Tactics.v2
-rw-r--r--tools/fake_ide.ml2
24 files changed, 462 insertions, 89 deletions
diff --git a/checker/votour.ml b/checker/votour.ml
index 7c954d6f9..01965bb4b 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -203,12 +203,45 @@ let rec visit v o pos =
(** Loading the vo *)
+type header = {
+ magic : string;
+ (** Magic number of the marshaller *)
+ length : int;
+ (** Size on disk in bytes *)
+ size32 : int;
+ (** Size in words when loaded on 32-bit systems *)
+ size64 : int;
+ (** Size in words when loaded on 64-bit systems *)
+ objects : int;
+ (** Number of blocks defined in the marshalled structure *)
+}
+
+let dummy_header = {
+ magic = "\000\000\000\000";
+ length = 0;
+ size32 = 0;
+ size64 = 0;
+ objects = 0;
+}
+
+let parse_header chan =
+ let magic = String.create 4 in
+ let () = for i = 0 to 3 do magic.[i] <- input_char chan done in
+ let length = input_binary_int chan in
+ let objects = input_binary_int chan in
+ let size32 = input_binary_int chan in
+ let size64 = input_binary_int chan in
+ { magic; length; size32; size64; objects }
+
type segment = {
name : string;
mutable pos : int;
typ : Values.value;
+ mutable header : header;
}
+let make_seg name typ = { name; typ; pos = 0; header = dummy_header }
+
let visit_vo f =
Printf.printf "\nWelcome to votour !\n";
Printf.printf "Enjoy your guided tour of a Coq .vo or .vi file\n";
@@ -216,11 +249,11 @@ let visit_vo f =
Printf.printf
"At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!";
let segments = [|
- {name="library"; pos=0; typ=Values.v_lib};
- {name="univ constraints of opaque proofs"; pos=0;typ=Values.v_univopaques};
- {name="discharging info"; pos=0; typ=Opt Any};
- {name="STM tasks"; pos=0; typ=Opt Values.v_stm_seg};
- {name="opaque proofs"; pos=0; typ=Values.v_opaques};
+ make_seg "library" Values.v_lib;
+ make_seg "univ constraints of opaque proofs" Values.v_univopaques;
+ make_seg "discharging info" (Opt Any);
+ make_seg "STM tasks" (Opt Values.v_stm_seg);
+ make_seg "opaque proofs" Values.v_opaques;
|] in
while true do
let ch = open_in_bin f in
@@ -229,13 +262,16 @@ let visit_vo f =
for i=0 to Array.length segments - 1 do
let pos = input_binary_int ch in
segments.(i).pos <- pos_in ch;
+ let header = parse_header ch in
+ segments.(i).header <- header;
seek_in ch pos;
ignore(Digest.input ch);
done;
Printf.printf "The file has %d segments, choose the one to visit:\n"
(Array.length segments);
- Array.iteri (fun i { name; pos } ->
- Printf.printf " %d: %s, starting at byte %d\n" i name pos)
+ Array.iteri (fun i { name; pos; header } ->
+ let size = if Sys.word_size = 64 then header.size64 else header.size32 in
+ Printf.printf " %d: %s, starting at byte %d (size %iw)\n" i name pos size)
segments;
Printf.printf "# %!";
let l = read_line () in
diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh
new file mode 100755
index 000000000..73e1fdbeb
--- /dev/null
+++ b/dev/make-installer-win64.sh
@@ -0,0 +1,26 @@
+#!/bin/sh
+
+NSIS="$BASE/NSIS/makensis"
+ZIP=_make.zip
+URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download
+URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download
+
+[ -e config/Makefile ] || ./configure -prefix ./ -with-doc no
+make -j2 coqide
+mkdir -p bin32
+cp bin/* bin32/
+make clean
+make archclean
+( . ${BASE}_64/environ; ./configure -prefix ./ -with-doc no; make -j2; make ide/coqidetop.cmxs )
+cp bin32/coqide* bin/
+if [ ! -e bin/make.exe ]; then
+ wget -O $ZIP $URL1 && 7z x $ZIP "bin/*"
+ wget -O $ZIP $URL2 && 7z x $ZIP "bin/*"
+ rm -rf $ZIP
+fi
+VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2`
+cd dev/nsis
+"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi
+echo Installer:
+ls -h $PWD/*exe
+cd ../..
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 797bf2434..47dc1ac1a 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -18,13 +18,11 @@ on small sets of short files.
This feature has some technical limitations that may make it unsuitable for
some use cases.
-For example, in interactive mode, errors coming from the kernel of Coq are
-signaled late. The most notable type of errors belonging to this category are
-universe inconsistencies or unsatisfied guardedness conditions for fixpoints
-built using tactics.
+For example, in interactive mode, some errors coming from the kernel of Coq
+are signaled late. The type of errors belonging to this category
+are universe inconsistencies.
-Last, at the time of writing, only opaque proofs (ending with \texttt{Qed}) can be
-processed asynchronously.
+Last, at the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously.
\subsection{Proof annotations}
diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang
index 4c488ae89..7cfc16701 100644
--- a/ide/coq-ssreflect.lang
+++ b/ide/coq-ssreflect.lang
@@ -190,6 +190,7 @@
<keyword>Eval</keyword>
<keyword>Load</keyword>
<keyword>Undo</keyword>
+ <keyword>Restart</keyword>
<keyword>Goal</keyword>
<keyword>Print</keyword>
<keyword>Save</keyword>
diff --git a/ide/coq.lang b/ide/coq.lang
index 35dff85e6..c65432bdb 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -161,6 +161,7 @@
<keyword>Print</keyword>
<keyword>Eval</keyword>
<keyword>Undo</keyword>
+ <keyword>Restart</keyword>
<keyword>Opaque</keyword>
<keyword>Transparent</keyword>
</context>
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index af728471f..2387d65c3 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -655,8 +655,6 @@ object(self)
buffer#remove_tag Tags.Script.unjustified ~start ~stop;
buffer#remove_tag Tags.Script.tooltip ~start ~stop;
buffer#remove_tag Tags.Script.to_process ~start ~stop;
- buffer#remove_tag Tags.Script.error ~start ~stop;
- buffer#remove_tag Tags.Script.error_bg ~start ~stop;
buffer#move_mark ~where:start (`NAME "start_of_input")
end;
List.iter (fun { start } -> buffer#delete_mark start) seg;
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 1f3fa3ed3..69d460b01 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -140,20 +140,22 @@ let display mode (view : #GText.view_skel) goals hints evars =
view#buffer#insert "No more subgoals."
| [], [], [], _ :: _ ->
(* A proof has been finished, but not concluded *)
- view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
+ view#buffer#insert "No more subgoals, but there are non-instantiated existential variables:\n\n";
let iter evar =
let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
view#buffer#insert msg
in
- List.iter iter evars
+ List.iter iter evars;
+ view#buffer#insert "\nYou can use Grab Existential Variables."
| [], [], _, _ ->
(* The proof is finished, with the exception of given up goals. *)
- view#buffer#insert "No more, however there are goals you gave up. You need to go back and solve them:\n\n";
+ view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
let iter goal =
let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
view#buffer#insert msg
in
- List.iter iter given_up_goals
+ List.iter iter given_up_goals;
+ view#buffer#insert "\nYou need to go back and solve them."
| [], _, _, _ ->
(* All the goals have been resolved but those on the shelf. *)
view#buffer#insert "All the remaining goals are on the shelf:\n\n";
@@ -168,11 +170,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
let goal_str index = Printf.sprintf
"______________________________________(%d/%d)\n" index total
in
- let vb, pl = if total = 1 then "is", "" else "are", "s" in
- let msg = Printf.sprintf "This subproof is complete, but there %s still %d \
- unfocused goal%s:\n\n" vb total pl
- in
- let () = view#buffer#insert msg in
+ view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
let iter i goal =
let () = view#buffer#insert (goal_str (succ i)) in
let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index c7b18b900..f06275862 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -12,6 +12,7 @@
#define _COQ_CAML_GC_
#include <caml/mlvalues.h>
#include <caml/alloc.h>
+#include <caml/memory.h>
typedef void (*scanning_action) (value, value *);
@@ -24,12 +25,22 @@ CAMLextern void minor_collection (void);
#define Caml_white (0 << 8)
#define Caml_black (3 << 8)
+#ifdef HAS_OCP_MEMPROF
+
+/* This code is necessary to make the OCamlPro memory profiling branch of
+ OCaml compile. */
+
+#define Make_header(wosize, tag, color) \
+ caml_make_header(wosize, tag, color)
+
+#else
+
#define Make_header(wosize, tag, color) \
(((header_t) (((header_t) (wosize) << 10) \
+ (color) \
+ (tag_t) (tag))) \
)
-
+#endif
#define Alloc_small(result, wosize, tag) do{ \
young_ptr -= Bhsize_wosize (wosize); \
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ada7ae737..f56b6f83e 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2015,9 +2015,13 @@ let rec compile_deps env sigma prefix ~interactive init t =
|| (Cmap_env.mem c const_updates)
then init
else
- let comp_stack, (mind_updates, const_updates) = match cb.const_body with
- | Def t ->
+ let comp_stack, (mind_updates, const_updates) =
+ match cb.const_proj, cb.const_body with
+ | None, Def t ->
compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
+ | Some pb, _ ->
+ let mind = pb.proj_ind in
+ compile_mind_deps env prefix ~interactive init mind
| _ -> init
in
let code, name =
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 4be8ced54..ce9e4e2b0 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -102,22 +102,23 @@ let compile_library dir code fn =
r
(* call_linker links dynamically the code for constants in environment or a *)
-(* conversion test. Silently fails if the file does not exist in bytecode *)
-(* mode, since the standard library is not compiled to bytecode with default *)
-(* settings. *)
+(* conversion test. *)
let call_linker ?(fatal=true) prefix f upds =
rt1 := dummy_value ();
rt2 := dummy_value ();
- if Dynlink.is_native || Sys.file_exists f then
+ if not (Sys.file_exists f) then
+ let msg = "Cannot find native compiler file " ^ f in
+ if fatal then Errors.error msg
+ else Pp.msg_warning (Pp.str msg)
+ else
(try
if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
register_native_file prefix
- with | Dynlink.Error e ->
- let msg = "Dynlink error, " ^ Dynlink.error_message e in
- if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg)
- | e when Errors.noncritical e ->
- if fatal then anomaly (Errors.print e)
- else Pp.msg_warning (Errors.print_no_report e));
+ with Dynlink.Error e as exn ->
+ let exn = Errors.push exn in
+ let msg = "Dynlink error, " ^ Dynlink.error_message e in
+ if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
+ else Pp.msg_warning (Pp.str msg));
match upds with Some upds -> update_locations upds | _ -> ()
let link_library ~prefix ~dirname ~basename =
diff --git a/library/universes.ml b/library/universes.ml
index 3a7a76907..16e6ebb02 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -739,15 +739,14 @@ let minimize_univ_variables ctx us algs left right cstrs =
let rec instance (ctx', us, algs, insts, cstrs as acc) u =
let acc, left =
try let l = LMap.find u left in
- List.fold_left (fun (acc, left') (d, l) ->
- let acc', (enf,alg,l') = aux acc l in
- (* if alg then assert(not alg); *)
- let l' =
- if enf then Universe.make l
- else l'
- (* match Universe.level l' with Some _ -> l' | None -> Universe.make l *)
- in
- acc', (d, l') :: left') (acc, []) l
+ List.fold_left
+ (fun (acc, left') (d, l) ->
+ let acc', (enf,alg,l') = aux acc l in
+ let l' =
+ if enf then Universe.make l
+ else l'
+ in acc', (d, l') :: left')
+ (acc, []) l
with Not_found -> acc, []
and right =
try Some (LMap.find u right)
@@ -755,24 +754,21 @@ let minimize_univ_variables ctx us algs left right cstrs =
in
let instantiate_lbound lbound =
let alg = LSet.mem u algs in
- if alg then
- (* u is algebraic and has no upper bound constraints: we
- instantiate it with it's lower bound, if any *)
- instantiate_with_lbound u lbound true false acc
- else (* u is non algebraic *)
- match Universe.level lbound with
- | Some l -> (* The lowerbound is directly a level *)
- (* u is not algebraic but has no upper bounds,
- we instantiate it with its lower bound if it is a
- different level, otherwise we keep it. *)
- if not (Level.equal l u) && not (LSet.mem l algs) then
- (* if right = None then. Should check that u does not
- have upper constraints that are not already in right *)
- instantiate_with_lbound u lbound false false acc
- (* else instantiate_with_lbound u lbound false true acc *)
- else
- (* assert false: l can't be alg *)
- acc, (true, false, lbound)
+ if alg then
+ (* u is algebraic: we instantiate it with it's lower bound, if any,
+ or enforce the constraints if it is bounded from the top. *)
+ instantiate_with_lbound u lbound true (not (Option.is_empty right)) acc
+ else (* u is non algebraic *)
+ match Universe.level lbound with
+ | Some l -> (* The lowerbound is directly a level *)
+ (* u is not algebraic but has no upper bounds,
+ we instantiate it with its lower bound if it is a
+ different level, otherwise we keep it. *)
+ if not (Level.equal l u) then
+ (* Should check that u does not
+ have upper constraints that are not already in right *)
+ instantiate_with_lbound u lbound false (LSet.mem l algs) acc
+ else acc, (true, false, lbound)
| None ->
try
(* if right <> None then raise Not_found; *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 09059b410..e8a1b512c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -249,7 +249,8 @@ GEXTEND Gram
[ [ IDENT "Hypotheses" -> (Some Discharge, Logical)
| IDENT "Variables" -> (Some Discharge, Definitional)
| IDENT "Axioms" -> (None, Logical)
- | IDENT "Parameters" -> (None, Definitional) ] ]
+ | IDENT "Parameters" -> (None, Definitional)
+ | IDENT "Conjectures" -> (None, Conjectural) ] ]
;
inline:
[ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index ac4e3b306..b4b6b8aab 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -271,7 +271,7 @@ and nf_atom env atom =
| Aevar (ev,_) -> mkEvar ev
| Aproj(p,c) ->
let c = nf_accu env c in
- mkProj(Projection.make p false,c)
+ mkProj(Projection.make p true,c)
| _ -> fst (nf_atom_type env atom)
and nf_atom_type env atom =
diff --git a/printing/printer.ml b/printing/printer.ml
index 141ae145d..652542825 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -559,8 +559,8 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
++ emacs_print_dependent_evars sigma seeds)
else
let pei = pr_evars_int sigma 1 exl in
- (str "No more subgoals but non-instantiated existential " ++
- str "variables:" ++ fnl () ++ (hov 0 pei)
+ (str "No more subgoals, but there are non-instantiated existential variables:"
+ ++ fnl () ++ (hov 0 pei)
++ emacs_print_dependent_evars sigma seeds ++ fnl () ++
str "You can use Grab Existential Variables.")
end
@@ -625,17 +625,17 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
begin match bgoals,shelf,given_up with
| [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
| [] , [] , _ ->
- msg_info (str "No more goals, however there are goals you gave up. You need to go back and solve them.");
+ msg_info (str "No more subgoals, but there are some goals you gave up:");
fnl ()
++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up
+ ++ fnl () ++ str "You need to go back and solve them."
| [] , _ , _ ->
msg_info (str "All the remaining goals are on the shelf.");
fnl ()
++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
| _ , _, _ ->
let end_cmd =
- strbrk "This subproof is complete, but there are still \
- unfocused goals." ++
+ str "This subproof is complete, but there are some unfocused goals." ++
(match Proof_global.Bullet.suggest p
with None -> str"" | Some s -> fnl () ++ str s) ++
fnl ()
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3e2c813e3..8677b854d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -74,7 +74,7 @@ type proof_object = {
}
type proof_ending =
- | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
+ | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
| Proved of Vernacexpr.opacity_flag *
(Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
proof_object
@@ -665,4 +665,7 @@ let freeze ~marshallable =
| `No -> !pstates
let unfreeze s = pstates := s; update_proof_mode ()
let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
+let copy_terminators ~src ~tgt =
+ assert(List.length src = List.length tgt);
+ List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 9d5038a3f..88e047782 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -66,7 +66,7 @@ type proof_object = {
}
type proof_ending =
- | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
+ | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
| Proved of Vernacexpr.opacity_flag *
(Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
proof_object
@@ -197,3 +197,4 @@ type state
val freeze : marshallable:[`Yes | `No | `Shallow] -> state
val unfreeze : state -> unit
val proof_of_state : state -> Proof.proof
+val copy_terminators : src:state -> tgt:state -> state
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 5eebd0d9d..c766f3fab 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -328,7 +328,7 @@ let check_exist =
let standard_proof_terminator compute_guard hook =
let open Proof_global in function
- | Admitted (id,k,pe) ->
+ | Admitted (id,k,pe,_) ->
admit (id,k,pe) hook ();
Pp.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
@@ -347,8 +347,8 @@ let standard_proof_terminator compute_guard hook =
let universe_proof_terminator compute_guard hook =
let open Proof_global in function
- | Admitted (id,k,pe) ->
- admit (id,k,pe) (hook None) ();
+ | Admitted (id,k,pe,ctx) ->
+ admit (id,k,pe) (hook (Some ctx)) ();
Pp.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
let is_opaque, export_seff, exports = match opaque with
@@ -480,14 +480,13 @@ let save_proof ?proof = function
error "Admitted requires an explicit statement";
let typ = Option.get const_entry_type in
let ctx = Evd.evar_context_universe_context universes in
- Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None))
+ Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
| None ->
let id, k, typ = Pfedit.current_proof_statement () in
- let ctx =
- let evd, _ = Pfedit.get_current_goal_context () in
- Evd.universe_context evd in
(* This will warn if the proof is complete *)
- let pproofs,_ = Proof_global.return_proof ~allow_partial:true () in
+ let pproofs, universes =
+ Proof_global.return_proof ~allow_partial:true () in
+ let ctx = Evd.evar_context_universe_context universes in
let sec_vars =
match Pfedit.get_used_variables(), pproofs with
| Some _ as x, _ -> x
@@ -497,7 +496,7 @@ let save_proof ?proof = function
let ids_def = Environ.global_vars_set env pproof in
Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
| _ -> None in
- Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None))
+ Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),universes)
in
Proof_global.get_terminator() pe
| Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/stm/stm.ml b/stm/stm.ml
index fa3ffc7c6..373fd0ba3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -671,11 +671,22 @@ end = struct (* {{{ *)
let assign id what =
if VCS.get_state id <> None then () else
try match what with
- | `Full s -> VCS.set_state id s
+ | `Full s ->
+ let s =
+ try
+ let prev = (VCS.visit id).next in
+ if is_cached prev
+ then { s with proof =
+ Proof_global.copy_terminators
+ ~src:(get_cached prev).proof ~tgt:s.proof }
+ else s
+ with VCS.Expired -> s in
+ VCS.set_state id s
| `Proof(ontop,(pstate,counters)) ->
if is_cached ontop then
let s = get_cached ontop in
- let s = { s with proof = pstate } in
+ let s = { s with proof =
+ Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
let s = { s with system =
States.replace_summary s.system
(Summary.surgery_summary
@@ -1119,7 +1130,7 @@ end = struct (* {{{ *)
when is_tac expr && State.same_env o n -> (* A pure tactic *)
Some (id, `Proof (prev, State.proof_part_of_frozen n))
| Some _, Some s ->
- msg_warning (str "Sending back a fat state");
+ msg_warning (str "STM: sending back a fat state");
Some (id, `Full s)
| _, Some s -> Some (id, `Full s) in
let rec aux seen = function
@@ -2328,9 +2339,9 @@ let edit_at id =
VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos
(Option.default brname bn)
(no_edit brinfo.VCS.kind);
- VCS.print ();
VCS.delete_cluster_of id;
VCS.gc ();
+ VCS.print ();
Reach.known_state ~cache:(interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
`NewTip in
@@ -2368,7 +2379,8 @@ let edit_at id =
end else begin
anomaly(str"Cannot leave an `Edit branch open")
end
- | false, None, _ -> backto id None
+ | false, None, Some(_,bn) -> backto id (Some bn)
+ | false, None, None -> backto id None
in
VCS.print ();
rc
diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v
new file mode 100644
index 000000000..4f29b76c6
--- /dev/null
+++ b/test-suite/bugs/closed/3446.v
@@ -0,0 +1,47 @@
+(* File reduced by coq-bug-finder from original input, then from 7372 lines to 539 lines, then from 531 lines to 107 lines, then from 76 lines to 46 lines *)
+(* Set Asymmetric Patterns. *)
+(* Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). *)
+(* Notation "A -> B" := (forall (_ : A), B). *)
+
+(* Notation "x → y" := (x -> y) *)
+(* (at level 99, y at level 200, right associativity): type_scope. *)
+(* Record sigT A (P : A -> Type) := *)
+(* { projT1 : A ; projT2 : P projT1 }. *)
+(* Arguments projT1 {A P} s. *)
+(* Arguments projT2 {A P} s. *)
+(* Set Universe Polymorphism. *)
+(* Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). *)
+(* Reserved Notation "x = y" (at level 70, no associativity). *)
+(* Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y). *)
+(* Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. *)
+(* Reserved Notation "{ x : A & P }" (at level 0, x at level 99). *)
+(* Notation "{ x : A & P }" := (sigT A (fun x => P)) : type_scope. *)
+
+
+(* Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v & transport _ p (projT2 u) = projT2 v}), u = v. *)
+(* Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}). *)
+
+(* Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) := *)
+(* @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _). *)
+
+Set Asymmetric Patterns.
+Set Universe Polymorphism.
+Arguments projT1 {_ _} _.
+Notation "( x ; y )" := (existT _ x y).
+Notation pr1 := projT1.
+Notation "x .1" := (projT1 x) (at level 3).
+Notation "x .2" := (projT2 x) (at level 3).
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Notation "g 'o' f" := (compose g f) (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
+Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3).
+Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT P) (pq : {p : u.1 = v.1 & p # u.2 = v.2}), u = v.
+Instance isequiv_pr1_contr {A} {P : A -> Type} : IsEquiv (@pr1 A P) | 100.
+Admitted.
+
+Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT P) : u.1 = v.1 -> u = v :=
+ path_sigma_uncurried P u v o pr1^-1. \ No newline at end of file
diff --git a/test-suite/bugs/closed/4057.v b/test-suite/bugs/closed/4057.v
new file mode 100644
index 000000000..4f0e696c9
--- /dev/null
+++ b/test-suite/bugs/closed/4057.v
@@ -0,0 +1,210 @@
+Require Coq.Strings.String.
+
+Set Implicit Arguments.
+
+Axiom falso : False.
+Ltac admit := destruct falso.
+
+Reserved Notation "[ x ]".
+
+Record string_like (CharType : Type) :=
+ {
+ String :> Type;
+ Singleton : CharType -> String where "[ x ]" := (Singleton x);
+ Empty : String;
+ Concat : String -> String -> String where "x ++ y" := (Concat x y);
+ bool_eq : String -> String -> bool;
+ bool_eq_correct : forall x y : String, bool_eq x y = true <-> x = y;
+ Length : String -> nat
+ }.
+
+Delimit Scope string_like_scope with string_like.
+Bind Scope string_like_scope with String.
+Arguments Length {_%type_scope _} _%string_like.
+Infix "++" := (@Concat _ _) : string_like_scope.
+
+Definition str_le {CharType} {String : string_like CharType} (s1 s2 : String)
+ := Length s1 < Length s2 \/ s1 = s2.
+Infix "≤s" := str_le (at level 70, right associativity).
+
+Module Export ContextFreeGrammar.
+ Import Coq.Strings.String.
+ Import Coq.Lists.List.
+
+ Section cfg.
+ Variable CharType : Type.
+
+ Section definitions.
+
+ Inductive item :=
+ | NonTerminal (name : string).
+
+ Definition production := list item.
+ Definition productions := list production.
+
+ Record grammar :=
+ {
+ Start_symbol :> string;
+ Lookup :> string -> productions
+ }.
+ End definitions.
+
+ Section parse.
+ Variable String : string_like CharType.
+ Variable G : grammar.
+
+ Inductive parse_of : String -> productions -> Type :=
+ | ParseHead : forall str pat pats, parse_of_production str pat
+ -> parse_of str (pat::pats)
+ | ParseTail : forall str pat pats, parse_of str pats
+ -> parse_of str (pat::pats)
+ with parse_of_production : String -> production -> Type :=
+ | ParseProductionCons : forall str pat strs pats,
+ parse_of_item str pat
+ -> parse_of_production strs pats
+ -> parse_of_production (str ++ strs) (pat::pats)
+ with parse_of_item : String -> item -> Type :=
+ | ParseNonTerminal : forall name str, parse_of str (Lookup G name)
+ -> parse_of_item str (NonTerminal
+name).
+ End parse.
+ End cfg.
+
+End ContextFreeGrammar.
+Module Export ContextFreeGrammarProperties.
+
+ Section cfg.
+ Context CharType (String : string_like CharType) (G : grammar)
+ (P : String.string -> Type).
+
+ Fixpoint Forall_parse_of {str pats} (p : parse_of String G str pats)
+ := match p with
+ | @ParseHead _ _ _ str pat pats p'
+ => Forall_parse_of_production p'
+ | @ParseTail _ _ _ _ _ _ p'
+ => Forall_parse_of p'
+ end
+ with Forall_parse_of_production {str pat} (p : parse_of_production String G
+str pat)
+ := let Forall_parse_of_item {str it} (p : parse_of_item String G str
+it)
+ := match p return Type with
+ | @ParseNonTerminal _ _ _ name str p'
+ => (P name * Forall_parse_of p')%type
+ end in
+ match p return Type with
+ | @ParseProductionCons _ _ _ str pat strs pats p' p''
+ => (Forall_parse_of_item p' * Forall_parse_of_production
+p'')%type
+ end.
+
+ Definition Forall_parse_of_item {str it} (p : parse_of_item String G str it)
+ := match p return Type with
+ | @ParseNonTerminal _ _ _ name str p'
+ => (P name * Forall_parse_of p')%type
+ end.
+ End cfg.
+
+End ContextFreeGrammarProperties.
+
+Module Export DependentlyTyped.
+ Import Coq.Strings.String.
+
+ Section recursive_descent_parser.
+
+ Class parser_computational_predataT :=
+ { nonterminal_names_listT : Type;
+ initial_nonterminal_names_data : nonterminal_names_listT;
+ is_valid_nonterminal_name : nonterminal_names_listT -> string -> bool;
+ remove_nonterminal_name : nonterminal_names_listT -> string ->
+nonterminal_names_listT }.
+
+ End recursive_descent_parser.
+
+End DependentlyTyped.
+Import Coq.Strings.String.
+Import Coq.Lists.List.
+
+Section cfg.
+ Context CharType (String : string_like CharType) (G : grammar).
+ Context (names_listT : Type)
+ (initial_names_data : names_listT)
+ (is_valid_name : names_listT -> string -> bool)
+ (remove_name : names_listT -> string -> names_listT).
+
+ Inductive minimal_parse_of
+ : forall (str0 : String) (valid : names_listT)
+ (str : String),
+ productions -> Type :=
+ | MinParseHead : forall str0 valid str pat pats,
+ @minimal_parse_of_production str0 valid str pat
+ -> @minimal_parse_of str0 valid str (pat::pats)
+ | MinParseTail : forall str0 valid str pat pats,
+ @minimal_parse_of str0 valid str pats
+ -> @minimal_parse_of str0 valid str (pat::pats)
+ with minimal_parse_of_production
+ : forall (str0 : String) (valid : names_listT)
+ (str : String),
+ production -> Type :=
+ | MinParseProductionNil : forall str0 valid,
+ @minimal_parse_of_production str0 valid (Empty _)
+nil
+ | MinParseProductionCons : forall str0 valid str strs pat pats,
+ str ++ strs ≤s str0
+ -> @minimal_parse_of_item str0 valid str pat
+ -> @minimal_parse_of_production str0 valid strs
+pats
+ -> @minimal_parse_of_production str0 valid (str
+++ strs) (pat::pats)
+ with minimal_parse_of_item
+ : forall (str0 : String) (valid : names_listT)
+ (str : String),
+ item -> Type :=
+ | MinParseNonTerminal
+ : forall str0 valid str name,
+ @minimal_parse_of_name str0 valid str name
+ -> @minimal_parse_of_item str0 valid str (NonTerminal name)
+ with minimal_parse_of_name
+ : forall (str0 : String) (valid : names_listT)
+ (str : String),
+ string -> Type :=
+ | MinParseNonTerminalStrLt
+ : forall str0 valid name str,
+ @minimal_parse_of str initial_names_data str (Lookup G name)
+ -> @minimal_parse_of_name str0 valid str name
+ | MinParseNonTerminalStrEq
+ : forall str valid name,
+ @minimal_parse_of str (remove_name valid name) str (Lookup G name)
+ -> @minimal_parse_of_name str valid str name.
+ Definition parse_of_item_name__of__minimal_parse_of_name
+ : forall {str0 valid str name} (p : @minimal_parse_of_name str0 valid str
+name),
+ parse_of_item String G str (NonTerminal name).
+ Proof.
+ admit.
+ Defined.
+
+End cfg.
+
+Section recursive_descent_parser.
+ Context (CharType : Type)
+ (String : string_like CharType)
+ (G : grammar).
+ Context {premethods : parser_computational_predataT}.
+ Let P : string -> Prop.
+ Proof.
+ admit.
+ Defined.
+
+ Let mp_parse_nonterminal_name str0 valid str nonterminal_name
+ := { p' : minimal_parse_of_name String G initial_nonterminal_names_data
+remove_nonterminal_name str0 valid str nonterminal_name & Forall_parse_of_item
+P (parse_of_item_name__of__minimal_parse_of_name p') }.
+
+ Goal False.
+ Proof.
+ clear -mp_parse_nonterminal_name.
+ subst P.
+ simpl in *.
+ admit.
+ Qed.
diff --git a/test-suite/ide/bug4246.fake b/test-suite/ide/bug4246.fake
new file mode 100644
index 000000000..16b552f67
--- /dev/null
+++ b/test-suite/ide/bug4246.fake
@@ -0,0 +1,14 @@
+# first proof
+ADD { Lemma a : True. }
+ADD { Proof using. }
+ADD here { trivial. } # first error
+ADD { fail. }
+ADD { Qed. }
+WAIT
+EDIT_AT here
+# Fixing the proof
+ADD { Qed. }
+WAIT
+EDIT_AT here
+ADD { Qed. }
+JOIN
diff --git a/test-suite/ide/bug4249.fake b/test-suite/ide/bug4249.fake
new file mode 100644
index 000000000..20afe0fb8
--- /dev/null
+++ b/test-suite/ide/bug4249.fake
@@ -0,0 +1,16 @@
+ADD { Lemma a : True. }
+ADD here { Proof using. }
+ADD { fail. }
+ADD { trivial. } # first error
+ADD { Qed. }
+WAIT
+EDIT_AT here
+# Fixing the proof
+ADD fix { trivial. }
+ADD { Qed. }
+WAIT
+EDIT_AT fix
+ADD { Qed. }
+EDIT_AT fix
+ADD { Qed. }
+JOIN
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 0cf8d7337..c1d958b9d 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -41,7 +41,7 @@ Ltac do_nat n tac :=
(** Do something on the last hypothesis, or fail *)
Ltac on_last_hyp tac :=
- match goal with [ H : _ |- _ ] => first [ tac H | fail 1 ] end.
+ lazymatch goal with [ H : _ |- _ ] => tac H end.
(** Destructs one pair, without care regarding naming. *)
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index d7a292f4c..a9a7251c5 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -90,7 +90,7 @@ module Parser = struct (* {{{ *)
in find ~-1 0
else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s))
- let eat_blanks s = snd (eat_rex "[ \n\t]*") s
+ let eat_blanks s = snd (eat_rex "[ \r\n\t]*") s
let s = ref ""