Stream: Coq devs & plugin devs

Topic: Debugging make ci-mathcomp


view this post on Zulip Ana de Almeida Borges (May 27 2021 at 15:47):

I realize that other people have asked similar things, but I'm still stuck. I want to locally run CI for some projects, eg mathcomp. From a fresh coq clone:

export COQ_USE_DUNE=true
make world
make ci-mathcomp

leads to

[...]
+ command make
make[1]: Entering directory '/home/ana/coq/_build_ci/mathcomp/mathcomp'
/home/ana/coq/_build/install/default/bin/coq_makefile  -f Make -o Makefile.coq
make -f Makefile.coq --no-print-directory
COQC ssreflect/ssreflect.v
/bin/sh: 1: time: not found
make[3]: *** [Makefile.coq:763: ssreflect/ssreflect.vo] Error 127
make[2]: *** [Makefile.coq:386: all] Error 2
make[1]: *** [Makefile.common:99: this-build] Error 2
make[1]: Leaving directory '/home/ana/coq/_build_ci/mathcomp/mathcomp'
make: *** [Makefile.ci:110: ci-mathcomp] Error 2

I do have the command time working, which was my only guess after reading the error. This is with OCaml 4.12.0.
As extra examples, the same strategy works with ci-flocq and fails with ci-bignums

view this post on Zulip Théo Zimmermann (May 27 2021 at 16:10):

This is quite unexpected, the sequence of commands you used should normally work...

view this post on Zulip Théo Zimmermann (May 27 2021 at 16:11):

Is this an issue that you didn't have before the Dune switch?

view this post on Zulip Ana de Almeida Borges (May 27 2021 at 16:12):

I never tried to locally run CI before

view this post on Zulip Guillaume Melquiond (May 27 2021 at 16:14):

Make sure you have an actual time command. (I don't know how it could not be the case, but it could theoretically happen.)

$ \time
Usage: time [-apvV] [-f format] [-o file] [--append] [--verbose]
       [--portability] [--format=format] [--output=file] [--version]
       [--quiet] [--help] command [arg...]
$ time
real    0m0,000s
user    0m0,000s
sys 0m0,000s

(Notice the backslash before the command.)

view this post on Zulip Ana de Almeida Borges (May 27 2021 at 16:16):

Um, ok, \time is indeed not found, time does stuff. What's the difference?

view this post on Zulip Guillaume Melquiond (May 27 2021 at 16:17):

The first one is an actual command; the second one is a builtin from your shell.

view this post on Zulip Ana de Almeida Borges (May 27 2021 at 16:18):

Oook, in that case installing time does make sense and indeed after I do so things start to work as expected

view this post on Zulip Ana de Almeida Borges (May 27 2021 at 16:20):

Is there a list of utilities needed to run CI? I found I also needed remake and autoconf

view this post on Zulip Théo Zimmermann (May 27 2021 at 16:22):

It really depends a lot on the external project you are building. If you want the full list, the best strategy is to look into the Dockerfile used in CI.

view this post on Zulip Théo Zimmermann (May 27 2021 at 16:22):

https://github.com/coq/coq/blob/master/dev/ci/docker/bionic_coq/Dockerfile

view this post on Zulip Théo Zimmermann (May 27 2021 at 16:23):

FWIW, we also provide Nix tooling to get required dependencies automatically, but I'm working on making it more accessible.

view this post on Zulip Guillaume Melquiond (May 27 2021 at 16:26):

Regarding remake, you do not have to install it beforehand, as it will be compiled on the fly (assuming you have a C++ compiler) and made available as ./remake.


Last updated: Mar 28 2024 at 22:01 UTC