Build #212 (Sep 16, 2019 6:03:13 PM)

1. tuned (detail / hgweb)
2. merged (detail / hgweb)
3. tuned; (detail / hgweb)
4. clarified theory status; (detail / hgweb)
5. dump ZF in parallel to HOL Main; (detail / hgweb)
6. tuned messages; (detail / hgweb)
7. more ambitious options (again); (detail / hgweb)
8. more ambitious options (again, after 93aa546ffbac); (detail / hgweb)
9. tuned signature; (detail / hgweb)
10. proper clean_theories wrt. dynamic dep_graph; (detail / hgweb)
11. tuned signature; (detail / hgweb)
12. potentially more robust: read under lock if not yet set; (detail / hgweb)
13. tuned; (detail / hgweb)
14. New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours (detail / hgweb)
15. session directories need to exist; (detail / hgweb)
16. clarified signature: eliminated unused option; (detail / hgweb)
17. merged (detail / hgweb)
18. importation fix (detail / hgweb)
19. merged (detail / hgweb)
20. new material on Analysis, plus some rearrangements (detail / hgweb)
21. eliminated pointless theory graph (reverting parts of a56eab490f4e): it caused problems with loaded vs. non-loaded node names, e.g. for theory Pure (see also 29bb1ebb188f); (detail / hgweb)
22. discontinued obsolete "isabelle imports" and all_known data; (detail / hgweb)
23. avoid duplicate directories wrt. synthetic session; (detail / hgweb)
24. disallow accidental duplicates within the same session specification -- proper total match; (detail / hgweb)
25. find theory files via session structure: much faster Prover IDE startup; (detail / hgweb)
26. find theory node name via session directories; (detail / hgweb)
27. disallow overlapping session directories; (detail / hgweb)
28. tidied up some massive ugliness (detail / hgweb)
29. clarified messages; (detail / hgweb)
30. clarified syntax: 'directories' and 'theories' belong together; (detail / hgweb)
31. more documentation; (detail / hgweb)
32. check session directories; (detail / hgweb)
33. declare session directories; (detail / hgweb)
34. clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories); (detail / hgweb)
35. theory_name based on session_directories: no need for expensive all_known; (detail / hgweb)
36. clarified session_directories: relative to session_path, with overlapping information; (detail / hgweb)
37. clarified signature: retain global session information, unaffected by later restriction; (detail / hgweb)
38. disable fragile options for now; (detail / hgweb)
39. avoid overlapping session directories; (detail / hgweb)
40. support for explicit session directories; (detail / hgweb)
41. obsolete (see 94442fce40a5); (detail / hgweb)
42. optional trace output; (detail / hgweb)
43. prefer commands_accepted: fewer protocol messages; (detail / hgweb)
44. prefer define_commands_bulk: fewer protocol messages; (detail / hgweb)
45. clarified signature; (detail / hgweb)
46. tuned signature -- prefer bulk messages; (detail / hgweb)
47. tuned signature; (detail / hgweb)
48. proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe); (detail / hgweb)
49. more robust; (detail / hgweb)
50. unused; (detail / hgweb)
51. proper finished_theory status for result; (detail / hgweb)
52. more central checkpoint; (detail / hgweb)
53. disable share_common_data for now (amending 0f8742b5a9e8) -- potentially more robust; (detail / hgweb)
54. merged (detail / hgweb)
55. load theories in stages, to reduce ML heap requirements; (detail / hgweb)
56. more complete graph; (detail / hgweb)
57. tuned messages; (detail / hgweb)
58. tuned signature; (detail / hgweb)
59. clarified signature; (detail / hgweb)
60. tuned important special case; (detail / hgweb)
61. tuned signature; (detail / hgweb)
62. more dump_checkpoints; (detail / hgweb)
63. clarified signature; (detail / hgweb)
64. clarified state variable: avoid extra mutability via Promise; (detail / hgweb)
65. Removal of the redundant ancestor Continuous_Extension (detail / hgweb)
66. Half of Brouwer_Fixpoint split off to form a separate theory: Retracts. (detail / hgweb)
67. Theory Derivative no longer depends on Path_Connected (detail / hgweb)
68. more explicit type Dump.Session, with context information; (detail / hgweb)
69. proper orientation; (detail / hgweb)
70. clarified signature: prefer operations without position; (detail / hgweb)
71. prefer Theory_Ordering theory names are unique (due to proper session context); (detail / hgweb)
72. clarified signature: full dependency graph; (detail / hgweb)
73. merged (detail / hgweb)
74. more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML; (detail / hgweb)
75. tuned signature; (detail / hgweb)
76. merged (detail / hgweb)
77. more rules for ordered real vector spaces (detail / hgweb)
78. simplified proofs (detail / hgweb)
79. simplified setup (detail / hgweb)
80. tuned proof (detail / hgweb)
81. merged (detail / hgweb)
82. enable share_common_data for "isabelle dump" and its derivatives (e.g. "isabelle mmt_import"): this has the potential to reduce ML heap size considerably, after initial command definitions; (detail / hgweb)
83. support for share_common_data after define_command and before actual update: this affects string particles of command tokens; (detail / hgweb)
84. more scalable -- less ML heap requirements; (detail / hgweb)
85. tuned whitespace; (detail / hgweb)
86. Integrate locale activation fallback diagnostics with 'trace_locales'. (detail / hgweb)

Started by an SCM change

This run spent:

• 8.9 sec waiting;
• 1 hr 22 min build duration;
• 1 hr 22 min total from scheduled to completion.