Changes

Summary

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