Build #718 (Aug 10, 2022, 9:42:08 PM)

Progress:

1. New theory of fixed length lists (detail / hgweb)
2. Added tag Isabelle2022-RC0 for changeset b42e20adaeed (detail / hgweb)
3. proper Java/Scala compiler classpath for standalone application (see also make_isabelle_app() in Pure/Admin/build_release.scala); (detail / hgweb)
4. clarified message; (detail / hgweb)
5. provide naproche-20220808 (inactive); (detail / hgweb)
6. more robust data representation: notably for Store.read_session_timing with database_server; (detail / hgweb)
7. tuned message; (detail / hgweb)
8. afford default cache policy, despite 6a29709906c6; (detail / hgweb)
9. tuned signature; (detail / hgweb)
10. clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory; (detail / hgweb)
11. tuned; (detail / hgweb)
12. tuned signature; (detail / hgweb)
13. clarified signature; (detail / hgweb)
14. clarified modules; (detail / hgweb)
15. merged (detail / hgweb)
16. tuned; (detail / hgweb)
17. clarified message; (detail / hgweb)
18. clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
    discontinued obsolete operations; (detail / hgweb)
19. clarified signature: prefer Export.Context; (detail / hgweb)
20. clarified signature: find session_database within Session_Context.db_hierarchy; (detail / hgweb)
21. clarified signature: prefer Export.Session_Context; (detail / hgweb)
22. prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context; (detail / hgweb)
23. clarified signature; (detail / hgweb)
24. tuned signature, following hints by IntelliJ IDEA; (detail / hgweb)
25. clarified signature: more robust treatment of server; (detail / hgweb)
26. discontinued Export.Provider in favour of Export.Context and its derivatives;
    uniform treatment of all sessions, including Pure; (detail / hgweb)
27. clarified signature: less redundant -- Sessions.Base_Info already specifies the main session; (detail / hgweb)
28. tuned signature: more operations; (detail / hgweb)
29. misc tuning and clarification; (detail / hgweb)
30. clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
    clarified treatment of Session_Context.theory_names, added export_names;
    clarified treatment of document_snapshot: sites on top of the session_stack; (detail / hgweb)
31. clarified database query: refer to semantic theories; (detail / hgweb)
32. clarified signature: more operations; (detail / hgweb)
33. clarified signature: persistent theory_names in lexical order; (detail / hgweb)
34. proper session_databases for database_server: need to follow precise session_hierarchy; (detail / hgweb)
35. redundant; (detail / hgweb)
36. clarified signature: more robust close operation; (detail / hgweb)
37. more uniform exports: proper encoding of empty parents for Pure; (detail / hgweb)
38. clarified signature: more uniform treatment of empty exports; (detail / hgweb)
39. clarified session name: treat PIDE session as Sessions.DRAFT with imports from other sessions; (detail / hgweb)
40. more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log);
    removed unused imports_hierarchy; (detail / hgweb)
