Build #77 (Nov 7, 2021, 12:14:00 AM)

1. cover all possible kinds, notably for references outside of this theory (amending 129fb11b357f); (detail)
2. proper foundational order; (detail)
3. back to non-strict Export_Theory.read_theory (without warning): theories could have been skipped due to "condition"; (detail)
4. use all entity kinds from theory export, e.g. "method", "attribute"; (detail)
5. clarified signature; (detail)
6. clarified physical_ref; (detail)
7. proper treatment of session build hierarchy; (detail)
8. proper used_theories for session build hierarchy, not known_theories from imported sessions; (detail)
9. present theories from imported sessions as required; (detail)
10. avoid multiple copies of fonts;
    proper fonts prefix for aux. files; (detail)
11. more compact persistent data; (detail)
12. tuned; (detail)
13. proper term_cache; (detail)
14. prefer "NAME|KIND" format, as already used in Isabelle/MMT and Isabelle/Dedukti; (detail)
15. tuned; (detail)
16. observer proper session hierarchy (according to build_graph): thus exported artifacts are always valid; (detail)
17. tuned; (detail)
18. clarified order: prefer bottom-up construction of partial content; (detail)
19. more thorough update_global_index: overwrite old content; (detail)
20. tuned; (detail)
21. tuned; (detail)
22. clarified HTML_Context: just one context type; (detail)
23. unused (see also 217e6cf61453, 5e7916535860); (detail)
24. merged (detail)
25. clarified Theory_Cache: prefer immutable data with Synchronized variable;
    clarified Export_Theory.Theory vs. Entity tables;
    entity_ref: proper treatment of entity kind; (detail)
26. tuned signature; (detail)
27. unused; (detail)
28. proper support of verit's return code for timeout (detail)
29. tuned whitespace; (detail)
30. updated to verit-2021.06.1-rmx, to address "Abnormal termination with exit code 14"; (detail)
31. clarified signature; (detail)
32. prefer official Export.explode_name;
    avoid string interpolation: Isabelle/Scala is closer to Isabelle/ML than Python/Perl; (detail)
33. tuned; (detail)
34. avoid conflict with future keyword; (detail)
35. tuned messages; (detail)
36. clarified signature: more direct XML.symbol_length; (detail)
37. more direct Symbol.length: Symbol.decode is redundant, symbol counts are invariant under it; (detail)
38. tuned -- eliminate clones stemming from d28a51dd9da6; (detail)
39. more to ANNOUNCE; (detail)
40. clarified link style: similar to Isabelle/jEdit; (detail)
41. tuned; (detail)
42. improved HTML presentation by Fabian Huch; (detail)
43. proper HTTPS; (detail)
44. proper markup type (amending be49c660ebbf); (detail)
45. merged; (detail)
46. more PIDE markup; (detail)
47. tuned signature; (detail)
48. more PIDE markup; (detail)
49. recover library_index_content.template from c337c798f64c: required for website/build/main; (detail)
50. merged (detail)
51. simplified some ugly proofs (detail)
52. more generous timeout: support build on Raspberry Pi; (detail)
53. add documentation for pred_mono (detail)
54. merged (detail)
55. added "mono" attribute to BNF generated pred_mono theorems (detail)
56. merged (detail)
57. do not declare $let-bound variables in TPTP output (detail)
58. IDE build actually works (but somewhat pointless); (detail)
59. suppress sources from jEdit/test, which prevent regular build of the generated scala_project; (detail)
60. removed junk; (detail)
61. improve pagebreaks by *not* using supertabular too much; (detail)
62. updated to scala-2.13.7 --- problems with jline disappear after purging $HOME/.inputrc; (detail)
63. more robust "isabelle scala_project": Gradle has been replaced by Maven; (detail)
64. tuned; (detail)
65. support linux_arm as well, e.g. native Docker on Apple Silicon; (detail)
66. update paths at TUM; (detail)
67. Added tag Isabelle2021-1-RC1 for changeset 81cc8f2ea9e7 (detail)
68. updated for release; (detail)
69. some reordering for release; (detail)
70. updated to jdk-17.0.1+12; (detail)
71. tuned message; (detail)
72. clarified antiquotations; (detail)
73. tuned; (detail)
74. minor performance tuning; (detail)
75. more robust; (detail)
76. provide native executables for arm64-darwin, for more robust startup without Rosetta 2; (detail)
77. tuned proofs -- avoid z3, which is unavailable on arm64-linux; (detail)
78. prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms; (detail)
79. discontinued pointless check of kodkodi_version, it is implicit in the bundled component; (detail)

1. Correctness_Algebras: increase session timeout (detail)
2. tuned signature, according to Isabelle/df12779c3ce8; (detail)
3. feat(SpecCheck) add possibility to make builds fail on failure and extend README (detail)
4. added missing funding information (detail)
5. restored theory structure for simple genericity. (detail)
6. Backed out changeset af549be0a8cd (detail)
7. restored different entrance points a before Isabelle2021 (detail)
8. proper parentheses (amending 354560d7143a); (detail)
9. Adjusted to prospective release Isabelle2021-2. (detail)
10. Correctness_Algebras: uncomment counterexamples (detail)
11. clarified identity of theory data: avoid accidental pointer_eq, use equality on unique serial instead; (detail)
12. clarified identity of theory data: pointer_eq is not well-defined (and fails on ARM64), use equality on unique serial instead; (detail)
13. merge from afp-2021 (detail)
14. remove unused functions (detail)
15. silence sitegen warning (detail)
16. new entry X86_Semantics (detail)
17. adjust to isabelle@549019b4a808 (detail)
18. merge from afp-2021 (detail)
19. metadata for Belief_Revision (detail)
20. new entry Belief_Revision (detail)
21. New entry Correctness_Algebras (detail)
22. prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms; (detail)

Started by timer

This run spent:

• 0.14 sec waiting;
• 1 day 6 hr build duration;
• 1 day 6 hr total from scheduled to completion.

Timeout has been exceeded