Email Gateway (Aug 22 2022 at 10:16): Email Gateway (Aug 22 2022 at 10:16):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi Lars,
I was too optimistic ...
... because I found myself with strange errors, which probably are caused by
faulty settings [1]. Correction of the settings is tricky if we want to keep
our repository clean. So I'd prefer to start from scratch with Isabelle2015.
However, trying
Isabelle2015$ ./bin/isabelle jedit -l HOL ~/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Protocol.thy &
causes the error
Undefined ML antiquotation: "command_spec"⌂
Do you have time to update to Isabelle2015 ?
Walther
[1] https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-June/msg00122.html
Email Gateway (Aug 22 2022 at 10:16):From: Lars Hupel <hupel@in.tum.de>
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
Last updated: Nov 21 2024 at 12:39 UTC