41. clarified context for retrieval: more explicit types, with optional close() operation; (detail / hgweb)
42. tuned; (detail / hgweb)
43. unused; (detail / hgweb)
44. retrieve information about used files; (detail / hgweb)
45. tuned signature -- more robust; (detail / hgweb)
46. tuned signature; (detail / hgweb)
47. clarified signature: Export.Provider knows its (accidental) theory_names; (detail / hgweb)
48. clarified signature; (detail / hgweb)
49. tuned, following hints by IntelliJ IDEA; (detail / hgweb)
50. clarified signature: proper session_name for Sessions.Base (like Sessions.Info); (detail / hgweb)
51. tuned signature; (detail / hgweb)
52. clarified signature; (detail / hgweb)
53. clarified signature; (detail / hgweb)
54. clarified signature; (detail / hgweb)
55. avoid multiple load_commands; (detail / hgweb)
56. avoid redundant dependencies.load_commands with potential errors (amending ea4f86914cb2); (detail / hgweb)
57. tuned signature -- avoid redundant arguments; (detail / hgweb)
58. tuned -- following hints by IntelliJ IDEA; (detail / hgweb)
59. tuned signature; (detail / hgweb)
60. tuned comments; (detail / hgweb)
61. removed somewhat pointless transaction: db is meant to be finished (or updated monotonically); (detail / hgweb)
62. tuned signature; (detail / hgweb)
63. clarified signature; (detail / hgweb)
64. clarified signature: avoid repeated db_context.input_database; (detail / hgweb)
65. clarified signature: more robust; (detail / hgweb)
66. removed somewhat pointless operations (see a6c69599ab99); (detail / hgweb)
67. clarified signature; (detail / hgweb)
68. tuned; (detail / hgweb)
69. tuned; (detail / hgweb)
70. clarified signature; (detail / hgweb)
71. clarified names; (detail / hgweb)
72. clarified signature; (detail / hgweb)
73. clarified names; (detail / hgweb)
74. clarified signature; (detail / hgweb)
75. clarified signature: more explicit types; (detail / hgweb)
76. unused (see 0d30ea76756c); (detail / hgweb)
77. tuned; (detail / hgweb)
78. clarified signature; (detail / hgweb)
79. tuned; (detail / hgweb)
80. unused (see 3064e165c660); (detail / hgweb)
81. merge (detail / hgweb)
82. changed the order of Zipperposition slices in Sledgehammer (detail / hgweb)
83. merged (detail / hgweb)
84. The wellordering instantiation for length-ordered lists (detail / hgweb)
85. show sum_list defn (detail / hgweb)
86. prettified def (detail / hgweb)
87. More lemmas. (detail / hgweb)
88. Some more proofs. (detail / hgweb)
89. a few new theorems (detail / hgweb)
90. tuned; (detail / hgweb)
91. clarified while-loops; (detail / hgweb)
92. updated to postgresql-42.4.0; (detail / hgweb)
93. updated to flatlaf-2.4; (detail / hgweb)
94. updated to pdfjs-2.14.305;
    prefer "legacy" distribution: more portable, notably for old Node.js/Electron of VSCodium; (detail / hgweb)
95. more robust: retain Classpath value; (detail / hgweb)
96. tuned; (detail / hgweb)
97. mor robust; (detail / hgweb)
98. clarified modules; (detail / hgweb)
99. clarified signature; (detail / hgweb)
100. update documentation, following 21c1f82e7f5d; (detail / hgweb)
101. proper classpath for Scala compiler invocation (amending 14e22b525b13); (detail / hgweb)
102. merged (detail / hgweb)
103. support for dynamic classpath from exports; (detail / hgweb)
104. clarified signature; (detail / hgweb)
105. tuned signature; (detail / hgweb)
106. Avoid shadowing original List._ namespace. (detail / hgweb)
107. replaced complicated lemma by a simpler one (detail / hgweb)
108. clarified signature; (detail / hgweb)
109. clarified modules; (detail / hgweb)
110. merged (detail / hgweb)
111. more documentation; (detail / hgweb)
112. tuned; (detail / hgweb)
113. removed obsolete commands; (detail / hgweb)
114. command 'scala_build_generated_files' with proper management of source dependencies;
     support more file-formats; (detail / hgweb)
115. clarified signature; (detail / hgweb)
116. tuned messages; (detail / hgweb)
117. support more file types; (detail / hgweb)
118. support for Java language; (detail / hgweb)
119. clarified signature; (detail / hgweb)
120. clarified signature; (detail / hgweb)
121. support for classpath artifacts within session structure: (detail / hgweb)
122. clarified names; (detail / hgweb)
123. clarified signature; (detail / hgweb)
124. clarified signature; (detail / hgweb)
125. clarified signature; (detail / hgweb)
126. clarified signature; (detail / hgweb)
127. unused; (detail / hgweb)
128. clarified signature; (detail / hgweb)
129. tuned signature: more explicit types; (detail / hgweb)
130. fix document build error (detail / hgweb)
131. tuned (some HOL lints, by Yecine Megdiche); (detail / hgweb)
132. moved lemma fromm AFP (detail / hgweb)
133. tuned names (detail / hgweb)
134. refined code equations for characters (detail / hgweb)
135. prefer non-JNI SAT solvers by default in Nitpick (detail / hgweb)
136. milder Sledgehammer messages (detail / hgweb)
137. moved lemmas from AFP (detail / hgweb)
138. refined code equations for characters (detail / hgweb)
139. tuned comments; (detail / hgweb)
140. support for Isabelle/Scala/Java modules in Isabelle/ML; (detail / hgweb)
141. more robust Scala 3 indentation, for the sake of IntelliJ IDEA; (detail / hgweb)
142. clarified signature: read_theory_exports is already ordered; (detail / hgweb)
143. clarified signature; (detail / hgweb)
144. tuned; (detail / hgweb)
145. sketch for word-specific lsb and msb (detail / hgweb)

Started by an SCM change

This run spent 6.8 sec waiting in the queue.