1. 10 Jan, 2017 3 commits
  2. 03 Jan, 2017 3 commits
  3. 22 Dec, 2016 3 commits
  4. 14 Dec, 2016 1 commit
  5. 13 Dec, 2016 3 commits
  6. 12 Dec, 2016 5 commits
  7. 16 Nov, 2016 1 commit
  8. 14 Nov, 2016 2 commits
  9. 13 Nov, 2016 2 commits
  10. 08 Nov, 2016 1 commit
    • Ralf Jung's avatar
      Merge branch 'ci' into 'master' · 7c6793f3
      Ralf Jung authored
      Iris as submodule; CI support
      
      This adds Iris as a submodule, matching the structure in https://gitlab.mpi-sws.org/FP/LambdaRust-coq/. Furthermore, it sets up the CI so after pushing, the repo is built against the given Iris version (with a cache to avoid needless rebuilding of Iris).
      
      @zhangz if you have any unpushed changes, please push them. This branch moves all files to a subfolder `theories/`, so it will conflict with any other change.
      
      See merge request !2
      7c6793f3
  11. 07 Nov, 2016 4 commits
    • Ralf Jung's avatar
      remove now unnecessary IRIS_VERSION · 541920fb
      Ralf Jung authored
      541920fb
    • Ralf Jung's avatar
      add CI file · 32554672
      Ralf Jung authored
      32554672
    • Ralf Jung's avatar
      889f7c78
    • Ralf Jung's avatar
      Merge branch 'uncurried-specs' into 'master' · 8d5768cb
      Ralf Jung authored
      Simpler syncer specs
      
      This simplifies the syncer specs.
      The sequential syncer only is slightly improved, by changing
      ```
        Definition synced R (f' f: val) :=
          (□ ∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) →
                             ({{ P x }} f' x {{ v, Q x v }}))%I.
      ```
      such that `P`, `Q` don't factor in a dependency on `x` any more. Since all three are quantified at the same time, the two specs are equivalent -- and the one where `P` is not a predicate and `Q` is exactly the postcondition is arguably simpler:
      ```
        Definition synced R (f f': val) :=
          (□ ∀ P Q (x: val), ({{ R ★ P }} f x {{ v, R ★ Q v }}) →
                             ({{ P }} f' x {{ Q }}))%I.
      ```
      
      For the atomic spec, the changes are deeper. The currying on some location `l` is entirely removed. `is_atomic_syncer` better mirrors `is_syncer` from the sequential version. And finally, we use "original" atomic triples and not some modified version thereof (so `atomic_triple_base` is killed).
      
      TODO: Fix `atomic_pcas.v`, it relied on the location currying done by `atomic_sync.v`. However, I don't entirely grok that file. @zhangz could you give that a look?
      
      See merge request !1
      8d5768cb
  12. 02 Nov, 2016 4 commits
  13. 01 Nov, 2016 3 commits
  14. 25 Oct, 2016 1 commit
  15. 24 Oct, 2016 4 commits