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
[...] + command make make: 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: *** [Makefile.coq:763: ssreflect/ssreflect.vo] Error 127 make: *** [Makefile.coq:386: all] Error 2 make: *** [Makefile.common:99: this-build] Error 2 make: 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
This is quite unexpected, the sequence of commands you used should normally work...
Is this an issue that you didn't have before the Dune switch?
I never tried to locally run CI before
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.)
\time is indeed not found,
time does stuff. What's the difference?
The first one is an actual command; the second one is a builtin from your shell.
Oook, in that case installing
time does make sense and indeed after I do so things start to work as expected
Is there a list of utilities needed to run CI? I found I also needed
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.
FWIW, we also provide Nix tooling to get required dependencies automatically, but I'm working on making it more accessible.
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
Last updated: Feb 06 2023 at 00:03 UTC