*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Finishing all proofs in use_thy*From*: Dominique Unruh <unruh at ut.ee>*Date*: Wed, 21 Nov 2018 09:46:30 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <a577ce04-dbbc-065b-f56e-239f0501c695@sketis.net>*References*: <CAPFfTE4Ude8jnPU9dFkBxdNCvmTAiYoJoGOSFoV_YLiGM3HOdQ@mail.gmail.com> <a577ce04-dbbc-065b-f56e-239f0501c695@sketis.net>

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

**Follow-Ups**:**Re: [isabelle] Finishing all proofs in use_thy***From:*Lars Hupel

**References**:**[isabelle] Finishing all proofs in use_thy***From:*Dominique Unruh

**Re: [isabelle] Finishing all proofs in use_thy***From:*Makarius

- Previous by Date: [isabelle] New AFP entry: Deriving generic class instances for datatypes
- Next by Date: Re: [isabelle] New AFP entry: Deriving generic class instances for datatypes
- Previous by Thread: Re: [isabelle] Finishing all proofs in use_thy
- Next by Thread: Re: [isabelle] Finishing all proofs in use_thy
- Cl-isabelle-users November 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list