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

[Makarius]

On 23/02/2021 00:22, Makarius wrote:
> 
> 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.)

Here is another fine point:

  - Just like any other Scala function invoked from ML,
    Isabelle_System.bash_process requires a proper PIDE session context.
    This could be a regular batch session (e.g. "isabelle build"), a
    PIDE editor session (e.g. "isabelle jedit"), or headless PIDE (e.g.
    "isabelle dump" or "isabelle server"). Note that old "isabelle
    console" or raw "isabelle process" don't have that.

See also Isabelle/637e3e85cd6f.


In principle the requirement of a proper PIDE session context is already
present in Isabelle2021, but there are hardly any relevant Scala functions
invoked from ML.

>From now on there will be more and more coming, to do the hardcore system
programming properly in the physical world (Scala) instead of mathematics
(ML). (To download a file, copy a directory hierarchy etc.)


I am still unsure what to do about "isabelle console" and "isabelle process".

My main use of the console is with option -r, to bootstrap Pure in case of
error, when the PIDE editing of Pure does not work. So it could be replaced by
"isabelle bootstrap" as administrative tool (unavailable in a regular Isabelle
release).

The "isabelle process" was once our main "isabelle" script, e.g. for direct
TTY use or as inferior Emacs process. Now it is occasionally used for
generated code from the ML environment. So it could become another Scala
function from ML, using the ML_Process module in Isabelle/Scala. That would
make it much lighter, because the surrounding Scala/JVM is already running,
i.e. the one of the required PIDE session context.


So are there other remaining uses of "isabelle console" or "isabelle process"
that don't fit into this picture? And that cannot be done more directly in
Isabelle/Scala, instead of old-fashioned scripting in bash/perl/python/...?


	Makarius