Discussion of the Coq Theorem Prover

Victor Porton | 12 Nov 2011 00:33

Re: An other bug of Coq 8.3pl2

12.11.2011, 03:23, "Tom Prince" <tom.prince <at> ualberta.net>:
> On Sat, 12 Nov 2011 02:55:59 +0400, Victor Porton <porton <at> narod.ru> wrote:
>
>>  $ coqc test.v
>>  File "./test.v", line 18, characters 4-27:
>>  Anomaly: type_of: variable Other unbound. Please report.
>>
>>  I assume that "Anomaly" means a bug and to report it means to report
>>  bug. Excuse if I have misunderstood this error message.
>
> That is true, but it is best to report bugs to http://coq.inria.fr/bugs/
> That what, they are tracked, and don't get lost.

I reported the bug at http://coq.inria.fr/bugs/ .

For now, I pause my using and learning of Coq until the next release, because dealing with bugs is not what I
want to do.

When to expect the next release?

--

-- 
Victor Porton - http://portonvictor.org

headers

Alexandre Pilkiewicz | 12 Nov 2011 00:40

Re: An other bug of Coq 8.3pl2

2011/11/11 Victor Porton <porton <at> narod.ru>:
> For now, I pause my using and learning of Coq until the next release, because dealing with bugs is not what I
want to do.

You really have a nice way to put it... No doubt. Especially when one
of the two bugs you told us about was not even a bug.

Maybe you could juste stop using structured proofs, which are not well
supported, and stick with the normal way of proving (the one described
in Software Foundation and CPDT for examples). Those are well
supported (I spent 5 to 10 hours a day for the past months proving
stuff, and I don't think I was confronted ton any bugs).

Cheers

Alexandre

headers

Andrej Bauer | 12 Nov 2011 14:15

Re: An other bug of Coq 8.3pl2

> For now, I pause my using and learning of Coq until the next release, because dealing with bugs is not what I
want to do.

I think this is a very wise idea. Check again when Coq 8.6 is out,
perhaps it will work then. No point in dealing with a bunch of buggy
software.

Farewell,

Andrej