Stream: Mirror: Isabelle Users Mailing List

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

Email Gateway (Jan 03 2021 at 09:45):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Starting from a plain mercurial checkout:

$ isabelle build -b Pure

Building Isabelle/Scala ...

Building Pure ...
*** Consumer thread failure: "Isabelle.Session.manager"
*** I/O error:
/srv/data/tum/isabelle/devel/src/Tools/jEdit/dist/Isabelle-jEdit.shasum
(Datei oder Verzeichnis nicht gefunden)

and then the process hangs.

Whereas

$ isabelle jedit -b
$ isabelle build -b Pure

works as expected.

Cheers,
Florian
signature.asc

Email Gateway (Jan 03 2021 at 11:27):

From: Makarius <makarius@sketis.net>
OK, I have made it more robust here:
https://isabelle-dev.sketis.net/rISABELLE03e78b35ebbc

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'

Makarius

Last updated: Jan 04 2025 at 20:18 UTC