[Jenkins]Jenkins
log in
Started 20 days ago
Took 4 hr 0 min on workermta1

Build #734 (Sep 13, 2022, 12:57:18 PM)

Changes
  1. merged (detail / hgweb)
  2. proper path; (detail / hgweb)
  3. Added tag Isabelle2022-RC1 for changeset 6308eaaa88f1 (detail / hgweb)
  4. tidied a few ugly proofs (detail / hgweb)
  5. clarified release packaging: naproche-20220910 lacks arm64-linux support (and crashes); (detail / hgweb)
  6. more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command); (detail / hgweb)
  7. merged; (detail / hgweb)
  8. update for release; (detail / hgweb)
  9. more command-line options; (detail / hgweb)
  10. less specialized euclidean relation on int (detail / hgweb)
  11. update to Isabelle2022 and Ubuntu 22.04; (detail / hgweb)
  12. proper comment: Phabricator remains on Ubuntu 20.04, which is still required as build environment for old Mercurial 3.9.2 with Python 2; (detail / hgweb)
  13. more operations: for testing purposes; (detail / hgweb)
  14. provide naproche-20220910 (inactive); (detail / hgweb)
  15. clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge; (detail / hgweb)
  16. unused; (detail / hgweb)
  17. update for release; (detail / hgweb)
  18. tuned: prefer Scala Regex operations; (detail / hgweb)
  19. tuning and updates for release; (detail / hgweb)
  20. NEWS; (detail / hgweb)
  21. discontinued somewhat pointless option: Proof_Display.pretty_goal_inst should always work smoothly (and not crash unexpectedly); (detail / hgweb)
  22. give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results; (detail / hgweb)
  23. merged (detail / hgweb)
  24. discontinue fragile operations; (detail / hgweb)
  25. proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options); (detail / hgweb)
  26. enable show_goal_inst by default: match failure is merely a warning (see 730638d4e37a); (detail / hgweb)
  27. updated documentation; (detail / hgweb)
  28. support multiple sessions, with cumulative errors;
    tuned command usage; (detail / hgweb)
  29. support regex patterns on messages; (detail / hgweb)
  30. support Pretty.unformatted, similar to ML version; (detail / hgweb)
  31. removed odd TODO item (see 3391a493f39a); (detail / hgweb)
  32. tuned signature; (detail / hgweb)
  33. tuned output: more Pretty.item; (detail / hgweb)
  34. tuned signature; (detail / hgweb)
  35. clarified failure: warning for logical error, exception for program breakdown; (detail / hgweb)
  36. print goal instantiation for global qed (and variations); (detail / hgweb)
  37. clarified output; (detail / hgweb)
  38. more robust: capture corner case seen in line 631 of "$AFP/Automatic_Refinement/Autoref_Bindings_HOL.thy" (AFP/6c87f24bb773); (detail / hgweb)
  39. clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General); (detail / hgweb)
  40. updated to postgresql-42.5.0; (detail / hgweb)
  41. tool to build Isabelle component for PostgreSQL JDBC; (detail / hgweb)
  42. clarified goal structure with proper instantiation of main goal, to support "show_goal_inst"; (detail / hgweb)
  43. option "show_states" for more verbosity of batch-builds; (detail / hgweb)
  44. tuned --- avoid warnings; (detail / hgweb)
  45. proper antiquotations; (detail / hgweb)
  46. 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 / hgweb)
  47. proper antiquotations; (detail / hgweb)
  48. clarified options, following e.g. "show_consts"; (detail / hgweb)
  49. proper Envir.subst operations: env is already normalized, using Envir.norm may lead to non-termination; (detail / hgweb)
  50. unused (see 15758fced053); (detail / hgweb)
  51. clarified modules; (detail / hgweb)
  52. show goal instantiation, notably for 'schematic_goal' command (inactive by default); (detail / hgweb)
  53. proper umlauts; (detail / hgweb)
  54. tuned signature; (detail / hgweb)
  55. tuned signature; (detail / hgweb)
  56. tuned; (detail / hgweb)
  57. tuned; (detail / hgweb)
  58. tuned error message; (detail / hgweb)
  59. merged (detail / hgweb)
  60. merged (detail / hgweb)
  61. moved antimono to Fun and redefined it as an abbreviation (detail / hgweb)
  62. moved mono and strict_mono to Fun and redefined them as abbreviations (detail / hgweb)
  63. clarified generic euclidean relation (detail / hgweb)
  64. added a bound in SMT on the number of schematic constants considered -- the code (in for_schematics) is exponential in that number (detail / hgweb)
  65. tuned signature; (detail / hgweb)
  66. check imports more strictly, e.g. reject ".../Pure" or ".../HOL-Library.Multiset"; (detail / hgweb)
  67. tuned signature; (detail / hgweb)
  68. tuned --- more robust syntax; (detail / hgweb)
  69. tuned signature; (detail / hgweb)
  70. back to more traditional import_name (reverting cceb10dcc9f9), e.g. relevant for "isabelle jedit -l CTT src/CTT/ex/Elimination.thy" to produce proper error "Cannot update finished theory CTT.Elimination"; (detail / hgweb)
  71. unused (see 347ed6219dab); (detail / hgweb)
  72. tuned signature; (detail / hgweb)
  73. more CONTRIBUTORS + NEWS; (detail / hgweb)
  74. tuned; (detail / hgweb)
  75. proper description; (detail / hgweb)
  76. tuned whitespace; (detail / hgweb)
  77. option "sort_updates" for record update simproc. Make proper record simproc definitions. (detail / hgweb)

Started by an SCM change

This run spent:

  • 1 day 22 hr waiting;
  • 4 hr 0 min build duration;
  • 2 days 2 hr total from scheduled to completion.
Revision: 02a743911ffe74222a67850321c8f0fd3f2d0c78