avoid notation clash with ssr to make examples-ssr build again

[palmskog]

@co-dan here is a way to preserve the SSR examples as-is by fiddling with what is imported. Only the MathComp version of ssrfun exports the offending notations, so we just avoid it.

[RalfJung]

@palmskog thanks! Could you rebase onto master and change this line to build the all target, so that CI ensures that this does indeed build?

FWIW, I don't really have a preference either way between #19 and this. Whatever is fine for Dan is also fine for me.

[co-dan]

Ah, so only the mathcomp's ssrfun was the offender? I just assumed that all the ssreflect modules from Coq are equivalent to the corresponding ssreflect modules from mathcomp, bu tturns out that's not the case...

I would prefer to have this over #19.

[palmskog]

@RalfJung I did the rebase/changes you asked, and CI seems to pass fine. I don't think having a special CI opam package is a good long-term solution, but this is something to address in a future PR.

[RalfJung]

I don't know the semantics of this field, but it looks a bit like this says we require mathcomp, when really we don't (just for one of the tests). Is that a potential problem?

[palmskog]

The way the all target works is that it will always require coq-mathcomp-ssreflect to be installed. To save time in CI, I select Docker images that already have the ssreflect package installed along with Coq. I doubt people will read the CI configuration to figure out dependencies (this is what the README and opam packages are for).

[RalfJung]

I saw the CI config changes in .github/workflows/coq-ci.yml; how is meta.yml related to that?

[palmskog]

I use our configuration templates to generate .github/workflows/coq-ci.yml based on the data in meta.yml. The boilerplate in the target yaml file is based on best practices for using the Coq Docker Action and maintained centrally. This is our response to the ever-changing configuration file requirements on GitHub and elsewhere.

[RalfJung]

I don't think having a special CI opam package is a good long-term solution, but this is something to address in a future PR.

Other proposals to achieve this are welcome. :) I just had to find a way to make CI build something that should not be built on a regular opam install.

[palmskog]

@RalfJung yes, I will do a separate proposal PR for improved opam/CI handling soon, but I believe this can be merged now.

[RalfJung]

Sure, this looks good and Dan also agreed. Thank @palmskog!