[isabelle-dev] Isabelle2013-2 release

[Gerwin Klein]

Sorry, missed all this, because I was away (and the rest of NICTA had a quite busy week).


On 21.11.2013, at 10:56 pm, Makarius <makarius at sketis.net> wrote:

> On Wed, 20 Nov 2013, Makarius wrote:
>
>> Did anybody test WWW_Find?
>
> WWW_Find is a NICTA-only tool.  Did any of the NICTA guys test it in the Isabelle2013-1 RC phase?

Good question. I did not, I assumed others in the group did. Will double-check this week on Isabelle2013-2 RC.


> There was also zero feedback about the context selector in the Find panel of Isabelle/jEdit, e.g. if it can supersede WWW_Find or if it is useless.

Neither. It is somewhat useful, but the main use case for WWW_Find is with images that are potentially too big to build yourself or that you don’t have on your machine for some other reason (e.g. too big for a laptop or small desktop).


> That context is not fully native in the document model so far, and it would require a bit more work to make it fit tightly.  That work is well-invested if the resources for WWW_Find maintenance could be freed eventually (by removing it from the source tree).

If the find_theorems panel could connect to a remote resource similar to sledgehammer's remote provers, we could remove WWW_Find.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.