Process logging - #295
Conversation
Sorry, something went wrong.
The --debug polyproc option logs a single line at start-up identifying the process: the UTC start time, the process id, the Poly/ML release and git versions, and the full command line. Add TCHARFMT to diagnostics.h for printing a TCHAR string, following the POLYUFMT convention in globals.h.
The --logfile option truncates the log file at start-up, so only the last run survives. The new --logappend option keeps earlier runs, letting several accumulate in one file. The command-line interface is backward compatible: Without --logappend, the log file is truncated as before.
|
I'm probably missing something, but wouldn't it be better to manage log files from multiple runs outside of Poly/ML? --logappend strikes me as a bit of a footgun: it makes logs less trustworthy by allowing unrelated runs to be mixed together, which can make debugging and reproducing issues harder. It also adds API surface for what seems like a relatively niche use case. Wouldn't it be preferable to leave log rotation, archiving, or combining logs to external tooling, where users can choose the workflow that best fits their needs? |
Sorry, something went wrong.
|
Hi @tjark, thanks for the feedback. There is precedent for supporting this kind of logging directly:
I considered using %p/%t substitutions, but chose --logappend because it is a small change that lets several (sequential) runs share one log file without overwriting earlier results. Because it is opt-in, the existing default behaviour remains unchanged. Users who need to limit the size of an accumulated log can combine it with an external log-rotation tool. The %p/%t approach would serve a somewhat different use case: it would keep the output of each run separate and avoid filename collisions between concurrent Poly/ML processes. I am open to implementing that approach instead—or potentially in addition—if it would be preferable. |
Sorry, something went wrong.
Hi @dcjm,
for debugging purposes, I would like to run Poly/ML with debug output to a file when building multiple Isabelle sessions. For each session, a new Poly/ML process is gets started. As of now, the file specified by --logfile gets opened in write mode, which means that the content of the file gets overridden every time.
To get the output for all sessions, I propose to add a new option --logappend to specify that the log file should be opened in append mode. The command-line interface is backward compatible: Without the option, the current behaviour of overriding the file is kept.
I also propose to add a new debug option --debug polyproc to output some information about the Poly/ML process at startup; the aim is to help identify which output corresponds to which Poly/ML process (e.g., in my case, this identifies the corresponding Isabelle session). The output looks like that: