Karl Palmskog (Oct 05 2020 at 10:09): Karl Palmskog (Oct 05 2020 at 10:09):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.
Karl Palmskog (Oct 05 2020 at 10:11):If it turns out to be MetaCoq, you need to add conf-time as an OPAM dependency in the appropriate package(s).
Karl Palmskog (Oct 05 2020 at 10:14):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
Guillaume Claret (Oct 05 2020 at 10:21):Ah, I have seen this error. Weird indeed
Guillaume Claret (Oct 05 2020 at 10:22):This is because sh does not have a 'time' command, while 'bash' doed
Guillaume Claret (Oct 05 2020 at 10:23):I changed the bench code in order to run commands into 'sh' rather than 'bash'
Guillaume Claret (Oct 05 2020 at 10:23):I mean 'bash' rather than 'sh'
Karl Palmskog (Oct 05 2020 at 10:24):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).
Guillaume Claret (Oct 05 2020 at 10:24):I agree that the standard install does not need timings
Guillaume Claret (Oct 05 2020 at 10:25):OK for the dependency on conf-time
Matthieu Sozeau (Oct 05 2020 at 10:31):We use that mainly for the CI, let's make it configurable. Also the timing scripts depend on python IIRC
Karl Palmskog (Oct 05 2020 at 10:40):@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
Karl Palmskog (Oct 05 2020 at 10:41):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)
Karl Palmskog (Oct 05 2020 at 10:43):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.
Matthieu Sozeau (Oct 05 2020 at 10:59):Ah I see your point, we could indeed change those sub-makefiles to use more delegations
Karl Palmskog (Oct 05 2020 at 11:07):@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.
Matthieu Sozeau (Oct 05 2020 at 11:18):Sure, that'd be great !
Karl Palmskog (Oct 05 2020 at 12:03):any particular reason you're using 8.11.0 rather than 8.11.2 in the CI?
Matthieu Sozeau (Oct 05 2020 at 12:04):Nope
Karl Palmskog (Oct 05 2020 at 12:09):interesting, it seems pretty-timed was already being passed explicitly: https://travis-ci.com/github/MetaCoq/metacoq/jobs/394094049#L4188
Matthieu Sozeau (Oct 05 2020 at 12:56):I think what you're seeing is due to the make pretty-timed in translations/Makefile
Karl Palmskog (Oct 05 2020 at 13:28):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