Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: MLton compiler for x86_64-linux

Email Gateway (Sep 17 2022 at 21:44):

From: Makarius <makarius@sketis.net>
* System *

• The MLton compiler for x86_64-linux has been bundled as Isabelle
  component, since Ubuntu 22.04 no longer provides a suitable package.
  Note that on macOS, MLton is readily available via Homebrew:
  https://formulae.brew.sh/formula/mlton

The Isabelle settings refer to an executable "$ISABELLE_MLTON" and
command-line options $ISABELLE_MLTON_OPTIONS, which need to fit
together. Potential INCOMPATIBILITY for existing
$ISABELLE_HOME_USER/etc/settings.

This refers to Isabelle/1a31d1551eb3.

Example settings:

ISABELLE_MLTON="mlton"
ISABELLE_MLTON_OPTIONS=""

No special options are required for mlton taken from the underlying Linux
distribution; but the default options by the component might be in conflict.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Sep 18 2022 at 11:23):

From: Makarius <makarius@sketis.net>
It is occasionally used with SML codegeneration, to produce a high-end
executable. AFP/59b24f0e98b1 has the following occurrences of ISABELLE_MLTON:

Buchi_Complementation
Native_Word
PAC_Checker

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Feb 01 2025 at 20:19 UTC