Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. keep original bottom-up order of proof forks, which potentially reduces thread congestion due to Proofterm.consolidate;
  3. consolidate proofs more simultaneously;
  4. more informative task_statistics;
  5. more informative task_statistics;
Changeset 66170:cad55bc7e37d by wenzelm:
merged
Changeset 66169:8cfa8c7ee1f6 by wenzelm:
keep original bottom-up order of proof forks, which potentially reduces thread congestion due to Proofterm.consolidate;
The file was modified src/Pure/Isar/toplevel.ML (diff)
Changeset 66168:fcd09fc36d7f by wenzelm:
consolidate proofs more simultaneously;
The file was modified src/HOL/SPARK/Tools/spark_vcs.ML (diff)
The file was modified src/Pure/Concurrent/lazy.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 66167:1bd268ab885c by wenzelm:
more informative task_statistics;
The file was modified src/Pure/Concurrent/cache.ML (diff)
The file was modified src/Pure/Concurrent/lazy.ML (diff)
The file was modified src/Pure/Isar/code.ML (diff)
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/document.ML (diff)
The file was modified src/Pure/Syntax/syntax.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 66166:c88d1c36c9c3 by wenzelm:
more informative task_statistics;
The file was modified src/Pure/Concurrent/event_timer.ML (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/task_queue.ML (diff)
The file was modified src/Pure/PIDE/active.ML (diff)
The file was modified src/Pure/System/invoke_scala.ML (diff)