Skip to content

Latest commit

 

History

History
192 lines (137 loc) · 4.98 KB

DEV.md

File metadata and controls

192 lines (137 loc) · 4.98 KB
Raw

Notes for developers

Build

This project is built using the dune build system. There is also a build using make, mainly for legacy reasons, and also to generate documentation.

Install dependencies with opam.

opam install coq-paco coq-ext-lib dune

Then dune build will compile everything: library, tutorial (toy compiler from Imp to Asm), and tests.

dune build

To be able to edit Coq files interactively, copy the _CoqProject file:

cp _CoqProject.dune _CoqProject

(_CoqProject is not included by default because it can also be generated by the make build. Clean the project when switching between make and dune builds.)

Other build targets (note all of them will build theories as a dependency):

dune build theories
dune build tutorial
dune build tests
dune build examples

Run tests (a bunch of extracted examples):

dune runtest

Build with make

This uses the same dependencies, minus dune.

opam install coq-paco coq-ext-lib

Build everything with make all.

make all -j  # Build the library, tutorial (example compiler), and tests.

Other targets:

make  # Build the library
make tutorial
make tests

The above commands run any extracted test executables too.

Build the Documentation

1. Basic Documention

Build the coqdoc generated html files by doing:

make html

Then visit html/toc.html in your web browser.

2. Prettier Documentation

coqdocjs adds some modern-looking CSS and JS to coqdoc's output.

  1. Download and unzip coqdocjs-master.zip.

  2. Create a link to the unzipped directory (or move the directory into this repo):

    ln -s path/to/coqdocjs-master coqdocjs

  3. Run

    make html

3. Updating Github pages

The documentation is stored in the gh-pages branch. The recommended setup is to create a fresh clone in the doc directory.

git clone -b gh-pages [email protected]:DeepSpec/InteractionTrees doc

There is a script in that branch to update the documentation.

cd doc
sh ./update.sh
git add -u
git commit -m "Update"

It will run "make html" in the parent directory and move the output where it should go, in doc/docs/master. Past releases are maintained in doc/docs/$VERSION.

Library internal organization

We keep most theorems separated into *Facts modules, to allow parallel compilation and to contain potential universe inconsistencies, so the computational definitions may still be usable for testing.

  • Basics: General-purpose definitions not tied to interaction trees.

    • Basics: The ~> notation and names of common monad transformers.

    • Category: A simple theory of categories, monoidal and iterative.

      • CategoryOps: Interfaces of operations to define categories.
      • CategoryTheory: Properties of categories.
      • CategoryFacts: General facts about categories.
      • CategoryFunctor: Classes of functors.
      • CategorySub: Definition of sub-categories.
      • CategoryKleisli: Kleisli categories (for monads in the category of functions).
      • CategoryKleisliFacts

    • Function: The category of Coq functions A -> B.

    • FunctionFacts

    • Monad: Properties of monads (in the category of functions).

    • MonadState: The state monad transformer.

    • MonadProp: The nondeterminism monad.

  • Core: Main definitions for interaction trees.

    • ITreeDefinition: Interaction trees, type declaration and primitives.
    • KTree: Continuation trees A -> itree E B, the first Kleisli category of itree.
    • KTreeFacts
    • Subevent: Combinators for extensible effects, injecting events into sums.
    • ITreeMonad: Instantiation of the Basics.Monad interface with itree.

  • Eq: Equational theory of interaction trees.

    • Shallow: One-step unfolding of cofixpoints.
    • Eq: Strong bisimulation.
    • UpToTaus: Weak bisimulation.
    • SimUpToTaus: Weak simulation.
    • EqAxiom: Axiom that strong bisimulation is propositional equality. The library exports that axiom but does not itself make use of it.

  • Indexed: Indexed types Type -> Type.

    • Sum: Sum of indexed types.
    • Function: The category of parametric functions between indexed types, i.e., event morphisms E ~> F.
    • FunctionFacts
    • Relation: Relations on indexed types, i.e., forall T, E T -> E T -> Prop.

  • Interp: Interaction tree transformations.

    • Interp: Interpret itrees (translate, interp).
    • TranslateFacts, InterpFacts
    • Handlers: Event handlers E ~> itree F, the second Kleisli category of itree.
    • HandlerFacts
    • Recursion: Recursion combinators (mrec, rec).
    • RecursionFacts
    • Traces: Interpretation of itrees as sets of traces.

  • Events: Common event types (see theories/Events.v for a summary).