From 5ac6c86ad8e18161151d53687da1e2825f0a6b46 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 13 Oct 2016 13:49:04 +0200 Subject: [pp] Try to properly tag error messages in cError. In order to get proper coloring, we must tag the headers of error messages in `CError`. This should fix bug https://coq.inria.fr/bugs/show_bug.cgi?id=5135 However, note that this could interact badly with the richpp printing used by the IDE. At this level, we have no clue which tag we'd like to apply, as we know (and shouldn't) nothing about the top level backend. Thus, for now I've selected the console printer, hoping that the `Richpp` won't crash the IDE. --- test-suite/output/Arguments_renaming.out | 6 ++++-- test-suite/output/ltac.out | 3 ++- 2 files changed, 6 insertions(+), 3 deletions(-) (limited to 'test-suite') diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 1633ad9765..e665db47d5 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -2,7 +2,8 @@ File "stdin", line 1, characters 0-36: Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. [arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: +To rename arguments the "rename" flag must be specified. Argument A renamed to B. File "stdin", line 2, characters 0-25: Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. @@ -125,5 +126,6 @@ File "stdin", line 53, characters 0-26: Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. [arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: +To rename arguments the "rename" flag must be specified. Argument A renamed to R. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index f4254e4e2f..a2d545202d 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,5 +1,6 @@ The command has indeed failed with message: -Error: Ltac variable y depends on pattern variable name z which is not bound in current context. +Error: +Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize dependent z -- cgit v1.2.3 From 0aec9033a0b78ee1629f7aabce1c8a2e3cfbe619 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 12 Oct 2016 16:18:02 +0200 Subject: sections/hints: prevent Not_found in get_type_of due to cleared/reverted section variables. This fixes the get_type_of but requires keeping information around about the section hyps available in goals during resolution. It's optimized for the non-section case (should incur no cost there), and the case where no section variables are cleared. --- test-suite/success/clear.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'test-suite') diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v index 976bec7371..e25510cf09 100644 --- a/test-suite/success/clear.v +++ b/test-suite/success/clear.v @@ -13,3 +13,21 @@ Goal forall y z, (forall x:nat, x=y -> True) -> y=z -> True. reflexivity. Qed. +Class A. + +Section Foo. + + Variable a : A. + + Goal A. + solve [typeclasses eauto]. + Undo 1. + clear a. + try typeclasses eauto. + assert(a:=Build_A). + solve [ typeclasses eauto ]. + Undo 2. + assert(b:=Build_A). + solve [ typeclasses eauto ]. + Qed. +End Foo. \ No newline at end of file -- cgit v1.2.3 From 7ba4dee1dd9bf600256827b3517db338d7390566 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 24 Oct 2016 14:54:05 +0200 Subject: Test file for #5127: Memory corruption with the VM --- test-suite/bugs/closed/5127.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 test-suite/bugs/closed/5127.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v new file mode 100644 index 0000000000..831e8fb507 --- /dev/null +++ b/test-suite/bugs/closed/5127.v @@ -0,0 +1,15 @@ +Fixpoint arrow (n: nat) := + match n with + | S n => bool -> arrow n + | O => bool + end. + +Fixpoint apply (n : nat) : arrow n -> bool := + match n return arrow n -> bool with + | S n => fun f => apply _ (f true) + | O => fun x => x + end. + +Axiom f : arrow 10000. +Definition v : bool := Eval compute in apply _ f. +Definition w : bool := Eval vm_compute in v. -- cgit v1.2.3 From 5da679d276e106a62cc3368ceb7358da289ea10a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 24 Oct 2016 01:25:40 +0200 Subject: Complete overhaul of the Arguments vernacular. The main point of this change is to fix #3035: Avoiding trailing arguments in the Arguments command, and related issues occurring in HoTT for instance. When the "assert" flag is not specified, we now accept prefixes of the list of arguments. The semantics of _ w.r.t. to renaming has changed. Previously, it meant "restore the original name inferred from the type". Now it means "don't change the current name". The syntax of arguments is now restricted. Modifiers like /, ! and scopes are allowed only in the first arguments list. We also add *a lot* of missing checks on input values and fix various bugs. Note that this code is still way too complex for what it does, due to the complexity of the implicit arguments, reduction behaviors and renaming APIs. --- test-suite/.csdp.cache | Bin 89077 -> 89077 bytes test-suite/output/Arguments.out | 2 +- test-suite/output/Arguments_renaming.out | 32 +++++++++++-------------------- test-suite/output/Arguments_renaming.v | 6 +++--- 4 files changed, 15 insertions(+), 25 deletions(-) (limited to 'test-suite') diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache index b8c07512f3..b99d80e95f 100644 Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 2c7b04c62a..a2ee2d4c8e 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -101,4 +101,4 @@ Error: Unknown interpretation for notation "$". w 3 true = tt : Prop The command has indeed failed with message: -Error: Extra argument _. +Error: Extra arguments: _, _. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 1633ad9765..8c5efcd897 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,20 +1,12 @@ -File "stdin", line 1, characters 0-36: -Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: To rename arguments the "rename" flag must be +specified. Argument A renamed to B. File "stdin", line 2, characters 0-25: -Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] -File "stdin", line 2, characters 0-25: -Warning: This command is just asserting the number and names of arguments of -identity. If this is what you want add ': assert' to silence the warning. If -you want to clear implicit arguments add ': clear implicits'. If you want to -clear notation scopes add ': clear scopes' [arguments-assert,vernacular] -File "stdin", line 4, characters 0-40: -Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] +Warning: This command is just asserting the names of arguments of identity. +If this is what you want add ': assert' to silence the warning. If you want +to clear implicit arguments add ': clear implicits'. If you want to clear +notation scopes add ': clear scopes' [arguments-assert,vernacular] @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -112,18 +104,16 @@ Expands to: Constant Top.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: -Error: All arguments lists must declare the same names. +Error: Arguments lists should agree on names they provide. The command has indeed failed with message: -Error: The following arguments are not declared: x. +Error: Sequences of implicit arguments must be of different lengths The command has indeed failed with message: Error: Arguments names must be distinct. The command has indeed failed with message: Error: Argument z cannot be declared implicit. The command has indeed failed with message: -Error: Extra argument y. -File "stdin", line 53, characters 0-26: -Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] +Error: Extra arguments: y. The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: To rename arguments the "rename" flag must be +specified. Argument A renamed to R. diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index e42c983361..2d14c94ac8 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -1,5 +1,5 @@ Fail Arguments eq_refl {B y}, [B] y. -Arguments identity T _ _. +Arguments identity A _ _. Arguments eq_refl A x : assert. Arguments eq_refl {B y}, [B] y : rename. @@ -46,9 +46,9 @@ About myplus. Check @myplus. Fail Arguments eq_refl {F g}, [H] k. -Fail Arguments eq_refl {F}, [F]. +Fail Arguments eq_refl {F}, [F] : rename. Fail Arguments eq_refl {F F}, [F] F. -Fail Arguments eq {F} x [z]. +Fail Arguments eq {F} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. -- cgit v1.2.3 From ebb5bd7c2048daa7241bb07d8b53d07e0be27e62 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 25 Oct 2016 13:47:45 +0200 Subject: Add missing dot to impargs error message. --- test-suite/output/Arguments_renaming.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite') diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 8c5efcd897..9d90de47cb 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -106,7 +106,7 @@ Expands to: Constant Top.myplus The command has indeed failed with message: Error: Arguments lists should agree on names they provide. The command has indeed failed with message: -Error: Sequences of implicit arguments must be of different lengths +Error: Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: Error: Arguments names must be distinct. The command has indeed failed with message: -- cgit v1.2.3 From 9c0bec7cb273ec00be45bfe728f87150c3d2f925 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 27 Oct 2016 19:17:37 +0200 Subject: Fixing #5161 (case of a notation with unability to detect a recursive binder). Type annotations in unrelated binders were badly interfering with detection of recursive binders in notations. --- test-suite/bugs/closed/5161.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 test-suite/bugs/closed/5161.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/5161.v b/test-suite/bugs/closed/5161.v new file mode 100644 index 0000000000..d28303b8ab --- /dev/null +++ b/test-suite/bugs/closed/5161.v @@ -0,0 +1,27 @@ +(* Check that the presence of binders with type annotation do not + prevent the recursive binder part to be found *) + +From Coq Require Import Utf8. + +Delimit Scope C_scope with C. +Global Open Scope C_scope. + +Delimit Scope uPred_scope with I. + +Definition FORALL {T : Type} (f : T → Prop) : Prop := ∀ x, f x. + +Notation "∀ x .. y , P" := + (FORALL (λ x, .. (FORALL (λ y, P)) ..)%I) + (at level 200, x binder, y binder, right associativity) : uPred_scope. +Infix "∧" := and : uPred_scope. + +(* The next command fails with + In recursive notation with binders, Φ is expected to come without type. + I would expect this notation to work fine, since the ∀ does support + type annotation. +*) +Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" := + (∀ Φ : _ → _, + (∀ x, .. (∀ y, Q ∧ Φ pat) .. ))%I + (at level 20, x closed binder, y closed binder, + format "{{{ P } } } e {{{ x .. y ; pat , Q } } }") : uPred_scope. -- cgit v1.2.3