Email Gateway (May 02 2025 at 13:38): Email Gateway (May 02 2025 at 13:38):From: Simon Wimmer <wimmersimon@gmail.com>
The executable polyc of Poly/ML 5.9.1 is broken in multiple ways on Mac.
This pertains both to the versions bundled with Isabelle2025 as well as the
homebrew build.
This issue (https://github.com/polyml/polyml/issues/194) names the
problems, and suggests fixes (in polyc):
-ld_classic to EXTRALDFLAGSLINKI stumbled upon this since I wanted to compile exported SML code with
polyc in compile_generated_files for an AFP entry.
Until a new version of Poly/ML is released, what is a recommended
workaround?
Is there something like theories [condition= ] (in a ROOT file) to skip
the theory with the call to compile_generated_files on macOS?
Thanks,
Simon
Email Gateway (May 22 2025 at 14:09):From: Makarius <makarius@sketis.net>
On 02/05/2025 15:37, Simon Wimmer wrote:
The executable
polycof Poly/ML 5.9.1 is broken in multiple ways on Mac.This pertains both to the versions bundled with Isabelle2025 as well as the
homebrew build.
This issue (https://github.com/polyml/polyml/issues/194 <https://github.com/
polyml/polyml/issues/194>) names the problems, and suggests fixes (inpolyc):
- Add-ld_classictoEXTRALDFLAGS
- Remove quotes aroundLINKI stumbled upon this since I wanted to compile exported SML code with
polyc
incompile_generated_filesfor an AFP entry.
Note that polyc is inherently non-portable: it depends on many side-conditions
of the underlying C development environment.
That is not included in the standard repertoire of Isabelle tools, and the AFP
editors should reject an entry that uses "polyc" (if they actually notice it).
To test generated ML program text with Poly/ML, the usual approach is to use
the running Isabelle/ML environment, and essentially "eval" the source (as
done in LISP many decades ago). E.g. see the Isabelle/Isar command "value
[PolyML]".
Until a new version of Poly/ML is released, what is a recommended workaround?
Is there something liketheories [condition= ](in a ROOT file) to skip the
theory with the call tocompile_generated_fileson macOS?
There is no workaround, because using polyc is not supported.
Makarius
Email Gateway (May 29 2025 at 07:59):From: Simon Wimmer <wimmersimon@gmail.com>
Thanks, Makarius.
I solved the issue by adding a switch (enabled by default) for "eval" with
the Isabelle//ML environment rather than compilation with polyc.
I couldn't really work out what "value [PolyML]" refers to, but I found
some helpful breadcrumbs by looking at HOL/Library/code_test.ML.
Simon
Am Do., 22. Mai 2025 um 16:00 Uhr schrieb Makarius <makarius@sketis.net>:
On 02/05/2025 15:37, Simon Wimmer wrote:
The executable
polycof Poly/ML 5.9.1 is broken in multiple ways on
Mac.This pertains both to the versions bundled with Isabelle2025 as well as
the
homebrew build.
This issue (https://github.com/polyml/polyml/issues/194 <
https://github.com/
polyml/polyml/issues/194>) names the problems, and suggests fixes (in
polyc):
- Add-ld_classictoEXTRALDFLAGS
- Remove quotes aroundLINKI stumbled upon this since I wanted to compile exported SML code with
polyc
incompile_generated_filesfor an AFP entry.Note that polyc is inherently non-portable: it depends on many
side-conditions
of the underlying C development environment.That is not included in the standard repertoire of Isabelle tools, and the
AFP
editors should reject an entry that uses "polyc" (if they actually notice
it).To test generated ML program text with Poly/ML, the usual approach is to
use
the running Isabelle/ML environment, and essentially "eval" the source (as
done in LISP many decades ago). E.g. see the Isabelle/Isar command "value
[PolyML]".Until a new version of Poly/ML is released, what is a recommended
workaround?
Is there something liketheories [condition= ](in a ROOT file) to
skip the
theory with the call tocompile_generated_fileson macOS?There is no workaround, because using polyc is not supported.
Makarius
Last updated: May 30 2025 at 04:27 UTC