Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Issues with `polyc` on macOS

view this post on Zulip 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):

I 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

Last updated: May 06 2025 at 08:28 UTC