[tools] Add mlogselect tool

[maranget]

The new tool extracts test output by (test) names from one log. If follows the usual techniques for selection by names.

% mlogselect7
usage: mlogselect7 [options]* log?
  -select <name> specify test or test index  file, can be repeated
  -names <name> specify file of names, can be repeated
  -oknames <name,..,name> <name,...,name> names of tests to be selected
  -excl <name> specify file of names to be excluded, can be repeated
  -nonames <name,..,name> <name,...,name> names of tests to be excluded
  -rename <name> specify a rename mapping, hashes are checked
  -help  Display this list of options
  --help  Display this list of options

[fsestini]

$ dune exec mlogselect7 -- -oknames SB-PPC doc/SB-PPC2.log
Test SB-PPC Allowed
Histogram (3 states)
1765  *>0:r3=0; 1:r3=0;
498741:>0:r3=1; 1:r3=0;
499494:>0:r3=0; 1:r3=1;
Ok
Witnesses
Positive: 1765, Negative: 998235
Condition exists (0:r3=0 /\ 1:r3=0) is validated
Hash=4edecf6abc507611612efaecc1c4a9bc
Observation SB-PPC Sometimes 1765 998235
Time SB-PPC 0.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for STFW-PPC.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC STFW-PPC
"Rfi PodRR Fre Rfi PodRR Fre"

If I understand the tool correctly, everything past Time SB-PPC 0.57 should not be in the output.

I've left some other comments in the code. Overall, the lexing/parsing logic is a bit involved, so it would be good if this PR came with some (cram) tests. The example above could be a good test case to start with.

[fsestini]

Could we not, instead, change herd7, litmus7 etc. so that they produce a unified, standardised log format, thus making this kind of lexing/parsing easier?

I also think some of the complexity arises from the fact that tools like mlogselect, mlog2names, moutcomes, etc. , need to interface with a logging format that seems primarily meant for human consumption. I think ideally herd7 and litmus7 would instead provide a way to generate logs in a standard machine-readable format, such as JSON. That would make parsing a non-problem and would remove ambiguity arising from presentation details like blank lines etc. Moreover, with logs in a standard machine-readable format, many of the workflows that now require a bespoke tool like mlogselect could be implemented in a few line using existing tools. As a simple example:

$ cat results.jsonl
{"name":"Test1", "states":[{...},{...}], ...}
{"name":"Test2", "states":[], ...}

# select logs by name (similar to mlogselect7)
$ jq 'select(.name == "Test2")' results.jsonl
{
  "name": "Test2",
  "states": [],
  ...
}

# select logs with at least one outcome state (similar to mlog2name7)
$ jq -r 'select(.states | length > 0) | .name' results.jsonl
Test1

[maranget]

Slighty changing the log format looks a very good idea. What can easily be done is:

1. Keep the start marker Test <name>
2. Adopt the empty line as the end marker. This is a small change to litmus7.
   Unfortunately, we sill have to lex old logs... In partcular I have a decade of litmus logs at hand.

I remain attached to readable text format for logs. I want to be able to read logs without the mediation of a tool. But of course, we should facilitate the processing of logs. In my opinion, mlogselect is not a very complex lexer, even more so if the format of logs is changed a bit.

[psafont]

I think ideally herd7 and litmus7 would instead provide a way to generate logs in a standard machine-readable format, such as JSON.

I've been thinking about a logging module, that can be used to centralize decisions regarding loglevel, as well as verbosity. My main concern was to reduce the number of functors since logging is per-process usually instead of per-module.

Regardless of my initial purpose, this could be used as an opportunity to start generating structured logging and easily select the format of the logging, using different formatters. There's a nice library available in the ecosystem that allows this kind of separation of concerns: https://erratique.ch/software/logs

Would people be open to this kind change to the codebase?

[fsestini]

I remain attached to readable text format for logs. I want to be able to read logs without the mediation of a tool.

