Commits · ci/for_proph · Iris / Iris

18 Jun, 2019 1 commit
- add 'atomic triple' for compare-and-set, and use it in one example · 10809c68
  Ralf Jung authored Jun 18, 2019
  
  10809c68
17 Jun, 2019 2 commits
- add lemmas for combining CAS and Resolve · 011eb020
  Ralf Jung authored Jun 17, 2019
  
  011eb020
- turn CAS into compare-and-swap instead of compare-and-set: make it return the old value · b97c5886
  Ralf Jung authored Jun 17, 2019
  
  b97c5886
14 Jun, 2019 8 commits
- comparison: treat prophecies like unit · b3217e8f
  Ralf Jung authored Jun 14, 2019
  
  b3217e8f
- make variable names a bit more consistent between Coq and LaTeX · ce20ffb1
  Ralf Jung authored Jun 14, 2019
  
  ce20ffb1
- temporary link to prophecy MR, until we can reference a paper instead · 8f443ec0
  Ralf Jung authored Jun 14, 2019
  
  8f443ec0
- note that observations are observable events · e262cd8e
  Ralf Jung authored Jun 14, 2019
  
  e262cd8e
- docs: fix typo · 4f526c98
  Ralf Jung authored Jun 14, 2019
  
  4f526c98
- Merge branch 'typo' into 'master' · 6a0ad444
  Ralf Jung authored Jun 14, 2019
```
Adequacy: Fix typo

See merge request iris/iris!268
```
  6a0ad444
- Adequacy: Fix typo · b8b80ba7
  Paolo G. Giarrusso authored Jun 14, 2019
  
  b8b80ba7
- say what C does · 4032acd1
  Ralf Jung authored Jun 14, 2019
  
  4032acd1
13 Jun, 2019 9 commits
- make sure we actually use babel and microtype · 98fc837e
  Ralf Jung authored Jun 13, 2019
  
  98fc837e
- centralize all heap_lang notation in one file · 05bccfb8
  Ralf Jung authored Jun 13, 2019
  
  05bccfb8
- Merge branch 'lazy_coin' into 'master' · a555a33c
  Ralf Jung authored Jun 13, 2019
```
Add the lazy_coin example

See merge request iris/iris!264
```
  a555a33c
- Add the lazy_coin example · 1b6cfe1a
  Amin Timany authored Jun 13, 2019
  
  1b6cfe1a
- re-do adequacy section · 5bdb226b
  Ralf Jung authored Jun 13, 2019
  
  5bdb226b
- docs: remove some commented-out outdated rules · 9b2f534f
  Ralf Jung authored Jun 13, 2019
  
  9b2f534f
- Merge branch 'ralf/adequacy' into 'master' · 860bd8e4
  Ralf Jung authored Jun 13, 2019
```
tweak adequacy: treat stuckness like the other WP indices

See merge request iris/iris!265
```
  860bd8e4
- avoid some evars · 70fef82c
  Ralf Jung authored Jun 13, 2019
  
  70fef82c
- tweak adequacy: treat stuckness like the other WP indices · 3584bf89
  Ralf Jung authored Jun 13, 2019
  
  3584bf89
12 Jun, 2019 14 commits
- `IntoSep` instance for `tc_opaque`. · ae1dd418
  Robbert Krebbers authored Jun 12, 2019
  
  ae1dd418
- Coqdoc tweaks. · 52baecf8
  Robbert Krebbers authored Jun 12, 2019
  
  52baecf8
- Add lemma `meta_token_difference`. · 1a0c5860
  Robbert Krebbers authored Jun 12, 2019
  
  1a0c5860
- Merge branch 'robbert/adequacy' into 'master' · 78d3d724
  Robbert authored Jun 12, 2019
```
A strong adequacy statement to rule them all

See merge request iris/iris!258
```
  78d3d724
- move comments out-of-line to please the extremely picky macOS shell · 243d8707
  Ralf Jung authored Jun 12, 2019
  
  243d8707
- try to fix test suite for macOS · 95ae2473
  Ralf Jung authored Jun 12, 2019
  
  95ae2473
- note on macOS sed usage · 5e962360
  Ralf Jung authored Jun 12, 2019
  
  5e962360
- state adequacy helper lemma more positively · d857cb91
  Ralf Jung authored Jun 08, 2019
  
  d857cb91
- update docs for new adequacy statement · cd49700f
  Ralf Jung authored Jun 08, 2019
  
  cd49700f
- Remove useless import. · fec84da6
  Robbert Krebbers authored Jun 07, 2019
  
  fec84da6
- Tweak the proof of `wp_adequacy`. · 9200cc77
  Robbert Krebbers authored Jun 07, 2019
  
  9200cc77
- CHANGELOG entry. · 1354f02c
  Robbert Krebbers authored Jun 07, 2019
  
  1354f02c
- Comment about traces. · b3e74c0d
  Robbert Krebbers authored Jun 07, 2019
  
  b3e74c0d
- A strong adequacy statement to rule them all. · a5ad91e5
  Robbert Krebbers authored Jun 07, 2019
```
The new adequacy statement unifies `wp_strong_adequacy`, `wp_strong_all_adequacy`,
and `wp_invariance`.
```
  a5ad91e5
11 Jun, 2019 6 commits
- add sed script for frac_auth changes · 53ed9d87
  Ralf Jung authored Jun 11, 2019
  
  53ed9d87
- with reftest normalization, whitelisting Coq 8.11 should not be needed any more · a51fa3cf
  Ralf Jung authored Jun 11, 2019
  
  a51fa3cf
- Merge branch 'ralf/frac_auth' into 'master' · 2418fccd
  Ralf Jung authored Jun 11, 2019
```
change frac_auth notation

See merge request !259
```
  2418fccd
- change frac_auth notation · 94cfebc2
  Ralf Jung authored Jun 07, 2019
  
  94cfebc2
- Fix compilation with Coq master. · 265c2a13
  Robbert Krebbers authored Jun 11, 2019
  
  265c2a13
- Merge branch 'robbert/ufrac' into 'master' · e65b06a7
  Jacques-Henri Jourdan authored Jun 11, 2019
```
The unbounded fractional authoritative camera

See merge request !187
```
  e65b06a7