Email Gateway (Jun 17 2026 at 08:17): Email Gateway (Jun 17 2026 at 08:17):From: Tobias Nipkow <nipkow@in.tum.de>
I was trying to build (with Isabelle2025-2) a recent submission to the AFP that
(directly or indirectly) builds on AFP/Buchi_Complementation, but I ran into
this problem on my Mac:
*** /Applications/Isabelle2025-2.app/contrib/mlton-20241230-1/arm64-darwin/lib/
mlton/include/cenv.h:49:10: fatal error: 'gmp.h' file not found
*** #include <gmp.h>
*** ^~~~~~~
The problem is the same in devel. It looks like the mlton component expects gmp
to be installed but on Macs that is (no longer?) guaranteed.
[Aside: "brew install gmp" ran into some permission problems ...]
Tobias
Email Gateway (Jun 29 2026 at 19:19):From: Makarius <makarius@sketis.net>
On 17/06/2026 10:16, Tobias Nipkow wrote:
I was trying to build (with Isabelle2025-2) a recent submission to the AFP
that (directly or indirectly) builds on AFP/Buchi_Complementation, but I ran
into this problem on my Mac:*** /Applications/Isabelle2025-2.app/contrib/mlton-20241230-1/arm64-darwin/
lib/ mlton/include/cenv.h:49:10: fatal error: 'gmp.h' file not found
*** #include <gmp.h>
*** ^~~~~~~
This actually conforms to the specification in NEWS for Isabelle2025 (March 2025):
The NEWS don't say how to provide libgmp, because there are too many
possibilities, and none is really canonical.
I usually do a build from source https://gmplib.org --- essentially
"./configure && make && make install" with results /usr/local
Alternatively, you can try "brew install mlton", and add a suitable
"ISABELLE_MLTON=..." to $ISABELLE_HOME_USER/etc/settings to bypass the
Isabelle component --- I used to do that long ago, but now try to avoid
spilling too much beer on my macOS systems.
If you merely want to avoid a failure of "isabelle build", you can add "unset
ISABELLE_MLTON" to $ISABELLE_HOME_USER/etc/settings --- so theories with
[condition = ISABELLE_MLTON] will be skipped.
It looks like the mlton component expects
gmp to be installed but on Macs that is (no longer?) guaranteed.
As far as I remember, macOS has never provided libgmp, neither for run-time
nor for compile/link-time. That is a constant cause of problems.
For finished executables (e.g. Poly/ML), we bundle libgmp.so with some
manipulation of executable files to refer to the correct library location.
This does not quite work for MLton, because it needs libgmp at
compile/link-time of the target program --- the game is a bit different.
I have now spent some time at https://github.com/MLton/mlton/releases which
now provides more downloads that before, notably for arm64. The latest version
is still MLton 20241230 what we provide already. The arm64 versions work only
half-way, notably without "-codegen native".
So MLton looks like a half-finished / half-dead product after so many decades.
Makarius
Last updated: Jul 02 2026 at 07:34 UTC