[isabelle-dev] NEWS: Command-line tool "isabelle log" and option "show_states"

[Rafal Kolanski]

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

On 10/09/2022 00:15, Makarius wrote:
 > *** 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 at in.tum.de
 > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev