[isabelle-dev] Building Pure on Windows

[Makarius]

On Thu, 18 Feb 2016, Fabian Meier wrote:

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

What happens when you use the Cygwin from Isabelle2016 with the Isabelle 
repository?


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.

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.


To simplify experimentation, you can invoke the bash_process tool like 
this:

   isabelle env bash
   "$ISABELLE_BASH_PROCESS" - bash -c "true"
   "$ISABELLE_BASH_PROCESS" - bash -c "false"

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 $?").


 	Makarius