[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