1 Isabelle NEWS -- history of user-relevant changes |
1 Isabelle NEWS -- history of user-relevant changes |
2 ================================================= |
2 ================================================= |
3 |
3 |
4 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) |
4 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) |
|
5 |
|
6 |
|
7 New in this Isabelle version |
|
8 ---------------------------- |
|
9 |
|
10 *** HOL *** |
|
11 |
|
12 * Theory Multiset: dedicated predicate "multiset" is gone, use |
|
13 explict expression instead. Minor INCOMPATIBILITY. |
|
14 |
|
15 * HOL-Analysis/HOL-Probability: indexed products of discrete |
|
16 distributions, negative binomial distribution, Hoeffding's inequality, |
|
17 Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some |
|
18 more small lemmas. Some theorems that were stated awkwardly before were |
|
19 corrected. Minor INCOMPATIBILITY. |
|
20 |
|
21 |
|
22 *** ML *** |
|
23 |
|
24 * External bash processes are always managed by Isabelle/Scala, in |
|
25 contrast to Isabelle2021 where this was only done for macOS on Apple |
|
26 Silicon. |
|
27 |
|
28 The main Isabelle/ML interface is Isabelle_System.bash_process with |
|
29 result type Process_Result.T (resembling class Process_Result in Scala); |
|
30 derived operations Isabelle_System.bash and Isabelle_System.bash_output |
|
31 provide similar functionality as before. Rare INCOMPATIBILITY due to |
|
32 subtle semantic differences: |
|
33 |
|
34 - Processes invoked from Isabelle/ML actually run in the context of |
|
35 the Java VM of Isabelle/Scala. The settings environment and current |
|
36 working directory are usually the same on both sides, but there can be |
|
37 subtle corner cases (e.g. unexpected uses of "cd" or "putenv" in ML). |
|
38 |
|
39 - Output via stdout and stderr is line-oriented: Unix vs. Windows |
|
40 line-endings are normalized towards Unix; presence or absence of a |
|
41 final newline is irrelevant. The original lines are available as |
|
42 Process_Result.out_lines/err_lines; the concatenated versions |
|
43 Process_Result.out/err *omit* a trailing newline (using |
|
44 Library.trim_line, which was occasional seen in applications before, |
|
45 but is no longer necessary). |
|
46 |
|
47 - Output needs to be plain text encoded in UTF-8: Isabelle/Scala |
|
48 recodes it temporarily as UTF-16. This works for well-formed Unicode |
|
49 text, but not for arbitrary byte strings. In such cases, the bash |
|
50 script should write tempory files, managed by Isabelle/ML operations |
|
51 like Isabelle_System.with_tmp_file to create a file name and |
|
52 File.read to retrieve its content. |
|
53 |
|
54 New Process_Result.timing works as in Isabelle/Scala, based on direct |
|
55 measurements of the bash_process wrapper in C: elapsed time is always |
|
56 available, CPU time is only available on Linux and macOS, GC time is |
|
57 unavailable. |
|
58 |
5 |
59 |
6 |
60 |
7 New in Isabelle2021 (February 2021) |
61 New in Isabelle2021 (February 2021) |
8 ----------------------------------- |
62 ----------------------------------- |
9 |
63 |