Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. back to compression in Isabelle/Scala (in contrast to f7174238b5e3), e.g. relevant for old_command_timings_blob, but also for prospective heaps;
  3. vacuum everything in the database;
  4. tuned;
  5. proper vacuum of session_info tables: only once per build process;
  6. tuned signature;
  7. more thorough database checks;
  8. more thorough treatment of build prefs, guarded by system option "build_through": avoid accidental rebuild of HOL etc.;
  9. clarified build options;
  10. clarified ML option vs. Scala option (see also caa182bdab7a);
  11. merge conflict
  12. unified function update and map update syntaxes
Changeset 77682:a76f49a03448 by wenzelm:
merged
Changeset 77681:1db732e6c3d2 by wenzelm:
back to compression in Isabelle/Scala (in contrast to f7174238b5e3), e.g. relevant for old_command_timings_blob, but also for prospective heaps;
The file was modified src/Pure/General/sql.scala (diff)
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 77680:bc8e2fec9650 by wenzelm:
vacuum everything in the database;
The file was modified src/Pure/Admin/isabelle_devel.scala (diff)
Changeset 77679:e92000492895 by wenzelm:
tuned;
The file was modified src/Pure/Admin/build_log.scala (diff)
Changeset 77678:e7d8e990d378 by wenzelm:
proper vacuum of session_info tables: only once per build process;
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 77677:daaaf59375e9 by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 77676:649708f75c6f by wenzelm:
more thorough database checks;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 77675:9e5f8f6e58a0 by wenzelm:
more thorough treatment of build prefs, guarded by system option "build_through": avoid accidental rebuild of HOL etc.;
The file was modified NEWS (diff)
The file was modified etc/options (diff)
The file was modified src/Pure/General/sha1.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 77674:488a48453d74 by wenzelm:
clarified build options;
The file was modified NEWS (diff)
The file was modified etc/options (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 77673:08fcde7c55c0 by wenzelm:
clarified ML option vs. Scala option (see also caa182bdab7a);
The file was modified src/Pure/ML/ml_compiler.ML (diff)
Changeset 77672:34176328fc67 by nipkow:
merge conflict
Changeset 77671:8a6a79ed5a83 by nipkow:
unified function update and map update syntaxes
The file was modified NEWS (diff)
The file was modified src/HOL/Map.thy (diff)