Issues · Iris / Iris

New issue

iRewrite: Support rewriting with Coq hypotheses

#152 · opened Feb 07, 2018 by Ralf Jung A-coq C-enhancement T-proofmode
- 0
updated Nov 01, 2019
Exponential slowdown in `iFrame` and the number of laters

#153 · opened Feb 08, 2018 by Robbert Krebbers
- CLOSED
- 1
- 0
updated Feb 20, 2018
Bring back side-conditionals for `iMod`

#154 · opened Feb 12, 2018 by Robbert Krebbers T-proofmode
- CLOSED
- 1
- 5
updated Jul 13, 2018
Make `iPureIntro` able to introduce affine pure assertions when the context is emtpy.

#155 · opened Feb 13, 2018 by Jacques-Henri Jourdan C-enhancement
- CLOSED
- 8
updated Feb 15, 2018
How to deal with `emp`, `True`, and friends when the BI is ambigious

#156 · opened Feb 14, 2018 by Robbert Krebbers Generalized Proofmode Merger T-proofmode
- CLOSED
- 1
- 4
updated Jul 13, 2018
`done` loops in proofmode

#157 · opened Feb 20, 2018 by Robbert Krebbers Generalized Proofmode Merger
- CLOSED
- 8
updated Mar 07, 2018
Make clear which arguments of tactics are optional in `ProofMode.md`

#158 · opened Feb 23, 2018 by Robbert Krebbers A-docs C-enhancement Good First Issue T-proofmode
- CLOSED
- 2
updated Dec 19, 2020
Find better name for "emp |- P"

#159 · opened Feb 26, 2018 by Ralf Jung Generalized Proofmode Merger T-proofmode
- CLOSED
- 10
updated Jul 13, 2018
Figure out the best place for the plainly modality

#160 · opened Feb 26, 2018 by Ralf Jung Generalized Proofmode Merger
- CLOSED
- 15
updated Mar 03, 2018
Use `plainly_alt` as an axiom and replace most of the current ones

#161 · opened Feb 26, 2018 by Jacques-Henri Jourdan A-theory C-project T-bi
- CLOSED
- 66
updated Mar 18, 2020
Have `iFrame` smartly instantiate existentials

#162 · opened Feb 27, 2018 by Jacques-Henri Jourdan
- CLOSED
- 13
updated Mar 03, 2018
Dealing with nested modalities in `iModIntro` 1 of 3 tasks completed

#163 · opened Feb 28, 2018 by Robbert Krebbers A-coq C-project T-proofmode
- 33
updated Jun 29, 2020
Take a closer look at the interaction of fancy updates and plainly

#164 · opened Mar 03, 2018 by Ralf Jung
- CLOSED
- 1
- 16
updated Oct 31, 2018
Better (?) approach to control typeclass resolution based on whether some arguments are evars

#165 · opened Mar 06, 2018 by Ralf Jung A-coq C-project T-proofmode
- 0
updated Nov 01, 2019
iDestruct on a conjunction magically transforms hypothesis

#166 · opened Mar 07, 2018 by Ralf Jung A-coq C-project T-linear T-proofmode
- 15
updated Nov 01, 2019
iMod should be able to eliminate <pers> and <plain> in the intuitionistic context

#167 · opened Mar 07, 2018 by Ralf Jung A-coq C-enhancement T-proofmode
- 8
updated Nov 01, 2019
iSpecialize on implications behaves inconsistently

#168 · opened Mar 07, 2018 by Ralf Jung A-coq C-project T-proofmode
- 7
updated Nov 01, 2019
Applying plain implications fails

#169 · opened Mar 08, 2018 by Ralf Jung A-coq C-bug T-proofmode
- 0
updated Nov 01, 2019
iFresh should reserve fresh names

#170 · opened Mar 08, 2018 by Joseph Tassarotti T-proofmode
- CLOSED
- 2
updated Jul 13, 2018
Split derived_laws.v

#171 · opened Mar 08, 2018 by Ralf Jung T-proofmode
- CLOSED
- 1
updated Mar 21, 2018
String-free proofterms

#172 · opened Mar 10, 2018 by Ralf Jung A-coq C-project I-performance T-proofmode
- 6
updated Sep 08, 2020
Ambiguous reference to eqb in coq_tactics.v

#173 · opened Mar 12, 2018 by Ghost User
- CLOSED
- 3
updated Mar 12, 2018
Confusing result by `wp_op`

#174 · opened Mar 19, 2018 by Robbert Krebbers
- CLOSED
- 1
updated Apr 22, 2018
Replace booleans in proofmode typeclasses by a more informative type

#175 · opened Mar 19, 2018 by Ralf Jung A-coq C-enhancement T-proofmode
- 0
updated Nov 01, 2019
Reconsider normalizing `/\ emp` into `<affine>`

