[isabelle-dev] next release

[Thomas Sewell]

OK, I'll respond to these points in-line.

> A discussion without sources to look at is difficult.

OK, I attach my working version. Colleagues of mine were told off
recently for producing patches without the relevant authority, so these
days I begin these discussions in abstract. Feel free to tell me that
I'm doing it wrong some new way.

> Generally, these hooks are rather old, predating the managed
> evaluation of the PIDE document model.  There used to be more hooks in
> ancient times, but we have managed to get rid of most of them.

OK. I'm not familiar with the history. What I'm proposing is somewhat
orthogonal to the document model as I understand it though. Sure,
essential parts of the system/protocol should be built in rather than
"hooked" in. But rarely used add-on features can be more cleanly
supported by small "hooks" than by building e.g. mirabelle directly into
the system toplevel.

> The general plan (for many years already) is to unify the batch build
> mode further with the managed evaluation of PIDE interaction.  In
> particular there should be proper ways to fork (and maybe ignore)
> proofs in the document model.  Odd flags like skip_proofs or
> quick_and_dirty/sorry might eventually disappear.

Such a consolidation might be nice, though obviously the performance
implications have to be managed. Some of these add-ons could perhaps
observe the proofs being done from the Isabelle/Scala side. Is that what
you're getting at? It sounds a bit involved.

> As usual there is a conflict of proper principles done right, and
> small adhoc patches to an already complex system.

However, doing things right seems to take a long time. Empirically,
fiddling with skip_proofs etc allows some users to see a 2-3x
improvement in their productivity. The question is just how official
this fiddling is allowed to be.

Cheers,
     Thomas.


________________________________

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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: skip_hook.patch
Type: text/x-patch
Size: 4473 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160118/273c7fa3/attachment-0002.bin>