[isabelle-dev] NEWS: External bash processes are always managed by Isabelle/Scala

[Makarius]

*** ML ***

* External bash processes are always managed by Isabelle/Scala, in
contrast to Isabelle2021 where this was only done for macOS on Apple
Silicon.

The main Isabelle/ML interface is Isabelle_System.bash_process with
result type Process_Result.T (resembling class Process_Result in Scala);
derived operations Isabelle_System.bash and Isabelle_System.bash_output
provide similar functionality as before. Rare INCOMPATIBILITY due to
subtle semantic differences:

  - Processes invoked from Isabelle/ML actually run in the context of
    the Java VM of Isabelle/Scala. The settings environment and current
    working directory are usually the same on both sides, but there can be
    subtle corner cases (e.g. unexpected uses of "cd" or "putenv" in ML).

  - Output via stdout and stderr is line-oriented: Unix vs. Windows
    line-endings are normalized towards Unix; presence or absence of a
    final newline is irrelevant. The original lines are available as
    Process_Result.out_lines/err_lines; the concatenated versions
    Process_Result.out/err *omit* a trailing newline (using
    Library.trim_line, which was occasional seen in applications before,
    but is no longer necessary).

  - Output needs to be plain text encoded in UTF-8: Isabelle/Scala
    recodes it temporarily as UTF-16. This works for well-formed Unicode
    text, but not for arbitrary byte strings. In such cases, the bash
    script should write tempory files, managed by Isabelle/ML operations
    like Isabelle_System.with_tmp_file to create a file name and
    File.read to retrieve its content.

New Process_Result.timing works as in Isabelle/Scala, based on direct
measurements of the bash_process wrapper in C: elapsed time is always
available, CPU time is only available on Linux and macOS, GC time is
unavailable.


This refers to Isabelle/04c9a2cd7686, which provides these updated NEWS. A lot
of text for previously to adjust previous customs of weakly specified
behaviour, or mere customs. Also an interesting consequence of providing Scala
function invocation in ML, and using it on the spot to avoid macOS/Rosetto
problems with threads vs. processes (for Isabelle2021).

There might be very fine points still to be sorted out, but conceptually it is
right to do the systems programming in Scala instead of ML. (A few more system
operations will move from ML to Scala soon.)


	Makarius