From: Makarius <email@example.com>
* System *
Command-line tool "isabelle log" has been refined to support multiple
sessions, and to match messages against regular expressions (using Java
System option "show_states" controls output of toplevel command states
(notably proof states) in batch-builds; in interactive mode this is
always done on demand. The option is relevant for tools that operate on
exported PIDE markup, e.g. document presentation or diagnostics. For
isabelle build -o show_states FOL-ex
isabelle log -v -U FOL-ex
Option "show_states" is also the default for the configuration option
"show_results" within the formal context.
Note that printing intermediate states may cause considerable slowdown
in building a session.
This refers to Isabelle/13ae8dff47b6.
isabelle-dev mailing list
From: Rafal Kolanski <firstname.lastname@example.org>
This looks like an interesting development, thank you.
What are your thoughts on including timing info in the log? Gerwin put
together a version of this for us for 2021-1 here:
and the functionality comes in very useful for finding troublesome
performance spots in large image builds, as well as for comparison.
Perhaps one day the log will be a database table where each row is a
single command, and the relevant properties (file location, command
text, timing info, state, warnings, outputs, ...) are columns. This
would simplify construction of arbitrary introspection, comparison and
presentation tools that look at the log alone, which are tricky at the
moment with the timing info being a single cell with XZ compressed YXML
on its own (hence the need to modify isabelle log).
Last updated: Mar 04 2024 at 10:08 UTC