Commit 308ec6d5 authored by Heiko Becker's avatar Heiko Becker
Browse files

Add config scripts and current state README contains instructions on...

Add config scripts and current state README contains instructions on installing and running hol-light
parent 6d692ba6
# Using HOL Light #
1. Clone the latest release from the Github Repository
https://github.com/jrh13/hol-light/
2. Do steps (0) and (1) from the Installation part in the README
3. Run the `configure_ocaml.sh` script
This script currently only creates the necessary .ocamlinit file such that it is not necessary to load HOL Light by hand.
4. Open emacs and add the following line to your customized variables in your .emacs file:
`'(warning-suppress-types (quote ((undo discard-info))))`
This line will suppress the warnings that the ocaml buffer is too long.
5. Add the following line to your .emacs:
`(load "ABSOLUTE_PATH_TO_DAISY_REPO_HOL_DIR/hol-light.el")`
6. After restarting emacs, you can open any .ml file in this directory and use M-x hol-light-mode to get syntax highlighting working
To get an interactive prompt do M-x hol-light-run-caml. When prompted for an hol-light binary simply enter ocaml.
## Keybindings ##
The file hol-light.el contains all the keybindings in the variable `hol-light-mode-map`. The most important one is C-x C-e which sends the line under the cursor to the ocaml shell.
#!/bin/bash
###################################################
# configuration Script to set up the ocaml #
# environment file, needed for ease of using HOL #
###################################################
#check wether HOLLIGHT_HOME is set
PG_DIR=
CURR_DIR=`pwd`
if [ -z "$HOLLIGHT_HOME" ];
then
echo "Please configure HOLLIGHT_HOME to point to your local HOL Light directory";
exit 1;
fi
#if [ -z "$1" ];
#then
# echo "No Proof General directory supplied. Not including PG Tactics";
# echo "If needed, provide the absolute path to the ho-light subdirectory of Proof General as first argument"
#else
# PG_DIR=$1
#fi
echo "#cd \""$HOLLIGHT_HOME"\";;" > .ocamlinit
echo "#use \"hol.ml\";;" >> .ocamlinit
#if [ ! -z "$PG_DIR" ]
#then
# echo "#cd \""$PG_DIR"\";;" >>.ocamlinit
# echo "#use \"pg_prompt.ml\";;" >>.ocamlinit
# echo "#use \"pg_tactics.ml\";;" >>.ocamlinit
#fi
echo "#cd \""$CURR_DIR"\";;" >>.ocamlinit
(*
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
*)
(* FIXME: num -> real for Const *)
let exp_INDUCT, exp_REC= define_type
"exp = Var num
| Const real
| Plus exp exp
| Sub exp exp
| Mult exp exp
| Div exp exp";;
let exp_eval = define
`(exp_eval (Var x) E = E x) /\
(exp_eval (Const r) E = r) /\
(exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
(exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
(exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
(exp_eval (Div e1 e2) E = (exp_eval e1) E * (exp_eval e2) E)`;;
let s_env_EQ =
define `s_env:num->real = (\x. 1:real)`;;
let test_EQ =
define `test:num = exp_eval (Var 1) s_env`;;
g `test = 1`;;
e (REWRITE_TAC[test_EQ; s_env_EQ; exp_eval]);;
let bexp_INDUCT, bexp_REC = define_type
"bexp = leq exp exp
| less exp exp";;
(* Simplify arithmetic later by making > >= only abbreviations *)
let gr = `\e1. \e2. less e2 e1`;;
let greq = `\e1. \e2. leq e2 e1`;;
let cmd_INDUCT, cmd_REC = define_type
"cmd = Ass num exp
| Seq cmd cmd
| Ite bexp cmd cmd";;
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment