Summary
- more thorough cleanup;
- tuned;
- tuned: more robust Scala syntax;
- merged
- no compression for database server: let PostgreSQL/TOAST do the job;
- prefer Zstd compression, notably for database exports;
- tuned: avoid redundant copy of potentially large array;
- merged
- tuned proof
The file was modified | src/Pure/Admin/build_history.scala (diff) |
The file was modified | src/Pure/Admin/build_history.scala (diff) |
The file was modified | src/Pure/Admin/build_history.scala (diff) |
The file was modified | src/Pure/Admin/isabelle_cronjob.scala (diff) |
The file was modified | src/Pure/General/sql.scala (diff) |
The file was modified | src/Pure/Thy/export.scala (diff) |
The file was modified | src/Pure/General/compress.scala (diff) |
The file was modified | src/Pure/General/bytes.scala (diff) |
The file was modified | src/HOL/Library/Multiset.thy (diff) |