Skip to content
Success

Changes

Summary

  1. more options for performance tuning;
  2. more operations;
  3. support for management of build cluster;
  4. clarified modules;
  5. renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
  6. more conservative build_delay (despite 9600720071e6): avoid exessive build_database operations, notably via ssh;
  7. proper running limit, based on this worker process; prefer bulk jobs: much faster cancellation;
  8. more robust: implicit locking of tables in standard order;
  9. more uniform guard (!exists_table(table)): avoid "ALTER TABLE" on already existing table, which could lead to deadlocks if this is presently locked;
  10. removed unused "create_index": implicit index from primary_key is usually sufficient;
  11. clarified "vacuum" (again, reverting 0bd366fad888);
  12. clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888);
  13. update for release;
Changeset 78400:63d55ba90a9f by wenzelm:
more options for performance tuning;
The file was modified etc/options (diff)
The file was modified src/Pure/Admin/build_log.scala (diff)
The file was modified src/Pure/General/sql.scala (diff)
The file was modified src/Pure/Thy/store.scala (diff)
Changeset 78399:facf1a324807 by wenzelm:
more operations;
The file was modified src/Pure/Tools/build_cluster.scala (diff)
Changeset 78398:ea5adf7acc2d by wenzelm:
support for management of build cluster;
The file was addedsrc/Pure/Tools/build_cluster.scala
The file was modified etc/build.props (diff)
Changeset 78397:c8df7abb8707 by wenzelm:
clarified modules;
The file was modified src/Pure/Tools/server.scala (diff)
Changeset 78396:7853d9072d1b by wenzelm:
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
The file was modified src/Pure/ML/ml_heap.scala (diff)
The file was modified src/Pure/System/host.scala (diff)
The file was modified src/Pure/System/progress.scala (diff)
The file was modified src/Pure/Thy/document_build.scala (diff)
The file was modified src/Pure/Thy/export.scala (diff)
The file was modified src/Pure/Thy/store.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
The file was modified src/Pure/Tools/server.scala (diff)
Changeset 78395:c39819e3adc5 by wenzelm:
more conservative build_delay (despite 9600720071e6): avoid exessive build_database operations, notably via ssh;
The file was modified etc/options (diff)
Changeset 78394:761d12b043d0 by wenzelm:
proper running limit, based on this worker process;<br>prefer bulk jobs: much faster cancellation;
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 78393:a2d22d519bf2 by wenzelm:
more robust: implicit locking of tables in standard order;
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 78392:27c2fa1db6ed by wenzelm:
more uniform guard (!exists_table(table)): avoid &quot;ALTER TABLE&quot; on already existing table, which could lead to deadlocks if this is presently locked;
The file was modified src/Pure/General/sql.scala (diff)
Changeset 78391:e47233dbeab7 by wenzelm:
removed unused &quot;create_index&quot;: implicit index from primary_key is usually sufficient;
The file was modified src/Pure/General/sql.scala (diff)
Changeset 78390:a84f8fca0833 by wenzelm:
clarified &quot;vacuum&quot; (again, reverting 0bd366fad888);
The file was modified src/Pure/General/sql.scala (diff)
Changeset 78389:41e8ae87184d by wenzelm:
clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888);
The file was modified src/Pure/Admin/build_log.scala (diff)
The file was modified src/Pure/General/sql.scala (diff)
The file was modified src/Pure/System/progress.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 78388:475600ef98b8 by wenzelm:
update for release;
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)