Email Gateway (Aug 18 2022 at 19:39): Email Gateway (Aug 18 2022 at 19:39):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
I was just testing the document preparation system tools in the
Windows-Cigwin-2012-RC2 and got the
following error message;
Alfio Martini@AlfioMartini-PC ~/Isabelle/PropTh/ISAR-PROP
$ ./makescriptWhite space in ISABELLE_HOME may cause strange problems!
ISABELLE_HOME="/cygdrive/c/Users/Alfio
Martini/Desktop/Isabelle2012-RC2"
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
make: *** [/cygdrive/c/Users/Alfio] Error 127
Somehow the command "isabelle make" here is not able to cope with the space
in the string "Alfio Martini".
Since this environment Isabelle variables are set automatically I do not
know how to solve it.
I took a look at the IsaMakeFile and the System Manual, but it was not that
helpful (for the time being)!
Many thanks!
Email Gateway (Aug 18 2022 at 19:39):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 18 2022 at 19:39):From: Alfio Martini <alfio.martini@acm.org>
Dear Makarius,
Email Gateway (Aug 18 2022 at 19:39):From: Michael Norrish <Michael.Norrish@nicta.com.au>
This is inherently not true. Make has many infelicities but this is not one of them. On Windows, you may also need to use the "call" command in order to get your command-lines to work.
If you use appropriate escaping (backslashes in dependency and target lines; quoting in command lines), make will do the right thing.
See the attached for an example.
HOL4 on Windows has always coped with spaces in filenames and so can be installed in such 'awkward' places as C:\program files\HOL.
Amusingly, HOL4 can't be installed in directories with spaces on Unix (at least under Moscow ML), because Moscow ML's shell scripts haven't been written with sufficient care. Dealing with spaces is a pain, but it's doable.
Michael
Makefile
signature.asc
Email Gateway (Aug 18 2022 at 19:39):From: Makarius <makarius@sketis.net>
I did not know these tricks. Last time when we made an effort to improve
the situation was in 2004, and it was not possible to escape. But it also
means that it becomes again dependent on precise make versions -- there
are too many of them.
Anyway, I will make an effort to get rid of the static makefiles for the
next Isabelle release, or the one after it ...
Makarius
Email Gateway (Aug 18 2022 at 19:44):From: Makarius <makarius@sketis.net>
Google reveals some further slightly odd tricks for GNU Make:
http://www.cmcrossroads.com/ask-mr-make/7859-gnu-make-meets-file-names-with-spaces-in-them
Other mutants like BSD make appears to support quotes more directly:
http://www.netbsd.org/docs/pkgsrc/makefile.html#quoting-guideline
This is again just some more motivation to get rid of make really soon
now.
Makarius
Email Gateway (Aug 18 2022 at 19:44):From: Michael Norrish <michael.norrish@nicta.com.au>
On 17/05/2012, at 22:57, Makarius <makarius@sketis.net> wrote:
Google reveals some further slightly odd tricks for GNU Make:
http://www.cmcrossroads.com/ask-mr-make/7859-gnu-make-meets-file-names-with-spaces-in-them
You'll need to check these all carefully yourself: this page's claim that you should use double backslashes does not work with the version of GNU make on my system. Indeed, single backslashes do work.
This is again just some more motivation to get rid of make really soon
now.
I hope the brave new world will make it easy to generate files using things like mlyacc and mllex and to have the dependencies analysed and used in a make-like fashion. Otherwise, you will just be off-loading the use of make to users and the build system will be less useful. If you are worried about different versions of make behaving differently, can't you just package make yourself (just as you do Java etc)?
Michael
Last updated: Apr 18 2024 at 08:19 UTC