Why do we have command line typing options like indices-matter and impredicative-set? Can these not be made options like universe polymorphism?
Some of them are already options, like
Unset Universe Checking,
Allow StrictProp. We should probably also have options for
not sure the system can switch these things on and off as it goes. either always on or off.
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
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?
I am however under the understanding that every constant carries around the environment when it was defined, and by extension the flags in question.
So I understand
-impredicative-set is perhaps something we don't want to switch on and off all the time, but
-bytecode-compiler etc. are more what I had in mind.
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.
Universe polymorphism can't be made "global" for performance reasons, otherwise it should just be on.
performance and backward compatibility
I don't see these options very different from, say,
gcc so having them a place in the source file seems not natural to me.
@Enrico Tassi According to stack overflow, you can do
#pragma GCC push_options #pragma GCC optimize ("O0") your code #pragma GCC pop_options
-indices-matter is closer to positivity checking or
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
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