Stream: Coq users

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


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

view this post on Zulip Enrico Tassi (Feb 08 2022 at 10:29):

Can you post your Makefile.local please?

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

view this post on Zulip Gaëtan Gilbert (Feb 08 2022 at 10:36):

do you have anything in your rc file?

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

view this post on Zulip Enrico Tassi (Feb 08 2022 at 10:41):

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

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

view this post on Zulip Louise Dubois de Prisque (Feb 08 2022 at 11:12):

This new code does not work because of a syntax error but I created a rule for each file and it works so thank you

view this post on Zulip Notification Bot (Feb 08 2022 at 11:16):

Enrico Tassi has marked this topic as resolved.

view this post on Zulip Ali Caglayan (Feb 08 2022 at 14:17):

We don't support coqc a.v b.v and we should probably disallow it.

view this post on Zulip Gaëtan Gilbert (Feb 08 2022 at 14:18):

it is disallowed

view this post on Zulip Gaëtan Gilbert (Feb 08 2022 at 14:19):

since 8.14 https://github.com/coq/coq/pull/13876

view this post on Zulip Enrico Tassi (Feb 08 2022 at 14:34):

So that is the error @LouiseDDP was talking about maybe?

view this post on Zulip Ali Caglayan (Feb 08 2022 at 14:39):

The repo is for coq 8.13 so it is still possible to pass two .v files to coqc

view this post on Zulip Ali Caglayan (Feb 08 2022 at 14:40):

It probably mangles the syntax giving a syntax error

view this post on Zulip Ali Caglayan (Feb 08 2022 at 14:40):

Hence why it was disabled in 8.14

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 16:18):

Yes it has not been safe since a long time


Last updated: Jan 29 2023 at 01:02 UTC