Re: [isabelle] New error messages in Isabelle 2013



Hi Makarius,

BTW, you can try to set "Parallel Proofs" to 0 (in Plugin Options /
> Isabelle / General) to see if it becomes less confusing to you.  There is
> also a tiny chance left, that some technical problem remains, but I could
> not see it on the mail thread so far.


It did not change anything.

I sent you [yesterday] the file error_test.thy so you could see more
precisely what is really making me feel uncomfortable
with this. Maybe is a lack of proper interpretation of the message
displayed in the output window from
my part. I attach here again an image that shows the situation. I would
expect the output window to show
exactly what appears in the tooltip window. Nothing more than this. What is
shown in the tooltip window
is fine. On the other hand, what is shown in the output seems to be highly
ambiguous to me.

Best!

On Wed, Jan 30, 2013 at 1:03 PM, Makarius <makarius at sketis.net> wrote:

> On Wed, 30 Jan 2013, Alfio Martini wrote:
>
>  I am still confused about this confusion
>>
>
> Peter Lammich indeed increased the confusion, by raising a different
> issue, one that I could not even see so far.
>
>
>
>  See the e-mail I sent in the sequence. The problem is the ambiguous error
>> message in the output window.
>>
>
> Maybe "sequence" is a good keyword.  Your original confusion was about the
> non-sequential error reporting in a forked proof.
>
> BTW, you can try to set "Parallel Proofs" to 0 (in Plugin Options /
> Isabelle / General) to see if it becomes less confusing to you.  There is
> also a tiny chance left, that some technical problem remains, but I could
> not see it on the mail thread so far.
>
> Since you are also writing Isar proofs, you should try practicing that
> "blindly", in the sense that you keep Output closed by default, and see how
> far you get.  When you type on your keyboard, you also don't really look at
> the keys, right?
>
> When I was preparing the Isabelle/Isar course last October, I maybe
> managed 90% without Output, the rest just from the position of the red
> squiggles and occasionally inspection about the error text behind that.
>
>
>         Makarius
>



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

Attachment: error_test_image.PNG
Description: PNG image

Attachment: error_test.thy
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.