Skip to content
Success

Changes

Summary

  1. more thorough cleanup;
  2. tuned;
  3. tuned: more robust Scala syntax;
  4. merged
  5. no compression for database server: let PostgreSQL/TOAST do the job;
  6. prefer Zstd compression, notably for database exports;
  7. tuned: avoid redundant copy of potentially large array;
  8. merged
  9. tuned proof
Changeset 76367:3ace8ac64f20 by wenzelm:
more thorough cleanup;
The file was modified src/Pure/Admin/build_history.scala (diff)
Changeset 76366:640ab184efb4 by wenzelm:
tuned;
The file was modified src/Pure/Admin/build_history.scala (diff)
Changeset 76365:24e951a8a318 by wenzelm:
tuned: more robust Scala syntax;
The file was modified src/Pure/Admin/build_history.scala (diff)
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 76364:2c0f252fb11c by wenzelm:
merged
Changeset 76363:f7174238b5e3 by wenzelm:
no compression for database server: let PostgreSQL/TOAST do the job;
The file was modified src/Pure/General/sql.scala (diff)
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 76362:1928405a409b by wenzelm:
prefer Zstd compression, notably for database exports;
The file was modified src/Pure/General/compress.scala (diff)
Changeset 76361:3b9f36ef7365 by wenzelm:
tuned: avoid redundant copy of potentially large array;
The file was modified src/Pure/General/bytes.scala (diff)
Changeset 76360:2b204e11141c by desharna:
merged
Changeset 76359:f7002e5b15bb by desharna:
tuned proof
The file was modified src/HOL/Library/Multiset.thy (diff)