Build #459 (May 3, 2021 11:09:10 PM)

1. A nice cardinality lemma (detail / hgweb)
2. tuned (detail / hgweb)
3. more robust indentation: proper line context after insert; (detail / hgweb)
4. more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().getModeName(); (detail / hgweb)
5. support nested cases; (detail / hgweb)
6. tuned; (detail / hgweb)
7. tuned; (detail / hgweb)
8. early definition of ML antiquotations; (detail / hgweb)
9. tuned; (detail / hgweb)
10. clarified signature: more operations; (detail / hgweb)
11. clarified signature: more operations; (detail / hgweb)
12. clarified signature; (detail / hgweb)
13. tuned signature; (detail / hgweb)
14. clarified command-line, following other build_XYZ tools; (detail / hgweb)
15. more recent OCaml and GHC stack: better support for Apple Silicon; (detail / hgweb)
16. merged (detail / hgweb)
17. avoid "exec" to change the winpid; (detail / hgweb)
18. clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c); (detail / hgweb)
19. fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running); (detail / hgweb)
20. clarified signature; (detail / hgweb)
21. rebuild executable for x86_64-darwin; (detail / hgweb)
22. clarified command-line; (detail / hgweb)
23. update Linux base-line; (detail / hgweb)
24. tuned comments; (detail / hgweb)
25. tuned signature; (detail / hgweb)
26. simplified typesetting of \<guillemotleft>...\<guillemotright>; (detail / hgweb)
27. collecting more lemmas concerning multisets (detail / hgweb)
28. proper use of antiquotations; (detail / hgweb)
29. more documentation on "Conversions"; (detail / hgweb)
30. tuned (detail / hgweb)
31. updated example; (detail / hgweb)
32. clarified options (again); (detail / hgweb)
33. more options: update ISABELLE_IDENTIFIER; (detail / hgweb)
34. clarified conditional ML; (detail / hgweb)
35. support for conditional ML text; (detail / hgweb)
36. updated example; (detail / hgweb)
37. clarified options; (detail / hgweb)
38. proper context variable handling when stripping leadings quantifiers from test goals (detail / hgweb)
39. proper etc/ISABELLE_ID from archive (amending 4cba4e250c28); (detail / hgweb)
40. eliminated perl: prefer elementary GNU printenv; (detail / hgweb)
41. more robust bootstrap of components; (detail / hgweb)
42. more self-contained support for macOS; (detail / hgweb)
43. misc tuning and clarification; (detail / hgweb)
44. tuned signature; (detail / hgweb)
45. support for base64 via Isabelle/Scala/ML; (detail / hgweb)
46. compile; (detail / hgweb)
47. clarified signature: avoid overlap of String vs. Bytes (both are CharSequence); (detail / hgweb)
48. clarified signature (again); (detail / hgweb)
49. merged (detail / hgweb)
50. clarified signature; (detail / hgweb)
51. unused; (detail / hgweb)
52. unused; (detail / hgweb)
53. clarified signature: more structured arguments, notably for remote provers; (detail / hgweb)
54. clarified signature; (detail / hgweb)
55. clarified signature: avoid tmp file; (detail / hgweb)
56. clarified signature for Scala functions; (detail / hgweb)
57. clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9); (detail / hgweb)
58. tuned; (detail / hgweb)
59. clarified cache; (detail / hgweb)
60. clarified signature: Bytes extends CharSequence already (see d201996f72a8); (detail / hgweb)
61. clarified exceptions; (detail / hgweb)
62. more uniform use of Byte_Message;
    support protocol_message with multiple chunks; (detail / hgweb)
63. tuned signature; (detail / hgweb)
64. tuned signature; (detail / hgweb)
65. more robust treatment of empty markup: it allows to produce formal chunks; (detail / hgweb)
66. collected combinatorial material (detail / hgweb)
67. tuned; (detail / hgweb)
68. tuned; (detail / hgweb)
69. more documentation; (detail / hgweb)
70. proper treatment of nested antiquotations;
    clarified signature; (detail / hgweb)
71. support for ML special forms: modified evaluation similar to Scheme; (detail / hgweb)
72. clarified signature: more detailed token positions for antiquotations; (detail / hgweb)
73. merged (detail / hgweb)
74. clarified signature; (detail / hgweb)
75. confluent preprocessing for floats in presence of target language numerals (detail / hgweb)
76. subclass relation (detail / hgweb)
77. some tinkering with npm versions; (detail / hgweb)
78. some tinkering with npm versions; (detail / hgweb)
79. back to post-release mode; (detail / hgweb)
80. tuned signature; (detail / hgweb)
81. auto-update due to "isabelle build_vscode"; (detail / hgweb)
82. tuned; (detail / hgweb)
83. tuned --- following hints by IntelliJ IDEA; (detail / hgweb)
84. fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes) (detail / hgweb)
85. simplified definition (detail / hgweb)

Started by an SCM change

This run spent:

• 7.4 sec waiting;
• 3 hr 15 min build duration;
• 3 hr 15 min total from scheduled to completion.