coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Boutillier <pierre.boutillier AT inria.fr>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Can you help us with coq bugs ?
- Date: Mon, 23 Jan 2012 10:17:14 +0100 (CET)
Hi list,
I am currently going though the "trunk" bugs of Coq in order to tag the one that need to be fix before v8.4 release commenting dozens of:
"This bug should be fixed before v8.4 release."
I'm sorry but coqdevs won't be able to handle them in a reasonable amount of time. My hope in order not to fall in depression is that for some of them advanced users among you could maybe help us. For example, on the following example: http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2630
The easy tactic is written in ltac. In its code http://coq.inria.fr/distrib/V8.4beta/stdlib/Coq.Init.Tactics.html, you can see a "reflexivity". Anyway, it does not work in the
Require Import QArith.
Lemma kaas (x:Q) : Qle x x.
unfold Qle.
(* fails: easy. *)
(* works: *) reflexivity.
Qed.
example. Can an Ltac expert can see why ?
Thanks in advance if you accept to spare time on that and help is really, really, really, enjoyed in any example of http://www.lix.polytechnique.fr/coq/bugs/report.cgi?x_axis_field=version&y_axis_field=component&z_axis_field=&query_format=report-table&short_desc_type=allwordssubstr&short_desc=&long_desc_type=allwordssubstr&long_desc=&bug_file_loc_type=allwordssubstr&bug_file_loc=&deadlinefrom=&deadlineto=&bug_status=UNCONFIRMED&bug_status=NEW&bug_status=ASSIGNED&bug_status=REOPENED&emailassigned_to1=1&emailtype1=substring&email1=&emailassigned_to2=1&emailreporter2=1&emailcc2=1&emailtype2=substring&email2=&bugidtype=include&bug_id=&chfieldfrom=&chfieldto=Now&chfieldvalue=&format=table&action="wrap&field0-0-0=noop&type0-0-0=noop&value0-0-0=
(btw it is the exact moment to make fun of us and say that the solution is "info" :-) but please troll kindly)
All the best
Pierre Boutillier
I am currently going though the "trunk" bugs of Coq in order to tag the one that need to be fix before v8.4 release commenting dozens of:
"This bug should be fixed before v8.4 release."
I'm sorry but coqdevs won't be able to handle them in a reasonable amount of time. My hope in order not to fall in depression is that for some of them advanced users among you could maybe help us. For example, on the following example: http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2630
The easy tactic is written in ltac. In its code http://coq.inria.fr/distrib/V8.4beta/stdlib/Coq.Init.Tactics.html, you can see a "reflexivity". Anyway, it does not work in the
Require Import QArith.
Lemma kaas (x:Q) : Qle x x.
unfold Qle.
(* fails: easy. *)
(* works: *) reflexivity.
Qed.
example. Can an Ltac expert can see why ?
Thanks in advance if you accept to spare time on that and help is really, really, really, enjoyed in any example of http://www.lix.polytechnique.fr/coq/bugs/report.cgi?x_axis_field=version&y_axis_field=component&z_axis_field=&query_format=report-table&short_desc_type=allwordssubstr&short_desc=&long_desc_type=allwordssubstr&long_desc=&bug_file_loc_type=allwordssubstr&bug_file_loc=&deadlinefrom=&deadlineto=&bug_status=UNCONFIRMED&bug_status=NEW&bug_status=ASSIGNED&bug_status=REOPENED&emailassigned_to1=1&emailtype1=substring&email1=&emailassigned_to2=1&emailreporter2=1&emailcc2=1&emailtype2=substring&email2=&bugidtype=include&bug_id=&chfieldfrom=&chfieldto=Now&chfieldvalue=&format=table&action="wrap&field0-0-0=noop&type0-0-0=noop&value0-0-0=
(btw it is the exact moment to make fun of us and say that the solution is "info" :-) but please troll kindly)
All the best
Pierre Boutillier
- [Coq-Club] Can you help us with coq bugs ?, Pierre Boutillier
- Re: [Coq-Club] Can you help us with coq bugs ?, Thomas Braibant
- <Possible follow-ups>
- [Coq-Club] Can you help us with Coq bugs ?, Pierre Boutillier
Archive powered by MhonArc 2.6.16.