Issues · Iris / Iris · GitLab

Slow typechecking / nonterminating Qed when using auxiliary definitions in RAs

#406 · created Mar 03, 2021 by Armaël Guéneau A-coq C-bug I-performance T-algebra
- 3
updated Mar 18, 2021
iFrame performance issues

#402 · created Feb 03, 2021 by Ralf Jung A-coq C-enhancement I-performance T-proofmode
- 1
- 0
updated Feb 17, 2021
Decouple framing and IntoSep

#351 · created Sep 29, 2020 by Ralf Jung A-coq C-enhancement I-performance T-proofmode
- 1
updated Feb 03, 2021
"solve_inG" is very slow for larger RA combinators

#347 · created Sep 21, 2020 by Ralf Jung A-coq C-bug I-performance T-algebra
- 18
updated Mar 03, 2021
Make `contractive_proper` into a lemma, or control other instances that make it costly.

#321 · created May 27, 2020 by Paolo G. Giarrusso A-coq C-enhancement I-performance T-algebra
- 1
- 1
updated Oct 20, 2020
Use `byte` based strings for proof mode

#317 · created May 12, 2020 by Robbert Krebbers A-coq C-enhancement I-performance T-proofmode
- 1
- 7
updated May 16, 2020
Canonical structures have major performance impact

#303 · created Apr 05, 2020 by Robbert Krebbers A-coq C-enhancement I-performance T-bi
- 17
updated May 11, 2020
Guide typeclass search via more specialized typeclasses

#298 · created Mar 06, 2020 by Michael Sammler A-coq C-enhancement I-performance
- 2
updated Jun 17, 2020
Fix performance regressions in Iris and std++ in Coq 8.10.1 compared to Coq 8.9.0

#272 · created Nov 07, 2019 by Robbert Krebbers A-coq I-performance
- 14
updated Feb 12, 2020
Seal off local and frame-preserving update

#203 · created Jul 05, 2018 by Ralf Jung A-coq C-enhancement I-performance T-algebra
- 0
updated Nov 01, 2019
eauto very slow when there is a chain of Iris quantifiers

#188 · created May 23, 2018 by Ralf Jung A-coq C-bug I-performance T-proofmode
- 1
updated Nov 01, 2019
Explore performance implications of gen_proofmode

#180 · created Apr 10, 2018 by Ralf Jung A-coq C-project I-performance T-proofmode
- 3
updated Nov 01, 2019
String-free proofterms

#172 · created Mar 10, 2018 by Ralf Jung A-coq C-project I-performance T-proofmode
- 6
updated Sep 08, 2020