Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
Iris
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
116
Issues
116
List
Boards
Labels
Service Desk
Milestones
Merge Requests
21
Merge Requests
21
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Iris
Iris
Issues
Open
116
Closed
261
All
377
New issue
Recent searches
{{formattedKey}}
{{ title }}
{{ help }}
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
Upcoming
Started
{{title}}
None
Any
{{title}}
None
Any
{{title}}
None
Any
{{name}}
Yes
No
Yes
No
{{title}}
{{title}}
Due date
Priority
Created date
Last updated
Milestone due date
Due date
Popularity
Label priority
Manual
Add a logic-level version of gmap_view
#358
· opened
Oct 12, 2020
by
Ralf Jung
A-coq
C-enhancement
T-base_logic
1
5
updated
Dec 23, 2020
Cancelable locks
#357
· opened
Oct 12, 2020
by
Robbert
A-theory
C-enhancement
T-heap_lang
13
updated
Oct 21, 2020
Discardable camera improvements
#354
· opened
Oct 06, 2020
by
Ralf Jung
A-theory
C-enhancement
T-algebra
9
updated
Oct 09, 2020
Tracking issue for records
#352
· opened
Sep 29, 2020
by
Ralf Jung
Iris 3.4
A-coq
C-project
T-records
4
updated
Dec 05, 2020
Decouple framing and IntoSep
#351
· opened
Sep 29, 2020
by
Ralf Jung
A-coq
C-enhancement
I-performance
T-proofmode
1
updated
Sep 29, 2020
Parameterize WP (and more) by the notion of fancy update
#349
· opened
Sep 21, 2020
by
Ralf Jung
A-coq
C-enhancement
T-base_logic
4
updated
Sep 22, 2020
Always enabled invariants
#348
· opened
Sep 21, 2020
by
Ralf Jung
A-theory
C-enhancement
T-base_logic
3
updated
Sep 30, 2020
"solve_inG" is very slow for larger RA combinators
#347
· opened
Sep 21, 2020
by
Ralf Jung
A-coq
C-bug
T-algebra
18
updated
Oct 16, 2020
Make CI fail when proofs depend on auto-generated names
#343
· opened
Sep 08, 2020
by
Ralf Jung
A-coq
A-infra
C-enhancement
T-style
1
updated
Oct 07, 2020
Coecisting fractional and persistent read-only ownership
#341
· opened
Aug 16, 2020
by
Ralf Jung
A-coq
A-theory
C-enhancement
T-algebra
7
updated
Aug 25, 2020
Polymorphic equality for HeapLang
#340
· opened
Aug 08, 2020
by
Dan Frumin
A-theory
C-enhancement
T-heap_lang
16
updated
Aug 22, 2020
Add "reservation map" CMRA
#339
· opened
Aug 07, 2020
by
Ralf Jung
A-coq
C-enhancement
T-algebra
1
updated
Sep 09, 2020
Missing unseal tactic for siProp
#338
· opened
Jul 30, 2020
by
Paolo G. Giarrusso
A-coq
T-siprop
7
updated
Aug 30, 2020
iris.sty incompatible with acmart
#335
· opened
Jul 14, 2020
by
Ralf Jung
A-docs
C-bug
6
updated
Jul 15, 2020
Expand test coverage of proofmode
0 of 3 tasks completed
#334
· opened
Jul 13, 2020
by
Tej Chajed
A-coq
C-enhancement
T-proofmode
1
updated
Jul 14, 2020
Become part of Coq Platform?
#332
· opened
Jul 05, 2020
by
Ralf Jung
A-coq
A-meta
3
5
updated
Jul 21, 2020
simpl breaks error checking of `iNext (S i)`
#331
· opened
Jun 29, 2020
by
Paolo G. Giarrusso
A-coq
C-bug
T-proofmode
1
3
updated
Jul 14, 2020
Consider adding `iEnough` variants of `iAssert` ?
#330
· opened
Jun 25, 2020
by
Paolo G. Giarrusso
A-coq
C-enhancement
T-proofmode
3
updated
Jun 26, 2020
Iris Website Reform
#329
· opened
Jun 25, 2020
by
Ralf Jung
A-infra
A-meta
C-project
3
1
updated
Sep 29, 2020
Make `contractive_proper` into a lemma, or control other instances that make it costly.
#321
· opened
May 27, 2020
by
Paolo G. Giarrusso
A-coq
C-enhancement
I-performance
T-algebra
1
1
updated
Oct 20, 2020
Prev
1
2
3
4
5
6
Next