Skip to content
[Jenkins]Jenkins
log in
Started 2 yr 7 mo ago
Took 5 hr 0 min on workermtahpc
Aborted

#1576 (Oct 20, 2021, 1:35:39 AM)

Build Artifacts
Changes
  1. merged (detail / hgweb)
  2. tuned ML --- clarified use of context;
    tuned message; (detail / hgweb)
  3. tuned --- fewer clones; (detail / hgweb)
  4. updated to jEdit plugin Highlight 2.5; (detail / hgweb)
  5. proper tactic combinator; (detail / hgweb)
  6. proper file headers; (detail / hgweb)
  7. clarified context;
    clarified modules; (detail / hgweb)
  8. more accurate treatment of context; (detail / hgweb)
  9. updated email address (detail / hgweb)
  10. removed some 'private' modifiers from HOL-Computational_Algebra (detail / hgweb)
  11. merged (detail / hgweb)
  12. merged (detail / hgweb)
  13. more robust Variable.revert_bounds (see also b12f2cef3ee5); (detail / hgweb)
  14. more accurate treatment of context; (detail / hgweb)
  15. tuned -- proper names/scopes for contexts; (detail / hgweb)
  16. clarified context; (detail / hgweb)
  17. clarified context; (detail / hgweb)
  18. tuned; (detail / hgweb)
  19. unused; (detail / hgweb)
  20. more accurate treatment of context;
    declare generated bounds for the sake of recdef, which has variables leaking from local context; (detail / hgweb)
  21. isabelle regenerate_cooper; (detail / hgweb)
  22. revert bbfed17243af, breaks HOL-Proofs extraction; (detail / hgweb)
  23. tuned; (detail / hgweb)
  24. tuned; (detail / hgweb)
  25. proper p' instead of p (amending 52c7c42e7e27); (detail / hgweb)
  26. proper context for Goal.prove_internal; (detail / hgweb)
  27. discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
    Simplifier and equational conversions demand a proper proof context; (detail / hgweb)
  28. more accurate treatment of context, notably for nested Goal.proof / SUBPROOF; (detail / hgweb)
  29. tuned; (detail / hgweb)
  30. tuned; (detail / hgweb)
  31. tuned; (detail / hgweb)
  32. spelling; (detail / hgweb)
  33. clarified context; (detail / hgweb)
  34. clarified signature; (detail / hgweb)
  35. tuned Vampire configuration to use TFX in Sledgehammer (detail / hgweb)
  36. added Mirabelle action presburger (detail / hgweb)
  37. added timing to Mirabelle action arith (detail / hgweb)
  38. added error message on invalid Mirabelle action (detail / hgweb)

Started by an SCM change

This run spent:

  • 45 min waiting;
  • 5 hr 0 min build duration;
  • 5 hr 45 min total from scheduled to completion.
Revision: 375e8e1a2139a2466fb86814db2125a18ac5bdc2