HomeIsabelle/Phabricator
Command-line tool "isabelle log" and option "show_states"

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.

Written by makarius on Sep 9 2022, 4:15 PM.
User
Projects
None
Subscribers
None

Event Timeline