Lightweight Java Module System (LJAM)
=====================================

Making definitions from Ott source files
----------------------------------------

a) Get Ott source, make its native executable, and put it in your PATH. The
   source can be downloaded here:

      http://www.cl.cam.ac.uk/~pes20/ott/

   (The source Ott source files here were tested against version 0.20.1.)

b) Go into directory where Ott source files are located, and run "make". If you
   do not have the "make" command, run the following commands (assuming ott and
   pdflatex are in your PATH):


      ott -tex_wrap false -isabelle_inductive false \
          -o ljam_included.tex -o ljam.thy -merge true \
          lj_common.ott ljam_common.ott ljp_base.ott \
          ljm_base.ott ljam.ott
      pdflatex ljam.tex

c) Generated files:
   - ljam_included.tex
      LaTeX output of Ott. It is included in ljam.tex, which is then compiled
      with pdflatex. (We do not generate a wrapped LaTex document directly,
      since some of our tex homs are context dependent.)
   - ljam.pdf
      PDF version of the LJAM's definition.
   - ljam.thy
      A valid Isabelle 2008 source containing Isabelle definition of LJAM.



More Information
----------------

More information and related documents can be found at:

  http://www.cl.cam.ac.uk/research/pls/javasem/ljam/