[isabelle-dev] Building Pure on Windows

Makarius makarius at sketis.net
Tue Mar 1 17:18:59 CET 2016


On Wed, 24 Feb 2016, Makarius wrote:

> Maybe we find some clues about the actual difference, to get to the core 
> of the problem.
>
> The Cygwin of Isabelle2016 uses the quasi-mirror 
> http://isabelle.in.tum.de/cygwin_2016 which is just an alias for a 
> regular Cygwin mirror from Portugal with some tricks to lock it into a 
> fixed version.
>
> Moreover, a given Cygwin installation may have accidental "rebase" 
> addresses of shared libraries that happen to work or happen to fail.

I have made some more experiments with a fresh installation of 
http://isabelle.in.tum.de/cygwin_2016 on Windows 8.1 and 
Isabelle/b737f8f37454.

It all works as expected. I cannot see any problems with bash_process.


The speculative problem about "rebasing" executable does not exist: DLLs 
can be rebased, but not EXEs. See also 
http://isabelle.in.tum.de/repos/isabelle/rev/9d7ba380223c where this was 
once done for the DLLs of Poly/ML, but later discontinued because it 
became native on Windows.


 	Makarius


More information about the isabelle-dev mailing list