[isabelle-dev] NEWS: Message logs from session build database

Makarius makarius at sketis.net
Fri Dec 11 00:22:42 CET 2020


*** System ***

* The command-line tool "isabelle log" prints prover messages from the
build database of the given session, following the the order of theory
sources, instead of erratic parallel evaluation. Consequently, the
session log file is restricted to system messages of the overall build
process, and thus becomes more informative.

This refers to Isabelle/1dc2ad97e062. A few more refinements might be still
coming.

After more than 12 years, we are getting back to a sane session log facility,
not just random garbage.

Examples:

  isabelle build HOL
  isabelle log -U -m100 HOL
  isabelle log -U -m100 -v -T HOL.Set -T HOL.Nat HOL


(Technically this is based on PIDE markup + messages produced in batch-mode. I
will see what else can be done with it on the spot for the release.)


	Makarius



More information about the isabelle-dev mailing list