Stream: Coq devs & plugin devs

Topic: ci job for the refman


view this post on Zulip 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 :-/

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Dec 02 2021 at 22:53):

If the Dune build of the refman fails as well, then use Dune.

view this post on Zulip 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

view this post on Zulip 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'>

view this post on Zulip Enrico Tassi (Dec 03 2021 at 08:40):

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

view this post on Zulip Théo Zimmermann (Dec 03 2021 at 09:37):

The ci- targets are only for external projects.

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Dec 03 2021 at 09:38):

I did use the commands @Gaëtan Gilbert wrote up there

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Dec 03 2021 at 09:39):

yes, but I have one last thing to try

view this post on Zulip Enrico Tassi (Dec 03 2021 at 09:45):

nope... I'm out of ideas

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Dec 03 2021 at 09:47):

I'll try a blind commit, but that looks like the very last idea I have

view this post on Zulip Théo Zimmermann (Dec 03 2021 at 09:49):

I don't recall having a look at it, but sure, that could help.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Dec 03 2021 at 13:53):

Nix job in GitLab CI does:

view this post on Zulip 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: Feb 06 2023 at 20:02 UTC