Re: [isabelle] contrib's poly/ml directory includes a polyc with a stale path
On Mon, 15 Feb 2016, Michael Norrish wrote:
line 30: /Users/wenzelm/tmp/isadist/src/x86-darwin/bin/poly: No such
file or directory
I got the directory by looking at ML_HOME.
It would be nice if we could rely on having a polyc that was going to
polyc is not used in Isabelle, and I have never used it myself.
David Matthews introduced that script some years ago to make people who
expect a compiler to act like "cc" to feel comfortable with Poly/ML.
The script could be made position-independent via the usual tricks to
access the "self path" of the executable; it is also not robust wrt.
spaces in directory names. I can't say on the spot how this works
realiably in /bin/sh (as opposed to /bin/bash).
Maybe we should move this discussion over to the Poly/ML mailing list.
This archive was generated by a fusion of
Pipermail (Mailman edition) and