Re: [isabelle] Finishing all proofs in use_thy



> Of course it is possible to fabricate some Isabelle/ML snippets that
> hides errors in futures, but I suppose you have used regular proof
> language elements here (Isar commands and proof methods)?
>

I am using libisabelle. So *essentially* I do is: I instantiate Isabelle
with libisabelle. I issue a command from libisabelle to Isabelle to load a
theory which uses Thy_Info.use_thy. This operation completes (that is, I
know that I get a theory and not a "theory future" back because I do
successfully, e.g., print theorems from it). At some point I am asking for
a proof term, and this leads to a delayed exception. On the level of the
theory that is loaded, however, I don't do weird ML. I can get the error
with something as simple as a "sorry" in quick_and_dirty=false mode.

Thy_Info.use_thy should be strict under normal circumstances. Can you
> show an example where it succeeds?
>

I could, I think, but it would be quite some work. (Since I would have to
rewrite the whole setting involving libisabelle described above from
scratch since the problem is too deeply buried in my application. Including
setting up all the build environment etc. I don't see a way to make it
happen without libisabelle because, as you pointed out, using use_thy
inside a normal Isabelle session does not work.)

Interestingly, when trying to get the same to happen using
"Isabelle2018/bin/isabelle console -l HOL -s" and then entering
Thy_Info.use_thy, the problem does not occur (the theory fails right away).
So it might actually be a problem with libisabelle.

I will ask Lars Hupel, perhaps he knows something about this.

But if you know some hotfix (i.e., some way to force the theory to join
after it has loaded even if we don't understand why it hasn't been fully
joined in the first place) I would be happy. Because this problem looks
like it's going to be confusing to track down.


Again the usual questions: What is your greater application context?
> What are you trying to do?
>

I have a scala application (https://github.com/dominique-unruh/qrhl-tool)
that uses Isabelle as a backend for reasoning about terms. For this,
Isabelle gets loaded via libisabelle, the Isabelle session containing my
theories gets loaded via libisabelle, and then various ML-snippets (e.g.,
for calling the simplifier on a term) are invoked via libisabelle.

The new Isabelle PIDE server might be better for it, but it is still
> unused / untested in Isabelle2018. After the release, I have made my own
> applications on top of it: to process all of Isabelle + AFP and
> overserve resulting theory status and markup. This required some
> reworking on the server, and it probably needs more reworking to make it
> applicable in even more applications.
>

I had a look at the PIDE server. While I didn't fully understand the scope
of it, I had the feeling that it was more for "highlevel" operations (like
"build a theory"), and not for things like "simplify this particular term".

Best wishes,
Dominique.



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