Yann Leray (May 05 2021 at 12:06): Yann Leray (May 05 2021 at 12:06):I'm trying to use Isabelle remotely, on a server without X. However, it seems that Isabelle needs a first launch of jedit to initialise, which it cannot do without X.
Can I initialise Isabelle in another way?
Manuel Eberl (May 05 2021 at 12:07):What do you mean by "use remotely"?
Manuel Eberl (May 05 2021 at 12:07):Do you only want to use isabelle build?
Yann Leray (May 05 2021 at 12:09):I'm only using a custom component (Isabelle/dedukti), and I'm pretty sure it only relies on build under the Scala hood
Manuel Eberl (May 05 2021 at 12:21):I don't know what Dedukti needs, but you can try just doing isabelle build -b HOL. That's roughly what Isabelle/jEdit does on its first launch, I think.
Yann Leray (May 05 2021 at 12:27):I may have another issue: this raises "java.lang.InternalError: java.lang.reflect.InvocationTargetException"
Manuel Eberl (May 05 2021 at 12:27):Any more context on that?
Yann Leray (May 05 2021 at 12:39):I'm going to look into it more in a moment, thanks already
Yann Leray (May 05 2021 at 16:30):Well my interrogation will shift to this exception.
I have an up-to-date minimal Ubuntu 18.04 (without X server)
I downloaded https://isabelle.in.tum.de/dist/Isabelle2021_linux.tar.gz (and checked SHA256), decompressed it using the proposed command, and tried isabelle build -b HOL.
It raised *** java.lang.InternalError: java.lang.reflect.InvocationTargetException (so Isabelle caught it, considering the ***).
Does someone know what may cause this to happen ?
Manuel Eberl (May 05 2021 at 16:34):This may be a problem only Makarius can answer. Please ask it on the isabelle-users mailing list.
Manuel Eberl (May 05 2021 at 16:34):(Makarius does not read Zulip)
Yann Leray (May 05 2021 at 16:35):Alright, thanks
Manuel Eberl (May 05 2021 at 16:35):I found a similar post on the mailing list about Isabelle on WIndows, but it went nowhere: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-April/msg00120.html
Manuel Eberl (May 05 2021 at 16:35):(apparently because the person who asked never replied to him, from what I can see)
Yann Leray (May 05 2021 at 16:44):The conversation incited me to reproduce manually the docker setup, and apparently installing libfontconfig1 did the trick. I'll try to send this answer to the mailing list
Yann Leray (May 05 2021 at 18:16):I can't figure out how to reply to a thread in a mailing list, I guess this will stay here
Last updated: Dec 21 2024 at 16:20 UTC