Stream: Coq devs & plugin devs

Topic: test suite live report


view this post on Zulip Gaëtan Gilbert (Apr 03 2024 at 15:24):

while running the test suite, if you run watch "grep -F 'Error!' -r . -lZ --include='*.log' | xargs -0 cat" from the test suite directory you get a live report of failures
the log files contain their paths so it looks like a sequence of

==========> TESTING foo/bar <==========
Error: lorem ipsum error
0m0.000000s 0m0.000000s
0m3.310000s 0m0.500000s
==========> FAILURE <==========
    foo/bar...Error! (bla)

(just the errors)

not sure if we could expose this in a nicer way than just running the above command


Last updated: Oct 13 2024 at 01:02 UTC