Stream: Coq devs & plugin devs

Topic: ✔ `.coqrc` leaking into coq stdlib due to dune build?


view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 16:41):

I haven't reproduced this, but I built Coq with Set Nested Proofs Allowed. in .coqrc, and it seems to have leaked into the Coq stdlib... I've seen it for instance in:

Test Nested Proofs Allowed. (* off *)
From Ltac2 Require Import Ltac2.
Test Nested Proofs Allowed.  (* on *)

that might be due to user-contrib/Ltac2/dune having (flags -w -deprecated-native-compiler-option) instead of (flags :standard -w -deprecated-native-compiler-option) — the former will omit -q from the coqc command line, so I think such a leak is expected?

view this post on Zulip Gaëtan Gilbert (Jan 23 2023 at 16:45):

what coq version?

view this post on Zulip Gaëtan Gilbert (Jan 23 2023 at 16:46):

Also Set with default locality shouldn't have an effect beyond the current module

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 19:18):

Coq 8.16, and .coqrc had #[global] Set Nested Proofs Allowed. — _that_ is on me

view this post on Zulip Gaëtan Gilbert (Jan 23 2023 at 19:28):

yeah I guess ltac2 didn't have -q

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 19:28):

dune 3.6.1, but I understand that's only used by :standard

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 19:28):

ditto for theories

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 19:29):

I've learned this by forgetting :standard a few times. Anyway, coq master replaces that by dunestrap, checking there

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 19:36):

okay, dunestrap gets this right. Nothing to do here...

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 21:10):

FWIW, (untested) fix for 8.16, AFAICT: https://github.com/Blaisorblade/coq/commit/cff7918c92e5fc02472414b87e5baf725bae5ba9.

view this post on Zulip Notification Bot (Jan 23 2023 at 21:10):

Paolo Giarrusso has marked this topic as resolved.

view this post on Zulip Karl Palmskog (Jan 23 2023 at 21:14):

hmm, isn't the lesson here is that we should be vigilant for any missing :standard in dune files? (Those dune that specify flags)

view this post on Zulip Ali Caglayan (Jan 23 2023 at 23:29):

Please do upate the dune.disabled files we do have there however.


Last updated: May 28 2023 at 16:30 UTC