Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix snapshot-diff detection for extraneous files #2911

Merged
merged 5 commits into from
May 3, 2023
Merged

Fix snapshot-diff detection for extraneous files #2911

merged 5 commits into from
May 3, 2023

Conversation

mtzguido
Copy link
Member

@mtzguido mtzguido commented May 3, 2023

Plus, add a goodie to the workflow, a new section with a summary of the build failures, obtained by simply grepping for *** and (Error and adding some context lines.

You'll notice a previous build of this PR failed due to a missing menhir in the CI machine. The Output build log summary section contains only this:

#23 33.48 cd /home/opam/FStar/ocaml && { dune clean || true ; }
#23 33.48 rm -rf /home/opam/FStar/ocaml/fstar-lib/generated/*
#23 33.48 rm -rf /home/opam/FStar/ocaml/fstar-lib/dynamic/*
#23 33.48 make[2]: Leaving directory '/home/opam/FStar'
#23 33.48 make dune-bootstrap
#23 33.49 make dune-extract-all
#23 33.49 make -C src/ocaml-output dune-snapshot
#23 33.5[1](https://github.com/FStarLang/FStar/actions/runs/4874710672/jobs/8695985641#step:13:1) Makefile:49: *** Correct version of menhir not found (needs a version newer than 20[16](https://github.com/FStarLang/FStar/actions/runs/4874710672/jobs/8695985641#step:13:17)1115).  Stop.
#23 33.51 make[4]: Entering directory '/home/opam/FStar/src/ocaml-output'
#23 33.51 make[4]: Leaving directory '/home/opam/FStar/src/ocaml-output'
#23 33.51 make[3]: *** [Makefile:46: dune-extract-all] Error 2
#23 33.51 make[2]: *** [Makefile:56: dune-bootstrap] Error 2
#23 33.51 make[1]: *** [Makefile:52: dune-full-bootstrap] Error 2
#23 33.51 make: *** [Makefile:120: ci-utest-prelude] Error 2
#23 33.51 + echo Warm-up failed
#23 33.51 + echo Failure
#23 33.51 Warm-up failed
#23 33.51 + return 1
#23 ERROR: process "/bin/bash --login -c eval $(opam env) && Z3_LICENSE=\"$(opam config expand '%{prefix}%')/.opam-switch/sources/z3.4.8.5/LICENSE.txt\" CI_NO_KARAMEL=$CI_NO_KARAMEL DZOMO_GITHUB_TOKEN=$(sudo cat /run/secrets/DZOMO_GITHUB_TOKEN) .docker/build/build-standalone.sh $CI_TARGET $CI_THREADS $CI_BRANCH" did not complete successfully: exit code: 1
------
 > [stage-0 [18](https://github.com/FStarLang/FStar/actions/runs/4874710672/jobs/8695985641#step:13:19)/[19](https://github.com/FStarLang/FStar/actions/runs/4874710672/jobs/8695985641#step:13:20)] RUN --mount=type=secret,id=DZOMO_GITHUB_TOKEN eval $(opam env) && Z3_LICENSE="$(opam config expand '%{prefix}%')/.opam-switch/sources/z3.4.8.5/LICENSE.txt" CI_NO_KARAMEL= DZOMO_GITHUB_TOKEN=$(sudo cat /run/secrets/DZOMO_GITHUB_TOKEN) .docker/build/build-standalone.sh uregressions 24 guido_ci:
#23 33.51 make[4]: Entering directory '/home/opam/FStar/src/ocaml-output'
#23 33.51 make[4]: Leaving directory '/home/opam/FStar/src/ocaml-output'
#23 33.51 make[3]: *** [Makefile:46: dune-extract-all] Error 2
#23 33.51 make[2]: *** [Makefile:56: dune-bootstrap] Error 2
#23 33.51 make[1]: *** [Makefile:52: dune-full-bootstrap] Error 2
#23 33.51 make: *** [Makefile:1[20](https://github.com/FStarLang/FStar/actions/runs/4874710672/jobs/8695985641#step:13:21): ci-utest-prelude] Error 2
#[23](https://github.com/FStarLang/FStar/actions/runs/4874710672/jobs/8695985641#step:13:24) [33](https://github.com/FStarLang/FStar/actions/runs/4874710672/jobs/8695985641#step:13:34).[51](https://github.com/FStarLang/FStar/actions/runs/4874710672/jobs/8695985641#step:13:52) + echo Warm-up failed
#23 33.51 + echo Failure
#23 33.51 Warm-up failed
#23 33.51 + return 1
------
standalone.Dockerfile:88
--------------------
  86 |     ARG CI_BRANCH=master
  87 |     ARG CI_NO_KARAMEL=
  88 | >>> RUN --mount=type=secret

Adding menhir to the CI machine to fix this now.

@mtzguido mtzguido requested a review from tahina-pro May 3, 2023 17:47
@mtzguido mtzguido merged commit 3db4236 into master May 3, 2023
@mtzguido mtzguido deleted the guido_ci branch May 3, 2023 19:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant