fix: Remove "Variable A: Prop" & Lemma identity #56
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # a few tests, not intended for demo purposes | |
| name: misc-test | |
| on: | |
| push: | |
| branches: | |
| - master | |
| pull_request: | |
| branches: | |
| - '**' | |
| jobs: | |
| uid-test: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - run: id | |
| - uses: coq-community/docker-coq-action@v1 | |
| with: | |
| opam_file: './coq-demo.opam' | |
| coq_version: 'latest' | |
| ocaml_version: '4.07-flambda' | |
| custom_script: | | |
| # small test, not intended for demo purposes | |
| startGroup Test UID+GID | |
| id | |
| pwd | |
| ls -hal | |
| stat -c "UID=%u,GID=%g %n" $WORKDIR/$PACKAGE.opam | |
| endGroup | |
| startGroup Print opam config | |
| opam config list; opam repo list; opam list | |
| endGroup | |
| leak-test: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 'Define and export env vars' | |
| run: | | |
| # 1. Example of a repository secret | |
| echo ${{ secrets.SOME_REPO_SEC }} # automatically hidden | |
| # 2. Example of a locally-created secret | |
| SOME_LOCAL_SEC="$RANDOM" | |
| # echo $SOME_LOCAL_SEC # TO REMOVE! (just to say it's not yet hidden) | |
| echo "::add-mask::$SOME_LOCAL_SEC" | |
| # See https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions#masking-a-value-in-log | |
| echo "$SOME_LOCAL_SEC" # would be hidden | |
| printf "%s\n" "SOME_LOCAL_SEC=$(printf "%q" "$SOME_LOCAL_SEC")" >> $GITHUB_ENV | |
| # See https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions#setting-an-environment-variable | |
| # 3. Example of a locally-created local variable | |
| SOME_LOCAL_VAR='ok' | |
| printf "%s\n" "SOME_LOCAL_VAR=$(printf "%q" "$SOME_LOCAL_VAR")" >> $GITHUB_ENV | |
| - name: 'Run coq-community/docker-coq-action@v1 with debian:10' | |
| uses: coq-community/docker-coq-action@v1 | |
| env: | |
| SOME_OTHER_VAR: 'okok' | |
| SOME_OTHER_SEC: ${{ secrets.SOME_REPO_SEC }} | |
| with: | |
| export: 'SOME_LOCAL_VAR SOME_LOCAL_SEC SOME_OTHER_VAR SOME_OTHER_SEC' | |
| custom_image: 'debian:10' | |
| custom_script: | | |
| : A. This should print ok twice, and okok twice | |
| echo "$SOME_LOCAL_VAR" | |
| echo "$SOME_OTHER_VAR" | |
| : B. This should print '***' thrice | |
| echo $SOME_LOCAL_SEC | |
| echo $SOME_OTHER_SEC | |
| echo ${{ secrets.SOME_REPO_SEC }} | |
| # Note also that one can further harden docker-coq-action's logging | |
| # by disabling temporarily the trace of commands | |
| { set +x; } 2>/dev/null | |
| echo 'C. This should print ok only once' | |
| echo "$SOME_LOCAL_VAR" | |
| set -x |