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

1. publish component; (detail)
2. further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster; (detail)
3. clarified \<Zcomp> (small) vs. \<Zsemi> (big); (detail)
4. more CONTRIBUTORS; (detail)
5. more Z_Notation symbols, as proposed by Simon Foster;
   some LaTeX-art based on tex.stackexchange "How do you make a square element symbol (\in)"; (detail)
6. more accurate glyphs 0x25C1 / 0x25B7, based on 0x2A64 / 0x2A65 minus the "minus"; (detail)
7. clarified order for GUI panel; (detail)
8. prefer more direct interpretation (detail)
9. more Z_Notation symbols, as proposed by Simon Foster; (detail)
10. more accurate spacing, according to results seen in isar-ref (Appendix B), using 12pt or 10pt; (detail)
11. clarified order for presentation in isar-ref (Appendix B); (detail)
12. prefer explicit \<Zproject> (with its own Unicode codepoint); (detail)
13. more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
    NB: no bold version of 0x2900 due to fontforge crash "Internal Error: Some fragments did not join"; (detail)
14. tuned message; (detail)
15. proper directory of settings file;
    tuned; (detail)
16. tuned lemma (detail)
17. added lemma (detail)
18. tuned signature; (detail)
19. tuned signature (again); (detail)
20. tuned --- following hints by IntelliJ; (detail)
21. tuned comments; (detail)
22. proper shell quote; (detail)
23. removed spurious references to perl / libwww-perl; (detail)
24. invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
    clarified inlined command-line;
    clarified errors: exception ERROR becomes UnknownError (it could stem from Scala function); (detail)
25. clarified signature: refer to file name instead of file content; (detail)
26. compile; (detail)
27. clarified signature: more explicit types; (detail)
28. support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp; (detail)
29. clarified signature; (detail)
30. elapsed time to download content (and for the server to provide content); (detail)
31. more direct elapsed run_time via bash_process wrapper (via Scala and C); (detail)

1. neater proof (detail)
2. merged (detail)
3. Removal of an unused theorem. Plus lots of white space (detail)
4. switch new entries' documents to T1 encoding (detail)
5. merge from afp-2021 (detail)
6. corrected metadata (use acute's in names of J. Divasón and René T.) (detail)
7. sitegen for Modular_arithmetic_LLL_and_HNF_algorithms (detail)
8. metadata for Modular_arithmetic_LLL_and_HNF_algorithms (detail)
9. new entry Modular_arithmetic_LLL_and_HNF_algorithms (detail)
10. a slight streamlining (detail)
11. Hermite_Lindemann website (detail)
12. new entry Hermite_Lindemann (detail)
13. cosmetic changes (detail)
14. Projective_Measurements website (detail)
15. Projective_Measurements with files (detail)
16. new entry Projective_Measurements (detail)
17. add Andreas Lochbihler as editor (detail)
18. New entry: Mereology (detail)
19. New entry Sunflowers (detail)
20. refactored and added lemma state_behaves_forward_to_backward (detail)

Started by timer

This run spent:

• 0.19 sec waiting;
• 1 day 3 hr build duration;
• 1 day 3 hr total from scheduled to completion.