Stream: Coq users

Topic: .coqrc in coqc


view this post on Zulip Janno (Nov 24 2022 at 11:04):

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?

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 15:20):

Your initial impression is essentially right, because _typically_ build systems pass the "skip coqrc" option to coqc, -q.

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 15:21):

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.

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 15:22):

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