From b295d3402ddebfd2ca3aa052a32880df8d9060a2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 20 Apr 2016 09:45:46 +0200
Subject: One more word about checking 4.01.0 with -debug and camlp4.
---
configure.ml | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/configure.ml b/configure.ml
index 83005f0c50..9fdd451f19 100644
--- a/configure.ml
+++ b/configure.ml
@@ -598,10 +598,11 @@ let check_camlp5_version () =
| _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n"
let check_caml_version_for_camlp4 () =
- if caml_version_nums = [4;1;0] && !Prefs.debug then
- die ("Your version of OCaml is 4.01.0 which fails to compile Coq in -debug\n" ^
- "mode with Camlp4. Remove -debug option or use a different version of OCaml\n" ^
- "or use Camlp5.\n")
+ if caml_version_nums = [4;1;0] && !Prefs.debug && not !Prefs.force_caml_version then
+ die ("Your version of OCaml is detected to be 4.01.0 which fails to compile\n" ^
+ "Coq in -debug mode with Camlp4. Remove -debug option or use a different\n" ^
+ "version of OCaml or use Camlp5, or bypass this test by using option\n" ^
+ "-force-caml-version.\n")
let config_camlpX () =
try
--
cgit v1.2.3
From dc469f9aaf0d5b77458e40893d897de12339b9b3 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Sat, 9 Apr 2016 12:46:40 -0400
Subject: Print magic numbers in bad magic error message
---
lib/system.ml | 17 ++++++++++++-----
lib/system.mli | 6 ++++--
2 files changed, 16 insertions(+), 7 deletions(-)
diff --git a/lib/system.ml b/lib/system.ml
index 36fdf26089..205a5506cb 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -214,7 +214,8 @@ let skip_in_segment f ch =
seek_in ch stop;
stop, digest_in f ch
-exception Bad_magic_number of string
+type magic_number_error = {filename: string; actual: int; expected: int}
+exception Bad_magic_number of magic_number_error
let raw_extern_state magic filename =
let channel = open_trapping_failure filename in
@@ -224,8 +225,12 @@ let raw_extern_state magic filename =
let raw_intern_state magic filename =
try
let channel = open_in_bin filename in
- if not (Int.equal (input_binary_int filename channel) magic) then
- raise (Bad_magic_number filename);
+ let actual_magic = input_binary_int filename channel in
+ if not (Int.equal actual_magic magic) then
+ raise (Bad_magic_number {
+ filename=filename;
+ actual=actual_magic;
+ expected=magic});
channel
with
| End_of_file -> error_corrupted filename "premature end of file"
@@ -255,9 +260,11 @@ let intern_state magic filename =
let with_magic_number_check f a =
try f a
- with Bad_magic_number fname ->
+ with Bad_magic_number {filename=fname;actual=actual;expected=expected} ->
errorlabstrm "with_magic_number_check"
- (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++
+ (str"File " ++ str fname ++ strbrk" has bad magic number " ++
+ int actual ++ str" (expected " ++ int expected ++ str")." ++
+ spc () ++
strbrk "It is corrupted or was compiled with another version of Coq.")
(* Time stamps. *)
diff --git a/lib/system.mli b/lib/system.mli
index 062c8ea856..fa675a4f02 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -34,9 +34,11 @@ val file_exists_respecting_case : string -> string -> bool
(** {6 I/O functions } *)
(** Generic input and output functions, parameterized by a magic number
and a suffix. The intern functions raise the exception [Bad_magic_number]
- when the check fails, with the full file name. *)
+ when the check fails, with the full file name and expected/observed magic
+ numbers. *)
-exception Bad_magic_number of string
+type magic_number_error = {filename: string; actual: int; expected: int}
+exception Bad_magic_number of magic_number_error
val raw_extern_state : int -> string -> out_channel
--
cgit v1.2.3
From 2ee92b2e851c91776ed26b2461304867b0b8c98c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 25 Apr 2016 19:04:17 +0200
Subject: Fixing bug #4684: Singleton list notation unusable in 8.5pl1.
---
theories/Vectors/VectorDef.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 45c13e5cea..c692238041 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -297,7 +297,7 @@ Notation "[]" := [] : vector_scope.
Notation "h :: t" := (h :: t) (at level 60, right associativity)
: vector_scope.
Notation " [ x ] " := (x :: []) : vector_scope.
-Notation " [ x ; .. ; y ] " := (cons _ x _ .. (cons _ y _ (nil _)) ..) : vector_scope
+Notation " [ x ; y ; .. ; z ] " := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope
.
Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
Open Scope vector_scope.
--
cgit v1.2.3
From 3e57bde4e0ff1b9f65976f2de4d48a78131d4db3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 25 Apr 2016 13:31:45 +0200
Subject: Optimization in building a return clause by pattern-matching: do not
build a default case if the pattern is irrefutable. It did not matter in
practice because we did not check for unused clauses in this case.
---
pretyping/cases.ml | 35 ++++++++++++++++++++---------------
1 file changed, 20 insertions(+), 15 deletions(-)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3d6fa38d0d..0923dfeef2 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1759,12 +1759,12 @@ let build_inversion_problem loc env sigma tms t =
Pushed (true,((tm,tmtyp),deps,na)))
dep_sign decls in
let subst = List.map (fun (na,t) -> (na,lift n t)) subst in
- (* [eqn1] is the first clause of the auxiliary pattern-matching that
+ (* [main_eqn] is the main clause of the auxiliary pattern-matching that
serves as skeleton for the return type: [patl] is the
substructure of constructors extracted from the list of
constraints on the inductive types of the multiple terms matched
in the original pattern-matching problem Xi *)
- let eqn1 =
+ let main_eqn =
{ patterns = patl;
alias_stack = [];
eqn_loc = Loc.ghost;
@@ -1775,19 +1775,24 @@ let build_inversion_problem loc env sigma tms t =
rhs_vars = List.map fst subst;
avoid_ids = avoid;
it = Some (lift n t) } } in
- (* [eqn2] is the default clause of the auxiliary pattern-matching: it will
- catch the clauses of the original pattern-matching problem Xi whose
- type constraints are incompatible with the constraints on the
+ (* [catch_all] is a catch-all default clause of the auxiliary
+ pattern-matching, if needed: it will catch the clauses
+ of the original pattern-matching problem Xi whose type
+ constraints are incompatible with the constraints on the
inductive types of the multiple terms matched in Xi *)
- let eqn2 =
- { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl;
- alias_stack = [];
- eqn_loc = Loc.ghost;
- used = ref false;
- rhs = { rhs_env = pb_env;
- rhs_vars = [];
- avoid_ids = avoid0;
- it = None } } in
+ let catch_all_eqn =
+ if List.for_all (irrefutable env) patl then
+ (* No need for a catch all clause *)
+ []
+ else
+ [ { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl;
+ alias_stack = [];
+ eqn_loc = Loc.ghost;
+ used = ref false;
+ rhs = { rhs_env = pb_env;
+ rhs_vars = [];
+ avoid_ids = avoid0;
+ it = None } } ] in
(* [pb] is the auxiliary pattern-matching serving as skeleton for the
return type of the original problem Xi *)
(* let sigma, s = Evd.new_sort_variable sigma in *)
@@ -1804,7 +1809,7 @@ let build_inversion_problem loc env sigma tms t =
pred = (*ty *) mkSort s;
tomatch = sub_tms;
history = start_history n;
- mat = [eqn1;eqn2];
+ mat = main_eqn :: catch_all_eqn;
caseloc = loc;
casestyle = RegularStyle;
typing_function = build_tycon loc env pb_env s subst} in
--
cgit v1.2.3
From cd139311ecd872301077b9db2df812a828ce2e77 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 21:34:38 +0200
Subject: Fixing an incompatility introduced in a404360: kernel conversion was
not considering conversion of constants over their canonical name but on
their user name. This is observable when delta is off.
---
kernel/reduction.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 97c3e1b348..2f1df396b5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -193,7 +193,7 @@ let convert_instances ~flex u u' (s, check) =
let conv_table_key infos k1 k2 cuniv =
if k1 == k2 then cuniv else
match k1, k2 with
- | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' ->
+ | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' ->
if Univ.Instance.equal u u' then cuniv
else
let flex = evaluable_constant cst (info_env infos)
--
cgit v1.2.3
From e5fe4569f3eaeaa4e1ce377989e19f1f2c176da9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 28 Apr 2016 00:02:32 +0200
Subject: An example for cd139311e, showing a consequence of not converting
constants up to their canonical name (taken from Daniel's formalization of
Puiseux theorem).
---
test-suite/success/remember.v | 13 +++++++++++++
1 file changed, 13 insertions(+)
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
index 0befe054a3..b26a9ff1eb 100644
--- a/test-suite/success/remember.v
+++ b/test-suite/success/remember.v
@@ -14,3 +14,16 @@ let name := fresh "fresh" in
remember (1 + 2) as x eqn:name.
rewrite fresh.
Abort.
+
+(* An example which was working in 8.4 but failing in 8.5 and 8.5pl1 *)
+
+Module A.
+Axiom N : nat.
+End A.
+Module B.
+Include A.
+End B.
+Goal id A.N = B.N.
+reflexivity.
+Qed.
+
--
cgit v1.2.3
From 5055ba0abd1a36d6f33666b0f72fbd9cf6ae3971 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 28 Apr 2016 13:58:25 +0200
Subject: Fix missing newline in coqchk engagement (bug #4694).
---
checker/check_stat.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index d031975d79..84f5684d48 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -28,7 +28,7 @@ let pr_engagement (impr_set,type_in_type) =
match impr_set with
| ImpredicativeSet -> str "Theory: Set is impredicative"
| PredicativeSet -> str "Theory: Set is predicative"
- end ++
+ end ++ fnl() ++
begin
match type_in_type with
| StratifiedType -> str "Theory: Stratified type hierarchy"
--
cgit v1.2.3
From 1aa989f13a3d3a3171dd09e4727394b88bc4b8ce Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 28 Apr 2016 17:05:47 +0200
Subject: Update tutorial (fix bug #4699).
---
doc/tutorial/Tutorial.tex | 56 ++++++++++++++++++++++++++++-------------------
1 file changed, 33 insertions(+), 23 deletions(-)
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index e09feeb8eb..973a0b75e0 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -248,11 +248,14 @@ explicitly the type of the quantified variable. We check:
\begin{coq_example}
Check (forall m:nat, gt m 0).
\end{coq_example}
-We may clean-up the development by removing the contents of the
-current section:
+We may revert to the clean state of
+our initial session using the \Coq~ \verb:Reset: command:
\begin{coq_example}
-Reset Declaration.
+Reset Initial.
\end{coq_example}
+\begin{coq_eval}
+Set Printing Width 60.
+\end{coq_eval}
\section{Introduction to the proof engine: Minimal Logic}
@@ -658,10 +661,8 @@ respectively 1 and 2. Such abstract entities may be entered in the context
as global variables. But we must be careful about the pollution of our
global environment by such declarations. For instance, we have already
polluted our \Coq~ session by declaring the variables
-\verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:. If we want to revert to the clean state of
-our initial session, we may use the \Coq~ \verb:Reset: command, which returns
-to the state just prior the given global notion as we did before to
-remove a section, or we may return to the initial state using~:
+\verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:.
+
\begin{coq_example}
Reset Initial.
\end{coq_example}
@@ -770,7 +771,7 @@ Let us now close the current section.
End R_sym_trans.
\end{coq_example}
-Here \Coq's printout is a warning that all local hypotheses have been
+All the local hypotheses have been
discharged in the statement of \verb:refl_if:, which now becomes a general
theorem in the first-order language declared in section
\verb:Predicate_calculus:. In this particular example, the use of section
@@ -1105,8 +1106,14 @@ mathematical justification of a logical development relies only on
Conversely, ordinary mathematical definitions can be unfolded at will, they
are {\sl transparent}.
+
\chapter{Induction}
+\begin{coq_eval}
+Reset Initial.
+Set Printing Width 60.
+\end{coq_eval}
+
\section{Data Types as Inductively Defined Mathematical Collections}
All the notions which were studied until now pertain to traditional
@@ -1195,7 +1202,7 @@ That is, instead of computing for natural \verb:i: an element of the indexed
\verb:Set: \verb:(P i):, \verb:prim_rec: computes uniformly an element of
\verb:nat:. Let us check the type of \verb:prim_rec::
\begin{coq_example}
-Check prim_rec.
+About prim_rec.
\end{coq_example}
Oops! Instead of the expected type \verb+nat->(nat->nat->nat)->nat->nat+ we
@@ -1241,22 +1248,16 @@ Fixpoint plus (n m:nat) {struct n} : nat :=
For the rest of the session, we shall clean up what we did so far with
types \verb:bool: and \verb:nat:, in order to use the initial definitions
given in \Coq's \verb:Prelude: module, and not to get confusing error
-messages due to our redefinitions. We thus revert to the state before
-our definition of \verb:bool: with the \verb:Reset: command:
+messages due to our redefinitions. We thus revert to the initial state:
\begin{coq_example}
-Reset bool.
-\end{coq_example}
-
-
-\subsection{Simple proofs by induction}
-
-\begin{coq_eval}
Reset Initial.
-\end{coq_eval}
+\end{coq_example}
\begin{coq_eval}
Set Printing Width 60.
\end{coq_eval}
+\subsection{Simple proofs by induction}
+
Let us now show how to do proofs by structural induction. We start with easy
properties of the \verb:plus: function we just defined. Let us first
show that $n=n+0$.
@@ -1480,6 +1481,11 @@ Qed.
\chapter{Modules}
+\begin{coq_eval}
+Reset Initial.
+Set Printing Width 60.
+\end{coq_eval}
+
\section{Opening library modules}
When you start \Coq~ without further requirements in the command line,
@@ -1543,9 +1549,13 @@ definitions available in the current context, especially if large
libraries have been loaded. A convenient \verb:Search: command
is available to lookup all known facts
concerning a given predicate. For instance, if you want to know all the
-known lemmas about the less or equal relation, just ask:
+known lemmas about both the successor and the less or equal relation, just ask:
+\begin{coq_eval}
+Reset Initial.
+Set Printing Width 60.
+\end{coq_eval}
\begin{coq_example}
-Search le.
+Search S le.
\end{coq_example}
Another command \verb:SearchHead: displays only lemmas where the searched
predicate appears at the head position in the conclusion.
@@ -1553,9 +1563,9 @@ predicate appears at the head position in the conclusion.
SearchHead le.
\end{coq_example}
-A new and more convenient search tool is \textsf{SearchPattern}
+A new and more convenient search tool is \verb:SearchPattern:
developed by Yves Bertot. It allows finding the theorems with a
-conclusion matching a given pattern, where \verb:\_: can be used in
+conclusion matching a given pattern, where \verb:_: can be used in
place of an arbitrary term. We remark in this example, that \Coq{}
provides usual infix notations for arithmetic operators.
--
cgit v1.2.3
From 5bcccd7ed80acdb9904d5a623f1aba42183803a4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 28 Apr 2016 20:38:07 +0200
Subject: Make the language grammar much more precise. (Fix bugs #4682 and
#4683)
Rather than being isolated words, commands and tactics now extend till
dot separators. So bullets can be defined as living only at the top level
of proofs, which should make their detection much more robust.
---
ide/coq.lang | 59 +++++++++++++++++++++++++++++++++++++----------------------
1 file changed, 37 insertions(+), 22 deletions(-)
diff --git a/ide/coq.lang b/ide/coq.lang
index e25eedbca9..484264ece3 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -95,11 +95,24 @@
Type
-
+
+
+
+
+
+ \.\.
+
+
+
+
+
+
+
+
\%{decl_head}
@@ -110,14 +123,7 @@
-
-
-
- \.\.
-
-
-
-
+
@@ -127,21 +133,19 @@
-
-
-
-
-
- \%{dot_sep}\s*(?'bul'\%{bullet})
+
+ \%{bullet}
+
+
+ \%[
+ \%{dot_sep}
-
+
+
-
- ^\s*\%{bullet}
-
@@ -150,11 +154,19 @@
\%{dot_sep}
-
-
+
+
+
+
+
+
+
+ \%[
+ \%{dot_sep}
+
About
Check
@@ -166,7 +178,7 @@
Transparent
-
+
Add
Load
(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)
@@ -228,7 +240,10 @@
+
+
+
--
cgit v1.2.3
From 016f2dc3aee608b149097cc08d0720227addc18a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 29 Apr 2016 11:13:54 +0200
Subject: Fix incorrect cbv reduction of primitive projections. (Bug #4634)
As noticed by Cyprien Mangin, projected terms cannot directly be used as
head values. Indeed, they might be applications (e.g. constructors as in
the bug report) whose arguments would thus be missing from the evaluation
stack when doing any iota-reduction step.
The only case where it would make sense is when the evaluation stack is
empty, as an optimization. Indeed, in that case, the arguments are put on
the stack, and then immediately put back inside the term.
---
pretyping/cbv.ml | 2 +-
test-suite/bugs/closed/4634.v | 16 ++++++++++++++++
2 files changed, 17 insertions(+), 1 deletion(-)
create mode 100644 test-suite/bugs/closed/4634.v
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 43062a0e8d..afd86420e9 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -310,7 +310,7 @@ and cbv_stack_value info env = function
| (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk)))
when red_set (info_flags info) fIOTA && Projection.unfolded p ->
let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in
- cbv_stack_value info env (arg, stk)
+ cbv_stack_value info env (strip_appl arg stk)
(* may be reduced later by application *)
| (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl)
diff --git a/test-suite/bugs/closed/4634.v b/test-suite/bugs/closed/4634.v
new file mode 100644
index 0000000000..77e31e108f
--- /dev/null
+++ b/test-suite/bugs/closed/4634.v
@@ -0,0 +1,16 @@
+Set Primitive Projections.
+
+Polymorphic Record pair {A B : Type} : Type :=
+ prod { pr1 : A; pr2 : B }.
+
+Notation " ( x ; y ) " := (@prod _ _ x y).
+Notation " x .1 " := (pr1 x) (at level 3).
+Notation " x .2 " := (pr2 x) (at level 3).
+
+Goal ((0; 1); 2).1.2 = 1.
+Proof.
+ cbv.
+ match goal with
+ | |- ?t = ?t => exact (eq_refl t)
+ end.
+Qed.
--
cgit v1.2.3
From bd5da52c6c625cb4559dd92051384383473ecb1b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 29 Apr 2016 17:01:05 +0200
Subject: Reduce ide/coq.png to 256x256.
Commit 1774a87 increased the file to 1024x1024. This had two adverse
consequences. First, the icon was too large to be used as a window icon
("gdk_window_set_icon_list: icons too large"), so Coqide 8.5 no longer had
an icon at runtime. Second, the file was also used in the About message
box, which was thus exceeding the display size of any reasonably-priced
device. This commit reverts the file to a saner size (still larger than
the original 66x100 picture).
---
ide/coq.png | Bin 71924 -> 12907 bytes
1 file changed, 0 insertions(+), 0 deletions(-)
diff --git a/ide/coq.png b/ide/coq.png
index cccd5a9a19..136bfdd5fe 100644
Binary files a/ide/coq.png and b/ide/coq.png differ
--
cgit v1.2.3