Generated Code for Process Compositions

This repository contains code generated by Isabelle from the Process Composition theory's GitHub repository. It contains that repository as a submodule to track with relation to which version the code is generated.

At present, only Haskell code is generated. It is inserted into a Stack project that produces a library called process-composition. All generated modules are contained in ProcessComposition.Isabelle (the second component highlights the formally verified origin).

Generating Code

The generated code is tracked by this repository, so to use it one only needs to clone it. It needs to be regenerated only when the base theory being used changes, or when the code export configuration in theory/CodeExport.thy changes.

The export itself is automated by make and described in the Makefile. For this to work, we assume that the isabelle executable is available on the PATH. When the default target all is run, it clears the destination directory and exports the code from Isabelle.

We assume that none of the theories in this repository are already loaded as components of Isabelle. If you have a different instance of the Process Composition theory added (e.g. from the AFP), you will need to remove it. For certain simple cases, the script temp_components.sh will temporarily remove relevant components from your Isabelle configuration. (It looks for components whose path ends with ProcessComposition, matching in particular the name of the relevant repository.)

Using the Code

The intention is for the code to be used in other Stack projects by adding it to extra-deps with the following entry:

- github: pilif0/codegen-ProcessComposition
  commit: COMMIT
  subdirs:
  - haskell/isabelle

A local version can be loaded by using a relative path. This approach is discouraged in commits of the dependent project, as it loses reproducibility. However, it can be useful for testing changes to this repository.

Finally, this repository can also be included as a submodule of another. Then it can be included in extra-deps simply by listing the path to that submodule.

See also Stack documentation on specifying package location as a git repository.

(Once a stable form of this library is used wider, publishing to Hackage could be considered.)