Bitbucket is a code hosting site with unlimited public and private repositories. We're also free for small teams!

Close

Lem

Lem is a tool for lightweight executable mathematics, for writing, managing, and publishing large-scale semantic definitions, with export to LaTeX, executable code (currently OCaml) and interactive theorem provers (currently Coq, HOL4, and Isabelle/HOL).

It is also intended as an intermediate language for generating definitions from domain-specific tools, and for porting definitions between interactive theorem proving systems

This is the development version of Lem, which is not yet feature complete. It is made available under the BSD 3-clause license, with the exception of a few files derived from the OCaml, which are under the GNU Library GPL.

Lem depends on OCaml. Lem is tested against OCaml 3.12.1. Other versions might or might not work.

To build Lem run make in the top-level directory. This builds the executable lem, and places a symbolic link to it that directory. Now set the LEMLIB environment variable to PATH_TO_LEM/library, or alternately pass the -lib PATH_TO_LEM/library flag to lem when you run it. This tells Lem where to find its library of types for HOL/Isabelle/OCaml/Coq built-in functions.

The source language grammar and type system are defined in language/lem.ott, available in a typeset form in language/lem.pdf. There is also a very preliminary manual (not currently up to date) at http://www.cl.cam.ac.uk/~so294/lem/.

Recent activity

Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.