Rocq-verified Operational transformation for tree-like data structures

This fork of JetBrains/ot-coq is created to use it with Rocq 9.0.0. This is an independently maintained fork. The original authors are not responsible for this Rocq port. For this purpose, the following changes have been made:

• To use Hierarchy Builder to implement eqType

• To use Mczify instead of Omega

• To specify load paths with the From syntax

except for other minor changes on the proofs to avoid warnings. All of the admit and Admitted parts in RichText.v still remain as they have been. For this reason, this development is not currently submitted to the public Rocq opam archive.

Installation with opam

The development can be installed directly from a local checkout as a pinned opam package:

opam repo add rocq-released https://rocq-prover.org/opam/released
opam pin add rocq-ot .

Alternatively, pin the Git repository without making a local checkout first:

opam repo add rocq-released https://rocq-prover.org/opam/released
opam pin add rocq-ot git+https://github.com/ksk/ot-rocq.git

The installed library is available under the OTRocq logical path, for example:

From OTRocq Require Import Tree TreeOt OtDef.

Building from source

The development requires Rocq 9.0, Hierarchy Builder 1.10, Mathematical Components 2.4, and mczify 1.7. The required opam packages are declared in rocq-ot.opam.

Run the following commands to compile it without installing it:

rocq makefile -f _CoqProject -o CoqMakefile
make -f CoqMakefile

To install the compiled library into the active opam switch, run:

make -f CoqMakefile install

The original code (tag original-ot-coq) is preserved for reference. The branch master contains modifications to make it work on modern environments. The original README.md follows below.

---

Coq-verified Operational transformation for tree-like data structures

This repository contains Coq source code accompanying the paper "Verified Operational Transformation for Trees" by S. Sinchuk, P. Chuprikov and K. Solomatov published in proceedings of 7th International Conference, ITP 2016 (pp. 358--373). Link to the paper

Building

The original source code is compatible with Coq 8.4 and makes use of Ssreflect. The repository also contains version of the code compatible with Coq 8.8 and 8.13. Use make -f Makefile^†1 to build the project.

---

^†1 The Makefile has been removed from this repository to avoid confusion.