I was always under the impression that .coqrc
was only (automatically) used by coqtop
, not coqc
, and that also seems to be supported by local experiments. However, https://coq.inria.fr/refman/practical-tools/coq-commands.html#by-resource-file states that it is also supposed to be executed by coqc
. Am I misreading the documentation?
Your initial impression is essentially right, because _typically_ build systems pass the "skip coqrc" option to coqc, -q
.
e.g. coq_makefile
's output
COQFLAGS?=-q $(OTHERFLAGS) $(COQFILTEREDEXTRAFLAGS) $(COQNATIVEFLAG)
and rm _build/default/.../foo.vo; dune --display verbose --cache disabled
should also show bin/coqc -q
.
In _both_ cases, it's easy to forget -q
when overriding flags — e.g. in dune
files it's enough to write (flags your_flags)
instead of (flags :standard your_flags)
.
Last updated: Oct 13 2024 at 01:02 UTC