#1905 (Mar 3, 2023, 12:50:10 AM)

1. merged (detail / hgweb)
2. clarified execution context: main work happens within Future.thread;
   clarified signature: only one "join" operation; (detail / hgweb)
3. clarified timeout: closer to actual process; (detail / hgweb)
4. tuned names; (detail / hgweb)
5. clarified names; (detail / hgweb)
6. tuned, following ML_Statistics.monitor; (detail / hgweb)
7. unused (see also 0cebcbeac4c7); (detail / hgweb)
8. tuned; (detail / hgweb)
9. tuned; (detail / hgweb)
10. tuned comments; (detail / hgweb)
11. clarified modules;
    tuned signature;
    tuned comments; (detail / hgweb)
12. clarified modules; (detail / hgweb)
13. clarified modules; (detail / hgweb)
14. clarified signature; (detail / hgweb)
15. clarified modules; (detail / hgweb)
16. clarified modules; (detail / hgweb)
17. tuned; (detail / hgweb)
18. clarified modules; (detail / hgweb)
19. clarified modules; (detail / hgweb)
20. tuned; (detail / hgweb)
21. more robust: proper synchronization of transition from next_job to start_session; (detail / hgweb)
22. more thorough synchronized_database for internal *and* external state; (detail / hgweb)
23. simplified startup under "locked" condition (in contrast to f7e413e8d269); (detail / hgweb)
24. more explicit session name, in anticipation of variants like "session.document", "session.browser_info"; (detail / hgweb)
25. tuned signature; (detail / hgweb)
26. tuned signature; (detail / hgweb)
27. tuned signature; (detail / hgweb)
28. tuned signature: support general Build_Job instances; (detail / hgweb)
29. tuned signature; (detail / hgweb)
30. clarified signature: prefer static data; (detail / hgweb)
31. tuned signature; (detail / hgweb)
32. identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd); (detail / hgweb)
33. tuned signature; (detail / hgweb)
34. tuned signature; (detail / hgweb)
35. tuned signature; (detail / hgweb)
36. tuned; (detail / hgweb)
37. unused; (detail / hgweb)
38. tuned signature (again); (detail / hgweb)
39. tuned; (detail / hgweb)
40. tuned; (detail / hgweb)
41. proper deps from build_graph, not imports_graph (amending 0c704aba71e3); (detail / hgweb)
42. misc tuning: more direct access to ancestors, without build_graph; (detail / hgweb)
43. tuned signature (again); (detail / hgweb)
44. clarified signature: reduce explicit access to static Sessions.Structure; (detail / hgweb)
45. tuned signature; (detail / hgweb)
46. clarified modules (again); (detail / hgweb)
47. tuned; (detail / hgweb)
48. tuned signature; (detail / hgweb)
49. avoid premature Properties.uncompress: allow blob to be stored in another database; (detail / hgweb)
50. more robust: synchronized access to database; (detail / hgweb)
51. clarified signature: do not expose global state to object-oriented variants; (detail / hgweb)
52. tuned comments and outline; (detail / hgweb)
53. merged (detail / hgweb)
54. Imported a theorem about Infinite_Sum. Importing this theory a bit earlier is causing syntactic ambiguities with Infinite_Set_Sum however; no_notation needed (detail / hgweb)
55. A little bit more tidying up (detail / hgweb)

Started by an SCM change

This run spent:

• 9.1 sec waiting;
• 1 hr 52 min build duration;
• 1 hr 53 min total from scheduled to completion.