Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Message logs from session build data...

Email Gateway (Dec 10 2020 at 23:22):

From: Makarius <makarius@sketis.net>
* 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

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Apr 19 2024 at 20:15 UTC