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 123
    • Issues 123
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 15
    • Merge Requests 15
  • 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 123
  • Closed 269
  • All 392
New issue
  • Priority Created date Last updated Milestone due date Due date Popularity Label priority Manual
  • Use dfrac everywhere   0 of 7 tasks completed
    #412 · created Apr 19, 2021 by Ralf Jung   A-coq C-enhancement T-algebra T-base_logic
    • 0
    updated Apr 19, 2021
  • Taking ∃ out of ▷ without Inhabited, more easily
    #411 · created Mar 28, 2021 by Yusuke Matsushita   A-coq C-enhancement T-proofmode
    • 3
    updated Mar 29, 2021
  • Modality for `Timeless`
    #410 · created Mar 22, 2021 by Ralf Jung   A-theory C-project T-bi
    • 1
    • 2
    updated Apr 19, 2021
  • Proposed change to naming convention for "dataful" `*G`s
    #409 · created Mar 18, 2021 by Ralf Jung   A-coq C-enhancement T-style
    • 3
    updated Apr 19, 2021
  • bi.weakestpre imports a module from program_logic
    #408 · created Mar 17, 2021 by Ralf Jung   A-coq C-bug T-bi T-program_logic
    • 2
    • 7
    updated Mar 18, 2021
  • Tracking issue for list RA
    #407 · created Mar 17, 2021 by Ralf Jung   C-tracking-issue T-algebra
    • 0
    updated Mar 17, 2021
  • 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
  • Tracking issue for HeapLang interpreter
    #405 · created Feb 16, 2021 by Ralf Jung   C-tracking-issue T-heap_lang
    • 0
    updated Feb 16, 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
  • Integrate Tej's simp-lang?
    #400 · created Jan 28, 2021 by Ralf Jung   A-docs T-program_logic
    • 5
    updated Feb 17, 2021
  • Upstream more big_op lemmas from Perennial
    #399 · created Jan 27, 2021 by Ralf Jung   A-coq C-enhancement T-bi
    • 1
    updated Feb 17, 2021
  • Use `dom` instead of `∀ k, is_Some (.. !! k) ...`
    #398 · created Jan 26, 2021 by Robbert Krebbers   A-coq C-enhancement T-algebra T-bi
    • 0
    updated Feb 17, 2021
  • `iRename` fails with bad error message when not in proof mode
    #397 · created Jan 12, 2021 by Robbert Krebbers   A-coq C-bug Good First Issue T-proofmode
    • 1
    updated Feb 17, 2021
  • Intro pattern `>` has wrong behavior with side-conditions of `iMod`
    #396 · created Jan 12, 2021 by Robbert Krebbers   A-coq C-bug T-proofmode
    • 3
    updated Feb 17, 2021
  • Document relation between Discrete and Timeless (in appendix?)
    #394 · created Dec 23, 2020 by Paolo G. Giarrusso   A-docs T-algebra T-base_logic
    • 0
    updated Jan 06, 2021
  • Masks in step-taking fupd notation
    #392 · created Dec 10, 2020 by Ralf Jung   A-theory C-enhancement T-base_logic
    • 1
    • 0
    updated Dec 10, 2020
  • Add append-only list RA to Iris
    #391 · created Dec 08, 2020 by Ralf Jung   A-coq C-enhancement T-algebra T-base_logic
    • 1
    • 1
    updated Apr 05, 2021
  • Citation guide
    #389 · created Dec 06, 2020 by Tej Chajed   A-docs
    • 1
    updated Dec 08, 2020
  • reshape_expr does not recognize `fill`
    #385 · created Nov 27, 2020 by Ralf Jung   A-coq C-enhancement T-heap_lang
    • 0
    updated Dec 05, 2020
  • Make sure we have Hint Mode for every typeclass   0 of 1 task completed
    #381 · created Nov 12, 2020 by Ralf Jung   A-coq C-bug T-style
    • 0
    updated Nov 12, 2020
  • Prev
  • 1
  • 2
  • 3
  • 4
  • 5
  • …
  • 7
  • Next