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
The line "val response = ..." is the offending code which fails to give an
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,

On Wed, 21 Nov 2018 at 12:06, Lars Hupel <hupel at> 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

Description: Zip archive

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