Email Gateway (Aug 23 2022 at 08:50): Email Gateway (Aug 23 2022 at 08:50):From: Makarius <makarius@sketis.net>
On 26/04/2020 16:04, J. Juhas (TUM) wrote:
I'm trying to run the newest 2020 version of isabelle in headless mode
(Windows WSL over Visual Code Remote with Isabelle Plugin). But I'm
having some difficulties.I'm using this docker image (https://hub.docker.com/r/makarius/isabelle)
as a reference to enable the tool to work, but this line throws an
internal exception:isabelle build -o system_heaps -b HOL
*** java.lang.InternalError: java.lang.reflect.InvocationTargetException
What is the system context of the above command line? E.g. with docker on
Linux, I can do the following in a Terminal without problems:
docker run makarius/isabelle:Isabelle2020 build -o system_heaps -b HOLCF
There is no point to build HOL, because the docker image contains that already.
It should also work with macOS: just before the Isabelle2020 release I made
experiments with it.
I failed so far to run docker on my Windows 10 Home test machine: it lacks
Hyper-V.
I've also tried just using the Windows version but that fails with
messages ranging from ASLR, incorrect setting of ISABELLE_HOME, OS
detection and finally simply ERROR
What means ASLR?
The native Windows version of Isabelle presently works better than anything
with docker or WSL, according to my own experimentation (I am not using
Windows routinely, though.)
Makarius
Last updated: Apr 26 2024 at 16:20 UTC