#176 · opened Mar 20, 2018 by Ralf Jung Generalized Proofmode Merger T-proofmode
- CLOSED
- 1
- 3
updated Jul 13, 2018
Improve naming of lemmas about modalities 0 of 1 task completed

#177 · opened Mar 21, 2018 by Ralf Jung Generalized Proofmode Merger T-proofmode
- CLOSED
- 1
- 7
updated Jul 13, 2018
`MIEnvIsEmpty` and `MIEnvTransform` have inconsistent behaviors

#178 · opened Apr 09, 2018 by Jacques-Henri Jourdan A-coq C-bug T-proofmode
- 4
updated Nov 01, 2019
Strengthen strong allocation lemmas to work for any infinite set

#179 · opened Apr 09, 2018 by Ralf Jung
- CLOSED
- 1
updated Feb 17, 2019
Explore performance implications of gen_proofmode

#180 · opened Apr 10, 2018 by Ralf Jung A-coq C-project I-performance T-proofmode
- 3
updated Nov 01, 2019
wp_apply instantiates evars too far

#181 · opened Apr 19, 2018 by Ralf Jung T-proofmode
- CLOSED
- 2
updated Jul 13, 2018
done when goal is evar picks unnecessarily strong

#182 · opened Apr 19, 2018 by Ralf Jung T-proofmode
- CLOSED
- 1
- 3
updated Jul 13, 2018
Stronger/Weaker iFrame

#183 · opened Apr 20, 2018 by Ralf Jung A-coq C-project T-proofmode
- 6
updated Feb 03, 2021
`wp_binop` is not very useful for comparing arbitrary values

#184 · opened Apr 22, 2018 by Dan Frumin
- CLOSED
- 3
updated May 03, 2018
"iApply ... with" unifies with assumptions before taking goal into account

#185 · opened Apr 23, 2018 by Ralf Jung A-coq C-enhancement T-proofmode
- CLOSED
- 2
updated Nov 01, 2019
iAssert without any spatial assumptions should produce a persistent result

#186 · opened Apr 24, 2018 by Ralf Jung A-coq C-enhancement T-proofmode
- 2
- 2
updated Sep 29, 2020
Support framing in `iCombine`.

#187 · opened May 18, 2018 by Dan Frumin
- CLOSED
- 1
- 2
updated Jul 13, 2018
eauto very slow when there is a chain of Iris quantifiers

#188 · opened May 23, 2018 by Ralf Jung A-coq C-bug I-performance T-proofmode
- 1
updated Nov 01, 2019
Tests do not compile on MacOS

#189 · opened May 24, 2018 by Léon Gondelman
- CLOSED
- 11
updated May 31, 2018
Framing persistent hypotheses under a later in the goal

#190 · opened May 31, 2018 by Hai Dang
- CLOSED
- 1
- 1
updated Jul 13, 2018
Printing of the sequence operator `;;`

#191 · opened Jun 04, 2018 by Marianna Rapoport
- CLOSED
- 3
updated Jun 13, 2018
Document `iRewrite -...` in `ProofMode.md`

#192 · opened Jun 04, 2018 by Dan Frumin
- CLOSED
- 3
updated Jan 11, 2019
Remove or fix `base_logic/deprecated.v`

#193 · opened Jun 05, 2018 by Robbert Krebbers Generalized Proofmode Merger T-proofmode
- CLOSED
- 1
- 3
updated Jul 13, 2018
coq-speed: Measure using performance counters

#194 · opened Jun 05, 2018 by Ralf Jung A-infra
- CLOSED
- 15
updated Jun 22, 2018
Always qualify Instance with Local or Global

#195 · opened Jun 05, 2018 by Ralf Jung A-coq C-enhancement T-style
- CLOSED
- 1
- 6
updated Jan 07, 2021
Extend `iApply` to deal with pure goals

#196 · opened Jun 07, 2018 by Glen Mével A-coq C-enhancement T-proofmode
- 1
- 1
updated Nov 01, 2019
iFrame sometimes needs to be called twice

#197 · opened Jun 10, 2018 by Ralf Jung T-proofmode
- CLOSED
- 21
updated Jun 14, 2018
iAlways fails without a proper error message

#198 · opened Jun 10, 2018 by Ralf Jung T-proofmode
- CLOSED
- 1
- 1
updated Jul 13, 2018
iSplitL no longer checks if assumptions are spatial

#199 · opened Jun 10, 2018 by Ralf Jung T-proofmode
- CLOSED
- 3
updated Jun 10, 2018
Framing: Make* classes lead to suboptimal results

#200 · opened Jun 13, 2018 by Ralf Jung T-proofmode
- CLOSED
- 2
updated Jul 13, 2018
Improve "... not found" error messages

