What should I type exactly in order to reproduce locally a failure in the ci job for the refman?
I did something like ./configure; make coq; make install; make refman... and it did work :-/
I don't think you're supposed to make install
no idea if it can turn a failure into a success though
if the problem is only when building the refman using an installed coq you need
./configure -prefix $somewhere
make world
make install
make SPHINXENV='COQBIN="'"$somewhere"'/bin/"' SPHINX_DEPS= refman
If the Dune build of the refman fails as well, then use Dune.
I think only one job fails, the one using makefile.doc, https://github.com/coq/coq/pull/15220 /checks?check_run_id=4398000475
Yes, I confirm the dune-pdf job works, it is the other one which fails with
reading sources... [ 1%] addendum/canonical-structures
Exception occurred:
File "/usr/lib/python3/dist-packages/pexpect/expect.py", line 50, in eof
raise EOF(msg)
pexpect.exceptions.EOF: End Of File (EOF). Exception style platform.
<pexpect.pty_spawn.spawn object at 0x7ff28d8358d0>
command: /builds/coq/coq/_install_ci/bin/coqtop
args: [b'/builds/coq/coq/_install_ci/bin/coqtop', b'-q', b'-color', b'on']
buffer (last 100 chars): ''
before (last 100 chars): 'install/default/lib/\r\n/builds/coq/coq/_build/install/default/lib/\r\n/root/.opamcache/4.05.0/lib\r\n\r\n\r\n'
after: <class 'pexpect.exceptions.EOF'>
In a way I was hoping to find a ci-refman target to reproduce locally the failure.
I'll try again, but last time here it worked :-/
The ci-
targets are only for external projects.
and it works again :-(
it has been failing since the beginning of the PR I'm afraid
I did use the commands @Gaëtan Gilbert wrote up there
Are you saying that it consistently works on your machine but that it consistently fails in CI?
yes, but I have one last thing to try
nope... I'm out of ideas
the log says there is a longer log, maybe I should save it as an artifact? would that help? (I've never looked in that log)
I'll try a blind commit, but that looks like the very last idea I have
I don't recall having a look at it, but sure, that could help.
I think I understood what the 'last 100 characters' are about (it's the error message I wanted to read, spit by coqc).
The dune job works because dune sets OCAMLPATH correctly, but this hybrid make/dune does not... So try to hack SPHINXENV, let's see
So, I did hack a few lines in gitlab-ci to save the artifact even if the job fails, and it tries, but fails:
https://gitlab.com/coq/coq/-/jobs/1847067877
I guess the whildcard does not do what I think. Any GL-ci expert?
https://docs.gitlab.com/ee/ci/yaml/#artifactspaths
Paths are relative to the project directory ($CI_PROJECT_DIR) and can’t directly link outside it.
you need to do make || { cp /tmp/*.log . && false; }
then put the copied log in the artifacts path
Nix job in GitLab CI does:
# Use current worktree as tmpdir to allow exporting artifacts in case of failure
- export TMPDIR=$PWD
Last updated: Sep 25 2023 at 12:01 UTC