Update generate & Add template for GitHub container action

[erikmd]

This PR is a follow-up of a discussion with @Zimmi48, and of the release of docker-coq-action:

https://github.com/coq-community/docker-coq-action/releases/tag/v1.0.0

see the commit messages for more details

[Zimmi48]

@liyishuai As this PR takes us even further away from your own proposal to use a Makefile instead of the generate.sh script, maybe you want to participate to reviewing it and weight your own concerns in?

[liyishuai]

My main purpose for a Makefile was to avoid copying files or commands. Whatever approach that better automates the generation process is good to me.

[erikmd]

@liyishuai

Whatever approach that better automates the generation process is good to me.

👍 BTW note that from the current version of the PR, it'd be easy to add other yes/no (or open) questions within the script, e.g. to ask whether the user would like to get a Travis CI configuration or not, etc. (although such extra changes would deserve a separate PR, maybe)

[Zimmi48]

FTR, I also tried to install the npm "mustache" package but it doesn't support YAML, only JSON (like the OCaml version IIUC).

[erikmd]

FTR, I also tried to install the npm "mustache" package but it doesn't support YAML, only JSON (like the OCaml version IIUC).

Yes but this is not a issue at first sight, the mustache ecosystem is not very uniform, but I guess that the current script should be OK with any mustache supporting YAML − cf. the remark in the README anyway:

We suggest you rely on a YAML-compatible mustache implementation such as ruby-mustache (available for instance as an Ubuntu or Debian package).

[erikmd]

(FTR that README remark had been added in #17 )

[Zimmi48]

I confirm the current script works well with mustache-go.

[Zimmi48]

@erikmd What do you think of removing the prompt and making the generation of files entirely automated based on whether some variables are set or not in the meta.yml file? For instance, right now, we already have one such variable for travis because we put the badge in the README only if it is set. We could do the same for the GitHub Action (and include a badge as well).

[Zimmi48]

One major interest of a fully automated generation process (without any prompt) would be that we could add some more automation: CI checks that the generated files correspond to the ones checked in the repository / a call to @coqbot to regenerate the files based on the latest version of the template and the meta.yml in a PR...

[Zimmi48]

One inspirational example is the automation that is used to manage https://github.com/conda-forge (see in particular https://github.com/conda-forge/conda-smithy).

[erikmd]

@erikmd What do you think of removing the prompt and making the generation of files entirely automated based on whether some variables are set or not in the meta.yml file? For instance, right now, we already have one such variable for travis because we put the badge in the README only if it is set. We could do the same for the GitHub Action (and include a badge as well).

Yes, I fully agree with your idea :-)
(But I guess I won't be able to work on this before the evening.)

One major interest of a fully automated generation process (without any prompt) would be that we could add some more automation: CI checks that the generated files correspond to the ones checked in the repository / a call to @coqbot to regenerate the files based on the latest version of the template and the meta.yml in a PR...

👍 Looks great (IINM you suggest to incorporate in the Travis/GitHub actions config a job that would run on the target project repo, clone the coq-community templates repo, and do a checkup?), anyway that feature itself would probably deserve a separated PR ;-)

[Zimmi48]

👍 Looks great (IINM you suggest to incorporate in the Travis/GitHub actions config a job that would run on the target project repo, clone the coq-community templates repo, and do a checkup?), anyway that feature itself would probably deserve a separated PR ;-)

Yes, that's just an idea, but worth being discussed further of course. The problem of automatically checking compatibility with the latest templates would be that it would force people to manually update at every iteration of the templates, even if that wasn't needed for them. A possible solution could be:

1. Doing releases of the templates repo, at a rate TBD, so that updates happen only at a new release;
2. Providing a way to automatically migrate meta.yml files (if a variable is renamed, or if one is introduced whose value was implicit previously);
3. Having @coqbot open PRs on every coq-community repository with a meta.yml file to update the meta.yml and the auto-generated files.

Just food for thought for now. Related to #20.

[erikmd]

Hi @Zimmi48

What do you think of removing the prompt and making the generation of files entirely automated based on whether some variables are set or not in the meta.yml file? For instance, right now, we already have one such variable for travis because we put the badge in the README only if it is set. We could do the same for the GitHub Action (and include a badge as well).

done, feel free to react if you'd like that I refactor the generate.sh in another way.

[…] Just food for thought for now. Related to #20.

BTW this new version of the PR maybe reduces a bit the "discoverability" of the GitHub action template, as the selected examples do not contain action: true, anyway this just amounts to say this is related to #24 :-)

[Zimmi48]

BTW this new version of the PR maybe reduces a bit the "discoverability" of the GitHub action template, as the selected examples do not contain action: true, anyway this just amounts to say this is related to #24 :-)

Exactly!

[Zimmi48]

This looks great! Thank you very much.

[erikmd]

done, thanks @Zimmi48 for the review! in passing I fixed the condition related to travis:/action: so that the CI badge in the README will be inserted iff the .yml CI file is generated.

[erikmd]

sorry wait a minute before merging, I did a too aggressive rebase -i…

[erikmd]

@Zimmi48 done :) − sorry for the noise…

[Zimmi48]

I don't think generating default.nix or not should be based on whether travis is activated. You could test tested_coq_nix_versions instead.

[Zimmi48]

In particular, we might want to add support for building with Nix using GitHub Actions as well.

[Zimmi48]

Feel free to merge by yourself BTW 😉

[erikmd]

@Zimmi48 indeed; updated as suggested.