[isabelle-dev] Building Pure on Windows
makarius at sketis.net
Thu Feb 18 21:25:42 CET 2016
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
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
To simplify experimentation, you can invoke the bash_process tool like
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 $?").
More information about the isabelle-dev