Enrico Tassi (Dec 02 2021 at 16:37): Enrico Tassi (Dec 02 2021 at 16:37):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 :-/
Gaëtan Gilbert (Dec 02 2021 at 16:39):I don't think you're supposed to make install
no idea if it can turn a failure into a success though
Gaëtan Gilbert (Dec 02 2021 at 16:46):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.
Enrico Tassi (Dec 03 2021 at 06:17):I think only one job fails, the one using makefile.doc, https://github.com/coq/coq/pull/15220 /checks?check_run_id=4398000475
Enrico Tassi (Dec 03 2021 at 08:40):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 :-/
Théo Zimmermann (Dec 03 2021 at 09:37):The ci- targets are only for external projects.
Enrico Tassi (Dec 03 2021 at 09:37):and it works again :-(
it has been failing since the beginning of the PR I'm afraid
Enrico Tassi (Dec 03 2021 at 09:38):I did use the commands @Gaëtan Gilbert wrote up there
Théo Zimmermann (Dec 03 2021 at 09:38):Are you saying that it consistently works on your machine but that it consistently fails in CI?
Enrico Tassi (Dec 03 2021 at 09:39):yes, but I have one last thing to try
Enrico Tassi (Dec 03 2021 at 09:45):nope... I'm out of ideas
Enrico Tassi (Dec 03 2021 at 09:45):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)
Enrico Tassi (Dec 03 2021 at 09:47):I'll try a blind commit, but that looks like the very last idea I have
Théo Zimmermann (Dec 03 2021 at 09:49):I don't recall having a look at it, but sure, that could help.
Enrico Tassi (Dec 03 2021 at 10:01):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
Enrico Tassi (Dec 03 2021 at 13:44):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?
Gaëtan Gilbert (Dec 03 2021 at 13:51):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
Théo Zimmermann (Dec 03 2021 at 13:53):Nix job in GitLab CI does:
Théo Zimmermann (Dec 03 2021 at 13:53): # 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