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

On Mon, 15 Feb 2016, Michael Norrish wrote:


/Applications/ 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.


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