QUICKSTART

QUICK START WITH PROOF EDITOR

Starting MetaPRL:
  Default interface:
     editor/ml/mp     

  Custom interfaces:
     editor/ml/mpxterm  (will start MetaPRL CLI in a new xterm using a correct font)
     editor/ml/mpopt    (starts native code MetaPRL with default UI)
     editor/ml/mptop    (starts bytecode MetaPRL with default UI)
     editor/ml/mprun    (starts debugging toploop; not recommended for beginners)

Navigation:

ls: string -> unit
    lists the contents of the current  module (theory, proof)
  The string argument currently affect only top-level theory listings:
  ls "";;   -- lists the most interesting parts,
  ls "a";;  -- lists everything,
  ls "R";;  -- lists rules,
  ls "r";;  -- lists rewrites,
  ls "u";;  -- lists everything unproved,
  ls "f";;  -- lists all formal contents
  ls "d";;  -- lists all display-related items.
  Note that you can combine ls options, e.g. ls "rR" would list all rules
  and rewrites.

pwd ();;   returns current path in the _loaded_module_ tree.

cd: string -> unit
    provides navigation in the loaded module tree.
   Examples:
   cd "itt_int_base"
   cd "/";;
   cd "..";;
   cd "<rulename/rwname>";; --   cd to the proof of the rule/rewrite.

Navigation in proofs:
   root ();;
   down <subgoal number> ;;
   up <number of levels>;;

   next ();; - go to next unproved leaf in proof/modules (to be implemented).

Proof refinement:
   refine <tactic>;;  see doc/itt_quickref.txt for Base Theory and ITT tactics.

Save proof:
When you cd into some theory for the first time, MetaPRL reads the
newest among the .prla, .prlb and .cmoz
  save ();;  -- current module in .prlb file
                (but only if it was modified; for local use),
  save_all ();; -- all modified modules,
  export ();; -- in .prla file (stable format for subversion, MetaPRL upgrades)
------------------------
  export() function:
  Note that it uses the old .prla file as a part of
  input (it tries to keep as many lines as possible unchanged to be more
  CVS-friendly), so if you exported the same theory several times between
  commits, it may be a good idea to
  1) Start MetaPRL and load the theory
  2) save() (just in case)
  3) Remove the .prla file and do a CVS update to get the old version of
  it.
  4) Do export()
  5) commit.
-------------------------

Proof expansion:
   expand ();;
     -- re-runs the proof (that's at and under the current node you are at);
   expand_all ();;
     -- re-runs all proofs in the current node
     -- from root - re-runs all proofs in MetaPRL

Object status:
   status ();;
     -- tells the status of the current object
   status_all ();;
     -- re-runs all proofs in the current node and tells their status
     -- from root - same for all the proofs in MetaPRL

Proof checking:

   check ();;
     -- lists the dependencies of the current rule
   check_all ();;
     -- checks all rules in the current node
     -- displays if they're primitive or derived
     -- displays if the proofs are complete or incomplete

Changing display form mode:
    set_dfmode : string -> unit
Set display mode, string could be "prl" (default), "src", "tex", "html"
This command should be run before entering proof of rule/rewrite.

WHERE AND HOW TO TRY:

  As long as you have TESTS=yes in mk/config, it's easier to just use
  itt_test for tests.
  1) Check the variable TESTS in mk/config.
  2) Check itt_test.ml to contain lines

     include itt_theory
     open Refiner.Refiner.TermType
     open Tactic_type.Tacticals
     open Tactic_type.Conversionals

  and itt_test.mli    --

     open Refiner.Refiner.TermType
     open Tactic_type.Tacticals
     open Tactic_type.Conversionals

  3) Write  your rules/rewrites there and try to prove them.
  Use emacs interface and editor/prl-hack.el for good printing.


HOW TO USE prl-hack.el

Once:
  1) Make a symbolic link in your home directory to metaprl/   :
       cd
       ln -s <path>/metaprl/ ./

Every time:
  2) Start emacs
  3) Load prl_hack (in emacs, M-... usually means Alt-... ):
       M-x load-file
       metaprl/editor/emacs/prl-hack.el

     Comments:
               2+3) alternative:
               emacs -l metaprl/editor/emacs/prl-hack.el

               Another substitution for 3):
               Add the following line to your ~/.emacs
               (load-file "~/metaprl/editor/emacs/prl-hack.el")

  4) Start the shell for MetaPrl in emacs (uses Unicode font) :
       M-x metaprl
  5) In this shell cd to metaprl/editor/ml/ and
     start any toploop  (mptop, mp,  mpopt)


For Connection to Nuprl5

There are 2 possible connections to Nuprl5.  You can use either 1 or
both at the same time as they serve different functions.
  1. The "metaprl" connection gives nuprl access to the entire collection
     of theories with a variety of commands to edit and view the objects.
  2. The "jprover" connection gives acces to the jprover refiner so that one
     can call the tactic "Jprover" on any proof being viewed in nuprl.


Below we assume that:
  - Nuprl is running on host, <hostname>.
  - The Nuprl library environment is named <libenv>.
  - The Nuprl database is at <dbpathname>

To connect metaprl:

  Setup the nuprl *library* to listen for a connections on port <xxxx>.
  ML[(lib)] orb_start_accept <xxxx> `mathbus`;;

  1) Start editor/ml/mp
  2) # #use "x.ml";;
  3) # run_nuprl <xxxx> "<hostname>" "<libenv>" "<dbpathname>";;

To connect jprover:

  Setup the nuprl *refiner* to listen for a connections on port <xxxx>.
  ML[(ref)] orb_start_accept <xxxx> `mathbus`;;

  1) Start editor/ml/mp
  2) # #use "x.ml"
  3) # run_nuprljp <xxxx> "<hostname>" "<libenv>" "<dbpathname>"