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
// DESCRIPTION: number of processors reported by Poly/ML
object Tool extends isabelle.Isabelle_Tool.Body {
import isabelle._
def apply(args: List[String]): Unit =
{
val ml_text =
"TextIO.output (TextIO.stdErr, Int.toString (Option.getOpt (Thread.Thread.numPhysicalProcessors (), 0)))"
val options = Options.init()
val result =
ML_Process(options, sessions_structure = null, store = null,
raw_ml_system = true, eval_main = ml_text).result().check
Output.writeln(result.err, stdout = true)
}
}
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
