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

1. merged (detail)
2. tuned (thanks to J. Villadsen) (detail)
3. added padding to Mirabelle's output (detail)
4. merged (detail)
5. tuned generation of TPTP with $ite/$let in higher-order logics (detail)
6. tuned generation of TPTP with $ite in function position (detail)
7. tuned TPTP generation of If helper facts (detail)
8. merged (detail)
9. clarified signature: prefer static operations; (detail)
10. clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources; (detail)
11. more robust; (detail)
12. tuned signature; (detail)
13. clarified signature: more explicit class Entity_Context with private state + operations; (detail)
14. more hyperlinks, notably internal fact references; (detail)
15. Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.14UUXO (detail)
16. A tiny bit of tidying connected with Zorn's Lemma (detail)
17. tuned; (detail)
18. tuned; (detail)
19. proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition); (detail)
20. revert temporary workaround 6d111935299c; (detail)
21. added lemma (detail)
22. merged (detail)
23. tuned attributes to avoid looping (detail)
24. added eq_iff_swap for creating symmetric variants of thms; applied it in List. (detail)
25. tuned text; (detail)
26. more robust timeout, following df4449c6eff1; (detail)
27. more accurate Files.isRegularFile, exclude directories (e.g. jar_path); (detail)
28. proper java_version for isabelle_setup; (detail)
29. explicit option metric_argo_timeout, with reasonable default for Raspberry Pi; (detail)
30. tuned; (detail)
31. repackage minisat-2.2.1 with cygwin1.dll: required to run the executable without existing Cygwin context (normally provided by bash_process); (detail)
32. discontinued redundant document_preprocessor: in the worst case, a plain-old document/build script will do; (detail)
33. clarified messages, depending on option "document_echo"; (detail)
34. just one cache, via HTML_Context, via Sessions.Store or Session; (detail)
35. merged (detail)
36. new lemmas about convex, concave functions, + tidying (detail)
37. proper support for arm64; (detail)
38. no perl (amending 59ef23ac81ab); (detail)
39. merged (detail)
40. Added tag Isabelle2021-1-RC2 for changeset b92b5a57521b (detail)
41. merged (detail)
42. Preserve variable name z in VAR {z = t} (detail)
43. back to scala-2.13.5: avoid crash of Scala REPL on arm64-darwin; (detail)
44. updated to polyml-5.9-5d4caa8f7148, which also contains ARM64 on darwin (unused by default); (detail)
45. more precise URL (detail)
46. tuned page breaks (detail)

1. CTR and ETTS: integration with SpecCheck (detail)
2. used antiquotation to fix LaTeX failure (detail)
3. adapted to devel (detail)
4. updated to devel (detail)
5. merged (detail)
6. tuned proof for devel (detail)
7. clarified quotes vs. apostrophes vs. primes; (detail)
8. more accurate use of LaTeX ndash; (detail)
9. prefer portable LaTeX mdash; (detail)
10. tuned whitespace --- removed suspicious Unicode; (detail)
11. proper Unix linefeeds; (detail)
12. changed affiliation of eberl (this time properly) (detail)
13. changed affiliation of eberl (detail)
14. added author to Saturation_Framework_Extensions (detail)
15. derived calculus_with_standard_redundancy lemmas from calculus_with_finitary_standard_redundancy (detail)
16. added locale calculus_with_finitary_standard_redundancy (detail)
17. 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)
18. feat(SpecCheck) add better unit tests facilities, examples and exceptions property (detail)
19. discontinued somewhat pointless and slightly outdated document_preprocessor (after consultation with the author); (detail)
20. Correctness_Algebras: increase nitpick timeout (detail)
21. CZH: dagger monoidal categories (detail)
22. update it Isabelle/925b46043b84 (detail)
23. merge from afp-2021 (detail)
24. sitegen for Registers (detail)
25. new entry Registers (detail)

Started by timer

This run spent:

• 0.11 sec waiting;
• 19 hr build duration;
• 19 hr total from scheduled to completion.