Re: [isabelle] libisabelle for Isabelle2015?



Hi Walther,

>    Isabelle2015$ ./bin/isabelle jedit -l HOL
> ~/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Protocol.thy &
> 
> causes the error
> 
>    Undefined ML antiquotation: "command_spec"â

this error is as expected, since libisabelle does not (yet) support
Isabelle2015. Not only would the theory files need to be updated, but
also the Scala sources.

> Do you have time to update to Isabelle2015 ?

Not right now, sorry. It requires some more changes to implement
multi-tenancy for libisabelle, which is a prerequisite for robust
multi-Isabelle support. This will likely happen in August when I'm
visiting EPFL, since it's a required feature for my work there. It might
happen earlier if I can find another free weekend.

Cheers
Lars




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