#4472 (May 22, 2023, 8:12:24 PM)

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

1. merged (detail / hgweb)
2. misc tuning and clarification; (detail / hgweb)
3. tuned signature; (detail / hgweb)
4. tuned; (detail / hgweb)
5. tuned --- Token.make_string / Token.assign are value-oriented; (detail / hgweb)
6. more documentation; (detail / hgweb)
7. tuned signature; (detail / hgweb)
8. tuned signature; (detail / hgweb)
9. more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm); (detail / hgweb)
10. prefer static simpset; (detail / hgweb)
11. omit pointless morphism in global theory; (detail / hgweb)
12. more operations; (detail / hgweb)
13. more careful treatment of context for method source; (detail / hgweb)
14. clarified context; (detail / hgweb)
15. clarified signature; (detail / hgweb)
16. remove pointless context setup (see also b2e449c155a4); (detail / hgweb)
17. more careful reset_context for stored entity; (detail / hgweb)
18. more careful reset/set_context for stored declarations; (detail / hgweb)
19. tuned; (detail / hgweb)
20. tuned; (detail / hgweb)
21. clarified signature: more explicit types; (detail / hgweb)
22. clarified data: avoid pointless Morphism.transform; (detail / hgweb)
23. proper Token.Declaration for internal_declaration; (detail / hgweb)
24. more standard treatment of morphism context; (detail / hgweb)
25. tuned: avoid duplication; (detail / hgweb)
26. more standard treatment of morphism context, but hardly relevant here; (detail / hgweb)
27. tuned; (detail / hgweb)
28. more careful treatment of set_context / reset_context for persistent morphisms;
    avoid persistent theory for eq_morphism / eq_term_morphism, notably in 'class' definition; (detail / hgweb)
29. clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
    clarified signature; (detail / hgweb)
30. tuned signature; (detail / hgweb)
31. support for context within morphism (for background theory); (detail / hgweb)
32. proper transfer to supported "bundle ... begin unbundle ... end", e.g. see theory "AFP/Probabilistic_Timed_Automata.Graphs"; (detail / hgweb)
33. clarified signature; (detail / hgweb)
34. tuned; (detail / hgweb)
35. tuned; (detail / hgweb)
36. tuned signature; (detail / hgweb)
37. more accurate Thm.trim_context / Thm.transfer; (detail / hgweb)
38. clarified stored thm: result from notes;
    tuned; (detail / hgweb)
39. tuned whitespace; (detail / hgweb)
40. clarified signature: avoid convoluted operations; (detail / hgweb)
41. tuned signature; (detail / hgweb)
42. update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof; (detail / hgweb)
43. avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c); (detail / hgweb)
44. proper transfer / trim_context; (detail / hgweb)
45. more operations "without_context", assuming that the thm has been properly transferred already; (detail / hgweb)
46. proper trim_context / transfer; (detail / hgweb)
47. tuned: more accurate check (is_norm_hhf protect); (detail / hgweb)
48. clarified build options: reduce heap size by approx. 3%; (detail / hgweb)
49. more standard merge order, following logical structure of imports rather than physical serials; (detail / hgweb)
50. tuned; (detail / hgweb)
51. tuned; (detail / hgweb)
52. proper Thm.trim_context / Thm.transfer; (detail / hgweb)
53. proper Thm.trim_context / Thm.transfer; (detail / hgweb)
54. tuned: avoid pointless Proof_Context.init_global of Context.proof_of; (detail / hgweb)

Started by an SCM change

This run spent:

• 3 min 21 sec waiting;
• 4 hr 2 min build duration;
• 4 hr 5 min total from scheduled to completion.

• MiniSail
• Isabelle_C
• Goedel_HFSet_Semanticless
• Incompleteness
• Types_To_Sets_Extension
• Dependent_SIFUM_Type_Systems
• Robinson_Arithmetic
• XML
• Certification_Monads
• Launchbury
• Nominal2
• Goedel_HFSet_Semantic
• Partial_Function_MR