options for process policy, notably for multiprocessor machines;
authorwenzelm
Sat Oct 01 23:05:25 2016 +0200 (2016-10-01)
changeset 63986c7a4b03727ae
parent 63985 4effb93c2a09
child 63987 ac96fe9224f6
options for process policy, notably for multiprocessor machines;
NEWS
etc/options
src/Pure/Tools/ml_process.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/jedit_sessions.scala
     1.1 --- a/NEWS	Sat Oct 01 20:59:09 2016 +0200
     1.2 +++ b/NEWS	Sat Oct 01 23:05:25 2016 +0200
     1.3 @@ -970,6 +970,14 @@
     1.4  exhaust the small 32-bit address space of the ML process (which is used
     1.5  by default).
     1.6  
     1.7 +* System option "ML_process_policy" specifies an optional command prefix
     1.8 +for the underlying ML process, e.g. to control CPU affinity on
     1.9 +multiprocessor systems.
    1.10 +
    1.11 +* The "isabelle jedit" tool provides options -P and -p to specify an
    1.12 +optional command prefix for the Java and ML process, respectively (see
    1.13 +also option "ML_process_policy").
    1.14 +
    1.15  
    1.16  
    1.17  New in Isabelle2016 (February 2016)
     2.1 --- a/etc/options	Sat Oct 01 20:59:09 2016 +0200
     2.2 +++ b/etc/options	Sat Oct 01 23:05:25 2016 +0200
     2.3 @@ -129,6 +129,9 @@
     2.4  public option ML_system_64 : bool = false
     2.5    -- "ML system for 64bit platform is used if possible (change requires restart)"
     2.6  
     2.7 +public option ML_process_policy : string = ""
     2.8 +  -- "ML process command prefix (process policy)"
     2.9 +
    2.10  
    2.11  section "Editor Reactivity"
    2.12  
     3.1 --- a/src/Pure/Tools/ml_process.scala	Sat Oct 01 20:59:09 2016 +0200
     3.2 +++ b/src/Pure/Tools/ml_process.scala	Sat Oct 01 23:05:25 2016 +0200
     3.3 @@ -98,7 +98,9 @@
     3.4        (eval_init ::: eval_modes ::: eval_options ::: eval_process).
     3.5          map(eval => List("--eval", eval)).flatten ::: args
     3.6  
     3.7 -    Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),
     3.8 +    Bash.process(
     3.9 +      "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
    3.10 +        File.bash_args(bash_args),
    3.11        cwd = cwd,
    3.12        env =
    3.13          Isabelle_System.library_path(env ++ env_options ++ env_tmp,
     4.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sat Oct 01 20:59:09 2016 +0200
     4.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Oct 01 23:05:25 2016 +0200
     4.3 @@ -98,6 +98,7 @@
     4.4    echo "  Options are:"
     4.5    echo "    -D NAME=X    set JVM system property"
     4.6    echo "    -J OPTION    add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
     4.7 +  echo "    -P CMD       JVM process command prefix (process policy)"
     4.8    echo "    -b           build only"
     4.9    echo "    -d DIR       include session directory"
    4.10    echo "    -f           fresh build"
    4.11 @@ -106,6 +107,7 @@
    4.12    echo "    -l NAME      logic session name"
    4.13    echo "    -m MODE      add print mode for output"
    4.14    echo "    -n           no build of session image on startup"
    4.15 +  echo "    -p CMD       ML process command prefix (process policy)"
    4.16    echo "    -s           system build mode for session image"
    4.17    echo
    4.18    echo "  Start jEdit with Isabelle plugin setup and open FILES"
    4.19 @@ -132,6 +134,8 @@
    4.20  
    4.21  BUILD_ONLY=false
    4.22  BUILD_JARS="jars"
    4.23 +JAVA_PROCESS_POLICY=""
    4.24 +ML_PROCESS_POLICY=""
    4.25  JEDIT_SESSION_DIRS=""
    4.26  JEDIT_LOGIC=""
    4.27  JEDIT_PRINT_MODE=""
    4.28 @@ -140,7 +144,7 @@
    4.29  function getoptions()
    4.30  {
    4.31    OPTIND=1
    4.32 -  while getopts "D:J:bd:fj:l:m:ns" OPT
    4.33 +  while getopts "D:J:P:bd:fj:l:m:np:s" OPT
    4.34    do
    4.35      case "$OPT" in
    4.36        D)
    4.37 @@ -149,6 +153,9 @@
    4.38        J)
    4.39          JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
    4.40          ;;
    4.41 +      P)
    4.42 +        JAVA_PROCESS_POLICY="$OPTARG"
    4.43 +        ;;
    4.44        b)
    4.45          BUILD_ONLY=true
    4.46          ;;
    4.47 @@ -178,6 +185,9 @@
    4.48        n)
    4.49          JEDIT_BUILD_MODE="none"
    4.50          ;;
    4.51 +      p)
    4.52 +        ML_PROCESS_POLICY="$OPTARG"
    4.53 +        ;;
    4.54        s)
    4.55          JEDIT_BUILD_MODE="system"
    4.56          ;;
    4.57 @@ -361,6 +371,7 @@
    4.58  if [ "$BUILD_ONLY" = false ]
    4.59  then
    4.60    export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    4.61 +  export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
    4.62    classpath "$JEDIT_HOME/dist/jedit.jar"
    4.63 -  exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
    4.64 +  exec $JAVA_PROCESS_POLICY isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
    4.65  fi
     5.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Sat Oct 01 20:59:09 2016 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Sat Oct 01 23:05:25 2016 +0200
     5.3 @@ -26,13 +26,19 @@
     5.4  
     5.5    def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
     5.6  
     5.7 +  def session_options(): Options =
     5.8 +    Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
     5.9 +      case "" => PIDE.options.value
    5.10 +      case s => PIDE.options.value.string("ML_process_policy") = s
    5.11 +    }
    5.12 +
    5.13    def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
    5.14  
    5.15    def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
    5.16    {
    5.17      val mode = session_build_mode()
    5.18  
    5.19 -    Build.build(options = PIDE.options.value, progress = progress,
    5.20 +    Build.build(options = session_options(), progress = progress,
    5.21        build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
    5.22        dirs = session_dirs(), sessions = List(session_name())).rc
    5.23    }
    5.24 @@ -42,8 +48,9 @@
    5.25      val modes =
    5.26        (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
    5.27         space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
    5.28 +
    5.29      PIDE.session.start(receiver =>
    5.30 -      Isabelle_Process(PIDE.options.value, logic = session_name(), dirs = session_dirs(),
    5.31 +      Isabelle_Process(options = session_options(), logic = session_name(), dirs = session_dirs(),
    5.32          modes = modes, receiver = receiver,
    5.33          store = Sessions.store(session_build_mode() == "system")))
    5.34    }