Skip to content
Started 2 yr 5 mo ago
Took 3 hr 9 min on workermta1
Success

#18 (Oct 22, 2021, 5:09:13 PM)

Changes
  1. modify JinjaDCI (detail / hgweb)
  2. Merged. (detail / hgweb)
  3. Various tuning that for some reason didn't get merged from my master branch. (detail / hgweb)
  4. A spot of polishing (detail / hgweb)
  5. Merged. (detail / hgweb)
  6. Update metadata to reflect changes made in July, 2021. (detail / hgweb)
  7. Add a revision note concerning material added in July, 2021. (detail / hgweb)
  8. tuned signature, according to Isabelle/042041c0ebeb; (detail / hgweb)
  9. Merged. (detail / hgweb)
  10. Sync with my development repo. (detail / hgweb)
  11. Adjust Imperative List/Map/Set Specification for more lenient next operation

    This allows implementations of this iterator specification to make use of
    temporary variables for obtaining the next element of the list/set/map.
    This is required by some and especially more general iterators. (detail / hgweb)
  12. discontinued obsolete "val extend = I" for data slots; (detail / hgweb)
  13. tuned; (detail / hgweb)
  14. merged (detail / hgweb)
  15. metadata update for MFODL_Monitor_Optimized (detail / hgweb)
  16. fixed a mistake in MFODL_Monitor_Optimized (detail / hgweb)
  17. merge (detail / hgweb)
  18. adjusted Virtual-Substitution from 2021 to devel (detail / hgweb)
  19. merge of AFP 2021 (detail / hgweb)
  20. fixed duplicate "and" (detail / hgweb)
  21. sitegen for Virtual_Substitution (detail / hgweb)
  22. new entry: Virtual Substitution (detail / hgweb)
  23. updated website/email address (detail / hgweb)
  24. modify JinjaDCI (detail / hgweb)
  25. modifications in Jinja and DOminance_CHK (detail / hgweb)
  26. modifications in Jinja and Dominance_CHK (detail / hgweb)
  27. merged (detail / hgweb)
  28. adapted to Term.dest_abs_global / Logic.dest_all_global (e.g. Isabelle/f07761ee5a7f); (detail / hgweb)
  29. more accurate treatment of context; (detail / hgweb)
  30. more accurate treatment of context; (detail / hgweb)
  31. more accurate treatment of context; (detail / hgweb)
  32. tuned -- proper names/scopes for contexts; (detail / hgweb)
  33. tuned proofs; (detail / hgweb)
  34. more accurate treatment of context; (detail / hgweb)
  35. more accurate treatment of context; (detail / hgweb)
  36. proper antiquotations; (detail / hgweb)
  37. tuned messages; (detail / hgweb)
  38. more maintainable Isabelle/ML: proper signatures, proper names/scopes for contexts;
    tuned whitespace; (detail / hgweb)
  39. dead code!? (detail / hgweb)
  40. clarified signature, following Isabelle/de4f151c2a34; (detail / hgweb)
  41. modifications in Jinja and Dominance_CHK (detail / hgweb)
  42. CZH: large limits, generalizations, a variety of minor amendments (detail / hgweb)
  43. Simplified a definition (detail / hgweb)
  44. modify propa (detail / hgweb)
  45. bit singleton shifts recovered for the sake of backward compatibility (detail / hgweb)
  46. updated to 7422950f3955 (detail / hgweb)
  47. merge (detail / hgweb)
  48. EPO: simplify proof (detail / hgweb)
  49. primer (detail / hgweb)
  50. more complete simp rules (detail / hgweb)
  51. more complete simp rules (examples) (detail / hgweb)
  52. avoid overaggressive contraction of conversions (detail / hgweb)
  53. slightly more prominence for proof tools; more examples (detail / hgweb)
  54. ETTS: minor amendments (detail / hgweb)
  55. CTR and ETTS: integration with fd5f62176987 (detail / hgweb)
  56. adapted QHLProver to isabelle-dev/409ca22dee4c (detail / hgweb)
  57. adapted to isabelle-dev/409ca22dee4c (detail / hgweb)
  58. adapted to devel (detail / hgweb)
  59. Complex_Bounded_Operators: update to isabelle@ffb15f7f26d5 (detail / hgweb)
  60. Weighted_Path_Order: update to isabelle@ffb15f7f26d5 (detail / hgweb)
  61. merge from afp-2021 (detail / hgweb)
  62. add missing session dependency (detail / hgweb)
  63. new entry FOL_Axiomatic (detail / hgweb)
  64. regen website (detail / hgweb)
  65. minor editorial changes for CZH entries (detail / hgweb)
  66. New entry Weighted_Path_Order (detail / hgweb)
  67. fxed metadata (forgot .html) in link (detail / hgweb)
  68. metadata and sitegen for complex bounded operators (detail / hgweb)
  69. new entry: Complex_Bounded_Operators (detail / hgweb)
  70. restructure resultant algorithms, so that tuned code-equations are also availalbe for integral domains (detail / hgweb)
  71. removed obselete sorted_sorted_wrt, following Isabelle/06aeb9054c07; (detail / hgweb)
  72. clarified timeout;
    tuned whitespace; (detail / hgweb)
  73. hide_lams ~> opaque_lifting; (detail / hgweb)
  74. clarified antiquotations; (detail / hgweb)
  75. proper inst table; (detail / hgweb)
  76. clarified antiquotations; (detail / hgweb)
  77. clarified antiquotations; (detail / hgweb)
  78. proper inst table; (detail / hgweb)
  79. clarified antiquotations; (detail / hgweb)
  80. clarified antiquotations; (detail / hgweb)
  81. clarified antiquotations; (detail / hgweb)
  82. clarified antiquotations; (detail / hgweb)
  83. unused; (detail / hgweb)
  84. merged (detail / hgweb)
  85. clarified antiquotations; (detail / hgweb)
  86. proper match against const_name; (detail / hgweb)
  87. tuned; (detail / hgweb)
  88. tuned; (detail / hgweb)
  89. clarified antiquotations; (detail / hgweb)
  90. clarified antiquotations; (detail / hgweb)
  91. clarified antiquotations; (detail / hgweb)
  92. fix(ci): clarified addresses, set proper TLS version; (detail / hgweb)
  93. feat(ci): remove hard-coded address; (detail / hgweb)
  94. feat(SpecCheck/Show) tune pretty printing for environments (detail / hgweb)
  95. merge (detail / hgweb)
  96. eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib" (detail / hgweb)
  97. 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 / hgweb)
  98. New entry: Dominance_CHK (detail / hgweb)
  99. Schutz_Spacetime website (detail / hgweb)
  100. new entry Schutz_Spacetime (detail / hgweb)
  101. metadata for Logging_Independent_Anonymity (detail / hgweb)
  102. new entry Logging_Independent_Anonymity (detail / hgweb)
  103. repaired slip (detail / hgweb)
  104. feat(SpecCheck) folder renaming, types for tests (detail / hgweb)
  105. tuned (detail / hgweb)
  106. mproper proof command 'guess' moved to separate theory "Pure-ex.Guess", according to Isabelle/b49bd5d9041f; (detail / hgweb)
  107. ported Design-Theory from AFP 2021 to devel (detail / hgweb)
  108. ported Three-Circles from AFP 2021 to devel (detail / hgweb)
  109. move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations into Algebraic_Numbers (detail / hgweb)
  110. ported Cubic_Quartic_Equations from AFP 2021 to devel (detail / hgweb)
  111. merge of AFP 2021 (detail / hgweb)
  112. Cubic_Quartic_Equations sitegen (detail / hgweb)
  113. new entry Cubic_Quartic_Equations (detail / hgweb)
  114. sitegen for combinatorial design theory (detail / hgweb)
  115. new entry: Combinatorial Design Theory (detail / hgweb)
  116. sitegen for Three Circles (detail / hgweb)
  117. new entry: Three Circles (detail / hgweb)
  118. clarified modules, according to Isabelle/534b231ce041; (detail / hgweb)
  119. bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax, according to Isabelle/ead56ad40e15;
    subtle change of inf (infixl "\<sqinter>" 70) vs. (infixl "\<sqinter>" 65); (detail / hgweb)
  120. clarified signature, according to Isabelle/d882abae3379; (detail / hgweb)
  121. explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell) (detail / hgweb)
  122. tuned signature, according to Isabelle/28a582aa25dd; (detail / hgweb)
  123. eliminated Specification.definition', following Isabelle/6876e3d5e362; (detail / hgweb)
  124. clarified signature: more scalable operations, according to Isabelle/c2ee8d993d6a; (detail / hgweb)
  125. clarified signature, according to Isabelle/612b7e0d6721; (detail / hgweb)
  126. tuned signature, according to Isabelle/839a6e284545; (detail / hgweb)
  127. merged (detail / hgweb)
  128. Backed out changeset ef19e4e58b8c
    restoring old argument order on synthesized formulas (detail / hgweb)
  129. avoid hardwired document; (detail / hgweb)
  130. merged (detail / hgweb)
  131. tuned signature, according to Isabelle/9d9e7ed01dbb; (detail / hgweb)
  132. clarified signature, according to Isabelle/9d9e7ed01dbb; (detail / hgweb)
  133. clarified signature, according to Isabelle/9d9e7ed01dbb; (detail / hgweb)
  134. clarified signature, according to Isabelle/9d9e7ed01dbb; (detail / hgweb)
  135. simplified, using Isabelle/ML operations; (detail / hgweb)
  136. adapted to Isabelle/36774e8af3db: cannot rely on order of instantiation for vars; (detail / hgweb)
  137. tuned whitespace; (detail / hgweb)
  138. more scalable operations; (detail / hgweb)
  139. merged (detail / hgweb)
  140. synthesized formulas have their variables permuted (detail / hgweb)
  141. merged (detail / hgweb)
  142. fixes for cardinality lemmas (detail / hgweb)
  143. proper inst table; (detail / hgweb)
  144. Graphic rendering of Relational_Method PDF files refined. (detail / hgweb)
  145. Entry Relational_Method updated. (detail / hgweb)
  146. more realistic timeout; (detail / hgweb)
  147. clarified signature; (detail / hgweb)
  148. follow Isabelle/53e28c438f96; (detail / hgweb)
  149. clarified signature, following Isabelle/a3b0fc510705; (detail / hgweb)
  150. merged (detail / hgweb)
  151. tuned (detail / hgweb)
  152. consolidation of rules for bit operations (detail / hgweb)
  153. tuned name (detail / hgweb)
  154. Fix typo (detail / hgweb)
  155. Tune references

    ... using new name of BD_Security_Compositional (detail / hgweb)
  156. Remove redundant license (detail / hgweb)
  157. more realistic timeout: approx. 5min CPU time; (detail / hgweb)
  158. cleaning up (detail / hgweb)
  159. New entry CoSMeDis (detail / hgweb)
  160. New entry CoSMed (detail / hgweb)
  161. New entry: BD_Security_Compositional (detail / hgweb)
  162. New entry: CoCon (detail / hgweb)
  163. updated to devel (detail / hgweb)
  164. merge from AFP 2021 (detail / hgweb)
  165. New entry Fresh_Identifiers (detail / hgweb)
  166. New entry: Relational_Forests (detail / hgweb)
  167. cleaning up (detail / hgweb)
  168. merged (detail / hgweb)
  169. cleaning up (detail / hgweb)
  170. Update Bounded_Deducibility_Security

    - Generalise BD Security from I/O automata to nondeterministic transition
      systems, with the former retained as an instance of the latter (renaming
      locale BD_Security to BD_Security_IO)
    - Generalise unwinding conditions to allow making more than one transition at a
      time when constructing alternative traces, giving more flexibility for
      unwinding strategies
    - Add various helper lemmas and definitions
    - Add results about the expressivity of declassification triggers vs. bounds,
      due to Thomas Bauereiss (added as author) (detail / hgweb)
  171. tuned signature, following Isabelle/069f6b2c5a07; (detail / hgweb)
  172. metadata update for MFMC_Countable (detail / hgweb)
  173. derive rel_pmf characterization from bounded and unbounded MFMC theorem (detail / hgweb)
  174. merged (detail / hgweb)
  175. drop boundedness requirement for the sink (detail / hgweb)
  176. avoid global tmp file: pointless due to implicit theory export; (detail / hgweb)
  177. repaired syntax (detail / hgweb)
  178. tuned signature, following Isabelle/d030b988d470; (detail / hgweb)
  179. generalized gt_rat_sign_change to square-free polynomials (detail / hgweb)
  180. minor updates to bibliography (detail / hgweb)
  181. clarified signature; (detail / hgweb)
  182. clarified abstract and concrete boolean algebras (detail / hgweb)
  183. antiquotation for bundles (detail / hgweb)
  184. simplified hierarchy of type classes for bit operations (detail / hgweb)
  185. restored executable conversions (detail / hgweb)
  186. dropped junk (detail / hgweb)
  187. moved theory Bit_Operations into Main corpus (detail / hgweb)
  188. organize syntax for word operations in bundles (detail / hgweb)
  189. more systematic approach for instantiation (detail / hgweb)
  190. avoid seemingly unused transfer rules (detail / hgweb)
  191. cleaner presentation of analysis theorems in preliminaries (detail / hgweb)
  192. Update to new Epistemic_Logic.thy (detail / hgweb)
  193. Avoid typedefs (detail / hgweb)
  194. Clean: set AFP standard document options (detail / hgweb)
  195. Clean: re-add to chapter AFP (detail / hgweb)
  196. merge from afp-2021 (detail / hgweb)
  197. Finitely_Generated_Abelian_Groups website (detail / hgweb)
  198. new entry Finitely_Generated_Abelian_Groups (detail / hgweb)
  199. Added Finitely_Generated_Abelian_Groups to metadata (detail / hgweb)
  200. Sync with my development repo.  Add new material: "concrete bicategories" and
    "bicategory of categories".  Change sublocale declarations related to
    functor/natural transformation/natural isomorphism to avoid issues with
    global interpretations reported by Filip Smola, 2/2/2021. (detail / hgweb)
  201. compile (detail / hgweb)
  202. more realistic timeout: 50min CPU time; (detail / hgweb)
  203. Minor changes to Finitely_Generated_Abelian_Groups, simplified and extended Dirichlet_L by depending
    on Finitely_Generated_Abelian_Groups (detail / hgweb)
  204. new entry Finitely_Generated_Abelian_Groups (detail / hgweb)
  205. remove duplicate entry in metadata (detail / hgweb)
  206. more coherent dependencies (detail / hgweb)
  207. fix(Regex_Equivalence) update to new SpecCheck version (detail / hgweb)
  208. operations for symbolic computation of bit operations (detail / hgweb)
  209. fixed Proof_Strategy_Language following Isabelle/f58108b7a60c (detail / hgweb)
  210. SpecCheck now without _ (Regex_Equivalence is still broken) (detail / hgweb)
  211. T1 fontenc for new entries (detail / hgweb)
  212. sitegen (detail / hgweb)
  213. update hide_lams -> opaque_lifting (detail / hgweb)
  214. merged from afp2021 (detail / hgweb)
  215. website for SpecCheck (detail / hgweb)
  216. new entry SpecCheck (detail / hgweb)
  217. metadata and sitegen for MiniSail (detail / hgweb)
  218. new entry: MiniSail (detail / hgweb)
  219. sitegen for Public Announcement Logic (detail / hgweb)
  220. new entry "Public Announcement Logic"
    (and sorted ROOTS + removed duplicate entries in ROOTS) (detail / hgweb)
  221. fixed a messy reference (detail / hgweb)
  222. Van_der_Waerden website (detail / hgweb)
  223. new entry Van_der_Waerden (detail / hgweb)
  224. New entry IMP_Compiler (detail / hgweb)
  225. Removal of unintended files (detail / hgweb)
  226. Hidden.thy to Isar (detail / hgweb)
  227. merged (detail / hgweb)
  228. renamed hide_lams opaque_lifting (detail / hgweb)
  229. merged (detail / hgweb)
  230. changed to opaque_lifiting as suggested by Isabelle/Jenkins (detail / hgweb)
  231. changed hide_lams for opaque_lifting as suggested by Isabelle/Jenkins (detail / hgweb)

Started by an SCM change

This run spent:

  • 8.6 sec waiting;
  • 3 hr 9 min build duration;
  • 3 hr 10 min total from scheduled to completion.
Revision: 802a16fc10b0110d9a53116484dd4a6eded92492