[isabelle-dev] cygwin problem

Makarius makarius at sketis.net
Tue Apr 21 22:18:07 CEST 2009


On Tue, 21 Apr 2009, Chris Capel wrote:

> I just tried building Isabelle from a new machine, and somehow my
> Cygwin got configured to make its home directory
> /cygdrive/c/Documents\ and\ Settings/chris.

I have played around with new installs of Cygwin just last week, without 
experiencing this problem.  Since many Unixish tools fail to work with 
spaces in file names, it seems unlikely that the Cygwin people make it the 
default for home.


> The directory name having spaces seems to be a problem in IsaMakefile, 
> leading to a whole string of messages like this at various line numbers:
>
> IsaMakefile:204: warning: overriding commands for target `/cygdrive/c/Documents'
> IsaMakefile:116: warning: ignoring old commands for target
> `/cygdrive/c/Documents'

As far as I know, the usual versions of "make" cannot work with spaces in 
file names.  At some point we hope to get rid of Makefiles altogether.


> If this is the default configuration of Cygwin nowadays (and I'm pretty 
> sure I didn't change anything away from the default) then it's probably 
> worth fixing.

All Isabelle scripts should work with spaces, but often external tools 
don't, e.g. Proof General, or E prover.


In any case you should be able to circumvent these problems by producing a 
symlink (via ln -s) in a place without spaces, but pointing to the space 
infested spot.  E.g. like this:

   /home/chris/windows -> /cygdrive/c/Documents and Settings/chris

This should work in general, because Unixish tools do not expand symlinks 
under normal circumstances.


 	Makarius



More information about the isabelle-dev mailing list