Coq Bugs affecting Iris development
Priority [HIGH] means that this actively affects how we do things and we have not found a workaround. For [MEDIUM] we have an acceptable workaround or accounted for it sufficiently by changing our design. The rest is [LOW].
- [HIGH] #5752:
Hint Modebehaves differently for local context
- [HIGH] #9058:
Hint Modecancels entire search too early. For this reason we cannot use
Hint Mode Equiv ! : typeclass_instances, so we suffer from backtracking and loops whenever
Equiv ?comes up.
- [HIGH] #7916: Cannot set mode for
setoid_rewritemakes some strange queries, so we suffer from backtracking and slow rewriting whenever
Reflexive ?comes up.
- [MEDIUM] #6714:
Set Typeclasses Unique Instancesdoes not have any (or at least not the expected) effect. Work-around:
- [MEDIUM] #7914: TC resolution is unable to use the fact that
Propis a subtype of
Type. Work-around: Have a separate typeclass
- [MEDIUM] #6583:
applytriggers TC resolution on unrelated goals so proof mode tactics randomly fail when the user has other typeclass goals open. Work-around: Use
typeclasses eautoinstead of
apply _and otherwise
notypeclasses refineinstead of
apply. It's hard to tell if we got this all right, though, and it may not just be
applythat does this.
- [LOW] #7364: Debugging TC issues is very hard.
- [LOW] #9643: We could use better profiling.
- [LOW] #9131: Custom error messages for TC search failure would help for IPM user experience
Unification / Type inference
- [HIGH] #6294:
apply(including TC search) and canonical structures don't mix very well, so we randomly use
apply:and cannot grow our algebraic hierarchy any further.
- [MEDIUM] #9135
refineand friends ignore
Opaque. See #301 (closed) for the corresponding issue in Iris.
- [MEDIUM] #5699:
rewrite /foodoes not work for primitive projections. Work-around: Use
- [LOW] #5698, #5250, #6994: Primitive projections behave strange.
- [HIGH] #4381:
Tactic Notationcannot set a scope for
constrarguments, so we very often have to write
- [MEDIUM] #2901:
destruct Hdoes not clear
Hif it is a section variable. Work-around in
naive_solver: Clear manually.
- [MEDIUM] #7773:
setoid_rewritefails where (ssreflect)
rewrite ->succeed. Work-around: Don't use
setoid_rewrite. (So far, no case has come up where we absolutely needed
- [MEDIUM] #12011:
rewrite ... in(ssreflect) fails where
rewrite -> ... inworks. Work-around: Use the latter instead of the former.
- [LOW] #6042:
Generalizable All Variablesaffects
- [LOW] #9661: Cannot disable generalization of implicit arguments in
Coq Bugs recently fixed / features recently introduced that we are not (yet) taking advantage of
#6923: Proper control over how
Setis propagated on imports. Available since 8.8.
- #7910: We can control type-checking to be more bidirectional, which helps enormously with telescopes and the like. Available starting with 8.11.
- #10076: We can make some projections non-canonical, to hopefully fix all these "redundant-canonical-projection" warnings. Available starting with 8.11.