Re: [isabelle] Isabelle2015-RC0 available for testing

>> 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.


[0] <>
[2] Lem (<>) comes to mind.

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