Shea Levy (Oct 12 2020 at 16:27): Shea Levy (Oct 12 2020 at 16:27):Over time I've found myself collecting flags I usually want on (Set Primitive Projections, Set Universe Polymorphism, etc.) and just splat them at the top of each file now. Do people/projects usually do this or do they try to limit it to flags actually needed for the file in question?
Paolo Giarrusso (Oct 12 2020 at 17:29):Some flags get put in all files; your two examples are too dangerous for that. I'm not an expert of the problems with Universe Polymorphism, but they might just be about performance when scaling.
Paolo Giarrusso (Oct 12 2020 at 17:31):OTOH, the semantics of unfolding Primitive Projections aren't that easy to explain, and that implementation detail is not actually fully encapsulated.
Théo Zimmermann (Oct 12 2020 at 20:14):If you want to set a particular file everywhere in your project, then you would save time and space by using the -set / -unset command-line options of coqc.
Enrico Tassi (Oct 13 2020 at 09:07):Paolo Giarrusso said:
OTOH, the semantics of unfolding Primitive Projections aren't that easy to explain, and that implementation detail is not actually fully encapsulated.
Hem, indeed primitive projections do not unfold (they are primitive, not defined). Their unfolding is part of the famous "compat layer" which we all would like to get rid of at some point. Rule of thumb, don't write unfold p for a primitive projection p in your code :-)
Janno (Oct 13 2020 at 11:17):I would like to add a further warning: calling lazy (and maybe other reduction strategies) might very well unfold your primitive projections. (Maybe this is only true on 8.11 but I doubt it.)
Last updated: Sep 23 2023 at 13:01 UTC