Skip to content
Started 7 days 13 hr ago
Took 5 hr 11 min on workermta1
Failed

#1019 (Apr 11, 2024, 2:15:11 PM)

Changes
  1. tweaked time functions for median-of-medians selection in HOL-Data_Structures (detail / hgweb)
  2. merged (detail / hgweb)
  3. rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04 beta; (detail / hgweb)
  4. Tiny tweaks to proofs (detail / hgweb)
  5. A bit of new material about type class "infinite", from Eval_FO (detail / hgweb)
  6. avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax; (detail / hgweb)
  7. proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...); (detail / hgweb)
  8. adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested; (detail / hgweb)
  9. Add entry on Sketch_and_Explore to CONTRIBUTORS (detail / hgweb)
  10. moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory (detail / hgweb)
  11. more portable: prefer official JDBC operation DatabaseMetaData.getColumns(); (detail / hgweb)
  12. tuned signature; (detail / hgweb)

Started by an SCM change

This run spent:

  • 7.9 sec waiting;
  • 5 hr 11 min build duration;
  • 5 hr 12 min total from scheduled to completion.
Revision: c0d689c4fd151973954199cea481dfd4b9829e04
Failed entries: