HomeIsabelle/Phabricator
System option pide_session is enabled by default

System

  • System option "pide_session" is enabled by default, notably for standard "isabelle build": it allows to invoke Isabelle/Scala operations from Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings:

    ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g"

This refers to Isabelle/80d7f004089d. See also Blog Post: Antiquotations for Isabelle systems programming.

It is still possible to opt-out, e.g. like this isabelle build -o pide_session=false, but at a later stage non-PIDE batch builds will be discontinued.

Written by makarius on Jun 17 2020, 9:55 PM.
User
Projects
None
Subscribers
None

Event Timeline