test_wholefile.v incompatible with 8.19

[hendriktews]

This time it is lt_irrefl, which has been deprecated in 8.16. See also #698 and commit bd3615b.

[hendriktews]

Tests that use test_wholefile.v have been disabled in a6ec628.

[erikmd]

Hi @hendriktews, good catch;
but IINM, the test_wholefile.v was intended to test PG capabilities on a realistic Coq example.
It appears the test file rusted, but maybe a better solution would be to adapt the test script, not to disable it?
WDYT?

[hendriktews]

Yes, polishing the Coq code to get the test running again would indeed be better. I had to adapt the test twice in the past. Seeing it now failing again because of a deprecated feature after nobody had reacted to #698 and seeing that the code is far below my coding standards (no indentation, no proof using,...) I was not motivated to touch it again. I would certainly appreciate if somebody takes care of test_wholefile.v, although I believe we have more urgent problems to address in PG.

[erikmd]

Seeing it now failing again because of a deprecated feature after nobody had reacted to #698

Yes, sorry 😅

and seeing that the code is far below my coding standards (no indentation, no proof using,...)

Actually, that file was just a theory from coq's stdlib - which does not impose as many coding conventions as, for example, ssreflect/mathcomp theories.

I was not motivated to touch it again. I would certainly appreciate if somebody takes care of test_wholefile.v, although I believe we have more urgent problems to address in PG.

Sure! no worries to keep the test as is for now! and I'll remember the task so I could address it in a couple of weeks.

BTW if I might help a bit at the beginning of next week, which issue/PR would be the more urgent from your viewpoint?