Stream: Coq devs & plugin devs

Topic: Why do we have command line typing options?


view this post on Zulip Ali Caglayan (Mar 31 2022 at 21:14):

Why do we have command line typing options like indices-matter and impredicative-set? Can these not be made options like universe polymorphism?

view this post on Zulip Jason Gross (Apr 01 2022 at 00:31):

Some of them are already options, like -type-in-type is Unset Universe Checking, -allow-sprop/-disallow-sprop is Allow StrictProp. We should probably also have options for -indices-matter and -impredicative-set.

view this post on Zulip Enrico Tassi (Apr 01 2022 at 06:19):

not sure the system can switch these things on and off as it goes. either always on or off.

view this post on Zulip Théo Zimmermann (Apr 01 2022 at 09:47):

Impredicative set changes the meaning of Set, so it seems a bit much to ask for an option to do this, but we could maybe have a separate an ImpredicativeSet sort.

view this post on Zulip Paolo Giarrusso (Apr 01 2022 at 09:56):

But IIUC -impredicative-set (used to) work transparently with the normal stdlib, which a separate sort wouldn’t do as well, so making this usable could have an excessive cost?

view this post on Zulip Ali Caglayan (Apr 01 2022 at 10:13):

I am however under the understanding that every constant carries around the environment when it was defined, and by extension the flags in question.

view this post on Zulip Ali Caglayan (Apr 01 2022 at 10:15):

So I understand -impredicative-set is perhaps something we don't want to switch on and off all the time, but -indices-matter, -bytecode-compiler etc. are more what I had in mind.

view this post on Zulip Enrico Tassi (Apr 01 2022 at 13:33):

About these flags, why do you want to have Set something for them? My feeling is that one prefers to put them in a config file (eg _CoqProject). I mean, they are thing you either enable or not for your entire project.

view this post on Zulip Enrico Tassi (Apr 01 2022 at 13:34):

Universe polymorphism can't be made "global" for performance reasons, otherwise it should just be on.

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2022 at 13:36):

performance and backward compatibility

view this post on Zulip Enrico Tassi (Apr 01 2022 at 13:36):

I don't see these options very different from, say, -O2 to gcc so having them a place in the source file seems not natural to me.

view this post on Zulip Jason Gross (Apr 01 2022 at 16:38):

@Enrico Tassi According to stack overflow, you can do

#pragma GCC push_options
#pragma GCC optimize ("O0")

your code

#pragma GCC pop_options

and __attribute__((optimize("O0")))

view this post on Zulip Jason Gross (Apr 01 2022 at 16:41):

I think -indices-matter is closer to positivity checking or -type-in-type (Universe Checking). It applies only to declarations of inductive types, and can very cleanly be granular on the level of inductives. (Furthermore, it might be nice to have coqchk / Print Assumptions report which inductives rely on indices not mattering.) -impredicative-set is a bit more subtle, but I think UniMath uses Unset Universe Checking to define a single "resizing axiom" that contains and makes explicit all uses of universe-unsound-code. I imagine something similar could be done with -impredicative-set?

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 16:57):

indices-matter is a bit annoying because the default is the less-strict mode
AFAIK unimath disables univ checking everywhere
I guess we could control impredicative set usage with something like

Record BoxImpredicativeSet (A:Type) (B:A->Set) : Set := boxImpredicativeSet (_:forall x, B x).

Last updated: Feb 02 2023 at 15:04 UTC