search

coq-community / docker-coq-action

GitHub Action using Docker-Coq [maintainers=@erikmd,@Zimmi48]
MIT License
12 stars 4 forks source link

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

Closed erikmd closed 3 years ago

erikmd commented 3 years ago

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

Zimmi48 commented 3 years ago

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

erikmd commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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: https://github.com/erikmd/docker-coq-github-action-demo/pull/12

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

erikmd commented 3 years ago

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:

and in PR #61:

Zimmi48 commented 3 years ago

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

erikmd commented 3 years ago

Thanks!

Le 11 août 2021 16:21:56 GMT+02:00, "Théo Zimmermann" @.> a écrit : @. commented on this pull request.

steps:

  • uses: @.***
  • uses: @.*** with:
  • opam_file: 'coq-demo.opam'
  • opam_file: 'folder/coq-proj.opam'

Any reason for this change?

No strong reason (both examples of .opam file are OK), actually I just rewrote this for the sake of uniformity (similarly to all other README.md occurrences of opam_file). So let me know if I need to change this and/or other occurrences...

  • image:
    • 'coqorg/coq:dev'
  • fail-fast: false # don't stop jobs if one fails +steps:
    • uses: @.***
    • uses: @.***
  • with:
  • opam_file: 'folder/coq-proj.opam'
  • custom_image: ${{ matrix.image }}
  • before_script: |
  • startGroup "Install APT dependencies"
  • cat /etc/os-release # Print the Debian OS version
  • sudo apt-get update -y -q # Mandatory
  • sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends \
  • emacs \
  • tree # for instance (in alphabetical order)

Is there a point to mention that the packages are listed in alphabetical order?

Actually when I wrote this, I just remembered reading this suggestion: https://docs.docker.com/develop/develop-images/dockerfile_best-practices/#sort-multi-line-arguments ("""Whenever possible, ease later changes by sorting multi-line arguments alphanumerically. This helps to avoid duplication of packages and make the list much easier to update. This also makes PRs a lot easier to read and review. Adding a space before a backslash () helps as well.""") But I can admit this is a minor suggestion, so no worries to remove it if you want!

Zimmi48 commented 3 years ago

Actually when I wrote this, I just remembered reading this suggestion: https://docs.docker.com/develop/develop-images/dockerfile_best-practices/#sort-multi-line-arguments ("""Whenever possible, ease later changes by sorting multi-line arguments alphanumerically. This helps to avoid duplication of packages and make the list much easier to update. This also makes PRs a lot easier to read and review. Adding a space before a backslash () helps as well.""") But I can admit this is a minor suggestion, so no worries to remove it if you want!

The problem is that thrown like that without reference or explanation, it's hard to understand what is meant.

Maybe you could change # for instance (in alphabetical order) into # alphabetical order is recommended for long package lists to ease review and update.