Tutorial

Installation

Install OCaml 4.11.0 (later version might also work) and CamlP5 7.13 (the only working version), and OMake. I installed these all from source tarball without opam, so maybe a little tweak is needed if you're using opam. The CamlP5 requires a tweak, before compile CamlP5 change the

Plexer.dollar_for_antiquotation.val := False;

line to

Plexer.dollar_for_antiquotation.val := True;

in etc/pa_o.ml. And ./configure it to use strict mode, which means camlp5 -pmode should give strict. Read CamlP5's manual for details.

clone owo-lang/metaprl and owo-lang/libmojave, cd metaprl and check out branch camlp5-7.13. Symlink the libmojave repo to metaprl/libmojave. omake it and it should build, while it is building it would complain missing some .cmx or .cmo files, just copy the missing files from CamlP5 building directory to the installed /usr/local/lib/ocaml/camlp5.

Running

now, execute metaprl/editor/ml/mp -cli, if you prefer xterm there's mpxterm starts MetaPRL in a xterm, without -cli it defaults to start a server which you can view and check proofs in a browser, it still works but sometimes SIGSEGV.

View the file QUICKSTART to learn some commands. save() saves proofs to .prlb format, which is ignored by version control, export() save proofs to .prla format which is a plain text file suitable for version control.

MetaPRL Tutorial

The following content is adapted from https://www.cs.cornell.edu/jyh/metaprl/tutorial/. Updated to reflect current version of MetaPRL.

Still WIP

In this tutorial we develop an account of classical first-order logic, and we relate it to the Nuprl type theory Itt_theory. The theory we develop is fully modular. It contains modules for each of the logical operators, and the constructive logic is a subtheory of the classical logic. We also investigate proof automation. Each module defines proof procedures for its operator, and the final logic defines an automated proof procedure for the logic.

The first step in creating a logic is creating a module for each of the logical operators. Initially, the framework has no notion of truth or falsehood in the logic; these concepts are defined by declaring syntax and logical rules. Our logic will include the logical operators in first-order logic (FOL), and it will include terms to represent true and false. We will use a single-conclusion sequent calculus (a multi-conclusion sequent calculus is also possible, but this choice will make it easier to relate the logic to the type theory).

These are the parts to the tutorial:

• Getting started
• A Constructive Logic
  • Well-formedness of terms