[isabelle-dev] NEWS: External bash processes are always managed by Isabelle/Scala
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Thu Feb 25 17:03:02 CET 2021
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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210225/5c5be180/attachment.sig>
More information about the isabelle-dev
mailing list