Build #38 (Mar 7, 2021, 12:14:00 AM)

1. obsolete (see f3378101f555); (detail)
2. merged (detail)
3. more direct unlimited smt_timeout;
   update of certificates: generated command-line options are part of input / digest; (detail)
4. clarified smt: support Timeout.ignored and Timeout.scale_time; (detail)
5. clarified timeouts in Isabelle/ML; (detail)
6. tuned --- more elementary Time operations; (detail)
7. removed unused/pointless operation: Time.start is the load/init time of this Scala module; (detail)
8. obsolete; (detail)
9. clarified signature --- augment existing structure Time; (detail)
10. rebuild SMT certificates from scratch; (detail)
11. added lemmas (sublist|prefix|suffix)_list_all (detail)
12. added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(take|drop)While (detail)
13. added lemmas list_all_(take|drop)I and list_all_(take|drop)WhileI (detail)
14. typo (detail)
15. merged (detail)
16. added upper bound on monomorphisation duplicate instances (detail)
17. tuned best_slices in atp_config (detail)
18. tuned exec field in atp_config (detail)
19. removed junk; (detail)
20. tuned proofs; (detail)
21. enforce full build, after significant changes in Isabelle/Scala; (detail)
22. clarified compiler options: show relevant warnings; (detail)
23. tuned --- avoid compiler warnings; (detail)
24. clarified signature --- fewer warnings; (detail)
25. clarified signature --- fewer warnings; (detail)
26. tuned --- fewer warnings; (detail)
27. more robust ordering (see also 88c96e836ed6); (detail)
28. proper scala.collection.immutable; (detail)
29. tuned --- fewer warnings; (detail)
30. tuned --- fewer warnings; (detail)
31. tuned; (detail)
32. tuned --- fewer warnings; (detail)
33. tuned --- fewer warnings; (detail)
34. tuned --- fewer warnings; (detail)
35. tuned --- fewer warnings; (detail)
36. more robust error; (detail)
37. tuned --- fewer warnings; (detail)
38. tuned --- fewer warnings; (detail)
39. tuned --- fewer warnings; (detail)
40. updated to scala-2.13.5 (with scala-swing_2.13-3.0.0); (detail)
41. slightly more efficient Term.fastype_of (only little impact in regular applications); (detail)
42. reduced dependencies on theory List_Permutation (detail)
43. Merge (detail)
44. reverted simprule status on a new lemma (detail)
45. merged (detail)
46. tiny bit of lemma hacking (detail)
47. tuned --- fewer warnings; (detail)
48. tuned --- fewer warnings; (detail)
49. tuned --- avoid deprecated conversions between certain number type; (detail)
50. tuned --- avoid deprecated Predef.any2stringadd; (detail)
51. tuned --- silence odd warning; (detail)
52. tuned --- fewer warnings; (detail)
53. tuned --- fewer warnings; (detail)
54. tuned --- fewer warnings; (detail)
55. tuned --- fewer warnings; (detail)
56. clarified signature, according to Isabelle/Scala; (detail)
57. download more directly, via means of JVM; (detail)
58. download on separate thread; (detail)
59. clarified signature; (detail)
60. tuned; (detail)
61. proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.); (detail)
62. tuned signature; (detail)
63. NEWS (detail)
64. lemma diffusion (detail)
65. more connections between mset _ = mset _ and permutations (detail)
66. dissolve theory with duplicated name from afp (detail)
67. more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept; (detail)
68. more Isabelle/ML/Scala operations; (detail)
69. more Isabelle/ML/Scala operations; (detail)
70. more Isabelle/ML/Scala operations;
    clarified errors; (detail)
71. proper src1, amending 20157c8ab3f3; (detail)
72. tuned; (detail)
73. proper File.eq, amending df49ca5da9d0; (detail)
74. tuned; (detail)
75. clarified modules: more like ML; (detail)
76. obsolete; (detail)
77. tuned; (detail)
78. more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552); (detail)
79. discontinued somewhat pointless "integrity test of build_history": it fails right now, but also failed to expose spurious incompatibilities when it was working; (detail)

1. tuned (detail)
2. Tuned presentation of Buffon's needle (detail)
3. tuned (detail)
4. reduced dependencies on theory List_Permutation (detail)
5. tidied up messy proofs (detail)
6. lemma diffusion (detail)
7. more connections between mset _ = mset _ and permutations (detail)
8. dissolve theory with duplicated name from afp (detail)

Started by timer

This run spent:

• 78 ms waiting;
• 20 hr build duration;
• 20 hr total from scheduled to completion.