Re: [isabelle] Build problems on Windows



Dear Makarius,

> 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 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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.