Skip to content
[Jenkins]Jenkins
log in
Started 1 mo 1 day ago
Took 4 hr 53 min on workermta1
Failed

#33 (Mar 26, 2024, 9:21:19 PM)

Changes
  1. merged (detail / hgweb)
  2. sitegen for Continued_Fractions (detail / hgweb)
  3. New entry "Continued_Fractions" (detail / hgweb)
  4. sitegen for Approximate_Model_Counting (detail / hgweb)
  5. tuned (removing warnings) (detail / hgweb)
  6. new entry Approximate_Model_Counting (detail / hgweb)
  7. Go: website updates (detail / hgweb)
  8. Go submission (detail / hgweb)
  9. adapt to Isabelle/11a1f4d7af51; (detail / hgweb)
  10. use emph instead of italic; (detail / hgweb)
  11. tuned; (detail / hgweb)
  12. clarified names; (detail / hgweb)
  13. tuned lemmas (detail / hgweb)
  14. merged (detail / hgweb)
  15. removed stuff moved to the Isabelle distribution (detail / hgweb)
  16. avoid java.net.URL, following Isabelle/a4118f530263; (detail / hgweb)
  17. updated: standard Borel (detail / hgweb)
  18. use time_fun command (detail / hgweb)
  19. merged (detail / hgweb)
  20. Splay tree analysis now uses time_fun command (detail / hgweb)
  21. tuned proofs to reduce verification time following Isabelle/7735645667f0 (detail / hgweb)
  22. merge (detail / hgweb)
  23. feat(Transport) major improvement of overloaded properties + new relational properties (detail / hgweb)
  24. fix(ML_Unification) replace binders before aeconv (avoids lowering) (detail / hgweb)
  25. feat(ML_Unification) add simplification+unification unifier; fix context merge bug for uhints; cleaner code (detail / hgweb)
  26. merged (detail / hgweb)
  27. adapted to new definition of wf following Isabelle/033f90dc441d (detail / hgweb)
  28. merged (detail / hgweb)
  29. Two new lemmas by Eberl (requested by Paulson) (detail / hgweb)
  30. adapted to isabelle/devel (detail / hgweb)
  31. adapted to new definition of wfP following Isabelle/233d70cad0cf (detail / hgweb)
  32. updated url (detail / hgweb)
  33. merged (detail / hgweb)
  34. tuned proof (detail / hgweb)
  35. Patching some proofs, for of_nat_int_ceiling (detail / hgweb)
  36. Deletion of material that had been moved to the distribution (detail / hgweb)
  37. Multirelations_Heterogeneous: further results for convex-closure (detail / hgweb)
  38. added some material about the Laurent expansion of zeta (detail / hgweb)
  39. Remove stuff following Isabelle/d0205dde00bb and related changesets (detail / hgweb)
  40. fixed broken definitions and proofs following Isabelle/8d153846f65f (detail / hgweb)
  41. Universal_Hash_Families: Remove accidental duplication of pmf_of_set_prod_eq. (detail / hgweb)
  42. Inserted a corollary to the main result (detail / hgweb)
  43. Updated a proof to the new formalisation of meromorphic (detail / hgweb)
  44. Relational_Cardinality: minor revision (detail / hgweb)
  45. adapted to Isabelle/2746dfc9ceae; (detail / hgweb)
  46. merge (detail / hgweb)
  47. adjusting HOL-CSP_OpSem from 2023 to devel (detail / hgweb)
  48. merge from AFP 2023 (detail / hgweb)
  49. metadata for HOL-CSP OpSem and sitegen (detail / hgweb)
  50. new entry: HOL-CSP OpSem (detail / hgweb)
  51. removed lemmas following Isabelle/ba8fb71587ae (detail / hgweb)
  52. merge from AFP 2023 (detail / hgweb)
  53. sitegen for Wieferich Kempner (detail / hgweb)
  54. new entry: Wieferich Kempner (detail / hgweb)
  55. merge from AFP 2023 (detail / hgweb)
  56. metadata and sitegen for QBF-Solver (detail / hgweb)
  57. new entry: QBF_Solver_Verification (detail / hgweb)
  58. further files for CubicalCategories (detail / hgweb)
  59. New entry CubicalCategories (detail / hgweb)
  60. update doc; (detail / hgweb)
  61. Correction of an error in the abstract (detail / hgweb)
  62. sitegen for Karatsuba (detail / hgweb)
  63. New submission: Karatsuba (detail / hgweb)
  64. adjusted proof (detail / hgweb)
  65. more accurate timeout;
    tuned whitespace; (detail / hgweb)
  66. move multiset lemmas into distro (detail / hgweb)
  67. non-executable files; (detail / hgweb)
  68. Moving library material into Analysis (Elementary_Metric_Spaces and Set_Integration) (detail / hgweb)
  69. New version consistent with paper (detail / hgweb)
  70. tuned proof: avoid z3 to make it work on arm64-linux; (detail / hgweb)
  71. tuned proof: avoid z3 to make it work on arm64-linux; (detail / hgweb)
  72. tuned proof: avoid z3 to make it work on arm64-linux; (detail / hgweb)
  73. tuned proof: avoid z3 to make it work on arm64-linux; (detail / hgweb)
  74. tuned whitespace; (detail / hgweb)
  75. tuned proof: avoid z3 to make it work on arm64-linux; (detail / hgweb)
  76. tuned whitespace; (detail / hgweb)
  77. backed out changeset ddf90847bfa5: still requires approx. 8-10h elapsed time / 50h CPU time on common test hardware (see 13b3e24a71b0), only latest x86_64-linux hardware is reasonably fast (3.5h elapsed time, 20h CPU time seen on of1.proof.cit.tum.de), but arm64-darwin is very slow; (detail / hgweb)
  78. tuned signature, following Isabelle/da4e82434985; (detail / hgweb)
  79. adapted to Isabelle/3648e9c88d0c; (detail / hgweb)
  80. Fixed a rewriting issue (detail / hgweb)
  81. Resolved a syntax clash involving Equipollence (now imported by Ramsey) (detail / hgweb)
  82. enable proof in session Lorenz_C1 (detail / hgweb)
  83. simplified proofs (detail / hgweb)
  84. simplified proof (detail / hgweb)
  85. Incorporating library material from AFP sessions (detail / hgweb)
  86. avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic (detail / hgweb)
  87. merged (detail / hgweb)
  88. Removed numerous z3 calls and tried to simplify some extremely messy proofs (detail / hgweb)
  89. Adjustments for recent changes to the main repository (detail / hgweb)
  90. A little tidying up. Removed some smt calls (detail / hgweb)
  91. avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic (detail / hgweb)
  92. tuned proofs (detail / hgweb)
  93. Simpl: remove stray thm command (detail / hgweb)
  94. CRYSTALS-Kyber_Security: adapt to isabelle@cff4576218fa (detail / hgweb)
  95. Interval_Analysis: adapt to isabelle@cff4576218fa (detail / hgweb)
  96. merge from afp-2023 (detail / hgweb)
  97. update Simpl entry; change license to BSD

    (submission by Norbert Schirmer) (detail / hgweb)
  98. sitegen for IMP_Noninterference (detail / hgweb)
  99. New entry IMP_Noninterference (detail / hgweb)
  100. sitegen for Sumcheck Protocol (detail / hgweb)
  101. new entry Sumcheck Protocol (detail / hgweb)
  102. New entry OmegaCatoidsQuantales (detail / hgweb)
  103. New submission Region_Quadtrees (detail / hgweb)
  104. sitegen and metadata for Isabelle_hoops (detail / hgweb)
  105. New entry Isabelle_hoops (with its name standardised) (detail / hgweb)
  106. sitegen and metadata for Interval_Analysis (detail / hgweb)
  107. New submission Interval_Analysis (detail / hgweb)
  108. New entry CRYSTALS-Kyber_Security (detail / hgweb)
  109. proper Homepage comparison: URL equals does not fulfil specification; (detail / hgweb)
  110. A lot of tidying (detail / hgweb)
  111. merged (detail / hgweb)
  112. Tidied up some messy proofs (detail / hgweb)
  113. Cleaning and simplifying notation (detail / hgweb)
  114. A little tidying. Removal of z3 smt calls (detail / hgweb)
  115. formally normalized definition of singleton shifts to their primitive form (detail / hgweb)
  116. Integration syntax (detail / hgweb)
  117. Importation of the infinite type class (detail / hgweb)
  118. the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now  requires parentheses (detail / hgweb)
  119. Moving a few facts from libraries into the main repository (detail / hgweb)
  120. Shortening some proofs (detail / hgweb)
  121. Correcting misleading notation (detail / hgweb)
  122. simplified class specification (detail / hgweb)
  123. more realistic timeouts; (detail / hgweb)
  124. Borrowed prod_mono_strict' for the distribution; adjusted proofs (detail / hgweb)
  125. merged (detail / hgweb)
  126. added lifting of forward simulation to transitive closure (detail / hgweb)
  127. Renamed a theorem involving convexity (detail / hgweb)
  128. Updated a proof for the corrected version of convex_on (detail / hgweb)
  129. Made the proof slightly more explicit (detail / hgweb)
  130. Fixed a problem involving sum_diff_split (detail / hgweb)
  131. New lemmas and renaming of lemmas (detail / hgweb)
  132. feat(ML_Unification,Transport) more robust unification + new unifiers (detail / hgweb)
  133. strengthened class parity (detail / hgweb)
  134. "Moving up" AFP library material to more appropriate places (detail / hgweb)
  135. merged (detail / hgweb)
  136. Simplification of some of the lemma libraries (detail / hgweb)
  137. merged (detail / hgweb)
  138. use define_time_function (detail / hgweb)
  139. common type class for trivial properties on div/mod (detail / hgweb)
  140. Expander_Graphs: Add additional tail bound for expander random walks. (detail / hgweb)
  141. rearranged and reformulated abstract classes for bit structures and operations (detail / hgweb)
  142. Universal_Hash_Families and Expander_Graphs: Framework for pseudorandom objects

    Pseudorandom objects as a combinator library was formerly incorrectly part of the Distribtued_Distinct_Elements
    AFP entry due to chronological reasons. But it belongs conceptually to the Universal_Hash_Families and
    Expander_Graphs entries, which this patch accomplishes.

    Compared to the former development in DDE the new framework also includes several improvements:
    - Constructive implementation of hash families
    - An object is always non-empty - this means every object induces naturally a PMF, which removes a lot of
       constraints from the theorems.

    Note: The theory DDE/Pseudorandom_Combinators is now obsolete. I will remove it shortly before the next release
    (to minimize the possibility of merge-conflicts). (detail / hgweb)
  143. tuned signature; (detail / hgweb)
  144. adapted to Isabelle/c7a98469c0e7; (detail / hgweb)
  145. Frequency_Moments and Expander_Graphs: Change the dependency between the entries.

    The dependency of Expander_Graphs to Frequency_Moments was due to the use of some auxiliary
    results (in particular those about HOL-Probability.Product_PMF).
    This change moves those to Universal_Hash_Families, so that the dependency
    can be avoided.

    Note: I added aliases and abbreviations to minimize the risk of merge-conflicts.

    This change will enable the introduction of further additional examples, that
    show how Expander Graphs can be used to further improve the space complexity
    of the verified algorithms in Frequency_Moments. (detail / hgweb)
  146. merge (detail / hgweb)
  147. feat(ML_Unification) fix exceptions and improve experience wrt. flex-flex instantiations (detail / hgweb)
  148. Universal_Hash_Families: Remove duplicate proofs (caused by previous commit.) (detail / hgweb)
  149. Finite_Fields: Add exectuable algorithms for the construction of (and calculation in) finite fields. (detail / hgweb)
  150. Finite Fields: Minor improvements to previous commit. (detail / hgweb)
  151. Finite_Fields: Add Rabin's test for the irreducibility of polynomials. (detail / hgweb)
  152. Finite Fields: Add more general lower estimate for cardinality of irreducible polynomials. (detail / hgweb)
  153. Distributed_Distinct_Elements: Add related entries. (detail / hgweb)
  154. Frequency_Moments: Remove duplication of lemmas from Concentration_Inequalities. (detail / hgweb)
  155. Renamed a theorem (detail / hgweb)
  156. streamlined type class specification (detail / hgweb)
  157. consolidated lemma name (detail / hgweb)
  158. simplified specification of type class (detail / hgweb)
  159. consolidated name of lemma analogously to nat/int/word_bit_induct (detail / hgweb)
  160. tuned finite proofs (detail / hgweb)
  161. merged (detail / hgweb)
  162. adapted to Isabelle/7d10708bbc32; (detail / hgweb)
  163. adapted to isabelle/devel (detail / hgweb)
  164. Relational_Disjoint_Set_Forests: minor revision (detail / hgweb)
  165. more realistic timeout; (detail / hgweb)
  166. fix(ML_Unification) use cartouches to fix document build error (detail / hgweb)
  167. feat(ML_Unification) more explanation (detail / hgweb)
  168. merge (detail / hgweb)
  169. feat(Transport) better relativised concept definitions and lemmas (detail / hgweb)
  170. feat(ML_Unification) add recursive unification hints fallback option (detail / hgweb)
  171. CZH_Foundations: integration with Cardinality_Continuum (detail / hgweb)
  172. tuned; (detail / hgweb)
  173. tuned; (detail / hgweb)
  174. adapted to Isabelle/e1895596e1b9; (detail / hgweb)
  175. adapted to Isabelle/c6c2e41cac1c; (detail / hgweb)
  176. proper terminology; (detail / hgweb)
  177. removed outdated comments; (detail / hgweb)
  178. adapted to Isabelle/70c0dbfacf0b; (detail / hgweb)
  179. tuned; (detail / hgweb)
  180. tuned, following Isabelle/8c9cce335a3d; (detail / hgweb)
  181. tuned; (detail / hgweb)
  182. tuned; (detail / hgweb)
  183. tuned; (detail / hgweb)
  184. tuned; (detail / hgweb)
  185. tuned; (detail / hgweb)
  186. tuned, following Isabelle/e7796c55d840; (detail / hgweb)
  187. Hello_World: add some descriptive text (detail / hgweb)
  188. Introduced definition for the sigma algebra at infinity for a filtration. (detail / hgweb)
  189. Fixed issue that caused Martingales to not compile. Sorry! (detail / hgweb)
  190. re-introduce code in session of Hello_World (detail / hgweb)
  191. adapted to Isabelle/032a31db4c6f; (detail / hgweb)
  192. adjusted HOL-CSPM from 2023 to development (Patch.thy might need further cleanup) (detail / hgweb)
  193. Updated entry Martingales. (detail / hgweb)
  194. adapted Disintegration to devel (detail / hgweb)
  195. adapted to isabelle-dev; (detail / hgweb)
  196. adjusted Concentration Inequalities from 2023 to devel (detail / hgweb)
  197. merge from AFP 2023 (detail / hgweb)
  198. tuned (detail / hgweb)
  199. New entry KnuthMorrisPratt (detail / hgweb)
  200. metadata and sitegen (detail / hgweb)
  201. new entry: HOL-CSPM (detail / hgweb)
  202. sitegen for Martingales (detail / hgweb)
  203. new entry Martingales (detail / hgweb)
  204. sitegen for Concentration_Inequalities (detail / hgweb)
  205. new entry Concentration_Inequalities (detail / hgweb)
  206. New entry: Lambert_Series (detail / hgweb)
  207. adjusted doi capitalization (detail / hgweb)
  208. sitegen for Q0_soundness (detail / hgweb)
  209. new entry Q0_Soundness (detail / hgweb)
  210. sitegen for Cardinality_Continuum (detail / hgweb)
  211. new entry Cardinality_Continuum (detail / hgweb)
  212. Polylog web files (detail / hgweb)
  213. sitegen for Polylog (detail / hgweb)
  214. New entry: Polylog (detail / hgweb)
  215. sitegen for Polynomial_Crit_Geometry (detail / hgweb)
  216. new entry Polynomial_Crit_Geometry (detail / hgweb)
  217. sitegen for Chebyshev_Polynomials (detail / hgweb)
  218. New entry Chebyshev_Polynomials (detail / hgweb)
  219. more website for LTL and PD (detail / hgweb)
  220. website for LTL and PD (detail / hgweb)
  221. Labeled_Transition_Systems and Pushdown_Systems (detail / hgweb)
  222. New entry: Nominal_Myhill_Nerode (detail / hgweb)
  223. more doc; (detail / hgweb)
  224. sitegen for Q0_Metatheory (detail / hgweb)
  225. updated LaTeX citations (detail / hgweb)
  226. new entry Q0_Metatheory (detail / hgweb)
  227. Perfect_Fields and Elimination_Of_Repeated_Factors incl sitegen (detail / hgweb)
  228. New entry Perfect_Fields (detail / hgweb)
  229. sitegen for /Users/lp15/.isabelle/Isabelle2023/browser_info/AFP/Disintegration (detail / hgweb)
  230. New entry "Disintegration" (detail / hgweb)
  231. allow partially detecting potential name conflicts; (detail / hgweb)
  232. added check to detect potential name conflicts; (detail / hgweb)
  233. add warning for missing DOI cache; (detail / hgweb)
  234. Eudoxus_Reals patch and sitegen (detail / hgweb)
  235. New entry, Eudoxus_Reals (detail / hgweb)
  236. New entry /Hypergraph_Colourings (detail / hgweb)
  237. adapted to Isabelle/99bc2dd45111; (detail / hgweb)
  238. adapted to simplified T convention (detail / hgweb)
  239. merged (detail / hgweb)
  240. adapted to new T conventions (detail / hgweb)
  241. extracted lemma finite_progress out of proof (detail / hgweb)
  242. simplified proof (detail / hgweb)
  243. merged (detail / hgweb)
  244. tuned lift_strong_simulation_to_bisimulation (detail / hgweb)
  245. simplified definition of match_bisim (detail / hgweb)
  246. strengthened lift_strong_simulation_to_bisimulation and simplified match_bisim (detail / hgweb)
  247. adadpted to [simp] changes in distrib (detail / hgweb)
  248. de-duplicated specification of class ring_bit_operations (detail / hgweb)
  249. adjusted T_sift_down: all primitives take 0 time. (detail / hgweb)
  250. added missing file following 2702f2046afa (detail / hgweb)
  251. documented change in VeriComp (detail / hgweb)
  252. added framework-independent lemma to lift simulation to bisimulation (detail / hgweb)
  253. tuned (detail / hgweb)
  254. added publication (detail / hgweb)
  255. slightly more elementary characterization of unset_bit (detail / hgweb)
  256. base abstract specification of NOT on recursive equation rather than bit projection (detail / hgweb)
  257. more realistic timeouts for lrzcloud2:threads=1; (detail / hgweb)
  258. tuned proof (detail / hgweb)
  259. more realistic timeouts for lrzcloud2:threads=1; (detail / hgweb)
  260. operations AND, OR, XOR are specified by characteristic recursive equation (detail / hgweb)
  261. some extensions to Cotangent_PFD_Formula (detail / hgweb)
  262. slightly less technical formulation of very specific type class (detail / hgweb)

Started by an SCM change

This run spent:

  • 9.1 sec waiting;
  • 4 hr 53 min build duration;
  • 4 hr 54 min total from scheduled to completion.
Revision: 070dbf86a3c1b2a62c64a902e89add2f7e4c0c02