#1987 (Jul 18, 2023, 12:50:10 AM)

1. merged (detail / hgweb)
2. more elementary transaction implementation (despite fda3f7a158b9 and 9da65bc75610); (detail / hgweb)
3. tuned signature; (detail / hgweb)
4. proper check (amending 234f2ff9afe6); (detail / hgweb)
5. more robust: exclude accidental nesting (synchronized block is re-entrant); (detail / hgweb)
6. clarified errors; (detail / hgweb)
7. removed junk (amending f8e3b228670c); (detail / hgweb)
8. tuned output; (detail / hgweb)
9. reuse SSH.Server connection for database server; (detail / hgweb)
10. tuned source structure; (detail / hgweb)
11. clarified check: uniform session_info_exists; (detail / hgweb)
12. more complete check; (detail / hgweb)
13. clarified signature: more specific exists_table --- avoid retrieving full list beforehand; (detail / hgweb)
14. reuse database_server connection; (detail / hgweb)
15. more informative trace; (detail / hgweb)
16. reuse SSH.Server connection database server; (detail / hgweb)
17. tuned output; (detail / hgweb)
18. make double-sure that this is a transaction context, notably for LOCK TABLE; (detail / hgweb)
19. more robust Java/Scala multithreading: transaction is always connection.synchronized; (detail / hgweb)
20. clarified signature: proper Scala function for command-line tool; (detail / hgweb)
21. tuned signature; (detail / hgweb)
22. clarified signature: more operations; (detail / hgweb)
23. more standard time unit; (detail / hgweb)
24. clarified options; (detail / hgweb)
25. tuned output; (detail / hgweb)
26. global transaction_count; (detail / hgweb)
27. tuned output; (detail / hgweb)
28. tuned output; (detail / hgweb)
29. prefer asynchronous operations: reduce time spent within synchronized_database("Build_Process.start_job"); (detail / hgweb)
30. clarified isabelle.transaction_log: support time_min (in ms); (detail / hgweb)
31. more operations; (detail / hgweb)
32. more informative trace; (detail / hgweb)
33. support trace of transaction_lock via property "isabelle.transaction_log"; (detail / hgweb)
34. proper db.transaction_lock instead of adhoc clone (amending 2df0f3604a67); (detail / hgweb)
35. tuned; (detail / hgweb)
36. proper close() operation; (detail / hgweb)
37. tuned comments; (detail / hgweb)
38. more robust: avoid nested transactions (on disjoint tables); (detail / hgweb)
39. potentially more robust: long-running operation only for build master, not workers; (detail / hgweb)
40. less ambitions transactions (amending 3f3dcf9f53f1): TRANSACTION_SERIALIZABLE may lead to spurious rollback exceptions; (detail / hgweb)
41. clarified signature: more operations; (detail / hgweb)
42. clarified signature: more operations; (detail / hgweb)
43. clarified signature; (detail / hgweb)
44. clarified signature; (detail / hgweb)
45. clarified signature: follow Store.open_database; (detail / hgweb)
46. tuned; (detail / hgweb)
47. clarified signature; (detail / hgweb)
48. clarified signature: more uniform SSH.Port_Forwarding; (detail / hgweb)
49. tuned signature; (detail / hgweb)

Started by an SCM change

This run spent:

• 8.9 sec waiting;
• 2 hr 4 min build duration;
• 2 hr 4 min total from scheduled to completion.