[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