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 -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
.
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 ImpredicativeSet
sort.
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 -indices-matter
, -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, -O2
to 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
and __attribute__((optimize("O0")))
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
?
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: Oct 13 2024 at 01:02 UTC