Skip to content
Started 2 yr 6 mo ago
Took 16 hr
Success

Build #73 (Oct 10, 2021, 12:14:00 AM)

Changes
  1. tuned text; (detail)
  2. recover NEWS from 78d1f73bbeaa; (detail)
  3. save 90 MB by excluding rlwrap and thus perl; (detail)
  4. save 45 MB by excluding rlwrap and thus perl; (detail)
  5. NEWS; (detail)
  6. clarified test of directories; (detail)
  7. misc tuning for release; (detail)
  8. merged (detail)
  9. updated to kodkodi-1.5.7. with more robust/portable management of files and processes; (detail)
  10. provide minisat-2.2.1 on all currently supported platforms, notably as external solver for Nitpick; (detail)
  11. tuned message; (detail)
  12. proper build on macOS; (detail)
  13. build minisat, using recent fork from original sources; (detail)
  14. proper platform_path for executables run from Java; (detail)
  15. tuned message; (detail)
  16. tuned; (detail)
  17. tuned whitespace; (detail)
  18. merged (detail)
  19. added timeout to veriT (detail)
  20. new notion of infinite sums in HOL-Analysis, ordering on complex numbers (detail)
  21. NEWS and CONTRIBUTORS (detail)
  22. merged (detail)
  23. added offset to Mirabelle's tptp output names (detail)
  24. tuned zipperposition config in sledgehammer (detail)
  25. considered slices overhead in sledgehammer (detail)
  26. tuned atp_prover sliding (detail)
  27. tuned Zipperposition slides in sledgehammer (detail)
  28. include arm64-linux; (detail)
  29. updated to Vampire 4.6, as proposed by Martin Desharnais; (detail)
  30. build from official downloads; (detail)
  31. build just one vampire version; (detail)
  32. clarified signature; (detail)
  33. maintain previous theory identifier to support semantic caching, notably in Isabelle/Naproche; (detail)
  34. more exports, notably for Isabelle/Naproche; (detail)
  35. include arm64-linux; (detail)
  36. prefer existing OCaml installation; (detail)
  37. include arm64-linux; (detail)
  38. no patchelf on macOS (undetected due to cached executables?); (detail)
  39. provide opam-2.1.0 for experimentation; (detail)
  40. rebuild cygwin-20211004.tar.gz; (detail)
  41. include arm64-linux; (detail)
  42. updated to cygwin-20211004: build again; (detail)
  43. merged (detail)
  44. removed pointless NEWS: both Docker/ubuntu and Cygwin provide perl by default; (detail)
  45. actually use cygwin-20211002 (amending ff0ca375457c); (detail)
  46. discontinued perl; (detail)
  47. clarified signature; (detail)
  48. proper term operation Term.dest_abs; (detail)
  49. tuned; (detail)
  50. tuned proofs;
    fewer warnings; (detail)
  51. more standard binder syntax; (detail)
  52. clarified 'let' syntax: avoid conflict with existing 'let' in FOL; (detail)
  53. tuned; (detail)
  54. tuned; (detail)
  55. merged (detail)
  56. removal of a redundant theorem (and white space) (detail)
  57. new material from the Roth development, mostly about finite sets, disjoint famillies and partitions (detail)
  58. clarified and updated for release; (detail)
  59. formal comment concerning 83d2208252d1 vs. d8dc8fdc46fc; (detail)
  60. more NEWS and CONTRIBUTORS; (detail)
  61. clarified comments; (detail)
  62. support symbol \<Parallel>, based on \bigparallel from stdmaryd (stmary10.pfb: move y=1100, scale 222%, embolden by 40 units, adjust spacing); (detail)
  63. clarified dependencies; (detail)
  64. updated for release; (detail)
  65. Added tag Isabelle2021-1-RC0 for changeset fedc0b659881 (detail)
  66. provide Isabelle/jEdit plugins as services, and thus allow user components do the same; (detail)
  67. merged (detail)
  68. updated for release; (detail)
  69. misc tuning for release; (detail)
  70. update dependency; (detail)
  71. trim whitespace; (detail)
  72. misc tuning for release; (detail)
  73. misc tuning for release; (detail)
  74. isabelle build_components -u; (detail)
  75. updated to Haskell Stach lts-18.12 with GHC ghc-8.10.7; (detail)
  76. updated to current Cygwin, near 3.2.0;
    discontinued perl; (detail)
  77. updated to sumatra_pdf-3.3.3; (detail)
  78. updated default version; (detail)
  79. updated to xz-java-1.9; (detail)
  80. updated to sqlite-jdbc-3.36.0.3; (detail)
  81. updated to postgresql-42.2.24; (detail)
  82. updated to jfreechart-1.5.3; (detail)
  83. updated to flatlaf-1.6; (detail)
  84. clarified signature; (detail)
  85. clarified Term.dest_abs (again, refining 71dfb835025d): only Free names are relevant for abstract terms, without syntax; (detail)
  86. clarified sledgehammer_provers, following d8dc8fdc46fc; (detail)
  87. proper term operation Term.dest_abs; (detail)
  88. tuned, following Syntax_Trans.variant_abs; (detail)
  89. proper patterns for (- numeral t), amending 03ff4d1e6784; (detail)
  90. tuned; (detail)
  91. merged (detail)
  92. update syntax for verit (detail)
  93. clarified antiquotations; (detail)
  94. clarified antiquotations; (detail)
  95. provide verit-2021.06-rmx; (detail)
