Stream: Coq devs & plugin devs

Topic: Local CI workflow


view this post on Zulip Andres Erbsen (Feb 22 2023 at 19:36):

Would anyone be willing to share their workflow for running the CI locally? I am specifically interested in (1) getting a list of developments that succeeded, failed, or couldn't be tried (2) getting their error messages separately (3) cleaning up for rebuild after Coq/stdlib changes and (4) committing and pushing the right message to the right repository. Thanks!

view this post on Zulip Gaëtan Gilbert (Feb 22 2023 at 19:38):

I don't think I understand the question

view this post on Zulip Andres Erbsen (Feb 22 2023 at 19:41):

FWIW, what I currently do is
/usr/bin/time sh -c 'make world ; dune build coq-core.install coq-stdlib.install coqide-server.install coq.install && make -k -j "$(nproc)" -f Makefile.ci ci-all 2>stderr.log | tee stdout.log && echo ok' to build,
dune exec -- sh -c 'env "PATH=$PWD/dev/shim:$PATH" vim ./_build_ci/jasmin/proofs/lang/utils.v' to edit files, git commit -am to commit with a handwritten message trying to get the Coq PR reference right by hand, upload using
git push "https://github.com/andres-erbsen/$(grep -m1 -oP '^\s*url\s*=\s*https://github.com/[^/\s]+/\K.*' .git/config)" HEAD:refs/heads/BRANCH and clean up by recreating the git worktree.

view this post on Zulip Andres Erbsen (Feb 22 2023 at 19:41):

I read stderr.log to find what failed and then search for that development and Error: in stdout.log to find how it failed.

view this post on Zulip Andres Erbsen (Feb 22 2023 at 19:42):

These are not recommendations; e.g. the push command does not work inside submodulues and it's sometimes hard to tell what error in stdout.log came from what development.

view this post on Zulip Andres Erbsen (Feb 22 2023 at 19:44):

(I also carry a local patch to disable -j1 and clone with --depth=1...)

view this post on Zulip Andres Erbsen (Feb 22 2023 at 19:46):

All this seems kinda painful and the list of kludges is growing; the question is how to do better. :pensive:

view this post on Zulip Gaëtan Gilbert (Feb 22 2023 at 19:56):

what's the point of running ci-all instead of getting what failed from the pipeline?
what's the point of running dune build after make world?

dune exec -- sh -c 'env "PATH=$PWD/dev/shim:$PATH" vim ./_build_ci/jasmin/proofs/lang/utils.v'

that seems wrong, you should be using _build/install/default/bin instead of the shim directory
I'm surprised that you don't get missing dependency errors using the shims


for me, after the pipeline fails on eg ci-foo (and assuming the error looks like something I want to investigate or fix locally, as opposed to wanting to auto minimize for instance):

view this post on Zulip Andres Erbsen (Feb 22 2023 at 20:04):

Thanks! I will adopt some of these, but first, some answers.

view this post on Zulip Gaëtan Gilbert (Feb 22 2023 at 20:05):

I think dune build without make world didn't work for me somehow

yes, but make world without dune build should work

view this post on Zulip Andres Erbsen (Feb 22 2023 at 20:07):

it fails on building coqide, I have not investigated

view this post on Zulip Andres Erbsen (Feb 22 2023 at 20:15):

view this post on Zulip Gaëtan Gilbert (Feb 22 2023 at 20:21):

create_overlays does not create commits or commit messages

is create_overlays appropriate for PRs that are intended to not require backwards-incompatible changes?

you don't have to commit the overlay file it produces
it is still convenient to add the remote and create the branch
also sometimes you may want to push the overlay file even for backward compatible overlays to check that it works in CI

view this post on Zulip Andres Erbsen (Feb 22 2023 at 20:27):

The ci- targets for some developments seem to just fail, for example ci-elpi says Makefile:18: *** Elpi not found, make sure it is installed in your PATH or set ELPIDIR. Stop.Is this expected / is there some setup step I need to do?

view this post on Zulip Paolo Giarrusso (Feb 22 2023 at 20:30):

coq-elpi depends on Coq-free elpi, so maybe elpi is preinstalled in CI? not sure where such setups would be listed (I'd speculate about Dockerfiles, but somebody here probably knows better)

view this post on Zulip Andres Erbsen (Feb 22 2023 at 20:31):

Ah that's probably it, I installed a bunch of other deps but I didn't know elpi has a non-coq version.

view this post on Zulip Paolo Giarrusso (Feb 22 2023 at 20:32):

s/version/package but yes — and there is some version coupling

view this post on Zulip Andres Erbsen (Feb 22 2023 at 20:32):

Next up is ci-jasmin, it says Error: Cannot find a physical path bound to logical path ssrZ with prefix mathcomp.word. and maybe started doing so only recently.

view this post on Zulip Gaëtan Gilbert (Feb 22 2023 at 21:22):

Paolo Giarrusso said:

coq-elpi depends on Coq-free elpi, so maybe elpi is preinstalled in CI? not sure where such setups would be listed (I'd speculate about Dockerfiles, but somebody here probably knows better)

https://github.com/coq/coq/blob/master/dev/ci/docker/bionic_coq/Dockerfile

view this post on Zulip Gaëtan Gilbert (Feb 22 2023 at 21:26):

mathcomp_word is one of our few scripts that use dune instead of make, so maybe related? I don't know


Last updated: Feb 22 2024 at 03:02 UTC