Email Gateway (Sep 09 2022 at 14:16): Email Gateway (Sep 09 2022 at 14:16):From: Makarius <makarius@sketis.net>
* System *
Command-line tool "isabelle log" has been refined to support multiple
sessions, and to match messages against regular expressions (using Java
Pattern syntax).
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
example:
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.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Sep 11 2022 at 05:27):From: Rafal Kolanski <xs@xaph.net>
Hi Makarius,
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:
https://github.com/seL4/isabelle/commit/f02f3ce4c38743ce10996e18893e22aad1ba26eb
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).
Rafal Kolanski
Last updated: Feb 01 2025 at 20:19 UTC