Dune Coq top skips loading .coqrc

[Blaisorblade]

Desired Behavior

Using dune coq top and dune build on the same source file should use different flags:
dune coq top should let coqtop load ~/.coqrc — to this end, it should not pass the -q flag.

Contrast with dune build, which correctly includes -q in Coq's :standard flag to skip loading .coqrc.

This follows existing practice with coq_makefile and editors and the documented purpose of coqrc: provide custom settings for interactive exploration, while keeping building .vo files reproducible.

---

I suggested this on Zulip and @Alizter asked for a ticket, so here it is.

[Alizter]

Here is a fix #6848

[ejgallego]

Umm, the business with -q is a bit tricky, but I guess we can allow it only on coqtop indeed.

But there is a lot of margin for this to create havoc; in particular users can compile a lib, then dune coq top will fail due to some setting or crap set in .coqrc.

What options are you setting in your .coqrc @Blaisorblade ? I'd rather improve the (coq.theory stanza to let dune know about special interactive-use flags than to hack the flags this way.

[Blaisorblade]

Having dune coq top diverge from dune build is the intended and present behavior; in practice, coq top should be more liberal than build.

then dune coq top will fail due to some setting or crap set in .coqrc.

That could be okay: the user suffering the breakage is the same writing .coqrc. I'm not sure a proposal can prevents this scenario and remain flexible enough. But I have a possible improvement in mind.

What options are you setting in your .coqrc @Blaisorblade ? I'd rather improve the (coq.theory stanza to let dune know about special interactive-use flags than to hack the flags this way.

• My main use case is .coqrc's to let me prototype dirty proofs in the IDE while ensuring they still fail dune build — here is a strawman (but I'll mention reality next):

#[global] Set Nested Proofs Allowed.
#[global] Set Ltac Backtrace.
#[global] Unset SsrIdents.

of course I don't need .coqrc, but without it people write those in their source and sometimes commit them — which is worse.

• .coqrc lets me avoid committing those directives to source code, compared to the coq.theory stanza or anything in-project; maybe we can give up that requirement, because it conflicts with the next one.
• OTOH, making these part of the project might work better in one respect: #[global] Unset SsrIdents. does not actually work. .coqrc needs to load Ltac and ssreflect before it can run Unset SsrIdents. But this would break most clients of Coq rewrite — so currently, my actual .coqrc comments out #[global] Unset SsrIdents..

(* Load Ltac *)
Require Import Ltac.
(* Settings for the coqrc proper. *)
#[global] Set Nested Proofs Allowed.
#[global] Set Ltac Backtrace.

(* Load ssreflect. Too invasive! *)
(*
From Coq.ssr Require Import ssreflect.

(* Settings for the coqrc proper. *)
#[global] Unset SsrIdents.
*)

• If something like .coqrc were project-local, the above #[global] Unset SsrIdents. could be enabled in projects that use ssreflect. OTOH, I'm not sure how many projects would bother committing these changes, so I might want to keep the settings private if possible, and ideally not as uncommitted changes. Maybe the settings could live some dune-local file, or that file could point to a .v file with the right settings, or <insert bikeshedding here>.

[ejgallego]

Very interesting, thanks @Blaisorblade ; I agree that interactive vs batch mode are different. coq-lsp should not require these kind of hacks tho (you need LTAC backtraces, you can ask them from the IDE, etc...)

I guess removing -q is fine then.

In general, I think that when interactively editing a .v file, when you save it, the .vo file should be written so you can reuse the checking done in the interactive edition. coq-lsp can already do that, but we won't enable it until 0.2

So you can just edit a file, don't worry if something is broken (coq-lsp recovers well), switch to a file depending on that, etc... IMHO much more seamless; but that requires forbidding .coqrc hacks in favor of proper features.

[Blaisorblade]

It sounds like you're fine with this patch for now. And it's fine if coq-lsp decides to not support .coqrc, since it's a completely different model anyway.

[Alizter]

FTR #3924 predicted this issue would happen.