Stream: MetaCoq

Topic: MetaCoq depends on time command?


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Guillaume Claret (Oct 05 2020 at 10:21):

Hi

view this post on Zulip Guillaume Claret (Oct 05 2020 at 10:21):

Ah, I have seen this error. Weird indeed

view this post on Zulip Guillaume Claret (Oct 05 2020 at 10:22):

This is because sh does not have a 'time' command, while 'bash' doed

view this post on Zulip Guillaume Claret (Oct 05 2020 at 10:23):

I changed the bench code in order to run commands into 'sh' rather than 'bash'

view this post on Zulip Guillaume Claret (Oct 05 2020 at 10:23):

I mean 'bash' rather than 'sh'

view this post on Zulip 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).

view this post on Zulip Guillaume Claret (Oct 05 2020 at 10:24):

I agree that the standard install does not need timings

view this post on Zulip Guillaume Claret (Oct 05 2020 at 10:25):

OK for the dependency on conf-time

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Oct 05 2020 at 10:42):

Currently we have a rather complicated setup but basically it does the same with multiple subdirectories (one per package)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Oct 05 2020 at 10:44):

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.

view this post on Zulip Matthieu Sozeau (Oct 05 2020 at 10:59):

Ah I see your point, we could indeed change those sub-makefiles to use more delegations

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Oct 05 2020 at 11:18):

Sure, that'd be great !

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Oct 05 2020 at 12:04):

Nope

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Oct 05 2020 at 12:56):

I think what you're seeing is due to the make pretty-timed in translations/Makefile

view this post on Zulip 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: Aug 11 2022 at 01:03 UTC