Here is an interesting MetaCoq error detected by coq-bench (full log):
# COQC sigma.v # /bin/sh: 1: time: not found # make: *** [Makefile.coq:716: sigma.vo] Error 127 # make: *** [Makefile.coq:339: all] Error 2 # rm: cannot remove 'pretty-timed-success.ok': No such file or directory # make: *** [Makefile.coq:379: make-pretty-timed] Error 1 # make: *** [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
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
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)
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?
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: Jun 01 2023 at 11:01 UTC