Started 3 days 13 hr ago
Took 1 hr 39 min on master

Success Build #135 (Jan 15, 2018 4:33:15 PM)

Changes
  1. various improvements for dictionary construction (detail / bitbucket)
  2. Removed entry from ROOT that no longer exists (detail / bitbucket)
  3. merge from afp-2017 (detail / bitbucket)
  4. more precise instructions (detail / bitbucket)
  5. removed unused thy with build problems

    (with author permission) (detail / bitbucket)
  6. PCF: add SmallStep

    also tune up existing proofs (detail / bitbucket)
  7. tune PCF proofs (detail / bitbucket)
  8. simplified; (detail / bitbucket)
  9. merged (detail / bitbucket)
  10. non-executable files; (detail / bitbucket)
  11. clarified formal comments; (detail / bitbucket)
  12. prefer formal comments;
    avoid outer verbatim token: Thy_Output.token / Antiquote.parse fails due to partitioning in operator ranges; (detail / bitbucket)
  13. clarified formal comment, based on version before 3ccb204d9c5f and educated guessing; (detail / bitbucket)
  14. prefer formal comments; (detail / bitbucket)
  15. \usepackage[normalem]{ulem} is already provided by isabelle.sty (Isabelle/efc9ec539224); (detail / bitbucket)
  16. removed old/unused clones of Isabelle distribution files; (detail / bitbucket)
  17. restored naming of lemmas after corresponding constants (detail / bitbucket)
  18. missing open-close (detail / bitbucket)
  19. tuned document; (detail / bitbucket)
  20. isabelle update_cartouches -c -t; (detail / bitbucket)
  21. prefer formal comments; (detail / bitbucket)
  22. Markov_Models: add AE_T_ev_HLD_infinite (detail / bitbucket)
  23. Markov_Models: transfer measures along a relation induced by a function (detail / bitbucket)
  24. Markov_Models: generalized coinduction rule for stream measures (detail / bitbucket)
  25. Fixed indentation (detail / bitbucket)
  26. Removed problematic smt call (detail / bitbucket)
  27. tuned (detail / bitbucket)
  28. updated to devel (detail / bitbucket)
  29. merge from afp-2017 (detail / bitbucket)
  30. update document info from metadata (detail / bitbucket)
  31. new entry: Green's theorem (detail / bitbucket)
  32. clarified theory imports; (detail / bitbucket)
  33. uniform use of Standard ML op-infix -- eliminated warnings; (detail / bitbucket)
  34. prefer formal comments; (detail / bitbucket)
  35. merged (detail / bitbucket)
  36. prefer formal comments; (detail / bitbucket)
  37. uniform inner and outer comments: isabelle update_cartouches -c; (detail / bitbucket)
  38. prefer formal comments; (detail / bitbucket)
  39. prefer formal comments; (detail / bitbucket)
  40. updated to devel (detail / bitbucket)
  41. updated to devel (detail / bitbucket)
  42. update_op (detail / bitbucket)
  43. Brought Mason_Stothers and Median_of_Medians_Selection up to speed with isabelle-dev (detail / bitbucket)
  44. merged (detail / bitbucket)
  45. Makefile is no longer needed ("isabelle afp_build HLDE" generates binary "generated/hlde" as specified in Solve_Code.thy by Florian Haftmann (detail / bitbucket)
  46. tuned proofs (detail / bitbucket)
  47. updated op's (detail / bitbucket)
  48. adapted to reverted <= syntax (detail / bitbucket)
  49. merged (detail / bitbucket)
  50. updated op syntax (detail / bitbucket)
  51. dropped more lemmas that are now already part of Main (detail / bitbucket)
  52. merged (detail / bitbucket)
  53. reuse lemmas that are now in Main (detail / bitbucket)
  54. merged (detail / bitbucket)
  55. updated to backed out infixes in Set & Ordereings (detail / bitbucket)
  56. adapted to AFP/07ea45e2d48b (detail / bitbucket)
  57. qualified imports in Taylor_Models (detail / bitbucket)
  58. merge from afp-2017 (detail / bitbucket)
  59. New entry Taylor_Models (detail / bitbucket)
  60. Falling_Factorial_Sum website (detail / bitbucket)
  61. Falling_Factorial_Sum (detail / bitbucket)
  62. website for Mason_Stothers (detail / bitbucket)
  63. new entry Mason_Stothers (detail / bitbucket)
  64. website for Median_Of_Medians_Selection; URL for Lammich (detail / bitbucket)
  65. new entry Median_Of_Medians_Selection (detail / bitbucket)
  66. tuned html (detail / bitbucket)
  67. New entry Knuth_Morris_Pratt (detail / bitbucket)
  68. Recovery after another giant fuckup (detail / bitbucket)
  69. Merge (detail / bitbucket)
  70. Stochastic_Matrices website (detail / bitbucket)
  71. new entry Stochastic_Matrices (detail / bitbucket)
  72. merged (detail / bitbucket)
  73. make Makefile work again (detail / bitbucket)
  74. website for Dirichlet_L (detail / bitbucket)
  75. merge (detail / bitbucket)
  76. (^) -> [^] in Dirichlet_L (detail / bitbucket)
  77. merge (detail / bitbucket)
  78. new submission: Dirichlet_L by Manuel Eberl (detail / bitbucket)
  79. prefer derived lemma over ad-hoc composition (detail / bitbucket)
  80. merged (detail / bitbucket)
  81. tuned proof of simple algorithm (detail / bitbucket)
  82. fixed infix problem due to new syntax (detail / bitbucket)
  83. merged (detail / bitbucket)
  84. tuned infixes (detail / bitbucket)
  85. "tl" is part of "generate"; replaced "in_" lemmas (what properties do elements of certain set satisfy) by "set_" lemmas (explicit equations to set comprehension) (detail / bitbucket)
  86. merged (detail / bitbucket)
  87. simplified definition (detail / bitbucket)
  88. tuned op's (detail / bitbucket)
  89. conversion of "op" syntax (detail / bitbucket)
  90. merged (detail / bitbucket)
  91. updated to Isabelle/998e01d6f8fd; (detail / bitbucket)
  92. merged (detail / bitbucket)
  93. tuned op's (detail / bitbucket)
  94. merged (detail / bitbucket)
  95. moved material from Euler_MacLaurin into main libraries (detail / bitbucket)
  96. renamed "lex2" to "generate_check" (detail / bitbucket)
  97. renamed "lexs" to "gen_check" (detail / bitbucket)
  98. use abbreviation "zeroes n" for "replicate n 0" (detail / bitbucket)
  99. merged (detail / bitbucket)
  100. dropped unused results (detail / bitbucket)
  101. tuned for new op syntax (detail / bitbucket)
  102. better tuning of op's (detail / bitbucket)
  103. tuned op's (detail / bitbucket)
  104. tuned op (detail / bitbucket)
  105. tuned op (detail / bitbucket)
  106. tuned op (detail / bitbucket)
  107. tuned op's (detail / bitbucket)
  108. tuned op (detail / bitbucket)
  109. tuned op (detail / bitbucket)
  110. tuned op (detail / bitbucket)
  111. tuned op's (detail / bitbucket)
  112. tuned op (detail / bitbucket)
  113. tuned op (detail / bitbucket)
  114. tuned op (detail / bitbucket)
  115. merged (detail / bitbucket)
  116. tuned op (detail / bitbucket)
  117. merged (detail / bitbucket)
  118. intermediate step via really simple algorithm (detail / bitbucket)
  119. added lemma (detail / bitbucket)
  120. tuned op (detail / bitbucket)
  121. (divides again (detail / bitbucket)
  122. collateral damage because (divides is now a token (detail / bitbucket)
  123. tuned op's (detail / bitbucket)
  124. tuned op's (detail / bitbucket)
  125. tuned op's (detail / bitbucket)
  126. tuned op's (detail / bitbucket)
  127. tuned op (detail / bitbucket)
  128. unused infix (detail / bitbucket)
  129. unused infix (detail / bitbucket)
  130. tuned op's (detail / bitbucket)
  131. restored space (detail / bitbucket)
  132. tuned op's (detail / bitbucket)
  133. tuned op's (detail / bitbucket)
  134. tuned op's (detail / bitbucket)
  135. tuned op's (detail / bitbucket)
  136. tuned op's (detail / bitbucket)
  137. tuned op's (detail / bitbucket)
  138. tuned op's (detail / bitbucket)
  139. tuned op's (detail / bitbucket)
  140. tuned op's (detail / bitbucket)
  141. tuned op's (detail / bitbucket)
  142. tuned op's (detail / bitbucket)
  143. tuned op's (detail / bitbucket)
  144. tuned op's (detail / bitbucket)
  145. tuned ops (detail / bitbucket)
  146. tuned op (detail / bitbucket)
  147. tuned op (detail / bitbucket)
  148. tuned op's (detail / bitbucket)
  149. tuned op (detail / bitbucket)
  150. tuned op's (detail / bitbucket)
  151. tuned op's (detail / bitbucket)
  152. tuned op (detail / bitbucket)
  153. tuned op (detail / bitbucket)
  154. tuned op (detail / bitbucket)
  155. reanedm (^) to [^] (detail / bitbucket)
  156. dropped "value" command (detail / bitbucket)
  157. proper computations and evaluators (detail / bitbucket)
  158. dropped superfluous use of Code_Char (detail / bitbucket)
  159. perfer official conversion in coercion (detail / bitbucket)
  160. removed superfluous import (detail / bitbucket)
  161. use new BNF-based datatypes in Nominal2 (detail / bitbucket)
  162. change dead email address (detail / bitbucket)
  163. eliminated suspicious Unicode characters -- using ambiguous notation; (detail / bitbucket)
  164. eliminated suspicious Unicode characters; (detail / bitbucket)
  165. proper use of @{cite}; (detail / bitbucket)
  166. proper bibtex entries; (detail / bitbucket)
  167. simplified ROOT: imports from other sessions are already excluded from document; (detail / bitbucket)
  168. more accurate timeout; (detail / bitbucket)
  169. Repaired some very fragile proofs (detail / bitbucket)
  170. Some changes to Dirichlet series etc. (detail / bitbucket)
  171. removed duplicate theorem (detail / bitbucket)
  172. corrected definition of mat_of_cols_list (mistake spotted by Dominique Unruh) (detail / bitbucket)
  173. More on Dirichlet series and the zeta function (detail / bitbucket)

Started by an SCM change

This run spent:

  • 5.8 sec waiting in the queue;
  • 1 hr 39 min building on an executor;
  • 1 hr 39 min total from scheduled to completion.
Revision: cda7cc51c3304f7fdc30e589489d93a0bf154da9
[Phase] - main
afp_testboard-afpbuild #135( 1 hr 39 min ) Console Output