(image courtesy of @tranngocma)
RedPRL is the People's Refinement Logic, a next-generation homage to Nuprl; RedPRL was preceeded by JonPRL, written by Jon Sterling, Danny Gratzer and Vincent Rahli.
The purpose of RedPRL is to consolidate several advances in refinement logics, including:
- a multi-sorted version of abstract binding trees
- support for nominal abstraction and unguessable atoms
- a dependent version of the LCF apparatus to support refinement rules whose premises depend on each other's evidence
RedPRL is a proof assistant for Nominal Multi-Sorted Computational Type Theory, whose semantics are defined in Sterling & Morrison's Type Refinements for the Working Class. The syntactic framework is described in Syntax and Semantics of Abstract Binding Trees, also by Sterling & Morrison.
This is the repository for the nascent development of RedPRL. RedPRL is an experiment which is constantly changing; we do not yet have strong documentation, but we have an IRC channel on Freenode (#redprl) where we encourage anyone to ask any question, no matter how silly it may seem.
First, fetch all submodules. If you are cloning for the first time, use
git clone --recursive git@github.com:RedPRL/sml-redprl.git
If you have already cloned, then be sure to make sure all submodules are up to date, as follows:
git submodule update --init --recursive
Next, make sure that you have the MLton compiler for Standard ML installed. Then, simply run
./script/mlton.sh
Then, a binary will be placed in ./bin/redprl
, which you may run as
follows
./bin/redprl my-development.prl
RedPRL is presently supported in Atom and Emacs.
The Atom plugin is available at atom.io.
The Emacs mode is a part of this repository. Additionally, it is available in MELPA.
The easiest way to install the package is from MELPA, using their getting
started instructions. The package is named
redprl
. It will probably be necessary to set the customization variable
redprl-command
to the path to the redprl
binary.
When redprl-mode
is installed, files ending in .prl
will automatically open
in the mode. If they do not, run M-x redprl-mode
. The mode supports the
following features:
-
Press
C-c C-l
to send the current development to RedPRL. -
Imenu (or wrappers such as
helm-imenu
) can be used to jump to definitions in the buffer. -
Completion is supported for names of declarations in the current buffer.
-
Flycheck is also supported, and can be used in lieu of
C-c C-l
if you like. Be sure that either theredprl
executable is in your path, or setflycheck-redprl-executable
in your own Emacs configuration.