Bas Spitters (Nov 12 2020 at 14:19): Bas Spitters (Nov 12 2020 at 14:19):What is the most convenient way to enable impredicative-set in vscoq. I assume using Coqproject works, but there may be easier ways.
Yannick Forster (Nov 12 2020 at 14:30):Interesting, I was about to say "There should be a command similar to the command which displays implicit arguments", but there isn't. I don't know an answer, but maybe the easiest way is to add a "Set Impredicative Set" command to vscoq. Once you know what you're doing (@Fabian Kunze, can you help?) that might even be easy and universally helpful
Gaëtan Gilbert (Nov 12 2020 at 14:34):coqproject is your best bet
for unclear reasons impredicative set may not be enabled except by the command line argument
Yannick Forster (Nov 12 2020 at 14:35):Oh, so it's not a vscoq issue, you can also not enable it in Proof General?
Pierre-Marie Pédrot (Nov 12 2020 at 14:41):@Gaëtan Gilbert rather, for unclear reason we allow to set some flags that don't get along together from inside a Coq file.
Théo Zimmermann (Nov 12 2020 at 14:42):In PG, you can do exactly the same (use -arg -impredicative-set in _CoqProject) or use one of the special custom PG configuration variables.
Théo Zimmermann (Nov 12 2020 at 14:42):Pierre-Marie Pédrot said:
Gaëtan Gilbert rather, for unclear reason we allow to set some flags that don't get along together from inside a Coq file.
Like?
Pierre-Marie Pédrot (Nov 12 2020 at 14:43):Like type-in-type.
Pierre-Marie Pédrot (Nov 12 2020 at 14:43):This breaks SR and currently one can fool the checker that way.
Pierre-Marie Pédrot (Nov 12 2020 at 14:44):I am not saying it's a fundamental problem, but being able to locally change the flags governing the kernel rules requires some serious changes in the checker architecture.
Pierre-Marie Pédrot (Nov 12 2020 at 14:44):Also, it's a footgun.
Gaëtan Gilbert (Nov 12 2020 at 14:53):flags that don't get along together
What doe that mean? They start a Coq fight?
Pierre-Marie Pédrot (Nov 12 2020 at 14:53):Or you beat the kernel up.
Pierre-Marie Pédrot (Nov 12 2020 at 14:54):And get random anomalies (in the best case).
Gaëtan Gilbert (Nov 12 2020 at 14:54):the checker already understands declaration-local flags though
(although it gets confused if you change the flag between a section variable and a definition using it)
Gaëtan Gilbert (Nov 12 2020 at 14:55):ty-in-ty is more about nontermination than anomalies
Pierre-Marie Pédrot (Nov 12 2020 at 14:55):If you set it then unset it, you'll have a hard time when unfolding type-in-type defs inside non-type-in-type ones.
Pierre-Marie Pédrot (Nov 12 2020 at 14:56):The only reasonable use of local type-in-type is for stuff that is not unfoldable, e.g. inductive types and axioms.
Gaëtan Gilbert (Nov 12 2020 at 14:56):so you get some type errors, isn't that the user's problem?
Pierre-Marie Pédrot (Nov 12 2020 at 14:56):Or anomalies.
Pierre-Marie Pédrot (Nov 12 2020 at 14:56):Maybe loops, who knows.
Gaëtan Gilbert (Nov 12 2020 at 14:57):what anomalies?
Pierre-Marie Pédrot (Nov 12 2020 at 14:57):I don't have a reproducible example right here but essentially both the checker and the kernel rely implicitly on SR in various parts.
Pierre-Marie Pédrot (Nov 12 2020 at 14:58):Since locally tweaking the kernel rules breaks SR, it's definitely a problem.
Pierre-Marie Pédrot (Nov 12 2020 at 14:59):(And I wouldn't bet on the absence of soundness issues in the checker from this kind of tricks either.)
Gaëtan Gilbert (Nov 12 2020 at 15:10):do they really? I've tried to find anomalies from lack of SR but couldn't figure out how to do it
Pierre-Marie Pédrot (Nov 12 2020 at 15:11):With SProp it should be even easier, shouldn't it?
Pierre-Marie Pédrot (Nov 12 2020 at 15:12):Like, if you can postulate SProp : SProp, you're breaking one of the assumptions of conversion
Pierre-Marie Pédrot (Nov 12 2020 at 15:12):That sorts are always proof relevant
Pierre-Marie Pédrot (Nov 12 2020 at 15:12):now you hide that SProp under a definition
Gaëtan Gilbert (Nov 12 2020 at 15:12):you can get errors easily, but not anomalies
Pierre-Marie Pédrot (Nov 12 2020 at 15:13):I had a few theoretical POCs from type-in-type at a point
Pierre-Marie Pédrot (Nov 12 2020 at 15:13):But it's stuff that is really hard to exploit because you need to hit right in the blind spots of UGraph and friends.
Pierre-Marie Pédrot (Nov 12 2020 at 15:14):I guess I could have crafted a vo but that's kind of heavyweight
Paolo Giarrusso (Nov 12 2020 at 16:00):wait I can enable type-in-type and get past the checker?
Paolo Giarrusso (Nov 12 2020 at 16:01):you know that the French certification authority gives some official trust on the checker :-P
Pierre-Marie Pédrot (Nov 12 2020 at 16:02):See https://github.com/coq/coq/issues/11477
Pierre-Marie Pédrot (Nov 12 2020 at 16:04):in this case it's closer to Pollack-inconsistency than actual inconsistency
Pierre-Marie Pédrot (Nov 12 2020 at 16:04):(but there are ways to build handcrafted vos proving False that the checker happily accepts.)
Théo Winterhalter (Nov 12 2020 at 16:17):And Print Assumptions doesn't track definitions that use local type in type I suppose?
Kenji Maillard (Nov 12 2020 at 16:25):It does
Unset Universe Checking.
Definition a : Type := nat.
Set Universe Checking.
Print Assumptions a.
(* Axioms: *)
(* a relies on an unsafe hierarchy. *)
So the proof of False Pierre-Marie mentions would not be marked as safe then.
Pierre-Marie Pédrot (Nov 12 2020 at 16:27):It's not safe by unfolding.
Pierre-Marie Pédrot (Nov 12 2020 at 16:27):Also Print Assumption is literal piece of garbage.
Pierre-Marie Pédrot (Nov 12 2020 at 16:28):It's a pile of hacks that tries to pierce opacity information in modules, with a bit of duct tape here and there to convince ourselves that we're not doing batshit crazy stuff.
Pierre-Marie Pédrot (Nov 12 2020 at 16:29):The checker is slightly saner but even there it's an approximation (hopefully a sound one, but it's not even clear)
Pierre-Marie Pédrot (Nov 12 2020 at 16:37):Here is a proof that print assumptions is not working:
Universe i j.
Monomorphic Constraint i < j.
Module Type S.
Parameter Inline T : Type@{i}.
End S.
Module F (X : S).
Include X.
End F.
Module LOL <: S.
Unset Universe Checking.
Definition T : Type@{i} := Type@{j}.
Set Universe Checking.
End LOL.
Module PROFIT := F(LOL).
Print PROFIT.T.
Print Assumptions PROFIT.T.
Similar hack without functors but with sections:
Universe i j.
Monomorphic Constraint i < j.
Section Foo.
Unset Universe Checking.
Let T : Type@{i} := Type@{j}.
Set Universe Checking.
Definition S : Type@{i} := T.
End Foo.
Print S.
Print Assumptions S.
On https://github.com/coq/coq/issues/11477, how hard would it be to change --output-context’s default for coqchk?
Paolo Giarrusso (Nov 12 2020 at 17:29):It sounds like it should be easy enough, even for contributors?
Bas Spitters (Nov 13 2020 at 09:27):Coqproject is a workable solution. In PG one can do this:
(* Remember to reload the buffer in Emacs for Proof General to take the local variables into account. *)
(*
*** Local Variables: ***
*** coq-prog-args: ("-impredicative-set") ***
*** End: ***
*)
Last updated: Jan 30 2023 at 19:04 UTC