Paolo Giarrusso (Jan 23 2023 at 16:41): 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?
Gaëtan Gilbert (Jan 23 2023 at 16:45):what coq version?
Gaëtan Gilbert (Jan 23 2023 at 16:46):Also Set with default locality shouldn't have an effect beyond the current module
Paolo Giarrusso (Jan 23 2023 at 19:18):Coq 8.16, and .coqrc had #[global] Set Nested Proofs Allowed. — _that_ is on me
Gaëtan Gilbert (Jan 23 2023 at 19:28):yeah I guess ltac2 didn't have -q
Paolo Giarrusso (Jan 23 2023 at 19:28):dune 3.6.1, but I understand that's only used by :standard
Paolo Giarrusso (Jan 23 2023 at 19:28):ditto for theories
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
Paolo Giarrusso (Jan 23 2023 at 19:36):okay, dunestrap gets this right. Nothing to do here...
Paolo Giarrusso (Jan 23 2023 at 21:10):FWIW, (untested) fix for 8.16, AFAICT: https://github.com/Blaisorblade/coq/commit/cff7918c92e5fc02472414b87e5baf725bae5ba9.
Notification Bot (Jan 23 2023 at 21:10):Paolo Giarrusso has marked this topic as resolved.
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)
Ali Caglayan (Jan 23 2023 at 23:29):Please do upate the dune.disabled files we do have there however.
Last updated: Dec 07 2023 at 06:38 UTC