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

1. merged (detail)
2. use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages; (detail)
3. clarified signature: let Sledgehammer handle SystemOnTPTP comments; (detail)
4. clarified signature: url may change dynamically and is part of result; (detail)
5. clarified error; (detail)
6. support timeout, similar to perl LWP::UserAgent; (detail)
7. clarified signature; (detail)
8. tuned; (detail)
9. clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML; (detail)
10. support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl); (detail)
11. clarified HTTP.Content: support encoding;
    more realistic HTTP.Client operations; (detail)
12. clarified signature: more explicit HTTP operations; (detail)
13. tuned; (detail)
14. more robust; (detail)
15. clarified signature; (detail)
16. clarified components; (detail)
17. avoid name clash (detail)
18. lemma (detail)
19. tuned; (detail)
20. another example for lift_bnf for quotients (detail)
21. merged (detail)
22. proper \usepackage[T1]{fontenc}; (detail)
23. more robust init: avoid spilling opam artifacts; (detail)
24. proper type-setting of cartouches (requires T1);
    \usepackage[T1]{fontenc} is default for mkroot;
    \usepackage[utf8]{inputenc} is obsolete in lualatex; (detail)
25. provide \usepackage{textcomp} (again), for the sake of Ubuntu 16.04; (detail)
26. more robust;
    eliminated perl; (detail)
27. removed unused latex packages; (detail)
28. obsolete (see 0c837beeb5e7); (detail)
29. proper Isabelle/Scala tool --- avoid perl; (detail)
30. generalized confluence-based subdistributivity theorem for quotients;
    new example that triggered the generalization (detail)
31. Backed out changeset 3fdb94d87e0e (detail)
32. Backed out changeset b867b436f372 (detail)
33. reduced dependencies on List_Permutation (detail)
34. follow corresponding precedence on sets (detail)
35. consolidated names (detail)
36. reduced dependencies on theory List_Permutation (detail)

1. avoid name clash (detail)
2. adapted to LuaLaTeX according to Isabelle/299f6a8faccc;
   \usepackage[T1]{fontenc} is default, it provides e.g. proper cartouche-delimiters;
   \usepackage{lmodern} is no longer required, since T1 in LuaLaTeX has proper scalable fonts;
   \usepackage[utf8]{inputenc} is obsolete in LuaLaTeX;
   tuned whitespace; (detail)
3. reduced dependencies on List_Permutation (detail)
4. follow corresponding precedence on sets (detail)
5. consolidated names (detail)
6. reduced dependencies on theory List_Permutation (detail)

Started by timer

This run spent:

• 74 ms waiting;
• 16 hr build duration;
• 16 hr total from scheduled to completion.