I was always under the impression that
.coqrc was only (automatically) used by
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,
COQFLAGS?=-q $(OTHERFLAGS) $(COQFILTEREDEXTRAFLAGS) $(COQNATIVEFLAG)
rm _build/default/.../foo.vo; dune --display verbose --cache disabled should also show
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: Feb 01 2023 at 13:03 UTC