Re: [isabelle] Finishing all proofs in use_thy



Hi Lars,

I managed to make a minimal example (attached).

The actual code is in src/main/scala/test/Test.thy, and the bad theory is
TestEx.thy.
The line "val response = ..." is the offending code which fails to give an
error.
Interestingly, a variation of this line (included and commented out) does
raise an error!

You can test the code simply using "sbt run".

Best wishes,
Dominique.




On Wed, 21 Nov 2018 at 12:06, Lars Hupel <hupel at in.tum.de> wrote:

> > 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.)
>
> I can corroborate this (mostly). When developing the Isabelle
> integration with Leon, I used "Goal.parallel_proofs := 0" quite
> liberally. In my case the problem was less with loading theories;
> rather, running arbitrary ML code that may or may not throw asynchronous
> exceptions.
>
> > I will ask Lars Hupel, perhaps he knows something about this.
>
> If you can send me a minimal example how I can reproduce the problem, I
> could take a look.
>
> Cheers
> Lars
>

Attachment: libisabelle-use-thy.zip
Description: Zip archive



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