docs: Add four Sections in README.md + one demo GHA job

[erikmd]

@Zimmi48 this is not a urgent PR (only about docs), but you may want to proofread it before we can merge it

[Zimmi48]

I'm not quite sure what the use case is. Is this about leaking secret variables?

[erikmd]

I'm not quite sure what the use case is. Is this about leaking secret variables?

Yes, the use case to "hide" some commands from the log would not very useful by itself, indeed, but the fact the variables' value is displayed is a side-effect of the set -x facility, just run:

bash -c 'export foo="42";
  set -x;
  bar="$foo"'

Here, $foo is expanded during the informative log. This is informative, indeed, but may leak secret variables if an user happens to do a curl-or-so deployment within the docker-coq script.

While it would also be possible for the users, and maybe more standard, to do a deployment in a later stage from a dedicated action, given that FYI, the sources files (and the whole workspace of the project that can be modified within the docker-coq-action container) is kept. Only the installed opam package is not available in the end, in particular because we run opam uninstall in the end (but this is not the only reason: the .opam folder itself is lost anyway).

So what's your opinion about this documentation PR?

At least, it seems to me that this limitation has to be documented. This way or another way?
unless you'd just be against set -x henceforth...

[Zimmi48]

It seems a good idea to document it, but I would make it even more explicit (giving explicitly the example of not leaking secret variables).

[erikmd]

Hi @Zimmi48, FYI the potential issue is not critical at all, given repository secrets ${{ secrets.STH }} are automatically hidden, and some secrets that would be obtained by other means can also be marked as hidden in a previous run: step.

FTR, I've tested this again in this now-merged PR: erikmd/docker-coq-github-action-demo#12

Nevertheless, I'll rework this PR #38 soon so that we can integrate that non-critical-albeit-useful documentation.

[erikmd]

Hi @Zimmi48, done: I've just finished my documentation rework 🙂

I can propose to do a point release v1.2.4 as soon as PRs #38 and #61 are merged (maybe tonight or tomorrow?)

Feel free to take a look at this new documentation if you want
(as experience tells that "documentation proofread" is always useful :)
but no worries if you can't do it right now and prefer that I merge the two PRs as is.

To sum up, I've added:

• A section Pitfall: do not use &&; use semicolons
• A section Artifacts along with a related job in the test-suite,
  which builds upon an old discussion with @JasonGross that had taken place on Zulip
• A section Install Debian packages
• A section Verbose output and variable leaking

and in PR #61:

• A section References with a link to the "self-documenting tests" from docker-coq-action's CI
• A section Versioning

[Zimmi48]

Thanks a lot @erikmd! I will have a look today.

[Zimmi48]

I will come back and review the last section and the other PR later today.

[Zimmi48]

LGTM