I have two items of interest for the coming release.
There is some interest here at Data61 (NICTA that was) in having a
localised record package in Isabelle-2016. I've done the initial
implementation and got the parts of the package I understand working
within locales etc, but something goes wrong with the code generation
aspect. Is there anyone who understands how to debug the code generator
who'd have time to look at that?
The second proposal is probably more contentious. I'm hoping to
reimplement a tool we had in the past that speeds up proof maintenance
work by selectively skipping proofs that are very likely to succeed. To
support that, I'm proposing adding a couple of hooks to Pure/goal.ML,
similar to the hook in Pure/Isar/toplevel.ML. One hook will allow the
tool to install an oberver (context -> thm -> unit) for completed
proofs. Another (context -> thm -> bool) will allow the tool to observe
proofs as they commence, and to optionally recommend they be skipped.
This second change essentially just gives the user a little more
control, they could skip the proofs with skip_proofs anyway. Still, I'm
sure it will provoke some interesting discussion.
Cheers,
Thomas.
On 14/01/16 02:55, Lawrence Paulson wrote:
I don't expect to contribute anything else before the next release. There are
little bits that I could add, but probably I should desist in the name of
stability.
Larry
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
________________________________
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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
