Re: [isabelle] "isabelle make" in windows-RC2

On Sun, 13 May 2012, Alfio Martini wrote:

Alfio Martini at AlfioMartini-PC ~/Isabelle/PropTh/ISAR-PROP
$ ./makescript
### White space in ISABELLE_HOME may cause strange problems!
### ISABELLE_HOME="/cygdrive/c/Users/Alfio Martini/Desktop/Isabelle2012-RC2"

make: /cygdrive/c/Users/Alfio: Command not found
IsaMakefile:25: recipe for target `/cygdrive/c/Users/Alfio' failed

Somehow the command "isabelle make" here is not able to cope with the space in the string "Alfio Martini".

The problem here is make, because it is inherently incapable of working with spaces in file names. This problem is known for a long time, and will only be solved when the "make" tool is discontinued. In the past, it was not so critical, because real Unix users never have spaces in their directory names. Now we support Mac OS X and Windows fully, so this needs more attention.

You have various possibilities for workarounds right now:

  * Ensure that $ISABELLE_HOME does not contain spaces, by moving the
    Isabelle distribution to a different place.

  * Try hard to use only relative directory names in the IsaMakefile;
    this might work for user projects, but not for the Isabelle
    distribution itself.

  * Produce a build script manually, without make.  Plain "isabelle
    usedir" with suitable options will do the job -- this odd dependency
    management is not really required for small sessions anyway.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.