Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bootstrap problem in Isabelle2021-RC1: Consume...

view this post on Zulip Email Gateway (Jan 03 2021 at 09:45):

From: Florian Haftmann <>
Starting from a plain mercurial checkout:

$ isabelle build -b Pure

Building Isabelle/Scala ...

Building Pure ...
*** Consumer thread failure: "Isabelle.Session.manager"
*** I/O error:
(Datei oder Verzeichnis nicht gefunden)

and then the process hangs.


$ isabelle jedit -b
$ isabelle build -b Pure

works as expected.


view this post on Zulip Email Gateway (Jan 03 2021 at 11:27):

From: Makarius <>
OK, I have made it more robust here:

Thus it will be in Isabelle2021-RC2, presumably to be published within 1 week.

Behind that is a funny trick to get Isabelle/Scala source positions into PIDE
markup produced by Isabelle/ML. For example:

ML ‹
@{scala echo} "abc"

Now C-hover-click on "echo" will jump to the implementation of that registered
Isabelle/Scala function.

Registration of such functions works in user-space, using a suitable
invocation of "isabelle_scala_service" in etc/settings (e.g. of an add-on
component). For Isabelle/Pure it happens in $ISABELLE_HOME/etc/settings like this:

isabelle_scala_service 'isabelle.Scala_Functions'


Last updated: Jul 15 2022 at 23:21 UTC