Email Gateway (Aug 22 2022 at 11:13): Email Gateway (Aug 22 2022 at 11:13):From: Makarius <makarius@sketis.net>
On Tue, 15 Sep 2015, Lars Hupel wrote:
Unknown logic "Codec" -- no heap file found in:
(This is using PIDE 'isabelle.Build.build', not the command line
'isabelle build'.)
What happens with the shell command-line tool?
The same happens when building in system mode. What's strange is that
the "Codec" session doesn't list its theory files (verbose is on).
The log file looks like nothing actually happened. Somehow the build
process was aborted, shortly after starting up the ML process.
It works just fine on another Windows box. Any ideas?
Environment: 32 bit, Windows Server 2012 R2
Does the other Windows box have the same version of Windows?
Makarius
Email Gateway (Aug 22 2022 at 11:13):From: Lars Hupel <hupel@in.tum.de>
What happens with the shell command-line tool?
I'm not sure how to invoke that. This is a headless installation where I
simply extracted the Tarball (which worked perfectly on the other machine).
Does the other Windows box have the same version of Windows?
No, it's got Windows 10.
Email Gateway (Aug 22 2022 at 11:26):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I'm seeing a strange problem when building under Windows:
Session Pure/Pure
Session Unsorted/Codec
Session Unsorted/Protocol2015
Building Pure ...
chmod:
/cygdrive/c/Users/appveyor/.isabelle/Isabelle2015/heaps/polyml-5.5.2_x86-cygwin/Pure:
new permissions are r--rwxr--, not r--r-xr--
Finished Pure (0:00:25 elapsed time, 0:00:13 cpu time, factor 0.52)
Building Codec ...
Finished Codec (0:00:04 elapsed time, 0:00:00 cpu time)
Building Protocol2015 ...
Unknown logic "Codec" -- no heap file found in:
/cygdrive/c/Users/appveyor/.isabelle/Isabelle2015/heaps/polyml-5.5.2_x86-cygwin
/cygdrive/c/projects/libisabelle/contrib/Isabelle2015/heaps/polyml-5.5.2_x86-cygwin
Protocol2015 FAILED
(see also
C:\Users\appveyor\.isabelle\Isabelle2015\heaps\polyml-5.5.2_x86-cygwin\log\Protocol2015)
Unfinished session(s): Protocol2015
(This is using PIDE 'isabelle.Build.build', not the command line
'isabelle build'.)
The same happens when building in system mode. What's strange is that
the "Codec" session doesn't list its theory files (verbose is on). It
works just fine on another Windows box. Any ideas?
Environment: 32 bit, Windows Server 2012 R2
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:29):From: Lars Hupel <hupel@in.tum.de>
I have now finally managed to get logfiles out of that box, which I have
attached.
Pure looks good. Codec starts good (the hashes of the sources are
identical to those on my Linux machine), but then nothing appears to
happen – theories are not being loaded.
Email Gateway (Aug 22 2022 at 11:35):From: Makarius <makarius@sketis.net>
Headless installation on Windows is not expected: you need to go through
isabelle.Main and its special tricks for Cygwin initialization. In
Isabelle2015 this requires to run the end-user application.
I've started to rework that for the coming release. We probably need to
discuss further fine-points separately, e.g. to make a generic jar bundle
that excludes the jdk.
Makarius
Email Gateway (Aug 22 2022 at 12:02):From: Lars Hupel <hupel@in.tum.de>
Dear Makarius,
I have an update to this thread. Some time passed since my last attempt
of bootstrapping a robust, reproducible setup on Windows with
libisabelle, I've tried again and (partially) succeeded. The results can
be witnessed here:
<https://ci.appveyor.com/project/larsrh/libisabelle/build/22>
Somewhere deep down the build logs you will find entires indicative of a
successful 'isabelle build'. What's interesting here is that this is
still Isabelle2015 with which I had problems initially. This means that
while headless setup is not supported, it works.
Now, this is only a partial success, because if I then – after the
installation has been bootstrapped – attempt to start an interactive
session, I get this exception:
java.net.SocketException: Connection reset
at java.net.SocketInputStream.read(SocketInputStream.java:209)
at java.net.SocketInputStream.read(SocketInputStream.java:141)
at java.net.SocketInputStream.read(SocketInputStream.java:223)
at
isabelle.Prover$$anonfun$isabelle$Prover$$message_output$1.read_int$1(prover.scala:279)
at
isabelle.Prover$$anonfun$isabelle$Prover$$message_output$1.read_chunk_bytes$1(prover.scala:294)
at
isabelle.Prover$$anonfun$isabelle$Prover$$message_output$1.read_chunk$1(prover.scala:316)
at
isabelle.Prover$$anonfun$isabelle$Prover$$message_output$1.apply$mcV$sp(prover.scala:323)
at isabelle.Simple_Thread$$anon$2.run(simple_thread.scala:24)
I have no idea why this happens, but this stack trace might be of
interest to you. This happens directly after 'start'. The session bus
'all_messages' only emits the following:
system [[Cannot read message:
Connection reset]]
system [[message_output terminated]]
system [[standard_output terminated]]
system [[standard_error terminated]]
system [[process terminated]]
system [[command_input terminated]]
system [[process_manager terminated]]
exit {return_code=0} [[Return code: 0]]
(I obtained this stack trace by inserting various 'println's into
otherwise unchanged Isabelle2015/Scala sources.)
Cheers
Lars
Last updated: Apr 20 2024 at 12:26 UTC