Started 6 days 8 hr ago
Took 1 hr 22 min on workermtahpc

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

Changes
  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.
Revision: 3e11f35496b3fdff432f3dabcc4e1ef82582a8d1