Re: [isabelle] Isabelle2015-RC0 available for testing



On 19/04/15 08:12, Lars Hupel wrote:
Iâve wasted a lot of time dragging the scroll bar to find hidden
errors, but I suppose my use case is unusual in that I am
automatically generating large proof files.

Here we are back to the canonical question: What is the purpose of
generated files?  Is there no better way?

For some reason, generating source files is the first idea that most
people have, and cannot imagine other ways.  It is like a spell that
needs to be broken.  There might be occasionally good reasons to do
that, but one should look critically at the problem, and prove that it
really has to be done like that.

Isabelle/HOL-SPARK is a simple example to do better.  More such work can
be imagined in integrating different tools into the Isabelle Prover IDE,
without having machine-generated sources edited by humans.

I'd also like to point out again my ongoing work on 'libisabelle' [0].
The README is slightly outdated, since the library is in fact able to
fetch and unpack an Isabelle distribution (setting appropriate
environment variables and building sessions is not implemented yet). I'm
also working on supporting multiple Isabelle versions at the same time.

It has already been demonstrated that this way of interaction works well
for sending proof obligations generated via other means to the prover to
have them checked. Right now, I'm also investigating how much useful
information I can get from the prover for performing further (syntactic)
analysis on theory sources. From that perspective, I tend to agree with
Makarius: There are very few remaining use cases of textual code
generation or manual interaction with the prover [2].

NB: Viorel's use case from earlier this month [1] can also be trivially
modelled with libisabelle.

Cheers
Lars

I can't speak of Stephen's use case, but I myself am generating C code and, at the same time,
generating correctness proofs of such code. The generated C code interoperates with hand-written C
code. A goal is for the generated lemmas to be usable in a manual proof of a top-level hand-written
correctness statement.

While it is true that generating textual theories like this is not the only way, it still seems the
path of least resistance to me. We are using a translation validation style approach to verify this
generation process, so it is important that we can inspect the resulting artefact. It is also
helpful for users to be able to inspect these theories and see lemmas and proofs in the manner they
would be expecting to have written them themselves. Alternatively we could be generating proof terms
directly or using something like libisabelle. While not a fundamental obstacle, it is a pragmatic
barrier that our code generator (which also produces Isabelle theories) is written in Python and is
not easily portable to a JVM language.

It's perhaps also worth noting that manual interaction within these large theories is _not_ the
intended use case. I am primarily exploring these theories within Isabelle/jEdit when debugging a
broken proof the theory generator has produced. Overall, I'm not wed to my current approach, but
from my current understanding it is still the most feasible way for me to pursue this. If someone
wants to try to persuade me otherwise, I am more than happy to listen :)

________________________________

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.




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