#2060 (Sep 10, 2022, 1:33:13 AM)

Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

1. clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge; (detail)
2. unused; (detail)
3. update for release; (detail)
4. tuned: prefer Scala Regex operations; (detail)
5. tuning and updates for release; (detail)
6. NEWS; (detail)
7. discontinued somewhat pointless option: Proof_Display.pretty_goal_inst should always work smoothly (and not crash unexpectedly); (detail)
8. give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results; (detail)
9. merged (detail)
10. discontinue fragile operations; (detail)
11. proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options); (detail)
12. enable show_goal_inst by default: match failure is merely a warning (see 730638d4e37a); (detail)
13. updated documentation; (detail)
14. support multiple sessions, with cumulative errors;
    tuned command usage; (detail)
15. support regex patterns on messages; (detail)
16. support Pretty.unformatted, similar to ML version; (detail)
17. removed odd TODO item (see 3391a493f39a); (detail)
18. tuned signature; (detail)
19. tuned output: more Pretty.item; (detail)
20. tuned signature; (detail)
21. clarified failure: warning for logical error, exception for program breakdown; (detail)
22. print goal instantiation for global qed (and variations); (detail)
23. clarified output; (detail)
24. more robust: capture corner case seen in line 631 of "$AFP/Automatic_Refinement/Autoref_Bindings_HOL.thy" (AFP/6c87f24bb773); (detail)
25. clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General); (detail)
26. updated to postgresql-42.5.0; (detail)
27. tool to build Isabelle component for PostgreSQL JDBC; (detail)
28. clarified goal structure with proper instantiation of main goal, to support "show_goal_inst"; (detail)
29. option "show_states" for more verbosity of batch-builds; (detail)
30. tuned --- avoid warnings; (detail)
31. proper antiquotations; (detail)
32. inline markup for Output.state (in contrast to c94bba7906d2): make messages available via Rendering.text_messages and thus "isabelle log" (see cb0c407fbc6e), while Rendering.output_messages of Isabelle/jEdit/VSCode is unaffected; (detail)
33. proper antiquotations; (detail)
34. clarified options, following e.g. "show_consts"; (detail)
35. proper Envir.subst operations: env is already normalized, using Envir.norm may lead to non-termination; (detail)
36. unused (see 15758fced053); (detail)
37. clarified modules; (detail)
38. show goal instantiation, notably for 'schematic_goal' command (inactive by default); (detail)
39. proper umlauts; (detail)
40. tuned signature; (detail)
41. tuned signature; (detail)
42. tuned; (detail)
43. tuned; (detail)
44. tuned error message; (detail)

Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

1. tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load; (detail)
2. tuned whitespace; (detail)
3. merged (detail)
4. some slight polishing in the UTM entry (detail)
5. added congruence rule for forallM of Error-Monad (detail)
6. updated to devel (detail)
7. merged (detail)
8. tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load; (detail)
9. removed obsolete workaround (see Isabelle/91ee232b4211); (detail)

Started by an SCM change

This run spent:

• 9.2 sec waiting;
• 10 hr build duration;
• 10 hr total from scheduled to completion.