Generate .opam and CI from coq-community/templates

[TheoWinterhalter]

The idea is to use https://github.com/coq-community/templates so that we probably use something more principled for our CI jobs. The template can do more but I'd say we're good with these two files for now.

[TheoWinterhalter]

It seems Github Action doesn't like the generated action:

Invalid workflow file : .github/workflows/docker-action.yml#L19
The workflow is not valid. .github/workflows/docker-action.yml (Line: 19, Col: 15): Unexpected value ''

---

EDIT: It's fixed.

[Nsidorenco]

I think this is a good idea but there is some limitations.
The docker container seem to be much faster than the previous solution, but only when no cache is available.

With the current CI the opam packages are cached after the first run.
Looking at the documentation for the docker action it seems they have no intention of caching the opam folder of the container.
https://github.com/coq-community/docker-coq-action#artifacts

[TheoWinterhalter]

Ah indeed. I don't know what would be the best then. Do you think we can modify the new CI script by hand to recover caching or if there's something inherently wrong with the image we're using? (I'm not so familiar with this stuff so I had hoped that the people that did the template knew better).

[Nsidorenco]

Maybe we could copy the .opam directory out of the container before it is destroyed?
I've played with it briefly and couldn't get it to work, but it might be possible.

Alternatively, we could make our own docker image with all the dependencies and then base the CI on that.
If we do this, then it might make sense to split the repo into a core part and a crypto examples part.

[TheoWinterhalter]

Well, but the point is to check also that you can install SSProve with the curent opam recipe so we avoid things like #20 no?

[Nsidorenco]

That's a good point.
I think the problem in #20 was the opam recipe was too permissive (and that a minor version update should really not be a breaking change).

I imagine that this error would not have been caught if the CI worked on a cached opam with a different package in the allowed interval?

If the opam recipe is restrictive enough then the cache would only need to change when the recipe is updated.

[TheoWinterhalter]

Right. It would have required a manual rerun of the action I guess…

[TheoWinterhalter]

It seems we can still use some caching, but I don't know how relevant it is for us: https://github.com/coq-community/templates/blob/master/ref.yml#L478