Skip to content
[Jenkins]Jenkins
log in
Started 2 yr 5 mo ago
Took 16 hr
Success

Build #79 (Nov 21, 2021, 12:14:00 AM)

Changes
  1. added lemmas (detail)
  2. merged (detail)
  3. tuned; (detail)
  4. removed redundant test (see also 86fac52c2795, a9fea3f11cc0); (detail)
  5. just one Presentation.State for all sessions: avoid duplication of already presented theories (very slow) and cached theory export (not very slow); (detail)
  6. proper version; (detail)
  7. back to Z3 4.4.0pre for all platforms except arm64-linux: avoid failure e.g. in Padic_Ints (AFP/7a2522dce834); (detail)
  8. less ambitious parallelism: more direct read/write saves overall heap space and GC time; (detail)
  9. slightly faster XML output: avoid too much regrowing of StringBuilder; (detail)
  10. updated NEWS: arm64-linux support is almost complete; (detail)
  11. update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux executable in Debian 9; (detail)
  12. more material for HOL-Analysis.Infinite_Sum (detail)
  13. more symbolic latex_output via XML; (detail)
  14. clarified signature; (detail)
  15. updated to polyml-5.9-610a153b941d -- close to final; (detail)
  16. tuned signature (again): latex_output is likely to depend on context; (detail)
  17. more symbolic latex output;
    discontinued Latex.output_text, which is in conflict with symbolic output; (detail)
  18. tuned signature; (detail)
  19. symbolic latex_output via XML, interpreted in Isabelle/Scala; (detail)
  20. tuned signature; (detail)
  21. clarified signature; (detail)
  22. clarified signature; (detail)
  23. clarified signature: more privacy; (detail)
  24. tuned output --- less redundancy; (detail)
  25. tuned whitespace; (detail)
  26. clarified signature: Latex.Output as parameter to Document_Build.Engine;
    tuned; (detail)
  27. proper detection of ARM platform variants; (detail)
  28. back to post-release mode; (detail)
  29. updated for release; (detail)
  30. Added tag Isabelle2021-1-RC3 for changeset 2b212c8138a5 (detail)
  31. merged (detail)
  32. updated to polyml-5.9-cc80e2b43c38, which also contains ARM64 on darwin (unused by default); (detail)
  33. clarified HTML_Context: more explicit directory structure; (detail)
  34. tuned comments; (detail)
  35. tuned; (detail)
  36. clarified signature; (detail)
  37. clarified properties: avoid empty entry; (detail)
  38. tuned signature; (detail)
Changes
  1. A slightly stronger lemma allowing slightly simpler proofs (detail)
  2. Complex_Bounded_Operators: Removed some lemmas from Extra_General that are now in Isabelle itself (detail)
  3. Elimination of all z3 calls (detail)
  4. Word_Lib sync from l4v; tweak word_eqI (detail)
  5. generalise word_eqI method; make sure it is exercised (detail)
  6. test_bit_size not longer needed; avoid potential nontermination (detail)
  7. Word_Lib tweaks for slightly more backwards compatibility (detail)
  8. use bit_simps in word_eqI method (detail)
  9. adapted to new version of Infinite_Sum in isabelle-dev (detail)
  10. avoid hardwired document output; (detail)
  11. CTR and ETTS: integration with SpecCheck: minor amendments (detail)
  12. Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL-Analysis.Infinite_Sum (detail)
  13. Banach_Steinhaus: Removed unused theory dependency Infinite_Set_Sum (detail)
  14. merge (detail)
  15. merge (detail)
  16. Merge Isabelle_C: New C11_Ast_Lib Interface, improved API's, improved doc. (detail)
  17. documentation fine-tuning. (detail)
  18. Added section on C11_Ast_Lib in chapter II. (detail)
  19. Example section restored and Documentation adapted. (detail)
  20. Stramge intermediate configuration: Example section zerschossen. (detail)
  21. Port to Isabelle2021-1 RC 2. (detail)
  22. Improved documentation. (detail)
  23. Examples for  iterator - applications: queries,  and translations into term. (detail)
  24. Rearranging standard root store; better documentation in C_Command. (detail)
  25. Rearranging the ML _programming Example Section C1. (detail)
  26. reorg 1 (detail)
  27. ... (detail)
  28. Improved Standard Interface to C11: Better signatures, a CEnv signature, C11 Std Ast Store (in C2.thy) (detail)
  29. Restructuring of Interfaces; more show cases. (detail)
  30. Updated meta-data for Optics (detail)
  31. Additional scene laws (detail)
  32. Branch merge (detail)
  33. Improved support for code generation, fixed a few bugs, and added a tactic to aid proof goal presentation of lens variables. (detail)
  34. feat(SpecCheck/Show) add parentheses for option SOME case (detail)
  35. merged (detail)
  36. weakened ordering requirements (detail)
  37. used well-founded pre-order in standard redundancy criterions (detail)
  38. derived refutational completeness from finitary and non-finitary standard redundancy criterion (detail)
  39. merge (detail)
  40. deleted incomplete methods for polynomial factorization or root computation in Algebraic-Numbers, since
    they are now available as complete methods in Factor-Algebraic-Polynomial (detail)
  41. factor_complex_poly delivers distinct list (detail)
  42. merged (detail)
  43. Removal of material that's going to be in Isabelle2021-1 (detail)
  44. merge (detail)
  45. refactoring (moving theories and lemmas around) (detail)
  46. sync from l4v (detail)
  47. adjusted Factor_Algebraic_Polynomial to Isabelle/devel (and Isabelle 2021-1, RC3) (detail)
  48. merge of afp-2021 (detail)
  49. new entry PAL (detail)
  50. new entry Factor_Algebraic_Polynomial (detail)
  51. merge from afp-2021 (detail)
  52. document `publish -` (detail)
  53. changed affiliation of eberl (this time properly) (detail)
  54. changed affiliation of Eberl (detail)
  55. sitegen for Real_Power (detail)
  56. new entry Real_Power (detail)
  57. New entry Szemeredi_Regularity (detail)
  58. tuned proofs -- avoid z3; (detail)

Started by timer

This run spent:

  • 0.11 sec waiting;
  • 16 hr build duration;
  • 16 hr total from scheduled to completion.
Revision: b61bd2c12de33999811106ae82bbc042e71b4bd6
Revision: 1fe98b11c66654d2724163fdbe6be28005b397f2