Merge branch 'askrcv' of github.com:vellvm/ctrees into askrcv

Author: YaZko

.envrc

@@ -0,0 +1,2 @@
+use flake
+unset COQPATH

.github/workflows/nix-build.yml

@@ -0,0 +1,21 @@
+name: "Build ctrees under nix"
+on:
+  pull_request:
+  push:
+jobs:
+  tests:
+    strategy:
+      matrix:
+        os:
+          - ubuntu-latest
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: "write"
+      contents: "read"
+    steps:
+    - uses: actions/checkout@v4
+    - uses: DeterminateSystems/nix-installer-action@v19
+    - uses: DeterminateSystems/magic-nix-cache-action@v13
+    - uses: DeterminateSystems/flake-checker-action@v12
+    - name: Run nix build
+      run: nix build .

README.md

@@ -0,0 +1,59 @@
+# Choice Trees
+[![Docker CI](https://github.com/vellvm/ctrees/workflows/Docker%20CI/badge.svg?branch=dev)](https://github.com/vellvm/ctrees/actions?query=workflow:"Docker%20CI")
+[![Nix](https://github.com/vellvm/ctrees/actions/workflows/nix-build.yml/badge.svg)](https://github.com/vellvm/ctrees/actions/workflows/nix-build.yml)
+
+We develop a cousin of Interaction Trees, dubbed _Choice Trees_, with native support for non-determinism.
+
+## Meta
+
+- Author(s):
+  - Nicolas Chappe
+  - Paul He
+  - Ludovic Henrio
+  - Eleftherios Ioannidis
+  - Yannick Zakowski
+  - Steve Zdancewic
+- License: MIT License
+- Compatible Rocq versions: 9.0
+- Additional dependencies:
+  - dune
+  - [Extlib](https://github.com/coq-community/coq-ext-lib)
+  - [InteractionTrees](https://github.com/DeepSpec/InteractionTrees)
+  - [Equations](https://github.com/mattam82/Coq-Equations)
+  - [Coinduction](https://github.com/damien-pous/coinduction)
+  - [RelationAlgebra](https://github.com/damien-pous/relation-algebra)
+- Rocq namespace: `CTree`
+
+## Related papers
+
+- https://hal.science/hal-05154458
+- https://dl.acm.org/doi/10.1145/3571254 (old)
+
+## Building instructions
+
+### Installing dependencies
+
+Installing the opam dependencies
+```shell
+opam install coq-ext-lib coq-itree coq-relation-algebra coq-coinduction coq-equations
+```
+
+### Obtaining the project
+
+```shell
+git clone https://github.com/vellvm/ctrees
+cd ctrees
+```
+
+### Building the project
+
+```shell
+dune build
+```
+
+## Universe issue
+
+We currently unset locally universe checking in several places of the library. This is an annoying, but purely technical issue that affects in no way the soundness of our results.
+
+Given the complexity of the issue, and its root tracing back to other libraries (for instance, importing simultaneously some parts of the [Interaction Tree] library and of the [RelationAlgebra] library triggers a universe inconsistency), we project to tackle the issue as part of the future support in Rocq for alegbraic universes and the release of a universe polymorphic prelude.
+

Readme.md

@@ -1,6 +1,6 @@
 (lang dune 3.8)
 (using coq 0.7)
-(name coq-ctree)
+(name rocq-ctree)
 
 (license "MIT")
 (authors "Nicolas Chappe" "Paul He" "Ludovic Henrio" "Yannick Zakowski" "Steve Zdancewic")
@@ -11,14 +11,25 @@
 (generate_opam_files true)
 
 (package
- (name coq-ctree)
+ (name rocq-ctree)
  (synopsis "Library for representing recursive, non-deterministic and impure programs with equational reasoning")
- (version 0.1)
+ (version 2.0-dev)
  (depends
-  (coq (= 8.20.1))
+  (rocq-core (>= 9.0))
+  (rocq-stdlib (>= 9.0))
   (coq-ext-lib (>= 0.11.3))
-  (coq-coinduction (= 1.20))
-  (coq-relation-algebra (>= 1.7.11))
-  (coq-equations (>= 1.2))
+  (rocq-coinduction (>= 1.21))
+  (rocq-relation-algebra (>= 1.8.0))
+  (rocq-equations (>= 1.3.1))
   (coq-itree (>= 5.0)))
+ (tags (
+   "category:CS/Semantics and Compilation/Semantics"
+   "category:CS/Concurrency/Theory of concurrent systems"
+   "keyword:simulation"
+   "keyword:bisimilarity"
+   "keyword:coinduction up-to"
+   "keyword:process algebra"
+   "keyword:cooperative multithreading"
+   "logpath:CTree"
+ ))
 )