Skip to content
Started 5 mo 23 days ago
Took 4 hr 50 min on workermta1
Success

#32 (Nov 6, 2023, 7:33:09 PM)

Changes
  1. fixed duplicate theory name in Polynomial_Factorization (detail / hgweb)
  2. refactored proof (detail / hgweb)
  3. merged (detail / hgweb)
  4. Removal of the original and obsolete development; replaced by links to the corresponding theorems in the Isabelle libraries (detail / hgweb)
  5. more realistic timeout; (detail / hgweb)
  6. proper document setup for \usepackage{times};
    drop extra copy of generated document; (detail / hgweb)
  7. more realistic timeout; (detail / hgweb)
  8. avoid hardwired document output; (detail / hgweb)
  9. merge (detail / hgweb)
  10. fix(ML_Unification/Parsing) change map_safe type to return an option (detail / hgweb)
  11. Fixed issues connected with cong_def vs unique_euclidean_semiring_class.cong_def and := syntax (detail / hgweb)
  12. Got rid of some global (and unnecessary) parameter settings. Also fixed a couple of slow proofs (detail / hgweb)
  13. feat(ML_Unification) use fixed parser from Isabelle distro (detail / hgweb)
  14. merged (detail / hgweb)
  15. removed unnecessary condition that decided literals are in N (detail / hgweb)
  16. added name to corollary (detail / hgweb)
  17. removed lemma now in distribution (detail / hgweb)
  18. added lemma right_unique_skip (detail / hgweb)
  19. Stone_Relation_Algebras: minor additions (detail / hgweb)
  20. merged (detail / hgweb)
  21. Standard_Borel_Spaces: removed an unnecessary file (detail / hgweb)
  22. Standard_Borel_Spaces and S_Finite_Measure_Monad: adjust theories to metric space in Isabelle2023 (detail / hgweb)
  23. remove ci-extras component (see Isabelle/f992769d); (detail / hgweb)
  24. use ci build mail server; (detail / hgweb)
  25. use Isabelle options for CI mail settings (see Isabelle/4c5aadf1); (detail / hgweb)
  26. removed unused/broken clone (see Isabelle/aff231884b20); (detail / hgweb)
  27. adaptred to Isabelle/d769a183d51d; (detail / hgweb)
  28. more standard simproc_setup using ML antiquotation; (detail / hgweb)
  29. adapted to Isabelle/807b249f1061; (detail / hgweb)
  30. clarified simproc_setup (passive); (detail / hgweb)
  31. avoid clash with outer syntax keyword 'passive'; (detail / hgweb)
  32. merge from afp-2023 (detail / hgweb)
  33. Transport sitegen (detail / hgweb)
  34. New submission Transport (detail / hgweb)
  35. update S_Finite_Measure_Monad to Isabelle2023 (detail / hgweb)
  36. web pages for Standard_Borel_Spaces and S_Finite_Measure_Monad (detail / hgweb)
  37. update Standard_Borel_Spaces to Isabelle2023 (detail / hgweb)
  38. theory files for S_Finite_Measure_Monad + Standard_Borel_Spaces (detail / hgweb)
  39. new entry IO_Language_Conformance (detail / hgweb)
  40. new entry Coupledsim_Contrasim (detail / hgweb)
  41. drop SN from standard wpo-assumptions; prove irreflexivity of WPO without SN (detail / hgweb)
  42. added proof: the multiset extension of two orders preserves irreflexivity (detail / hgweb)
  43. added lemmas on lexicographic extension (detail / hgweb)
  44. added code-unfold lemma (detail / hgweb)
  45. fix(ML_Unification) remove temporary files (detail / hgweb)
  46. update hugo to 0.119.0; (detail / hgweb)
  47. moved hugo component build tool to Isabelle distribution; (detail / hgweb)
  48. update hugo component and support more platforms; (detail / hgweb)

Started by an SCM change

This run spent:

  • 6.4 sec waiting;
  • 4 hr 50 min build duration;
  • 4 hr 51 min total from scheduled to completion.
Revision: a943f1d84bc01a1f960fe0905a3c7352a756c1bf