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!
I don't think I understand the question
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.
stderr.log to find what failed and then search for that development and
Error: in stdout.log to find how it failed.
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.
(I also carry a local patch to disable
-j1 and clone with
All this seems kinda painful and the list of kludges is growing; the question is how to do better. :pensive:
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
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
Thanks! I will adopt some of these, but first, some answers.
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.
I think dune build without make world didn't work for me somehow
yes, but make world without dune build should work
it fails on building coqide, I have not investigated
PATH=$PWD/_build/install/default/bin:$PATH seems to work, I'll switch back to using it (I don't remember why I stopped)
create_overlays appropriate for PRs that are intended to not require backwards-incompatible changes?
create_overlays only uses the PR number to name the overlay, not the commit messages. Is that correct?
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
ci- targets for some developments seem to just fail, for example
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?
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)
Ah that's probably it, I installed a bunch of other deps but I didn't know elpi has a non-coq version.
s/version/package but yes — and there is some version coupling
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.
Paolo Giarrusso said:
coq-elpidepends on Coq-free
elpi, so maybe
elpiis preinstalled in CI? not sure where such setups would be listed (I'd speculate about Dockerfiles, but somebody here probably knows better)
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