multiline Coq error matching?

[JasonGross]

I've been toying with a fancier way of doing problem matching by piping stderr through a script that aggregates Coq warnings and errors. In particular, it would use the following criterion to identify which chunks are warnings/errors:

• The first line must match "^(?:-\\s+)?File \"([^ \"]+)\", line (\\d+), characters (\\d+-\\d+):"
• The second line must match "^(?:-\\s+)?(Warning|Error):\\s*(.*?)
• If the second line ends with something matching \\[([^]]*)\\], then the error is just a two-line error
• The multiline error is considered to end at the first line ending with something matching \\[([^]]*)\\], unless a line matching one of the following is found first, in which case we assume that the matching has gone wrong and treat only the first two lines specially:
  • We encounter another line which matches the first-line pattern for errors/warnings
  • We encounter a line matching "^(?:-\\s+)?(COQC|OCAMLC|OCAMLOPT|COQDEP) .*" (new build file, presumably we missed the end of the error)
  • We encounter a line matching "^(?:-\\s+)?[^\\s]+ \\(real: [0-9\\.]*, user: [0-9\\.]*, sys: [0-9\\.]*, mem: [0-9]* ko)" (output of make TIMED=1, we probably missed the end of the warning/error)
  • We encounter a line matching "^(?:-\\s+)?make(?:\\[[0-9]+\\]):" (we ended up back in make output)

Would the docker coq action be interested in using such a script? (via something like 2> >(./process_coq_errors_to_annotations.sh >&2), or perhaps via { normal_cmd.sh 3>&1 1>&2 2>&3 3>&- | ./process_coq_errors_to_annotations.sh; } 3>&1 1>&2 2>&3 3>&- or similar, based on https://stackoverflow.com/a/3618308/377022 and the note at https://stackoverflow.com/questions/3618078/pipe-only-stderr-through-a-filter/52575213#comment105555334_52575087 that the system may kill the substituted process before it completes, once the main process exits)