Email Gateway (Feb 22 2021 at 23:22): Email Gateway (Feb 22 2021 at 23:22):From: Makarius <makarius@sketis.net>
* ML *
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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Feb 23 2021 at 22:18):From: Makarius <makarius@sketis.net>
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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Feb 25 2021 at 16:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Makarius,
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).
I also have an ancient tool which does something similar: check the Pure
sources and issue a parsable error message if something goes utterly wrong.
I would appreciate an official tool for that.
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/...?
In my drawer I found the following funny one-line to find out how many
threads PolyML thinks are available.
isabelle process -e 'writeln ("\n~~~ " ^ string_of_int (Thread.numProcessors ()) ^ " ~~~\n")' | grep -Po '(?<=~~~ )\d+(?= ~~~)'
To get a clue how the threads option could look like.
Don't know whether this is still of general interest.
Cheers,
Florian
signature.asc
Email Gateway (Feb 27 2021 at 15:14):From: Makarius <makarius@sketis.net>
On 25/02/2021 17:03, Florian Haftmann wrote:
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).I also have an ancient tool which does something similar: check the Pure
sources and issue a parsable error message if something goes utterly wrong.
Do you want to show me that (privately)?
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/...?In my drawer I found the following funny one-line to find out how many
threads PolyML thinks are available.isabelle process -e 'writeln ("\n~~~ " ^ string_of_int (Thread.numProcessors ()) ^ " ~~~\n")' | grep -Po '(?<=~~~ )\d+(?= ~~~)'
To get a clue how the threads option could look like.
See the included scala script, to be placed in a directory mentioned in
ISABELLE_TOOLS. I have used the stderr channel for clean output, without the
ML toplevel interfering.
Moreover, I have looked around where "isabelle process" still occurs in our
sources (Isabelle/736b8853189a):
* In the "system" manual, section about "The raw Isabelle ML process" /
"Batch mode": it gives a wrong / outdated impression of being able to process
theories etc: this strengthens my inclination to remove the tool altogether.
* In src/Tools/Code/code_ml.ML to invoke an external ML process to compile
generated modules. This used to be similar in src/HOL/Library/code_test.ML,
until I changed that for the Isabelle2021 release, e.g. see:
https://isabelle-dev.sketis.net/rISABELLEdfe150a246e6
https://isabelle-dev.sketis.net/rISABELLE697e5688f370
This approach to use the existing ML environment (and Scala, too) is much
simpler and lighter. Could it be done for regular Code_Target.add_language as
well?
Thus the old "isabelle process" (and "isabelle console") could just disappear,
without any special tricks replacing them.
Makarius
ml_processors.scala
Last updated: Jul 15 2022 at 23:21 UTC