Replace -type-in-type with something else to enable Alectryon?
#1925
Comments
|
@benediktahrens @DanGrayson @rmatthes @m-lindgren What do you think about this? |
|
I think that moving more command-l8ne arguments into Coq files will make it easier for people to use UniMath. (I would like to see the same for other arguments, such as indices-matter.) |
|
I support (2): export “Unset Universe Checking” from Foundations, instead of depending on (My feelings are mostly as they were in the earlier discussion #1696 : (4) seems the best long-term goal, but getting there will be a lot of work and so shouldn’t get entangled with simpler near-term issues; (3) has some disadvantages and no particular advantages over (1)/(2). The Alectryon point, plus the satellites no longer compiling with universe checking, have swung me from “no strong preference between (1) and (2) for now” to “definitely favour (2) for now”.) PR #1697 offered (2) at the time, and I hope it should still basically work — it would need a little updating now, but that shouldn’t be too hard. I’ll do that if I get the chance to, but I’m a bit busy at the moment, so if someone else does sooner that’d be great! |
Opening a new issue in favour of #1696, to revive the discussion here because of semi-recent developments.
In the past, there has been a proposal to replace
-type-in-typewith some form ofUnset Universe Checking, because Alectryon does not support-type-in-type. @peterlefanulumsdaine summarized that we have the following options (from which we might choose different combinations for the short and long term):-type-in-type(current approach)-type-in-typewithExport Unset Universe CheckinginUniMath.Foundations.Init#1697)-type-in-typeby#[local] Unset Universe Checkingin all necessary files #1698)@nmvdw mentioned that recent developments in coq mean that none of our satellites build without
-type-in-type, which means that there are now less objections againstExport Unset Universe Checking.At the very least, in this issue we want to choose:
-type-in-type, or do we want better documentation and implement Alectryon?-type-in-type, how will we get our files to still compile?The text was updated successfully, but these errors were encountered: