Started 10 mo ago
Took 3 hr 31 min on workermta1

Build #19 (Nov 26, 2021, 3:28:15 PM)

Changes
  1. fix dangerous context management (detail / hgweb)
  2. A slightly stronger lemma allowing slightly simpler proofs (detail / hgweb)
  3. Complex_Bounded_Operators: Removed some lemmas from Extra_General that are now in Isabelle itself (detail / hgweb)
  4. Elimination of all z3 calls (detail / hgweb)
  5. Word_Lib sync from l4v; tweak word_eqI (detail / hgweb)
  6. generalise word_eqI method; make sure it is exercised (detail / hgweb)
  7. test_bit_size not longer needed; avoid potential nontermination (detail / hgweb)
  8. Word_Lib tweaks for slightly more backwards compatibility (detail / hgweb)
  9. use bit_simps in word_eqI method (detail / hgweb)
  10. adapted to new version of Infinite_Sum in isabelle-dev (detail / hgweb)
  11. avoid hardwired document output; (detail / hgweb)
  12. CTR and ETTS: integration with SpecCheck: minor amendments (detail / hgweb)
  13. Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL-Analysis.Infinite_Sum (detail / hgweb)
  14. Banach_Steinhaus: Removed unused theory dependency Infinite_Set_Sum (detail / hgweb)
  15. merge (detail / hgweb)
  16. merge (detail / hgweb)
  17. Merge Isabelle_C: New C11_Ast_Lib Interface, improved API's, improved doc. (detail / hgweb)
  18. documentation fine-tuning. (detail / hgweb)
  19. Added section on C11_Ast_Lib in chapter II. (detail / hgweb)
  20. Example section restored and Documentation adapted. (detail / hgweb)
  21. Stramge intermediate configuration: Example section zerschossen. (detail / hgweb)
  22. Port to Isabelle2021-1 RC 2. (detail / hgweb)
  23. Improved documentation. (detail / hgweb)
  24. Examples for  iterator - applications: queries,  and translations into term. (detail / hgweb)
  25. Rearranging standard root store; better documentation in C_Command. (detail / hgweb)
  26. Rearranging the ML _programming Example Section C1. (detail / hgweb)
  27. reorg 1 (detail / hgweb)
  28. ... (detail / hgweb)
  29. Improved Standard Interface to C11: Better signatures, a CEnv signature, C11 Std Ast Store (in C2.thy) (detail / hgweb)
  30. Restructuring of Interfaces; more show cases. (detail / hgweb)
  31. Updated meta-data for Optics (detail / hgweb)
  32. Additional scene laws (detail / hgweb)
  33. Branch merge (detail / hgweb)
  34. Improved support for code generation, fixed a few bugs, and added a tactic to aid proof goal presentation of lens variables. (detail / hgweb)
  35. feat(SpecCheck/Show) add parentheses for option SOME case (detail / hgweb)
  36. merged (detail / hgweb)
  37. weakened ordering requirements (detail / hgweb)
  38. used well-founded pre-order in standard redundancy criterions (detail / hgweb)
  39. derived refutational completeness from finitary and non-finitary standard redundancy criterion (detail / hgweb)
  40. merge (detail / hgweb)
  41. 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 / hgweb)
  42. factor_complex_poly delivers distinct list (detail / hgweb)
  43. merged (detail / hgweb)
  44. Removal of material that's going to be in Isabelle2021-1 (detail / hgweb)
  45. merge (detail / hgweb)
  46. refactoring (moving theories and lemmas around) (detail / hgweb)
  47. sync from l4v (detail / hgweb)
  48. adjusted Factor_Algebraic_Polynomial to Isabelle/devel (and Isabelle 2021-1, RC3) (detail / hgweb)
  49. merge of afp-2021 (detail / hgweb)
  50. new entry PAL (detail / hgweb)
  51. new entry Factor_Algebraic_Polynomial (detail / hgweb)
  52. merge from afp-2021 (detail / hgweb)
  53. document `publish -` (detail / hgweb)
  54. changed affiliation of eberl (this time properly) (detail / hgweb)
  55. changed affiliation of Eberl (detail / hgweb)
  56. sitegen for Real_Power (detail / hgweb)
  57. new entry Real_Power (detail / hgweb)
  58. New entry Szemeredi_Regularity (detail / hgweb)
  59. tuned proofs -- avoid z3; (detail / hgweb)
  60. CTR and ETTS: integration with SpecCheck (detail / hgweb)
  61. used antiquotation to fix LaTeX failure (detail / hgweb)
  62. adapted to devel (detail / hgweb)
  63. updated to devel (detail / hgweb)
  64. merged (detail / hgweb)
  65. tuned proof for devel (detail / hgweb)
  66. clarified quotes vs. apostrophes vs. primes; (detail / hgweb)
  67. more accurate use of LaTeX ndash; (detail / hgweb)
  68. prefer portable LaTeX mdash; (detail / hgweb)
  69. tuned whitespace --- removed suspicious Unicode; (detail / hgweb)
  70. proper Unix linefeeds; (detail / hgweb)
  71. changed affiliation of eberl (this time properly) (detail / hgweb)
  72. changed affiliation of eberl (detail / hgweb)
  73. added author to Saturation_Framework_Extensions (detail / hgweb)
  74. derived calculus_with_standard_redundancy lemmas from calculus_with_finitary_standard_redundancy (detail / hgweb)
  75. added locale calculus_with_finitary_standard_redundancy (detail / hgweb)
  76. Registers:
    - Added mechanism for raising errors if autogenerated files need updating
    - Changed definition of Axioms_Quantum.register_pair (returns 0 for incompatible registers, see register_pair_is_register_converse for a useful consequence)
    - Slightly reducing namespace pollution in Classical_Extra (hiding consts x, y, X, Y etc.) (detail / hgweb)
  77. feat(SpecCheck) add better unit tests facilities, examples and exceptions property (detail / hgweb)
  78. discontinued somewhat pointless and slightly outdated document_preprocessor (after consultation with the author); (detail / hgweb)
  79. Correctness_Algebras: increase nitpick timeout (detail / hgweb)
  80. CZH: dagger monoidal categories (detail / hgweb)
  81. update it Isabelle/925b46043b84 (detail / hgweb)
  82. merge from afp-2021 (detail / hgweb)
  83. sitegen for Registers (detail / hgweb)
  84. new entry Registers (detail / hgweb)
  85. Correctness_Algebras: increase session timeout (detail / hgweb)
  86. tuned signature, according to Isabelle/df12779c3ce8; (detail / hgweb)
  87. feat(SpecCheck) add possibility to make builds fail on failure and extend README (detail / hgweb)
  88. added missing funding information (detail / hgweb)
  89. restored theory structure for simple genericity. (detail / hgweb)
  90. Backed out changeset af549be0a8cd (detail / hgweb)
  91. restored different entrance points a before Isabelle2021 (detail / hgweb)
  92. proper parentheses (amending 354560d7143a); (detail / hgweb)
  93. Adjusted to prospective release Isabelle2021-2. (detail / hgweb)
  94. Correctness_Algebras: uncomment counterexamples (detail / hgweb)
  95. clarified identity of theory data: avoid accidental pointer_eq, use equality on unique serial instead; (detail / hgweb)
  96. clarified identity of theory data: pointer_eq is not well-defined (and fails on ARM64), use equality on unique serial instead; (detail / hgweb)
  97. merge from afp-2021 (detail / hgweb)
  98. remove unused functions (detail / hgweb)
  99. silence sitegen warning (detail / hgweb)
  100. new entry X86_Semantics (detail / hgweb)
  101. adjust to isabelle@549019b4a808 (detail / hgweb)
  102. merge from afp-2021 (detail / hgweb)
  103. metadata for Belief_Revision (detail / hgweb)
  104. new entry Belief_Revision (detail / hgweb)
  105. New entry Correctness_Algebras (detail / hgweb)
  106. prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms; (detail / hgweb)
  107. updated metadata for Count_Complex_Roots (detail / hgweb)
  108. corrected the timeout for CZH_Universal_Constructions (detail / hgweb)
  109. CZH: further results about comma categories and Kan extensions, a variety of other minor amendments (detail / hgweb)
  110. more generic bit/word lemmas for distribution (detail / hgweb)
  111. Fixing a name clash between two different "restrict" operators (detail / hgweb)
  112. Merged (detail / hgweb)
  113. solved the roots-on-the-border problem (detail / hgweb)
  114. split Count_Complex_Roots (detail / hgweb)
  115. more realistic timeout; (detail / hgweb)
  116. clarified signature, according to Isabelle/ccf599864beb; (detail / hgweb)
  117. back to dedicated separate shift operations for infix syntax;
    more default simp rules on closed numeric expressions (detail / hgweb)

Started by an SCM change

This run spent:

  • 2 hr 22 min waiting;
  • 3 hr 31 min build duration;
  • 5 hr 53 min total from scheduled to completion.
Revision: a2b3a17e295d965452d2b62c0e07f3a807dbafd1