Skip to content
Started 2 yr 4 mo ago
Took 1 day 6 hr
Aborted

Build #82 (Dec 12, 2021, 12:14:00 AM)

Changes
  1. provide component naproche-20211211; (detail)
  2. merged (detail)
  3. more Mailman archives; (detail)
  4. more Mailman content; (detail)
  5. clarified signature; (detail)
  6. tuned metis to use map_index (detail)
  7. merged (detail)
  8. fixed HOL-TPTP (detail)
  9. tuned vars_of_iterm (detail)
  10. fixed TPTP generation of multi-arity expressions (detail)
  11. proper handling of Hilbert choice in TFX logics (detail)
  12. proper tptp_builtins (detail)
  13. reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle (detail)
  14. proper proxy for Hilbert choice in TPTP output (detail)
  15. proper polymorphism for TH1 format in Sledgehammer (detail)
  16. refactored $ite and $let configuration and added dummy_thf_reduced prover (detail)
  17. tuned TPTP file names generated by Sledgehammer (detail)
  18. tuned SMT-Lib file names generated by Mirabelle (detail)
  19. added support for higher-order SMT proof search in Sledgehammer (detail)
  20. separated FOOL from $ite/$let in TPTP output (detail)
  21. missing latex font (detail)
  22. Rewrite: added links to docu, made more prominent (detail)
  23. discontinued old-style {* verbatim *} tokens; (detail)
  24. tuned proof; (detail)
  25. isabelle update_cartouches; (detail)
  26. more symbolic latex_output via XML (using YXML within text); (detail)
  27. tuned signature: remove unused; (detail)
  28. prefer symbolic Latex.environment (typeset in Isabelle/Scala); (detail)
  29. tuned signature; (detail)
  30. clarified corner cases of syntax; (detail)
  31. clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2); (detail)
  32. a slightly simpler proof (detail)
Changes
  1. merged (detail)
  2. generalized standard formula redundancy out of standard redundancy (detail)
  3. merged (detail)
  4. discontinued Parse.text; (detail)
  5. discontinued old-style {* verbatim *} tokens; (detail)
  6. weakened locale assumptions: wfP implies asymp (detail)
  7. Add papers to metadata. (detail)
  8. refactored Standard_Redundancy_Criterion to not use ordering type classes (detail)
  9. isabelle update_cartouches; (detail)
  10. removed obsolete "extend" operation; (detail)
  11. more symbolic latex_output via XML (using YXML within text);
    re-use existing Latex.output_markup; (detail)
  12. prefer symbolic Latex.environment (typeset in Isabelle/Scala); (detail)
  13. tuned signature; (detail)

Started by timer

This run spent:

  • 0.12 sec waiting;
  • 1 day 6 hr build duration;
  • 1 day 6 hr total from scheduled to completion.
Revision: 0dd4dbe7bed387ab84124eac5ad991486698062c
Revision: b335908ca5ac773f75c7fb3ce569038a75d3df6e

Timeout has been exceeded