Stream: Coq devs & plugin devs

Topic: Local CI workflow

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!

Gaëtan Gilbert (Feb 22 2023 at 19:38):

I don't think I understand the question

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.

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.

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.

Andres Erbsen (Feb 22 2023 at 19:44):

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

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:

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):

• dune build (the default target is coq-core.install coq-stdlib.install coqide-server.install coqide.install)
• make -j $nprocs ci-foo
• in emacs/proof general run/edit the problem file(s) (NB I use https://github.com/coq/coq/blob/master/dev/tools/coqdev.el, for CI this means it auto sets the coqtop path (PS I have a local patch that I should push to use the _build/install coqtop instead of the shim for CI files))

• dev/tools/create_overlays.sh SkySkimmer $prnumber foo (SkySkimmer being my github handle), this adds my repo as a remote (without fetch), creates a new branch with name based on the checked out coq branch, and creates the overlay file for coq
  (this can also be run earlier, it will clone the upstream repo like make ci-foo but won't run the build commands)

• commit and push in emacs/magit

• open overlay PR(s) and link them in the coq PR

Andres Erbsen (Feb 22 2023 at 20:04):

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

• I usually expect several failures, waiting for a remote build to run its course just so I can avoid locally building repos that worked remotely doesn't make sense (or wouldn't if I didn't have unrelated failures locally...)
• I think dune build without make world didn't work for me somehow, I resumed running make world because it does some extra steps before dune build.

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

Andres Erbsen (Feb 22 2023 at 20:07):

it fails on building coqide, I have not investigated

Andres Erbsen (Feb 22 2023 at 20:15):

• PATH=$PWD/_build/install/default/bin:$PATH seems to work, I'll switch back to using it (I don't remember why I stopped)
• is create_overlays appropriate for PRs that are intended to not require backwards-incompatible changes?
• Looks likecreate_overlays only uses the PR number to name the overlay, not the commit messages. Is that correct?

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

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?

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)

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.

Paolo Giarrusso (Feb 22 2023 at 20:32):

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

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.

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

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: May 28 2023 at 13:30 UTC