Build #76 (Oct 31, 2021, 12:14:00 AM)

1. tuned proofs -- avoid z3, which is unavailable on arm64-linux; (detail)
2. tuned; (detail)
3. test version of prespective polyml-5.9; (detail)
4. clarified antiquotations; (detail)
5. updated for pre-5.9 testing; (detail)
6. clarified antiquotations; (detail)
7. clarified antiquotations; (detail)
8. clarified antiquotations; (detail)
9. more robust subgoal addressing; (detail)
10. proper subgoal addressing; (detail)
11. clarified antiquotations; (detail)
12. recursive find_eq, not find_dist; (detail)
13. misc tuning and clarification; (detail)
14. clarified antiquotations; (detail)
15. order_tac: prevent potential bug, improve perf and tracing
    
    - We need to be careful when the order operators contain schematic variables, e.g. <= = ccw' ?p. (detail)
16. misc tuning and clarification; (detail)
17. clarified antiquotations; (detail)
18. clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta; (detail)
19. clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta; (detail)
20. avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570); (detail)
21. added Thm.instantiate_beta;
    tuned; (detail)
22. moved generic implementation into HOL-Main (detail)
23. tuned; (detail)
24. tuned; (detail)
25. clarified antiquotations; (detail)
26. clarified antiquotations; (detail)
27. discontinued somewhat pointless antiquotations; (detail)
28. NEWS; (detail)
29. clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic; (detail)
30. clarified antiquotations; (detail)
31. clarified antiquotations; (detail)
32. clarified antiquotations; (detail)
33. clarified antiquotations; (detail)
34. support for "lemma";
    support for "schematic" mode;
    clarified error position; (detail)
35. tuned; (detail)
36. local fixes for "lemma" antiquotation; (detail)
37. clarified signature; (detail)
38. tuned; (detail)
39. clarified keywords: major take precedence for commands, but not used for antiquotations;
    clarified modules; (detail)
40. tuned modules; (detail)
41. more antiquotations; (detail)
42. moved a theorem to a sensible place (detail)
43. merged (detail)
44. tuned, continuing e955964d89cb; (detail)
45. avoid waste of resources due to dynamic simpset (amending 45c09620f726); (detail)
46. fix latex (detail)
47. clarified modules; (detail)
48. more generic bit/word lemmas for distribution (detail)
49. merged (detail)
50. Added / moved some simple set-theoretic lemmas (detail)
51. more CONTRIBUTORS and NEWS; (detail)
52. cleanup; add Apple reference (detail)
53. refine interface (detail)
54. generalized component lookup for syntax and distinctness proofs. added some tracing. (detail)
55. merged (detail)
56. tuned; (detail)
57. more antiquotations; (detail)
58. more antiquotations; (detail)
59. more robust: genuinely free variables need to be instantiated; (detail)
60. tuned comments; (detail)
61. clarified errors; (detail)
62. tuned; (detail)
63. clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs; (detail)
64. tuned; (detail)
65. clarified signature -- avoid clones; (detail)
66. Refinement of partitions (detail)
67. avoid persistence of static context: instantiation arguments should provide proper dynamic context; (detail)
68. more antiquotations; (detail)
69. more markup; (detail)
70. clarified name, syntax, messages; (detail)
71. more antiquotations; (detail)
72. more control symbols; (detail)
73. tuned signature; (detail)
74. ML antiquotations to instantiate types/terms/props; (detail)
75. tuned; (detail)
76. clarified modules; (detail)
77. clarified modules; (detail)
78. clarified modules; (detail)
79. discontinued obsolete "val extend = I" for data slots; (detail)
80. clarified modules; (detail)
81. clarified modules; (detail)
82. clarified signature; (detail)
83. tuned; (detail)
84. clarified keywords and reports; (detail)
85. clarified signature; (detail)
86. merged (detail)
87. proper veriT --max-time option (detail)
88. refactored tptp_builtins in Sledgehammer (detail)
89. merged (detail)
90. tuned ML --- clarified use of context;
    tuned message; (detail)
91. tuned --- fewer clones; (detail)
92. updated to jEdit plugin Highlight 2.5; (detail)
93. proper tactic combinator; (detail)
94. proper file headers; (detail)
95. clarified context;
    clarified modules; (detail)
