Email Gateway (Aug 30 2023 at 12:32): Email Gateway (Aug 30 2023 at 12:32):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Hi everyone,
I made a logger for Isabelle/ML, at some places inspired by Apache's
Log4j. It supports hierarchical logging configurations (e.g. log levels,
message filters, output channels).
The sources are available here:
Examples can be found in "ML_Logger_Examples.thy".
I was wondering whether this could, in some form or another, be a useful
addition to the Isabelle distribution (e.g. as part of the "Tools"
directory).
Best wishes,
Kevin
Email Gateway (Aug 30 2023 at 13:47):From: Makarius <makarius@sketis.net>
Apart from imitating log4j, what is the purpose of this tool? And how does it
fit into existing models of Isabelle/ML and Isabelle/Scala?
It looks by an order of magnitude too complex, to answer such questions on the
spot.
I failed to try it out (version 0cec3102eb94). Directory structure does not
fit to ROOT file!? Which Isabelle version?
Side-remark 1: We do have pending problems with the "tracing" function in
Isabelle/ML: it needs to be fit better into the Isabelle/Scala/PIDE model of
interaction. This mainly means to prevent "denial-of-service" of the GUI
document model by massive amounts of messages, and maybe some means to
interact with message streams (filtering etc.).
Side-remark 2: I've once had a brief look at Log4j, to see if it has a
potential purpose in Isabelle/Scala. I rejected it as far too complex and made
this tiny addition to Isabelle/Scala instead:
https://isabelle.sketis.net/repos/isabelle/annotate/9c1173a7e4cb/src/Tools/VSCode/src/logger.scala
or now
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2023-RC3/src/Pure/General/logger.scala
(I am rather glad that I did not include Log4j back then: afterwards it had
rather bad press due to big security problems.)
Makarius
Email Gateway (Aug 30 2023 at 14:23):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
On 30.08.23 15:47, Makarius wrote:
On 30/08/2023 14:27, Kevin Kappelmann wrote:
I made a logger for Isabelle/ML, at some places inspired by Apache's
Log4j. It supports hierarchical logging configurations (e.g. log
levels, message filters, output channels).Apart from imitating log4j,
It is not imitating log4j. Merely the log level names are based on log4j.
what is the purpose of this too
It is a hierarchical logger, that is loggers are registered in a
tree-like structure and configurations can be adjusted with respect to
this hierarchy. Its purpose is to simplify the process of creating log
messages, filter log messages, make tracing of ML code (e.g. tactics)
easier, etc.
Some simple examples are illustrated in "ML_Logger_Examples.thy"
Personally, I created it for a rather complex ML-development where
multiple unification algorithms had to be combined [1]. There was no
sensible way to trace and debug the interplay of the unification
algorithms without proper logging facilities.
[1]
https://github.com/kappelmann/ml-unification-isabelle/tree/master/Unifiers
And how does it fit into existing models of Isabelle/ML and Isabelle/Scala?
I do not understand what you mean by "model" of Isabelle/ML.
It looks by an order of magnitude too complex, to answer such questions
on the spot.
The core logic is here:
https://github.com/kappelmann/logger-isabelle/blob/main/logger.ML
I do not see why this should be complex and disagree with this point of
criticism.
I failed to try it out (version 0cec3102eb94).
Sorry, I forgot: it works with the latest development version 193a24f78b00
Directory structure does not fit to ROOT file!? Which Isabelle version?
I do not understand. The directory structure does match. Executing the
following from the root directory of the repository works as expected:
isabelle jedit -d . -R ML_Logger ML_Logger_Examples.thy
Side-remark 1: We do have pending problems with the "tracing" function
in Isabelle/ML: it needs to be fit better into the Isabelle/Scala/PIDE
model of interaction. This mainly means to prevent "denial-of-service"
of the GUI document model by massive amounts of messages, and maybe some
means to interact with message streams (filtering etc.).Side-remark 2: I've once had a brief look at Log4j, to see if it has a
potential purpose in Isabelle/Scala. I rejected it as far too complex
and made this tiny addition to Isabelle/Scala instead:
https://isabelle.sketis.net/repos/isabelle/annotate/9c1173a7e4cb/src/Tools/VSCode/src/logger.scala or now https://isabelle.sketis.net/repos/isabelle/file/Isabelle2023-RC3/src/Pure/General/logger.scala(I am rather glad that I did not include Log4j back then: afterwards it
had rather bad press due to big security problems.)Makarius
Email Gateway (Aug 30 2023 at 14:30):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Addendum: I think I have misinterpreted below part of your answer. You
may ignore it.
Last updated: Apr 29 2024 at 04:18 UTC