Changes

Summary

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

Summary

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