The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/27/2014 07:35 PM, Jason Gross wrote:
> I don't know if anyone has responded to you, or if you resolved this, and
> sorry for the rather late reply, but this sounds like a bug you should
> report on the bug tracker, if the behavior still exists.
>
> -Jason

Yes, it still exists - I'll report it.   I have switched to using 
"-async-proofs off" as a workaround.

-- Jonathan

> On Aug 17, 2014 3:54 AM, "Jonathan" 
> <jonikelee AT gmail.com>
>  wrote:
>
> > I just noticed the following behavior: when using asynchronous proof
> > processing, as in Coqide, a goal that ends in Abort won't fully process.
> > As with:
> >
> > Goal True.
> > idtac. (*or any one tactic that doesn't fail*)
> > fail. (*or any sequence of tactics that fails*)
> > Abort.
> >
> > Instead of the above goal failing, asynchronous processing mode skips from
> > the first tactic (idtac in this case - which is evaluated) directly to the
> > Abort, seeming to ignore everything in between (it's left colored blue in
> > Coqide, instead of green).  No failure occurs.
> >
> > I don't know if this is the desired behavior of Abort under asynchronous
> > processing mode, but some users might not anticipate such skipping, and
> > might be using Abort-ending goals as tests.
> >
> > -- Jonathan