Email Gateway (Aug 22 2022 at 11:37): Email Gateway (Aug 22 2022 at 11:37):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hello,
I have noticed that when running Isabelle in batch mode
to check a theory somethings are printed while other
are not.
For example class declarations are printed, but definitions
and theorems are not. However when using
thm SomeFact
then the theorem is printed also.
Is there a way to suppress all outputs from processing
the theory, but still have the output from explicit
writeln inside Isabelle/ML blocks.
Moreover, is it possible to turn this output on and off
from within a theory?
Best regards,
Viorel Preoteasa
Email Gateway (Aug 22 2022 at 11:37):From: Buday Gergely <gbuday@karolyrobert.hu>
Viorel Preoteasa wrote:
Moreover, is it possible to turn this output on and off from within a theory?
This mail answers your questions I guess:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-June/msg00144.html
Email Gateway (Aug 22 2022 at 11:38):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hi Gergely,
Thank you for your message. However it seems that the
solution described in the link is for suppressing output
in the latex document, and not the output on the terminal.
I am interested in processing a theory in batch mode, and
outputting at the end (in the terminal) some specific information,
and I want to suppress all the other output that is produced.
Best regards,
Viorel
Email Gateway (Aug 22 2022 at 11:54):From: Makarius <makarius@sketis.net>
Of course, you can always use your own private output channel, e.g. a
named pipe (fifo) on Unix-based systems.
A more basic approach is Outout.physical_stderr: it is used by the system
in rare situations to emit messages to the terminal, bypassing almost
everything else. You can hypersearch the Isabelle/ML sources, to see
where this is used.
Makarius
Last updated: Apr 25 2024 at 12:23 UTC