Ana de Almeida Borges (May 27 2021 at 15:47): 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
Théo Zimmermann (May 27 2021 at 16:10):This is quite unexpected, the sequence of commands you used should normally work...
Théo Zimmermann (May 27 2021 at 16:11):Is this an issue that you didn't have before the Dune switch?
Ana de Almeida Borges (May 27 2021 at 16:12):I never tried to locally run CI before
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.)
Ana de Almeida Borges (May 27 2021 at 16:16):Um, ok, \time is indeed not found, time does stuff. What's the difference?
Guillaume Melquiond (May 27 2021 at 16:17):The first one is an actual command; the second one is a builtin from your shell.
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
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
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.
Théo Zimmermann (May 27 2021 at 16:22):https://github.com/coq/coq/blob/master/dev/ci/docker/bionic_coq/Dockerfile
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.
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: Oct 13 2024 at 01:02 UTC