#201 · opened Jun 14, 2018 by Ralf Jung T-proofmode
- CLOSED
- 1
updated Jan 11, 2019
Use of `Into`/`From`/`As`/`Is` prefixes of classes is inconsistent

#202 · opened Jun 18, 2018 by Robbert Krebbers A-coq C-enhancement T-proofmode T-style
- 0
updated Nov 06, 2020
Seal off local and frame-preserving update

#203 · opened Jul 05, 2018 by Ralf Jung A-coq C-enhancement I-performance T-algebra
- 0
updated Nov 01, 2019
Support `iInduction .. using ...`

#204 · opened Jul 10, 2018 by Robbert Krebbers
- CLOSED
- 0
updated Aug 29, 2018
Make notation for pure and plainly affine

#205 · opened Jul 13, 2018 by Ralf Jung A-coq C-project T-linear
- 1
- 5
updated Jan 29, 2021
Missing error message with `iDestruct ... as "#..."`

#206 · opened Jul 31, 2018 by Ralf Jung T-proofmode
- CLOSED
- 1
- 4
updated Jan 23, 2019
Rule "Res-Alloc" in documentation is stronger than the Coq version

#207 · opened Aug 16, 2018 by Joseph Tassarotti
- CLOSED
- 1
- 6
updated Mar 06, 2019
Import Coq.Strings.Ascii before using ascii notations

#208 · opened Aug 24, 2018 by Ghost User
- CLOSED
- 10
updated Aug 24, 2018
Iris 3.1.0 is compatible with Coq 8.8.1 and coq-mathcomp-ssreflect 1.7.0

#209 · opened Aug 29, 2018 by Janno
- CLOSED
- 2
updated Aug 29, 2018
Generic subset construction for RAs

#210 · opened Aug 29, 2018 by Ralf Jung A-theory C-project T-algebra
- 2
updated Sep 08, 2020
Masks are coPsets in the Coq development, not arbitrary subsets of natural numbers

#211 · opened Oct 01, 2018 by Joseph Tassarotti A-docs C-enhancement
- CLOSED
- 1
- 1
updated Mar 18, 2020
iMod: Control which modality is reduced

#212 · opened Oct 03, 2018 by Ralf Jung A-coq C-project T-proofmode
- 10
updated Nov 01, 2019
Moving hypotheses from the intuitionistic to the spatial context

#213 · opened Oct 04, 2018 by Robbert Krebbers A-coq C-enhancement T-proofmode
- CLOSED
- 1
- 0
updated Feb 18, 2020
Werid bug with `env_notations` and stdpp's `destruct_and!` tactic.

#214 · opened Oct 11, 2018 by Dan Frumin
- CLOSED
- 4
updated Oct 12, 2018
Explore getting rid of implication

#215 · opened Oct 13, 2018 by Ralf Jung A-theory
- CLOSED
- 8
updated Nov 01, 2019
Replace most occurences of `.. || ..` by `first [..|..]`

#216 · opened Oct 14, 2018 by Robbert Krebbers A-coq C-bug T-proofmode
- 3
updated Feb 02, 2021
Remove duplicate abstraction

#218 · opened Oct 26, 2018 by Ghost User
- CLOSED
- 1
updated Oct 29, 2018
What are arrows in the category of CMRAs?

#219 · opened Nov 22, 2018 by Jacques-Henri Jourdan
- CLOSED
- 1
- 2
updated Nov 28, 2018
wp_cas_suc fails with total weakest precondition

#220 · opened Nov 27, 2018 by Aleš Bizjak
- CLOSED
- 1
updated Nov 30, 2018
Coqdocs should link to std++ coqdocs

#221 · opened Nov 30, 2018 by Ralf Jung Iris 3.2
- CLOSED
- 2
updated Jun 06, 2019
Can't iSpecialize/iDestruct with (("A" with "B") with "C")

#222 · opened Dec 03, 2018 by Paolo G. Giarrusso
- CLOSED
- 1
updated Dec 03, 2018
Module `iris.algebra.big_op` exports unqualified `foo`

#223 · opened Dec 08, 2018 by Paolo G. Giarrusso
- CLOSED
- 1
updated Dec 20, 2018
Define persistence otherwise (and get rid of core)

#224 · opened Dec 18, 2018 by Ralf Jung A-theory C-project T-bi
- 1
- 21
updated Aug 28, 2020
`is_closed_expr` is stronger than stability under `subst`

#225 · opened Dec 28, 2018 by Dan Frumin
- CLOSED
- 7
updated Jan 06, 2019
Typeclass interference does not work for Timeless (□ P)

#226 · opened Feb 12, 2019 by Michael Sammler
- CLOSED
- 4
updated Feb 12, 2019
Provide a convenient way to define non-recursive ghost state