Changes
  1. ETTS: minor amendments (detail)
  2. CTR and ETTS: integration with fd5f62176987 (detail)
  3. adapted QHLProver to isabelle-dev/409ca22dee4c (detail)
  4. adapted to isabelle-dev/409ca22dee4c (detail)
  5. adapted to devel (detail)
  6. Complex_Bounded_Operators: update to isabelle@ffb15f7f26d5 (detail)
  7. Weighted_Path_Order: update to isabelle@ffb15f7f26d5 (detail)
  8. merge from afp-2021 (detail)
  9. add missing session dependency (detail)
  10. new entry FOL_Axiomatic (detail)
  11. regen website (detail)
  12. minor editorial changes for CZH entries (detail)
  13. New entry Weighted_Path_Order (detail)
  14. fxed metadata (forgot .html) in link (detail)
  15. metadata and sitegen for complex bounded operators (detail)
  16. new entry: Complex_Bounded_Operators (detail)
  17. restructure resultant algorithms, so that tuned code-equations are also availalbe for integral domains (detail)
  18. removed obselete sorted_sorted_wrt, following Isabelle/06aeb9054c07; (detail)
  19. clarified timeout;
    tuned whitespace; (detail)
  20. hide_lams ~> opaque_lifting; (detail)
  21. clarified antiquotations; (detail)
  22. proper inst table; (detail)
  23. clarified antiquotations; (detail)
  24. clarified antiquotations; (detail)
  25. proper inst table; (detail)
  26. clarified antiquotations; (detail)
  27. clarified antiquotations; (detail)
  28. clarified antiquotations; (detail)
  29. clarified antiquotations; (detail)
  30. unused; (detail)
  31. merged (detail)
  32. clarified antiquotations; (detail)
  33. proper match against const_name; (detail)
  34. tuned; (detail)
  35. tuned; (detail)
  36. clarified antiquotations; (detail)
  37. clarified antiquotations; (detail)
  38. clarified antiquotations; (detail)
  39. fix(ci): clarified addresses, set proper TLS version; (detail)
  40. feat(ci): remove hard-coded address; (detail)
  41. feat(SpecCheck/Show) tune pretty printing for environments (detail)
  42. merge (detail)
  43. eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib" (detail)
  44. new entries by Mihails Milehins

    CZH_Elementary_Categories, CZH_Foundations,
    CZH_Universal_Constructions, Conditional_Simplification,
    Conditional_Transfer_Rule, Intro_Dest_Elim, and Types_To_Sets_Extension (detail)
  45. New entry: Dominance_CHK (detail)
  46. Schutz_Spacetime website (detail)
  47. new entry Schutz_Spacetime (detail)
  48. metadata for Logging_Independent_Anonymity (detail)
  49. new entry Logging_Independent_Anonymity (detail)

Started by timer

This run spent:

  • 57 sec waiting;
  • 16 hr build duration;
  • 16 hr total from scheduled to completion.
Revision: e593ea8804946ea119044593ae3dc961161775ca
Revision: 7ecd220edef393b39a75dc265c7b8dadcd9aa92b