<div dir="ltr"><div><div>Hello Makarius<br><br></div>Building it with the cygwin from Isabelle2016 worked.<br><br></div><div>I had trouble doing the other steps listed in your mail. When I run <span style="font-family:monospace,monospace">isabelle env bash</span> nothing happens (no new environment opens), thus I couldn't run the other two commands. <br></div><div><br></div>Cheers Fabian<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 18 February 2016 at 21:25, Makarius <span dir="ltr"><<a href="mailto:makarius@sketis.net" target="_blank">makarius@sketis.net</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Thu, 18 Feb 2016, Fabian Meier wrote:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
The log-file this error message references is empty. The same error occures when backtracking to commit d4e99aa28abc, but commit 658276428cfc works fine again. Also the Isabelle2016 commit works fine since these changes were merged later. This has possibly something to do with the changes of the bash_process components.<br>
</blockquote>
<br></span>
What happens when you use the Cygwin from Isabelle2016 with the Isabelle repository?<br>
<br>
<br>
There could be a conflict of Cygwin libraries vs. this separately compiled executable. Since bash_process requires a fork/exec, it is subject to odd problems that are usually solved by "rebasing" the executable.<br>
<br>
I can't say on the spot, what is the best way to do that. Cygwin has /bin/rebaseall to do that magic. In recent years, we did not take rebasing very seriously.<br>
<br>
<br>
To simplify experimentation, you can invoke the bash_process tool like this:<br>
<br>
  isabelle env bash<br>
  "$ISABELLE_BASH_PROCESS" - bash -c "true"<br>
  "$ISABELLE_BASH_PROCESS" - bash -c "false"<br>
<br>
This should print the pid on stdout and run the little bash script and produce with a proper return code (which can be display by "echo $?").<span class="HOEnZb"><font color="#888888"><br>
<br>
<br>
        Makarius<br>
</font></span></blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature"><div dir="ltr">Regards<br><br><div style="margin-left:40px">Fabian Meier <span style="color:rgb(153,153,153)">(10-919-280)</span></div></div></div>
</div>