Email Gateway (Aug 22 2022 at 12:38): Email Gateway (Aug 22 2022 at 12:38):From: Michael Norrish <Michael.Norrish@nicta.com.au>
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.
Michael
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 12:38):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 24 2024 at 01:07 UTC