#1907 (Mar 6, 2023, 1:34:16 AM)

1. enforce rebuild of Isabelle/ML, after various changes to build database management; (detail / hgweb)
2. more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances; (detail / hgweb)
3. tuned output; (detail / hgweb)
4. clarified database content: store actual value instead of index; (detail / hgweb)
5. more robust: disallow override; (detail / hgweb)
6. tuned messages; (detail / hgweb)
7. more complete coverage of non-final Progress methods, notably for Server.Connection_Progress; (detail / hgweb)
8. clarified signature: manage "verbose" flag via "progress"; (detail / hgweb)
9. removed unused arguments: avoid ambiguity concerning progress/verbose; (detail / hgweb)
10. clarified protocol for "verbose" messages; (detail / hgweb)
11. clarified signature: manage "verbose" flag via "progress"; (detail / hgweb)
12. tuned; (detail / hgweb)
13. tuned; (detail / hgweb)
14. more operations; (detail / hgweb)
15. tuned signature; (detail / hgweb)
16. more robust: proper bound checks; (detail / hgweb)
17. enforce rebuild of Isabelle/ML, after various changes to build database management; (detail / hgweb)
18. clarified modules; (detail / hgweb)
19. clarified signature: manage "verbose" flag via "progress"; (detail / hgweb)
20. clarified treatment of "verbose" messages, e.g. Progress.theory();
    always store messages within database, with explicit "verbose" flag: client-side will decide about output; (detail / hgweb)
21. proper "val verbose" (amending 2e2b2bd6b2d2); (detail / hgweb)
22. tuned whitespace; (detail / hgweb)
23. more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress); (detail / hgweb)
24. support progress backed by database;
    moved Build_Progress.Context.progress/log to class Build_Process: database is available here; (detail / hgweb)
25. tuned; (detail / hgweb)
26. tuned messages; (detail / hgweb)
27. clarified signature: require just one "override def echo(message: Progress.Message): Unit"; (detail / hgweb)
28. tuned signature; (detail / hgweb)
29. tuned signature; (detail / hgweb)
30. clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()"; (detail / hgweb)
31. proper Output.writeln_text (with clean_yxml) for all instances of Progress.echo; (detail / hgweb)

Started by an SCM change

This run spent:

• 44 min waiting;
• 1 hr 53 min build duration;
• 2 hr 38 min total from scheduled to completion.