✔ Error message while compiling using a Makefile.local · Coq users

Stream: Coq users

Topic: ✔ Error message while compiling using a Makefile.local

Louise Dubois de Prisque (Feb 08 2022 at 10:19):

Hello,

I tried to write a rule in a Makefile.local to run the benchmarks of my project.
When I run the command coqc foo.v or coqc benchs/foo.v, I do not have any mistake.
However, when I use make my_rule, in which my_rule will run coqc benchs/foo.v benchs/bar.v etc. I have a message Skipping rcfile loading., and I cannot compile foo.v because there is a syntax error.
Do you know what the problem is?
Thanks in advance for your help!

Enrico Tassi (Feb 08 2022 at 10:29):

Can you post your Makefile.local please?

Louise Dubois de Prisque (Feb 08 2022 at 10:35):

https://github.com/smtcoq/sniper/blob/with-trakt/Makefile.local
It is this Makefile and the problem occurs with the rule bench_snipe

Gaëtan Gilbert (Feb 08 2022 at 10:36):

do you have anything in your rc file?

Louise Dubois de Prisque (Feb 08 2022 at 10:41):

I've just discovered how to create Makefiles so I don't even know what it is

Enrico Tassi (Feb 08 2022 at 10:41):

Maybe it's a bug in running coqc a.v b.v

Enrico Tassi (Feb 08 2022 at 10:43):

could you try

bench_snipe: benchs/Arith_bench_snipe.v benchs/List_snipe.v
    $(SHOW)COQC $^
    $(HIDE)for f in $^; do $(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $$f $(TIMING_EXTRA); fi