Build #81 (Dec 5, 2021, 12:14:00 AM)

1. provide component naproche-2d99afe5c349; (detail)
2. merged (detail)
3. Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2 (detail)
4. more documentation about Type/Const antiquotations; (detail)
5. more documentation about document build options; (detail)
6. address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of 41d009462d3c); (detail)
7. tuned --- fewer IDE warnings; (detail)
8. more robust physical timeout (despite 1bea05713dde), especially relevant for quickcheck where large unary numerals may cause excessive heap allocations and resulting GC is better included in the timing; (detail)
9. added definitions multp{DM,HO} and corresponding lemmas (detail)
10. added wfP_less to wellorder and wfP_less_multiset (detail)
11. restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3 (detail)
12. merged (detail)
13. added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to Multiset (detail)
14. redefined less_multiset to be based on multp (detail)
15. added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp (detail)
16. added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max (detail)
17. added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp (detail)
18. added lemma wfP_multp (detail)
19. added lemma mono_multp (detail)
20. added Multiset.multp as predicate equivalent of Multiset.mult (detail)
21. address problems with launch4j and jdk-17 (see also 41d009462d3c); (detail)
22. more robust build on midrange hardware; (detail)
23. clarified tests: omit somewhat pointless (unstable) results; (detail)
24. proper fields for gnuplot (amending b614e3e4146a); (detail)
25. tuned output; (detail)
26. tuned; (detail)
27. merged (detail)
28. more robust build on midrange hardware (despite 67d6f1708ea4); (detail)
29. Added tag Isabelle2021-1-RC4 for changeset 2336356d4180 (detail)
30. updated to polyml-5.9; (detail)
31. NEWS on "isabelle mirabelle"; (detail)
32. tuned; (detail)
33. clarified default for kodkod_scala;
    NEWS for proper release; (detail)
34. maintain option kodkod_scala within theory context, to allow local modification; (detail)
35. NEWS for proper release; (detail)
36. updated to flatlaf-1.6.4; (detail)
37. avoid broken links: auxiliary files are not yet supported; (detail)
38. option document_comment_latex supports e.g. Dagstuhl LIPIcs; (detail)
39. more explicit type Latex.Tags;
    generate isabelletags.sty from Isabelle/Scala, including comment.sty setup; (detail)
40. more uniform treatment of optional_argument for Latex elements;
    discontinued somewhat pointless element position in Isabelle/Scala: semantic add-ons are better provided in Isabelle/ML;
    clarified signature of class Latex: overridable unknown_elem allows to extend the markup language; (detail)
41. removed pointless 'text_cartouche' command: regular 'text' already supports cartouches; (detail)
42. example: alternative document headings, based on more general document output markup; (detail)
43. more general document output: enclosing markup is defined in user-space; (detail)
44. clarified modules (see c299abcf7081); (detail)
45. output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction; (detail)
46. clarified modules; (detail)
47. tuned signature: more explicit types for presentation; (detail)
48. more robust support for Windows line-endings; (detail)
49. source positions for document markup commands, e.g. to retrieve PIDE markup in presentation; (detail)
50. more compact data during presentation: Entity_Context.Theory_Export instead of full Export_Theory.Theory; (detail)
51. clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true"; (detail)
52. more symbolic latex_output via XML (using YXML within text); (detail)
53. proper enclose_name (amending e77c5bfca9aa); (detail)
54. Latex.Output.latex_heading depends on option document_heading_prefix, e.g. relevant for Dagstuhl LIPIcs which prefers unaliased \section etc.; (detail)
55. more symbolic latex_output via XML; (detail)
56. clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab); (detail)
57. tuned; (detail)
58. tuned; (detail)
59. updated to verit-2021.06.2-rmx; (detail)
60. clarified HTML_Context.theory_exports: prefer value-oriented parallelism; (detail)
61. generate problems with correct logic for veriT (detail)
62. more parallelism, at the cost of potential duplicates of make_thy; (detail)
63. afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a); (detail)
64. more interrupts; (detail)
65. present only selected session theories (as in Isabelle2021), in contrast to 2bc24136bdeb, eb89b3a37826;
    eliminated implicit state: these theories are globally unique; (detail)
66. tuned; (detail)
67. clarified modules; (detail)
68. tuned (see also e0d1d9203275); (detail)
69. clarified signature; (detail)
70. tuned; (detail)
71. spelling; (detail)

1. feat(Auto2_HOL) fix setup such that auto2 can be used by other object logics and multiple times (detail)
2. Tuned: use a star in witness. (detail)
3. merge from afp-2021-1 (detail)
4. adjust for new tags in Isabelle2021-1-RC4 (detail)
5. fix dangerous context management (detail)
6. In the definition of regular pair, switched from strict to non-strict (detail)
7. Rename H to S in maximal_exactly_one. (detail)
8. Get rid of the sat abbreviation. (detail)
9. Add missing spaces in semantics_tm. (detail)
10. No space in front of object-logic forall. (detail)
11. Non-conflicting name for boolean denotation. (detail)
12. Simpler Hintikka definition. (detail)
13. Add syntactic abbreviation for constants. (detail)
14. fixed lemma following Isabelle/c256bba593f3 (detail)
15. fix dangerous context management (detail)

Started by timer

This run spent:

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