Skip to content
[Jenkins]Jenkins
log in
Aborted

Changes

Summary

  1. less ambitious parallelism, notably for threads=2;
  2. more informative error, notably for missing executable;
  3. tuned signature;
  4. clarified future scheduling parameters, with support for parallel_limit;
  5. record total number of tasks;
Changeset 68133:f6a22490cca8 by wenzelm:
less ambitious parallelism, notably for threads=2;
The file was modified src/HOL/ROOT (diff)
Changeset 68132:2a5ae592eafb by wenzelm:
more informative error, notably for missing executable;
The file was modified src/Pure/Thy/present.scala (diff)
Changeset 68131:62a3294edda3 by wenzelm:
tuned signature;
The file was modified src/Pure/General/exn.scala (diff)
The file was modified src/Pure/ROOT.scala (diff)
Changeset 68130:6fb85346cb79 by wenzelm:
clarified future scheduling parameters, with support for parallel_limit;
The file was modified etc/options (diff)
The file was modified src/Pure/Concurrent/future.ML (diff)
The file was modified src/Pure/Concurrent/lazy.ML (diff)
The file was modified src/Pure/Concurrent/multithreading.ML (diff)
The file was modified src/Pure/Concurrent/par_list.ML (diff)
The file was modified src/Pure/Isar/proof.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/ML/ml_compiler.ML (diff)
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/execution.ML (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/goal.ML (diff)
The file was modified src/Pure/par_tactical.ML (diff)
Changeset 68129:b73678836f8e by wenzelm:
record total number of tasks;
The file was modified src/Pure/Concurrent/future.ML (diff)
The file was modified src/Pure/Concurrent/task_queue.ML (diff)
The file was modified src/Pure/ML/ml_statistics.scala (diff)