Here is an interesting MetaCoq error detected by coq-bench (full log):
# COQC sigma.v
# /bin/sh: 1: time: not found
# make[4]: *** [Makefile.coq:716: sigma.vo] Error 127
# make[3]: *** [Makefile.coq:339: all] Error 2
# rm: cannot remove 'pretty-timed-success.ok': No such file or directory
# make[2]: *** [Makefile.coq:379: make-pretty-timed] Error 1
# make[1]: *** [Makefile.coq:399: pretty-timed] Error 2
It seems either MetaCoq or Coq itself has an undeclared dependency (in the OPAM package) on the Unix time
command. @Matthieu Sozeau may be the in the best position to comment.
If it turns out to be MetaCoq, you need to add conf-time
as an OPAM dependency in the appropriate package(s).
this is a quite strange default in my mind (from translations/Makefile
), why would every build need to be timed?
all: Makefile.coq
$(MAKE) -f Makefile.coq pretty-timed
Hi
Ah, I have seen this error. Weird indeed
This is because sh does not have a 'time' command, while 'bash' doed
I changed the bench code in order to run commands into 'sh' rather than 'bash'
I mean 'bash' rather than 'sh'
it's not possible to assume either sh
or bash
in practice, e.g., on macOS or Windows, so I think the solution is to add conf-time
as a dep. Nevertheless, I think MetaCoq devs might want to remove default build timings (just make it a parameter instead).
I agree that the standard install does not need timings
OK for the dependency on conf-time
We use that mainly for the CI, let's make it configurable. Also the timing scripts depend on python IIRC
@Matthieu Sozeau is there a particular reason not to use a "standard" completely delegating Makefile? This would make pretty-timed
a configuration option without anything else needed
Here's what we use in coq-community most of the time:
all: Makefile.coq
@+$(MAKE) -f Makefile.coq all
clean: Makefile.coq
@+$(MAKE) -f Makefile.coq cleanall
@rm -f Makefile.coq Makefile.coq.conf
Makefile.coq: _CoqProject
$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
force _CoqProject Makefile: ;
%: Makefile.coq force
@+$(MAKE) -f Makefile.coq $@
.PHONY: all clean force
Currently we have a rather complicated setup but basically it does the same with multiple subdirectories (one per package)
hmm, but translations/Makefile
currently looks like this:
all: Makefile.coq
$(MAKE) -f Makefile.coq pretty-timed
_CoqProject: _CoqProject.in metacoq-config
cat metacoq-config > _CoqProject
cat _CoqProject.in >> _CoqProject
Makefile.coq: _CoqProject
coq_makefile -f _CoqProject -o Makefile.coq
clean: Makefile.coq
$(MAKE) -f Makefile.coq clean
install: all
$(MAKE) -f Makefile.coq install
uninstall: all
$(MAKE) -f Makefile.coq uninstall
mrproper:
rm -f Makefile.coq
this doesn't do any delegation, so for each coq_makefile
task you want to have access to you will need to write a new task there.
Ah I see your point, we could indeed change those sub-makefiles to use more delegations
@Matthieu Sozeau if you like, I can do a quick MetaCoq PR for only translations/Makefile
to solve the dependency issue while making pretty-timed
a configuration option. The other makefiles are more complicated.
Sure, that'd be great !
any particular reason you're using 8.11.0 rather than 8.11.2 in the CI?
Nope
interesting, it seems pretty-timed
was already being passed explicitly: https://travis-ci.com/github/MetaCoq/metacoq/jobs/394094049#L4188
I think what you're seeing is due to the make pretty-timed in translations/Makefile
in any case, when https://github.com/MetaCoq/metacoq/pull/497 is merged I can do the same changes for coq-8.12
(or it can be cherry-picked on your end)
Last updated: Nov 29 2023 at 17:01 UTC