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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
