Yeah, example 55 seems indicative of an actual issue. And I'd like a backwards compatible patch, the minimizer should continue to work with older versions of Coq. Can we just use more regular expressions in the tests?

Yeah, example 55 seems indicative of an actual issue.

Yes, I don't know what's happening there, would you mind having a look (I'd be happy to help if needed but I'm not sure I can do it myself, not being familiar with the minimizer, I don't precisely know what's expected and what's a correct or incorrect minimization result)

And I'd like a backwards compatible patch, the minimizer should continue to work with older versions of Coq. Can we just use more regular expressions in the tests?

Other than this example_55 the remaining should be backward compatible

Yeah, example 55 seems indicative of an actual issue.

Yes, I don't know what's happening there, would you mind having a look (I'd be happy to help if needed but I'm not sure I can do it myself, not being familiar with the minimizer, I don't precisely know what's expected and what's a correct or incorrect minimization result)

According to the GitLab log, the relevant issue is

WARNING: One or more physical paths match logical path Stdlib.Bool.Bool, but none of them exist: ../../../../_install_ci/lib/coq/theories/Bool/Bool.v

The minimizer reads coqc -config for the COQLIB= line and then appends theories/ to find the location of the files, and then looks for files in that path according to the standard structure (reading from the .glob file). So it seems that the .glob file on rocq-prover/rocq#19530 still believes the library is Stdlib.Bool.Bool, and coqc -config claims the stdlib lives in ../../../../_install_ci/lib/coq/theories/, but the .v file is not there. Does this seem like a plausible explanation of what's going wrong to you? Can this issue be rectified on the Coq-side?

Source code in the minimizer:

Btw, probably examples/Makefile will need to be modified to move the relevant modified tests from DEFAULT_TESTS to ONLY_IF_FROM_TESTS, to avoid trying to build them on versions of Coq that are so old they do not support From.

Thanks for the detailled explanation. So the file is now at ../../../../_install_ci/lib/coq/user-contrib/Stdlib/Bool/Bool.v.
I fixed that, apparently it is now backward compatible, let CI confirm.

Btw, probably examples/Makefile will need to be modified to move the relevant modified tests from DEFAULT_TESTS to ONLY_IF_FROM_TESTS, to avoid trying to build them on versions of Coq that are so old they do not support From.

Do you know when was From added? Apparently, it's so old that it's not even in the changelog.

@JasonGross thanks for the help. CI seems mostly happy, it's only complaining on 8.4 about example_063 that you added earlier in the week. That error seems unrelated and that example shouldn't be in any way affected by the upstream PR. So as far as I'm concerned, this looks mergeable.
Of course, I can rebase if you want to confirm the green CI, but maybe not needed (and it is not green on master either, so probably hopeless).

Only example 63 fails, and I've been working on that one separately, so let's merge.

Thanks for your work preparing this!

Thanks for your help