Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
I
iris-coq
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Monitor
Incidents
Service Desk
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Marianna Rapoport
iris-coq
Repository graph
Repository graph
You can move around the graph by using the arrow keys.
fast_string
Select Git revision
Branches
20
atomic
ci/janno/vmcast
ci/ralf/atomic
ci/ralf/lia
ci/ralf/pm_red
ci/ralf/telescopes
fast_string
gen_proofmode
iris-3.0
iris-3.1
janno/metacoq
jh/done_contradiction
jh/evar_iframe
jh/independent_metric
jh/sprop_upred
jh_inductive_pairs
joe/defined_pers
less_canonical
less_canonical_new
marianna/prophecy
Tags
10
iris-3.1.0
iris-3.0.0
iris-2.0
iris-2.0-rc2
iris-2.0-rc1
iris-1.1
iris-1.0
hope-2015-coq-1
appendix-1.0.0
appendix-1
30 results
Begin with the selected commit
Created with Raphaël 2.2.0
24
Oct
23
20
19
18
12
10
9
7
5
4
29
Sep
28
27
26
25
24
21
20
19
18
17
16
15
14
11
9
8
6
28
Aug
26
24
23
22
21
20
18
17
7
6
4
28
Jul
14
12
10
27
Jun
13
12
8
6
25
May
17
12
9
27
Apr
26
19
13
12
11
7
5
4
31
Mar
30
28
24
23
22
21
20
16
15
14
12
11
10
9
7
6
5
1
24
Feb
23
22
21
20
18
17
16
15
14
13
12
11
10
9
8
7
6
3
2
1
30
Jan
29
28
27
26
25
24
23
22
21
20
17
13
12
11
10
9
8
7
6
5
4
3
1
28
Dec
27
26
23
22
21
20
19
18
17
16
15
14
13
12
11
9
8
7
6
Start work on a benchmark data exporter
Port the core to use the plain modality and prove it is non-expansive.
Proofmode support for introducing the plain modality.
Plainness and persistence of implications and wands.
Simplify soundness of the base logic.
Proof mode instances for eliminating plain basic updates.
Proof mode instances for the plain modality.
Avoid exponential proof search due to Plain → Persistent instance.
Derived rules of the plain modality.
Add the plain modality to the model of the base logic.
extractor: support grabbing logs from local all-artifacts zip folder
fix gitlab-extract
update README
and another test that depends on the barrier
remove a test that depends on the barrier
move barrier to new iris-examples repo; test that repo after each Iris commit
CI: rename REV parameter to IRIS_REV for iris.dev builds
CI: sync
CI: rename jobs for consistency
reverse-deps trigger: set Iris revision
trigger an iris-atomic build in the deploy stage
fix typo in .gitlab-ci.yml
rename 2nd stage
update CI system
opam: don't use the shell for no good reason
Bump coq-stdpp.
Coq CI does not need opam.pins any more
Merge branch 'ilocked' into 'master'
Proof mode instances for [tc_opaque].
Merge branch 'ci/primproj' into 'master'
use sections to scope options
Merge branch 'quickfix' into 'master'
Remove an unused argument
use primitive projections for our mixins
sync opam.pins
all opam caches are clear of the old pins by now
have Coq's dev repos only for dev builds
update opam.pins
more consistent grammar
make build-dep: prefer relative paths; they seem to work better on Windows
Loading