|
|
# Coq Bugs affecting Iris development
|
|
|
|
|
|
Bugs we cannot work around to a satisfying degree:
|
|
|
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].
|
|
|
|
|
|
* [#4381](https://github.com/coq/coq/issues/4381): `Tactic Notation` cannot set a scope for `constr` arguments, so we very often have to write `%I` manually.
|
|
|
* [#5735](https://github.com/coq/coq/issues/5735): Cannot use `Hint Mode Equiv ! : typeclass_instances`, so we suffer from backtracking and loops whenever `Equiv ?` comes up.
|
|
|
* [#6294](https://github.com/coq/coq/issues/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.
|
|
|
* [#6583](https://github.com/coq/coq/issues/6583): `apply` triggers TC resolution on unrelated goals so proof mode tactics randomly fail when the user has other typeclass goals open. Work-around: Use `typeclasses eauto` instead of `apply _` and otherwise `notypeclasses refine` instead of `apply`. It's hard to tell if we got this all right, though, and it may not just be `apply` that does this.
|
|
|
* [#7769](https://github.com/coq/coq/issues/7769): Ltac backtraces show up in proof mode error messages so the user is presented with (sometimes huge) amounts of noise. Partial work-around: Give names to locally bound functions so at least it does not print Ltac source code. However, Ltac function names are still printed.
|
|
|
* [#7910](https://github.com/coq/coq/issues/7910): Type inference needs lots of help for notations involving telescopes, with bad side-effects on printing that same notation. We have to write tons of annotations in our notation and live with printing not always working. (We could duplicate our notations to work around that but that's be lots of code duplication.)
|
|
|
* [#7916](https://github.com/coq/coq/issues/7916): Cannot set mode for `Reflexive` because `setoid_rewrite` makes some strange queries, so we suffer from backtracking and slow rewriting whenever `Reflexive ?` comes up.
|
|
|
* [#7922](https://github.com/coq/coq/issues/7922): Cannot convert between strings and identifiers in Ltac, leading to horrible code and lots of hacks all over the place.
|
|
|
### Ltac vs strings
|
|
|
|
|
|
Bugs for which we carry "good enough" work-arounds, or that influenced the design:
|
|
|
- [#7922](https://github.com/coq/coq/issues/7922): Cannot convert between strings and identifiers in Ltac, leading to horrible code and lots of hacks all over the place.
|
|
|
- There [is a prototype plugin](https://github.com/ppedrot/coq-string-ident), but it doesn't compile any more and also it never worked very well: `let x = "foo" in ident_of_string x` was not supported.
|
|
|
|
|
|
* [#2901](https://github.com/coq/coq/issues/2901): `destruct H` does not clear `H` if it is a section variable. Work-around in `naive_solver`: Clear manually.
|
|
|
* [#5699](https://github.com/coq/coq/issues/5699): `rewrite /foo` does not work for primitive projections. Work-around: Use `unfold`.
|
|
|
* [#6714](https://github.com/coq/coq/issues/6714): `Set Typeclasses Unique Instances` does not have any (or at least not the expected) effect. Work-around: `Class NoBackTrack`.
|
|
|
* [#7773](https://github.com/coq/coq/issues/7773): `setoid_rewrite` fails where (ssreflect) `rewrite` and `rewrite ->` succeed. Work-around: Don't use `setoid_rewrite`. (So far, no case has come up where we absolutely needed `setoid_rewrite`.)
|
|
|
* [#7914](https://github.com/coq/coq/issues/7914): TC resolution is unable to use the fact that `Prop` is a subtype of `Type`. Work-around: Have a separate typeclass `IntoPureT` that uses `refine` through a `Hint Extern`.
|
|
|
### Typeclasses
|
|
|
|
|
|
Nuisances affecting us but not changing the way we do things:
|
|
|
- [HIGH] [#5752](https://github.com/coq/coq/issues/5752): `Hint Mode` behaves differently for local context
|
|
|
- [HIGH] [#5735](https://github.com/coq/coq/issues/5735): `Hint Mode` cancels 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](https://github.com/coq/coq/issues/7916): Cannot set mode for `Reflexive` because `setoid_rewrite` makes some strange queries, so we suffer from backtracking and slow rewriting whenever `Reflexive ?` comes up.
|
|
|
- [MEDIUM] [#6714](https://github.com/coq/coq/issues/6714): `Set Typeclasses Unique Instances` does not have any (or at least not the expected) effect. Work-around: `Class NoBackTrack`.
|
|
|
- [MEDIUM] [#7914](https://github.com/coq/coq/issues/7914): TC resolution is unable to use the fact that `Prop` is a subtype of `Type`. Work-around: Have a separate typeclass `IntoPureT` that uses `refine` through a `Hint Extern`.
|
|
|
- [MEDIUM] [#6583](https://github.com/coq/coq/issues/6583): `apply` triggers TC resolution on unrelated goals so proof mode tactics randomly fail when the user has other typeclass goals open. Work-around: Use `typeclasses eauto` instead of `apply _` and otherwise `notypeclasses refine` instead of `apply`. It's hard to tell if we got this all right, though, and it may not just be `apply` that does this.
|
|
|
- [LOW] [#7364](https://github.com/coq/coq/issues/7364): Debugging TC issues is very hard.
|
|
|
- [LOW] [#9643](https://github.com/coq/coq/issues/9643): We could use better profiling.
|
|
|
- [LOW] [#9131](https://github.com/coq/coq/issues/9131): Custom error messages for TC search failure would help for IPM user experience
|
|
|
|
|
|
* [#5698](https://github.com/coq/coq/issues/5698), [#5250](https://github.com/coq/coq/issues/5250): Primitive projections behave strange.
|
|
|
* [#6042](https://github.com/coq/coq/issues/6042): `Generalizable All Variables` affects `Instance`.
|
|
|
### Unification / Type inference
|
|
|
|
|
|
* [HIGH] [#6294](https://github.com/coq/coq/issues/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.
|
|
|
* [HIGH] [#7910](https://github.com/coq/coq/issues/7910): Type inference needs lots of help for notations involving telescopes, with bad side-effects on printing that same notation. We have to write tons of annotations in our notation and live with printing not always working. (We could duplicate our notations to work around that but that's be lots of code duplication.)
|
|
|
|
|
|
### Primitive projections
|
|
|
|
|
|
* [MEDIUM] [#5699](https://github.com/coq/coq/issues/5699): `rewrite /foo` does not work for primitive projections. Work-around: Use `unfold`.
|
|
|
* [LOW] [#5698](https://github.com/coq/coq/issues/5698), [#5250](https://github.com/coq/coq/issues/5250), [#6994](https://github.com/coq/coq/issues/6994): Primitive projections behave strange.
|
|
|
|
|
|
### Miscellaneous
|
|
|
|
|
|
* [HIGH] [#4381](https://github.com/coq/coq/issues/4381): `Tactic Notation` cannot set a scope for `constr` arguments, so we very often have to write `%I` manually.
|
|
|
* [MEDIUM] [#2901](https://github.com/coq/coq/issues/2901): `destruct H` does not clear `H` if it is a section variable. Work-around in `naive_solver`: Clear manually.
|
|
|
* [MEDIUM] [#7773](https://github.com/coq/coq/issues/7773): `setoid_rewrite` fails where (ssreflect) `rewrite` and `rewrite ->` succeed. Work-around: Don't use `setoid_rewrite`. (So far, no case has come up where we absolutely needed `setoid_rewrite`.)
|
|
|
* [LOW] [#6042](https://github.com/coq/coq/issues/6042): `Generalizable All Variables` affects `Instance`.
|
|
|
* [LOW] [#9661](https://github.com/coq/coq/issues/9661): Cannot disable generalization of implicit arguments in `` `{...} ``.
|
|
|
|
|
|
# Coq Bugs recently fixed / features recently introduced that we are not (yet) taking advantage of
|
|
|
|
... | ... | |