96. more accurate treatment of context; (detail)
97. updated email address (detail)
98. removed some 'private' modifiers from HOL-Computational_Algebra (detail)
99. merged (detail)
100. merged (detail)
101. more robust Variable.revert_bounds (see also b12f2cef3ee5); (detail)
102. more accurate treatment of context; (detail)
103. tuned -- proper names/scopes for contexts; (detail)
104. clarified context; (detail)
105. clarified context; (detail)
106. tuned; (detail)
107. unused; (detail)
108. more accurate treatment of context;
     declare generated bounds for the sake of recdef, which has variables leaking from local context; (detail)
109. isabelle regenerate_cooper; (detail)
110. revert bbfed17243af, breaks HOL-Proofs extraction; (detail)
111. tuned; (detail)
112. tuned; (detail)
113. proper p' instead of p (amending 52c7c42e7e27); (detail)
114. proper context for Goal.prove_internal; (detail)
115. discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
     Simplifier and equational conversions demand a proper proof context; (detail)
116. more accurate treatment of context, notably for nested Goal.proof / SUBPROOF; (detail)
117. tuned; (detail)
118. tuned; (detail)
119. tuned; (detail)
120. spelling; (detail)
121. clarified context; (detail)
122. clarified signature; (detail)
123. tuned Vampire configuration to use TFX in Sledgehammer (detail)

1. updated metadata for Count_Complex_Roots (detail)
2. corrected the timeout for CZH_Universal_Constructions (detail)
3. CZH: further results about comma categories and Kan extensions, a variety of other minor amendments (detail)
4. more generic bit/word lemmas for distribution (detail)
5. Fixing a name clash between two different "restrict" operators (detail)
6. Merged (detail)
7. solved the roots-on-the-border problem (detail)
8. split Count_Complex_Roots (detail)
9. more realistic timeout; (detail)
10. clarified signature, according to Isabelle/ccf599864beb; (detail)
11. back to dedicated separate shift operations for infix syntax;
    more default simp rules on closed numeric expressions (detail)
12. modify JinjaDCI (detail)
13. modify JinjaDCI (detail)
14. Merged. (detail)
15. Various tuning that for some reason didn't get merged from my master branch. (detail)
16. A spot of polishing (detail)
17. Merged. (detail)
18. Update metadata to reflect changes made in July, 2021. (detail)
19. Add a revision note concerning material added in July, 2021. (detail)
20. tuned signature, according to Isabelle/042041c0ebeb; (detail)
21. Merged. (detail)
22. Sync with my development repo. (detail)
23. Adjust Imperative List/Map/Set Specification for more lenient next operation
    
    This allows implementations of this iterator specification to make use of
    temporary variables for obtaining the next element of the list/set/map.
    This is required by some and especially more general iterators. (detail)
24. discontinued obsolete "val extend = I" for data slots; (detail)
25. tuned; (detail)
26. merged (detail)
27. metadata update for MFODL_Monitor_Optimized (detail)
28. fixed a mistake in MFODL_Monitor_Optimized (detail)
29. merge (detail)
30. adjusted Virtual-Substitution from 2021 to devel (detail)
31. merge of AFP 2021 (detail)
32. fixed duplicate "and" (detail)
33. sitegen for Virtual_Substitution (detail)
34. new entry: Virtual Substitution (detail)
35. updated website/email address (detail)
36. modifications in Jinja and DOminance_CHK (detail)
37. modifications in Jinja and Dominance_CHK (detail)
38. modifications in Jinja and Dominance_CHK (detail)
39. merged (detail)
40. adapted to Term.dest_abs_global / Logic.dest_all_global (e.g. Isabelle/f07761ee5a7f); (detail)
41. more accurate treatment of context; (detail)
42. more accurate treatment of context; (detail)
43. more accurate treatment of context; (detail)
44. tuned -- proper names/scopes for contexts; (detail)
45. tuned proofs; (detail)
46. more accurate treatment of context; (detail)
47. more accurate treatment of context; (detail)
48. proper antiquotations; (detail)
49. tuned messages; (detail)
50. more maintainable Isabelle/ML: proper signatures, proper names/scopes for contexts;
    tuned whitespace; (detail)
51. dead code!? (detail)
52. clarified signature, following Isabelle/de4f151c2a34; (detail)

Started by timer

This run spent:

• 0.15 sec waiting;
• 15 hr build duration;
• 15 hr total from scheduled to completion.