[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