Skip to content
Started 1 yr 6 mo ago
Took 1 hr 51 min on workermtahpc
Success

#1770 (Sep 14, 2022, 12:50:10 AM)

Build Artifacts
Changes
  1. more robust adhoc shell script: work with Isabelle_System.export_isabelle_identifier; (detail / hgweb)
  2. more concise instance-specific rules on euclidean relation (detail / hgweb)
  3. merged (detail / hgweb)
  4. Tidied a few more proofs (detail / hgweb)
  5. merged (detail / hgweb)
  6. tidied a few ugly proofs (detail / hgweb)
  7. let rsync re-use ssh connection via control path; (detail / hgweb)
  8. clarified command-line; (detail / hgweb)
  9. clarified command-line; (detail / hgweb)
  10. tuned signature; (detail / hgweb)
  11. proper port for Mercurial; (detail / hgweb)
  12. clarified default: do not override port from ssh_config, which could be different from 22; (detail / hgweb)
  13. proper Scala expression; (detail / hgweb)
  14. clarified signature: separate unrelated modules; (detail / hgweb)
  15. tuned; (detail / hgweb)
  16. obsolete; (detail / hgweb)
  17. obsolete; (detail / hgweb)
  18. clarified error; (detail / hgweb)
  19. merged (detail / hgweb)
  20. removed remains of proxy_host management: delegated to .ssh/config; (detail / hgweb)
  21. ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
    tuned signature; (detail / hgweb)
  22. putting together related theorems (detail / hgweb)
  23. dropped auxiliary lemma (detail / hgweb)
  24. unused; (detail / hgweb)
  25. clarified operation: avoid perl; (detail / hgweb)
  26. discontinued unused operations; (detail / hgweb)
  27. clarified signature: avoid exposure of JSch types; (detail / hgweb)
  28. clarified signature: discontinue somewhat pointless SSH.Context; (detail / hgweb)
  29. tuned; (detail / hgweb)
  30. proper path; (detail / hgweb)
  31. Added tag Isabelle2022-RC1 for changeset 6308eaaa88f1 (detail / hgweb)
  32. clarified release packaging: naproche-20220910 lacks arm64-linux support (and crashes); (detail / hgweb)
  33. more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command); (detail / hgweb)
  34. merged; (detail / hgweb)
  35. update for release; (detail / hgweb)
  36. more command-line options; (detail / hgweb)
  37. less specialized euclidean relation on int (detail / hgweb)
  38. update to Isabelle2022 and Ubuntu 22.04; (detail / hgweb)
  39. 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)
  40. more operations: for testing purposes; (detail / hgweb)
  41. provide naproche-20220910 (inactive); (detail / hgweb)
  42. clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge; (detail / hgweb)
  43. unused; (detail / hgweb)
  44. update for release; (detail / hgweb)
  45. tuned: prefer Scala Regex operations; (detail / hgweb)
  46. tuning and updates for release; (detail / hgweb)
  47. NEWS; (detail / hgweb)
  48. discontinued somewhat pointless option: Proof_Display.pretty_goal_inst should always work smoothly (and not crash unexpectedly); (detail / hgweb)
  49. give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results; (detail / hgweb)
  50. merged (detail / hgweb)
  51. discontinue fragile operations; (detail / hgweb)
  52. proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options); (detail / hgweb)
  53. enable show_goal_inst by default: match failure is merely a warning (see 730638d4e37a); (detail / hgweb)
  54. updated documentation; (detail / hgweb)
  55. support multiple sessions, with cumulative errors;
    tuned command usage; (detail / hgweb)
  56. support regex patterns on messages; (detail / hgweb)
  57. support Pretty.unformatted, similar to ML version; (detail / hgweb)
  58. removed odd TODO item (see 3391a493f39a); (detail / hgweb)
  59. tuned signature; (detail / hgweb)
  60. tuned output: more Pretty.item; (detail / hgweb)
  61. tuned signature; (detail / hgweb)
  62. clarified failure: warning for logical error, exception for program breakdown; (detail / hgweb)
  63. print goal instantiation for global qed (and variations); (detail / hgweb)
  64. clarified output; (detail / hgweb)
  65. more robust: capture corner case seen in line 631 of "$AFP/Automatic_Refinement/Autoref_Bindings_HOL.thy" (AFP/6c87f24bb773); (detail / hgweb)
  66. clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General); (detail / hgweb)
  67. updated to postgresql-42.5.0; (detail / hgweb)
  68. tool to build Isabelle component for PostgreSQL JDBC; (detail / hgweb)
  69. clarified goal structure with proper instantiation of main goal, to support "show_goal_inst"; (detail / hgweb)
  70. option "show_states" for more verbosity of batch-builds; (detail / hgweb)
  71. tuned --- avoid warnings; (detail / hgweb)
  72. proper antiquotations; (detail / hgweb)
  73. 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)
  74. proper antiquotations; (detail / hgweb)
  75. clarified options, following e.g. "show_consts"; (detail / hgweb)
  76. proper Envir.subst operations: env is already normalized, using Envir.norm may lead to non-termination; (detail / hgweb)
  77. unused (see 15758fced053); (detail / hgweb)
  78. clarified modules; (detail / hgweb)
  79. show goal instantiation, notably for 'schematic_goal' command (inactive by default); (detail / hgweb)
  80. proper umlauts; (detail / hgweb)
  81. tuned signature; (detail / hgweb)
  82. tuned signature; (detail / hgweb)
  83. tuned; (detail / hgweb)
  84. tuned; (detail / hgweb)
  85. tuned error message; (detail / hgweb)

Started by an SCM change

This run spent:

  • 9 sec waiting;
  • 1 hr 51 min build duration;
  • 1 hr 51 min total from scheduled to completion.
Revision: e8d4013c49d1b9f924de52aab4f4887db3cb3e8f