Skip to content
Lem semantic definition language
OCaml Isabelle Standard ML Makefile Coq TeX Other
Branch: master
Clone or download
Type Name Latest commit message Commit time
Failed to load latest commit information.
coq-lib Fix some definitions to make coq-libs compile again Jun 5, 2019
doc typo Oct 22, 2014
etc Update copyright header with some new names based on github contribut… Apr 20, 2018
examples ppcmem-model example: ensured the generated directory exists. Dec 19, 2013
hol-lib Adapt to change in recent HOL4 versions Jul 26, 2019
html-lib git add directory for html-lib build Mar 12, 2017
isabelle-lib Declare failwith as unimplemented function for Isabelle's code generator Aug 14, 2019
language Reverse concatenation of whitespace May 9, 2018
library Add Isabelle constant Aug 14, 2019
manual META.lem: allow compilation of lem programs with ocamlfind Oct 8, 2013
ocaml-lib Add integerSqrt for testing purposes Dec 13, 2018
src Merge pull request #25 from rems-project/isabelle2019 Aug 14, 2019
tests git add directory for html-lib build Mar 12, 2017
tex-lib Apply new header. Apr 20, 2018
.gitignore Ignore generated files in hol-lib May 17, 2018 Add a pointer to opam repository in Jul 16, 2019
LICENSE import lem development source from svn repo Revision 8676 Mar 6, 2013
Makefile Make "make install" install Coq and HOL libraries Jan 22, 2019
Makefile-distrib import lem development source from svn repo Revision 8676 Mar 6, 2013 test commit Mar 12, 2017
descr First opam release on 2018-04-19. Apr 19, 2018 added Feb 20, 2017
opam Update opam version for release. May 17, 2019
readme-sources.txt make libraries work for ocaml Nov 8, 2013


Lem is a tool for lightweight executable mathematics, for writing, managing, and publishing large-scale portable 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.

Lem is under active development and has been used in several applications, some of which can be found in the examples directory. It is made available under the BSD 3-clause license, with the exception of a few files derived from OCaml, which are under the GNU Library GPL.

Lem depends on OCaml. Lem is tested against OCaml 3.12.1. and 4.02.0. Other versions might or might not work. Lem requires the OCaml ZArith library for arbitrary precision arithmetic. Lem has been tested against ZArith version 1.2. 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 in that directory. Instructions on building the libraries for particular targets are in the manual.

Documentation can be found in doc/built-doc, including:

  • a high-level description of Lem in the draft paper lem-draft.pdf;
  • the manual, in lem-manual.html and lem-manual.pdf;
  • the Ott grammar and type system for Lem, in lem.pdf, built from the definition in language/;
  • the Lem library documentation, in lem-libs.pdf;
  • the type signatures of the pervasives and pervasives-extra libaries, in lem-libs-pervasives.txt and lem-libs-pervasives-extra.txt; and
  • source documentation, in html-doc and lem-doc.pdf, with a dependency diagram of the source modules in dep.pdf.

Supported versions of software

Lem is tested against the following versions of the backend software:

  • OCaml: 3.12.1, 4.00.0, 4.01.0, and 4.02.0
  • Coq: 8.4pl3 and 8.4pl2
  • Isabelle: Isabelle-2013-2
  • HOL: HOL4 Kananaskis 9
You can’t perform that action at this time.