Build #65 (Aug 15, 2021, 12:14:00 AM)

1. provide bash_process server for Isabelle/ML and other external programs;
   clarified signature for Bash.params; (detail)
2. clarified signature; (detail)
3. clarified signature; (detail)
4. proper prover_options for batch-build; (detail)
5. clarified signature;
   clarified errors; (detail)
6. clarified signature: more options for bash_process; (detail)
7. tuned signature; (detail)
8. clarified signature; (detail)
9. clarified signature; (detail)
10. follow phabricator 2021 Week 26;
    follow arcanist 2021 Week 23; (detail)
11. tuned signature; (detail)
12. tuned; (detail)
13. clarified signature; (detail)
14. clarified signature; (detail)
15. unused; (detail)
16. clarified signature; (detail)
17. merged (detail)
18. clarified modules; (detail)
19. type classes for XML data representation; (detail)
20. tuned signature; (detail)
21. clarified types: prefer Isabelle byte strings; (detail)
22. merged (detail)
23. added option labels to Mirabelle actions (detail)
24. more operations: dest binders; (detail)
25. clarified abstract and concrete boolean algebras (detail)
26. antiquotation for bundles (detail)
27. prefer persistent hash code for cachable items (see also 72b13af7f266); (detail)
28. merged (detail)
29. more operations: record overall exported entities; (detail)
30. merged (detail)
31. added dummy_fof prover to Sledgehammer (detail)
32. fixed malconfigured option output_dir in mirabelle (detail)
33. merged (detail)
34. clarified export of formal entities: name space info is always present, but content depends on option "export_theory"; (detail)
35. proper name space "kind": this is a formal name, not comment; (detail)
36. more uniform signatures in ML and Scala; (detail)
37. merged (detail)
38. fixed typo (detail)
39. added dummy_thf prover to Sledgehammer (detail)
40. simplified hierarchy of type classes for bit operations (detail)
41. obsolete (detail)
42. more operations, notably free and bound variables as in Isabelle/Pure; (detail)
43. more operations on types and terms;
    abstract syntax operations for Pure and HOL; (detail)
44. clarified jEdit java sources; (detail)
45. clarified build.gradle: "compile" stopped working in gradle 6.x / 7.x for unknown reasons; (detail)
46. removed junk; (detail)
47. moved theory Bit_Operations into Main corpus (detail)
48. more operations; (detail)
49. clarified signature; (detail)
50. clarified signature; (detail)
51. organize syntax for word operations in bundles (detail)
52. support for Lazy.Text; (detail)
53. prefer compact Isabelle.Bytes; (detail)
54. clarified signature; (detail)
55. clarified signature --- more operations; (detail)
56. tuned; (detail)
57. clarified order of modules; (detail)
58. more operations; (detail)
59. tuned; (detail)

1. metadata update for MFMC_Countable (detail)
2. derive rel_pmf characterization from bounded and unbounded MFMC theorem (detail)
3. merged (detail)
4. drop boundedness requirement for the sink (detail)
5. avoid global tmp file: pointless due to implicit theory export; (detail)
6. repaired syntax (detail)
7. tuned signature, following Isabelle/d030b988d470; (detail)
8. generalized gt_rat_sign_change to square-free polynomials (detail)
9. minor updates to bibliography (detail)
10. clarified signature; (detail)
11. clarified abstract and concrete boolean algebras (detail)
12. antiquotation for bundles (detail)
13. simplified hierarchy of type classes for bit operations (detail)
14. restored executable conversions (detail)
15. dropped junk (detail)
16. moved theory Bit_Operations into Main corpus (detail)
17. organize syntax for word operations in bundles (detail)
18. more systematic approach for instantiation (detail)
19. avoid seemingly unused transfer rules (detail)

Started by timer

This run spent:

• 12 ms waiting;
• 7 hr 13 min build duration;
• 7 hr 13 min total from scheduled to completion.