Re: [isabelle] contrib's poly/ml directory includes a polyc with a stale path



On Mon, 15 Feb 2016, Michael Norrish wrote:

On OSX:

/Applications/Isabelle2015.app/Contents/Resources/Isabelle2015/contrib/polyml-5.5.2-3/x86-darwin/polyc: 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 work.

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.


	Makarius




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