[isabelle-dev] Building Pure on Windows

Fabian Meier meiefabi at student.ethz.ch
Wed Feb 24 10:16:40 CET 2016


Hello Makarius

Building it with the cygwin from Isabelle2016 worked.

I had trouble doing the other steps listed in your mail. When I run isabelle
env bash nothing happens (no new environment opens), thus I couldn't run
the other two commands.

Cheers Fabian

On 18 February 2016 at 21:25, Makarius <makarius at sketis.net> wrote:

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



-- 
Regards

Fabian Meier (10-919-280)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160224/ba4a72f7/attachment-0002.html>


More information about the isabelle-dev mailing list