Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Command-line tool "isabelle log" and...


view this post on Zulip Email Gateway (Sep 09 2022 at 14:16):

From: Makarius <makarius@sketis.net>
* System *

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

view this post on Zulip 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: Mar 04 2024 at 10:08 UTC