Started 1 day 8 hr ago
Took 2 hr 57 min on workermtahpc

Build #472 (Jun 21, 2021 7:21:09 PM)

Changes
  1. feat(Tools/Spec_Check) major upgrade

    term generators, lazy shrinking, detailled test output, pretty printing, modularisation, bug fixes (detail / hgweb)
  2. tuned --- following hints by IntelliJ; (detail / hgweb)
  3. tuned signature; (detail / hgweb)
  4. tuned; (detail / hgweb)
  5. tuned; (detail / hgweb)
  6. tuned signature; (detail / hgweb)
  7. tuned; (detail / hgweb)
  8. tuned signature (see 2d6a489adb01); (detail / hgweb)
  9. added support for TFX's and THF's $ite to Sledgehammer (detail / hgweb)
  10. tuned Mirabelle documentation (detail / hgweb)
  11. shortened long lines (detail / hgweb)
  12. fixed typos (detail / hgweb)
  13. updated Mirabelle documentation (detail / hgweb)
  14. changed Mirabelle's filter to use short theory names (detail / hgweb)
  15. more lemmas (detail / hgweb)
  16. added support for unbounded max calls to Mirabelle (detail / hgweb)
  17. added warnings when defining unamed or redefining Mirabelle action (detail / hgweb)
  18. tuned whitespace; (detail / hgweb)
  19. tuned Mirabelle (detail / hgweb)
  20. merged (detail / hgweb)
  21. refactored Mirabelle to produce output in real time (detail / hgweb)
  22. global interpretation into nested targets (detail / hgweb)
  23. more succint interfaces (detail / hgweb)
  24. merged (detail / hgweb)
  25. tuned messages; (detail / hgweb)
  26. NEWS; (detail / hgweb)
  27. proper profiling within command execution: messages require PIDE id; (detail / hgweb)
  28. more systematic treatment of profiling mode; (detail / hgweb)
  29. tuned message; (detail / hgweb)
  30. prefer less intrusive tracing message; (detail / hgweb)
  31. clarified documentation: tracing messages are not shown here; (detail / hgweb)
  32. add missing file; (detail / hgweb)
  33. more formal ML profiling messages; (detail / hgweb)
  34. clarified modules; (detail / hgweb)
  35. Lukas Steven's more general fold foctions for maps (detail / hgweb)
  36. follow Phabricator update 2021 Week 23; (detail / hgweb)
  37. tuned; (detail / hgweb)
  38. more formal theory and session names;
    tuned whitespace; (detail / hgweb)
  39. proper NEWS after Isabelle2021; (detail / hgweb)
  40. updated descriptions; (detail / hgweb)
  41. allow system option short form NAME for NAME=true for type string, not just bool;
    support short system options "-o document" and "-o system_log"; (detail / hgweb)
  42. tuned; (detail / hgweb)
  43. more robust within session "HOL"; (detail / hgweb)
  44. merged (detail / hgweb)
  45. suppress theories from other sessions, unless explicitly specified via mirabelle_theories; (detail / hgweb)
  46. clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT); (detail / hgweb)
  47. refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories; (detail / hgweb)
  48. tuned; (detail / hgweb)
  49. more uniform schedule_theories, notably for "present" and "commit" phase after loading; (detail / hgweb)
  50. tuned; (detail / hgweb)
  51. moved more legacy to AFP (detail / hgweb)
  52. clarified modules; (detail / hgweb)
  53. clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys); (detail / hgweb)
  54. tuned; (detail / hgweb)
  55. more thorough update of required files (amending 1529c3eb6bac); (detail / hgweb)
  56. clarified examples; (detail / hgweb)
  57. tuned proofs; (detail / hgweb)
  58. misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a); (detail / hgweb)
  59. tuned --- reduced source complexity; (detail / hgweb)
  60. proper usage (amending f7ea394490f5); (detail / hgweb)
  61. merged, resolving minor conflict; (detail / hgweb)
  62. allow build session setup, e.g. for protocol handlers; (detail / hgweb)
  63. unused; (detail / hgweb)
  64. tuned --- potentially more robust (e.g. session.phase_changed vs. isabelle_process.terminated); (detail / hgweb)
  65. clarified signature; (detail / hgweb)
  66. removed pointless option (see 3d0952893db8); (detail / hgweb)
  67. tuned --- avoid redundant future tasks from already loaded theories; (detail / hgweb)
  68. no comment --- topological order appears to be fine since 04-Mar-2013; (detail / hgweb)
  69. more predictable sequential presentation (2f9877db82a1), without somewhat pointless result_ord (e7fab0b5dbe7); (detail / hgweb)
  70. moved stride option from sledgehammer action to main mirabelle (detail / hgweb)
  71. merged (detail / hgweb)
  72. new lemmas mostly about paths (detail / hgweb)
  73. lexorders the locale way (detail / hgweb)

Started by an SCM change

This run spent:

  • 7.5 sec waiting;
  • 2 hr 57 min build duration;
  • 2 hr 58 min total from scheduled to completion.
Revision: 6c6938da7678ff0d482d2c56fe6d61be1ba23bf1
Failed entries: