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

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.

• Regex_Equivalence
• PLM