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

[Makarius]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ml_processors.scala
Type: text/x-scala
Size: 545 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210227/f27033ae/attachment.scala>