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!
Can you post your Makefile.local please?
It is this Makefile and the problem occurs with the rule
do you have anything in your rc file?
I've just discovered how to create Makefiles so I don't even know what it is
Maybe it's a bug in running
coqc a.v b.v
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
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
Enrico Tassi has marked this topic as resolved.
We don't support
coqc a.v b.v and we should probably disallow it.
it is disallowed
since 8.14 https://github.com/coq/coq/pull/13876
So that is the error @LouiseDDP was talking about maybe?
The repo is for coq 8.13 so it is still possible to pass two .v files to coqc
It probably mangles the syntax giving a syntax error
Hence why it was disabled in 8.14
Yes it has not been safe since a long time
Last updated: Jan 29 2023 at 01:02 UTC