Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] libisabelle for Isabelle2015?


view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 20:16 UTC