Note that "machine-readable" doesn't necessarily imply "hard to read by humans". E.g. YAML is a common machine-readable format that is also quite nice to read by humans, IMO. Moreover the machine-readable format doesn't need to (and shouldn't) replace the existing readable one; it could be put behind an opt-in flag litmus7 --json-logs. Of course these are just examples.

I think my overall point is that if we need tools to routinely consume logs, it's a good idea to make the log format easy to process, and ideally leverage existing standards and tools if possible. Whether that is achieved by making the current format more machine-readable, or by offering an option like litmus7 --json-logs to opt-in to a separate format, is to be determined.

[fsestini]

Regardless of my initial purpose, this could be used as an opportunity to start generating structured logging and easily select the format of the logging, using different formatters. There's a nice library available in the ecosystem that allows this kind of separation of concerns: https://erratique.ch/software/logs

Note, in fact, that logs is already included in the herdtools7.opam file, although its usage is not widespread at the moment. FWIW, in general, I'm very much in favour of a more logs-like approach, though I'm not sure it applies to simple tools like mlogselect.

[fsestini]

Fast lexing of logs, for selection

It seems this lexing module is doing quite a bit more than just lexing, as it currently implements the whole tool's functionality including mutable state updates and stdout printing.

Could we separate lexing from log selection and output? I think it would be cleaner if the lexer only classified tokens/lines, with a separate module/function taking care of log filtering and printing.

I would also like to point out that this module adds another lexer/parser alongside existing modules like lexLog_tools, lexHashLog, etc., which, from a quick look, seem to all implement their own slightly different parsing logic for the same log format. Is there a reason for this apparent duplication? Could we instead implement a single lexer/parser for log files that is shared among all the log-processing tools?

[maranget]

Fast lexing of logs, for selection

It seems this lexing module is doing quite a bit more than just lexing, as it currently implements the whole tool's functionality including mutable state updates and stdout printing.
Could we separate lexing from log selection and output? I think it would be cleaner if the lexer only classified tokens/lines, with a separate module/function taking care of log filtering and printing.

Having one pass tools is old fashioned, I admit. The task at hand here remains simple: identify begin and end markers, extract test name. In my old-fashioned (outdated, maybe) view, a simple tool that does everything is adequate.

I would also like to point out that this module adds another lexer/parser alongside existing modules like lexLog_tools, lexHashLog, etc., which, from a quick look, seem to all implement their own slightly different parsing logic for the same log format. Is there a reason for this apparent duplication? Could we instead implement a single lexer/parser for log files that is shared among all the log-processing tools?

We could do that, and would be more robust against log format evolution. However, this is more involved than writing the simple tool I have needed to select offending test outputs while debugging PR #1970....

[fsestini]

Having one pass tools is old fashioned, I admit. The task at hand here remains simple: identify begin and end markers, extract test name. In my old-fashioned (outdated, maybe) view, a simple tool that does everything is adequate.

Could you clarify what you mean by "one pass"? Is this about reading the input file once?

We could do that, and would be more robust against log format evolution. However, this is more involved than writing the simple tool I have needed to select offending test outputs while debugging PR #1970....

Of course, it doesn't need to happen now! Though perhaps I would add a "TODO" comment and/or create a Github ticket about it so that we don't forget.

[maranget]

$ dune exec mlogselect7 -- -oknames SB-PPC doc/SB-PPC2.log
Test SB-PPC Allowed
Histogram (3 states)
1765  *>0:r3=0; 1:r3=0;
498741:>0:r3=1; 1:r3=0;
499494:>0:r3=0; 1:r3=1;
Ok
Witnesses
Positive: 1765, Negative: 998235
Condition exists (0:r3=0 /\ 1:r3=0) is validated
Hash=4edecf6abc507611612efaecc1c4a9bc
Observation SB-PPC Sometimes 1765 998235
Time SB-PPC 0.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for STFW-PPC.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC STFW-PPC
"Rfi PodRR Fre Rfi PodRR Fre"

If I understand the tool correctly, everything past Time SB-PPC 0.57 should not be in the output.

I've left some other comments in the code. Overall, the lexing/parsing logic is a bit involved, so it would be good if this PR came with some (cram) tests. The example above could be a good test case to start with.

Your understanding is correct. I have fixed the problem and will add some cram tests.