Skip to content

Commit

Permalink
A bit more info in various CIs
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross committed Apr 16, 2024
1 parent 542732f commit de044e4
Show file tree
Hide file tree
Showing 6 changed files with 58 additions and 54 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/coq-debian.yml
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ jobs:
run: etc/ci/describe-system-config.sh
- name: chroot build params
shell: in-debian-chroot.sh {0}
run: CI=1 etc/ci/describe-system-config.sh
run: CI=1 GITHUB_STEP_SUMMARY="$GITHUB_STEP_SUMMARY" etc/ci/describe-system-config.sh
- name: make deps
shell: in-debian-chroot.sh {0}
run: etc/ci/github-actions-make.sh -j2 deps
Expand Down
16 changes: 8 additions & 8 deletions .github/workflows/coq-docker.yml
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ jobs:
with:
coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY
custom_script: |
eval $(opam env)
etc/ci/describe-system-config.sh
Expand All @@ -48,21 +48,21 @@ jobs:
with:
coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY
custom_script: etc/ci/github-actions-docker-make.sh COQBIN="$(dirname "$(which coqc)")/" -j2 deps
- name: all-except-generated-and-js-of-ocaml
uses: coq-community/docker-coq-action@v1
with:
coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY
custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated-and-js-of-ocaml
- name: pre-standalone-extracted
uses: coq-community/docker-coq-action@v1
with:
coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY
custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 pre-standalone-extracted
- name: upload OCaml files
uses: actions/upload-artifact@v3
Expand Down Expand Up @@ -100,7 +100,7 @@ jobs:
with:
coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY
custom_script: |
sudo git config --global --add safe.directory "*"
sudo make EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 COQBIN="$(dirname "$(which coqc)")/" install install-standalone-ocaml
Expand All @@ -109,7 +109,7 @@ jobs:
with:
coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY
custom_script: |
sudo git config --global --add safe.directory "*"
sudo make EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 COQBIN="$(dirname "$(which coqc)")/" install-without-bedrock2 install-standalone-ocaml
Expand All @@ -118,7 +118,7 @@ jobs:
with:
coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY
custom_script: |
sudo git config --global --add safe.directory "*"
sudo make EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 COQBIN="$(dirname "$(which coqc)")/" install install-standalone-ocaml
Expand Down Expand Up @@ -161,7 +161,7 @@ jobs:
with:
coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY
custom_script: etc/ci/github-actions-docker-make.sh TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"
if: env.SKIP_VALIDATE == '' && github.event_name != 'pull_request'

Expand Down
31 changes: 31 additions & 0 deletions etc/ci/describe-system-config-common-groups.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
#!/bin/sh

group uname -a
group ulimit -aH
group ulimit -aS
group ghc --version
group ghc -v
group gcc --version
group gcc -v
group opam switch
group opam list
group ocamlc -config
group ocamlc -where
group ocamlfind printconf destdir
group ocamlfind list
group ocamlfind query findlib
group ocamlfind query zarith
group ocamlfind query coq
group ocamlfind query coq-core
group ocamlfind query coq-core.plugins
group ocamlfind query coq-core.plugins.ltac
group "ocamlfind query coq | xargs find"
group js_of_ocaml --version
group wasm_of_ocaml --version
group coqc --config
group coqc --version
group coqtop </dev/null
group etc/machine.sh
group "echo PATH=$PATH"
group "echo SHELL=$SHELL"
group etc/ci/github-actions-record-coq-info.sh "$GITHUB_STEP_SUMMARY"
10 changes: 1 addition & 9 deletions etc/ci/describe-system-config-macos.sh
Original file line number Diff line number Diff line change
Expand Up @@ -25,14 +25,6 @@ fi

group sysctl -n machdep.cpu.brand_string
group "sysctl -a | grep machdep.cpu"
group uname -a
group sw_vers -productVersion
group system_profiler SPSoftwareDataType
group opam switch
group opam list
group ocamlc -config
group coqc --config
group coqc --version
group "true | coqtop"
group etc/machine.sh
etc/ci/github-actions-record-coq-info.sh
. etc/ci/describe-system-config-common-groups.sh
32 changes: 2 additions & 30 deletions etc/ci/describe-system-config.sh
Original file line number Diff line number Diff line change
Expand Up @@ -24,42 +24,14 @@ else
fi

group lscpu
group uname -a
group lsb_release -a
group ulimit -aH
group ulimit -aS
group cat /etc/os-release
group cat /proc/cpuinfo
group cat /proc/meminfo
group cat /etc/alpine-release
group apk info
group apk info coq
group apk --print-arch
group dpkg -l
group dpkg -l | cat
group pacman -Qs
group ghc --version
group ghc -v
group gcc --version
group gcc -v
group opam switch
group opam list
group ocamlc -config
group ocamlc -where
group ocamlfind printconf destdir
group ocamlfind list
group ocamlfind query findlib
group ocamlfind query zarith
group ocamlfind query coq
group ocamlfind query coq-core
group ocamlfind query coq-core.plugins
group ocamlfind query coq-core.plugins.ltac
group "ocamlfind query coq | xargs find"
group js_of_ocaml --version
group wasm_of_ocaml --version
group coqc --config
group coqc --version
group "true | coqtop"
group etc/machine.sh
group "echo PATH=$PATH"
group "echo SHELL=$SHELL"
etc/ci/github-actions-record-coq-info.sh
. etc/ci/describe-system-config-common-groups.sh
21 changes: 15 additions & 6 deletions etc/ci/github-actions-record-coq-info.sh
Original file line number Diff line number Diff line change
@@ -1,12 +1,21 @@
#!/bin/sh

outfile="${1:-$GITHUB_STEP_SUMMARY}"

# summarize coqc version to make it easier to read
COQC_VERSION_SHORT="$(coqc --print-version 2>/dev/null | cut -d " " -f 1)"
COQC_VERSION="$(coqc --version 2>/dev/null | tr '\n' ',' | sed 's/,$//g')"
COQTOP_VERSION="$(true | coqtop 2>&1)"
if [ ! -z "$GITHUB_STEP_SUMMARY" ] && [ ! -z "$COQC_VERSION" ]; then
printf '%s\n\n' "<details><summary>${COQC_VERSION}</summary>" >> "$GITHUB_STEP_SUMMARY"
printf '%s\n' '```' >> "$GITHUB_STEP_SUMMARY"
printf '%s\n' "${COQTOP_VERSION}" >> "$GITHUB_STEP_SUMMARY"
printf '%s\n%s\n' '```' '</details>' >> "$GITHUB_STEP_SUMMARY"
COQTOP_VERSION="$(coqtop </dev/null 2>&1)"
if [ ! -z "$outfile" ]; then
if [ ! -z "$COQC_VERSION" ]; then
echo "Writing $COQC_VERSION to $outfile..."
printf '%s\n\n' "<details><summary>${COQC_VERSION}</summary>" >> "$outfile"
printf '%s\n' '```' >> "$outfile"
printf '%s\n' "${COQTOP_VERSION}" >> "$outfile"
printf '%s\n%s\n' '```' '</details>' >> "$outfile"
else
echo "Not writing missing coqc version to $outfile"
fi
else
echo "GITHUB_STEP_SUMMARY is unset"
fi

0 comments on commit de044e4

Please sign in to comment.