Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 122
    • Issues 122
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 18
    • Merge Requests 18
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • Iris
  • Issues

  • Open 122
  • Closed 263
  • All 385
New issue
  • Priority Created date Last updated Milestone due date Due date Popularity Label priority Manual
  • 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
  • Prev
  • 1
  • 2
  • 3
  • 4
  • Next