Skip to content
Success

Changes

Summary

  1. prefer old-style import "=>";
  2. merged
  3. redundant (see also 3069da1743bc);
  4. removed obsolete table (see also 6acd1a2bd146);
  5. more robust init_database(); proper treatment of views, not tables (amending dd350a41594c);
  6. proper private_data.transaction_lock; prefer execute_batch_statement;
  7. clarified names;
  8. proper support for SSH;
  9. tuned signature;
  10. tuned imports;
  11. add module for faster scheduled builds;
  12. always use host database and make protected;
  13. read relative cpu from build log;
  14. prefer extensible next_node_info in build process over process_options in build engine (which needs the final node info anyway);
  15. added start date to build jobs, e.g., for build time estimation;
  16. added initial version of benchmark module, e.g., to compare performance of different hosts; added benchmark operation to build cluster;
  17. generalized node infos: allow addressing of numa node segments via relative cpus; add more node options and process policy options using taskset as alternative to NUMA for more fine-grained cpu controls (e.g., for cpus with heterogeneous cores in the same NUMA segment);
  18. add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
  19. added Range object to Host, e.g. to parse/unparse NUMA node ranges;
  20. defined statically known tables of Build_Log; read hostname from build logs, store in Session_Entry (e.g., to track hosts in distributed build);
Changeset 78855:6fdcd6c8c97a by wenzelm:
prefer old-style import "=>";
The file was modified src/Pure/General/bytes.scala (diff)
The file was modified src/Pure/General/mail.scala (diff)
Changeset 78854:35b406a5c105 by wenzelm:
merged
Changeset 78853:5826b24dd193 by wenzelm:
redundant (see also 3069da1743bc);
The file was modified src/Pure/Admin/build_log.scala (diff)
Changeset 78852:2700e4b484f7 by wenzelm:
removed obsolete table (see also 6acd1a2bd146);
The file was modified src/Pure/Admin/build_log.scala (diff)
Changeset 78851:db37cae970a6 by wenzelm:
more robust init_database();<br>proper treatment of views, not tables (amending dd350a41594c);
The file was modified src/Pure/Admin/build_log.scala (diff)
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 78850:3069da1743bc by wenzelm:
proper private_data.transaction_lock;<br>prefer execute_batch_statement;
The file was modified src/Pure/Admin/build_log.scala (diff)
Changeset 78849:df162316b6a7 by wenzelm:
clarified names;
The file was modified src/Pure/Admin/build_log.scala (diff)
The file was modified src/Pure/Admin/build_status.scala (diff)
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 78848:26a43785590b by wenzelm:
proper support for SSH;
The file was modified src/Pure/System/host.scala (diff)
Changeset 78847:3958180eaa72 by wenzelm:
tuned signature;
The file was modified src/Pure/System/host.scala (diff)
Changeset 78846:966aa081929f by wenzelm:
tuned imports;
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 78845:ff96d94957cb by fabian huch _huch@in.tum.de_:
add module for faster scheduled builds;
The file was addedsrc/Pure/Tools/build_schedule.scala
The file was modified etc/build.props (diff)
Changeset 78844:c7f436a63108 by fabian huch _huch@in.tum.de_:
always use host database and make protected;
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 78843:fc3ba0a1c82f by fabian huch _huch@in.tum.de_:
read relative cpu from build log;
The file was modified src/Pure/Admin/build_log.scala (diff)
Changeset 78842:eb572f7b6689 by fabian huch _huch@in.tum.de_:
prefer extensible next_node_info in build process over process_options in build engine (which needs the final node info anyway);
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 78841:7f61688d4e8d by fabian huch _huch@in.tum.de_:
added start date to build jobs, e.g., for build time estimation;
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 78840:4b528ca25573 by fabian huch _huch@in.tum.de_:
added initial version of benchmark module, e.g., to compare performance of different hosts;<br>added benchmark operation to build cluster;
The file was addedsrc/Pure/System/benchmark.scala
The file was modified etc/build.props (diff)
The file was modified src/Pure/System/host.scala (diff)
The file was modified src/Pure/System/isabelle_tool.scala (diff)
The file was modified src/Pure/Tools/build_cluster.scala (diff)
Changeset 78839:7799ec03b8bd by fabian huch _huch@in.tum.de_:
generalized node infos: allow addressing of numa node segments via relative cpus;<br>add more node options and process policy options using taskset as alternative to NUMA for more fine-grained cpu controls (e.g., for cpus with heterogeneous cores in the same NUMA segment);
The file was modified src/Pure/System/host.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 78838:4b014e6c1dfe by fabian huch _huch@in.tum.de_:
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
The file was modified src/Pure/Concurrent/isabelle_thread.scala (diff)
The file was modified src/Pure/System/host.scala (diff)
Changeset 78837:f97e23eaa628 by fabian huch _huch@in.tum.de_:
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
The file was modified src/Pure/System/host.scala (diff)
Changeset 78836:dd350a41594c by fabian huch _huch@in.tum.de_:
defined statically known tables of Build_Log;<br>read hostname from build logs, store in Session_Entry (e.g., to track hosts in distributed build);
The file was modified src/Pure/Admin/build_log.scala (diff)