#227 · opened Feb 19, 2019 by Ralf Jung A-coq A-theory C-project T-algebra T-base_logic
- 1
- 5
updated Dec 07, 2020
"expression validity" in WP

#228 · opened Feb 19, 2019 by Jonas Kastberg A-theory C-project T-program_logic
- 19
updated Nov 01, 2019
Odd Behavior for Substitution

#229 · opened Feb 20, 2019 by Daniel Gratzer
- CLOSED
- 6
updated Mar 12, 2020
"Generalizable All Variables" considered harmful

#230 · opened Feb 22, 2019 by Ralf Jung
- CLOSED
- 4
updated Feb 27, 2019
Allow swapping later^i and forall, later, etc.

#231 · opened Mar 02, 2019 by Paolo G. Giarrusso
- CLOSED
- 4
updated Nov 01, 2019
Investigate slowdown caused by gset change

#232 · opened Mar 14, 2019 by Ralf Jung
- CLOSED
- 1
- 9
updated Apr 24, 2019
Can't install on Coq 8.8.1

#233 · opened Mar 19, 2019 by Maximilian Wuttke
- CLOSED
- 2
updated Mar 20, 2019
Syntactic type system for heap_lang 0 of 2 tasks completed

#234 · opened Mar 29, 2019 by Robbert Krebbers A-theory C-project T-heap_lang
- CLOSED
- 31
updated Oct 01, 2020
Documentation for the algebra folder

#235 · opened Mar 30, 2019 by Robbert Krebbers A-docs C-enhancement T-algebra
- 2
- 1
updated Nov 01, 2019
Non-expansiveness for big ops

#236 · opened Apr 07, 2019 by Dan Frumin A-coq C-enhancement Good First Issue T-bi
- CLOSED
- 4
updated Mar 19, 2020
Stripping laterN from pure propositions when proving laterN *without except-0*

#237 · opened Apr 15, 2019 by Paolo G. Giarrusso
- CLOSED
- 2
updated Nov 01, 2019
Wish: iSimpl on multiple hypothesis

#238 · opened Apr 26, 2019 by Dan Frumin C-enhancement T-proofmode
- CLOSED
- 1
- 0
updated May 22, 2019
Iris logo

#239 · opened May 06, 2019 by Robbert Krebbers A-meta C-project
- CLOSED
- 27
updated Feb 05, 2021
We have ambiguous coercion paths

#240 · opened May 13, 2019 by Ralf Jung A-coq C-bug T-algebra
- CLOSED
- 1
- 7
updated Apr 02, 2020
"Flattened" introduction patterns for intuitionistic conjunction elimination.

#241 · opened May 27, 2019 by Dan Frumin A-coq C-project T-proofmode
- 2
updated Nov 01, 2019
Planning the Iris 3.2 release 0 of 1 task completed

#242 · opened Jun 06, 2019 by Ralf Jung Iris 3.2 A-meta C-enhancement
- CLOSED
- 1
- 1
- 3
updated Nov 01, 2019
Avoid type-level aliases for overloading of canonical structures

#243 · opened Jun 11, 2019 by Robbert Krebbers A-coq C-enhancement T-algebra
- 0
updated Nov 01, 2019
Add a general lattice RA to Iris

#244 · opened Jun 12, 2019 by Ralf Jung A-theory C-project T-algebra
- 1
- 9
updated Dec 10, 2020
Add IntoAnd instance (and more) for array

#245 · opened Jun 14, 2019 by Rodolphe Lepigre Iris 3.2
- CLOSED
- 1
updated Aug 13, 2019
iEval (eauto) "corrupts" goal

#246 · opened Jun 14, 2019 by Paolo G. Giarrusso
- CLOSED
- 1
updated Jun 15, 2019
iInv does not behave as intended when the goal is an accessor

#247 · opened Jun 18, 2019 by Ralf Jung
- CLOSED
- 1
updated Nov 01, 2019
Comparison with `=` and with CAS is not the same

#248 · opened Jun 18, 2019 by Ralf Jung T-heap_lang
- CLOSED
- 1
- 25
updated Jul 01, 2019
Better solvers for properness/contractiveness

#249 · opened Jun 21, 2019 by Paolo G. Giarrusso
- CLOSED
- 4
updated Feb 13, 2020
equivI lemma for sigT

#250 · opened Jun 24, 2019 by Paolo G. Giarrusso
- CLOSED
- 1
- 4
updated Jun 25, 2019
Simplification machinery for RA operations

#251 · opened Jun 24, 2019 by Ralf Jung A-coq C-project T-algebra
- 1
- 1
updated Apr 06, 2020
"Exponentiation" for separating conjunctions

#252 · opened Jul 09, 2019 by Dmitry Khalanskiy A-coq C-enhancement Good First Issue T-bi
- 3
updated Nov 01, 2019