Update read me to the present day and cause the makefile from the top level directory to be a bit more sensible

2 files changed, 79 insertions, 48 deletions

diff --git a/Makefile b/Makefile
index 0267f4a6..221bc554 100644
--- a/Makefile
+++ b/Makefile
@@ -1,9 +1,10 @@
 .PHONY: all sail language clean power test
 
-all: sail interpreter language
+all: sail
 
-sail: language
+sail:
 	$(MAKE) -C src
+	ln -s src/sail.native sail
 
 language:
 	$(MAKE) -C language
@@ -11,14 +12,6 @@ language:
 interpreter: 
 	$(MAKE) -C src interpreter
 
-test: 
-	$(MAKE) -C src test
-
-power: 
-	$(MAKE) -C src power
-
-test_power_interactive:
-	$(MAKE) -C src test_power_interactive
-
 clean:
 	$(MAKE) -C src clean
+	rm sail
diff --git a/README b/README
index 52f9b661..f4daaf40 100644
--- a/README
+++ b/README
@@ -1,18 +1,77 @@
 # Readme
 
-Guide to Sail, as of August 6 2014. Subject to possible change later.
+Guide to Sail, as of Feb 25, 2016. 
 
-Sail relies on external access to Lem, Ott, Lem libraries, and Power
-binaries for some testing, as well as Ocaml 4.01.0 or later. Some 
-dependencies are at present hard coded paths in makefiles. Thus 
-Sail expects to find a directory structure as the following
-External directory structure:
-Sail to be found in BASE/bitbucket/l2
-Lem to be found in BASE/bitbucket/lem
-idl to be found in BASE/rsem/idl
+Note: the repository name intends to change to sail for a public release
 
-(BASE might have to be the user homedirectory, but many connections
-are using ../../ etc)
+BUILDING
+
+The Sail type checker and compiler requires OCaml; it is tested
+on version 4.02.3.
+
+Run make in the top level l2 directory; this will generate an executable
+called sail in this directory. 
+
+make clean will remove this executable as well as the build files in
+subdirectories.
+
+The Sail interpreter relies on external access to Lem and Linksem
+for building and running the interpreter.
+
+Lem is a public bitbucket git repository. Linksem is a private bitbucket
+mercurial repsotory
+
+The Sail build system expects to find these repositories in in the same
+directory as the l2 repository by default. This can be changed with
+make variables LEM, LEMLIBOCAML, and ELFDIR
+
+To build the interpreter, first build Lem and the Lem ocaml libraries.
+Then call make interpreter from either the toplevel directory or the src
+directory.
+
+The interpreter currently only evaluates binaries and requires modifications
+to a file within the src/lem_interp directory to support new architectures.
+There is 'bit-rotted' support for evaluating separate sail files and function
+calls. 
+
+EMACS MODE
+
+There is an emacs mode implementation very similar to the Tuareg mode in l2/editors 
+
+RUNNING SAIL compiler
+
+./sail test.sail   % Type check sail file, do not generate any output.
+                   % Multiple files can be listed, the resulting specification is
+                   % equivalent to a concatenation in order of the given files
+
+Command-line options
+  -verbose           pretty-print out the file
+  -lem_ast           pretty-print a Lem AST representation of the file, for the interpreter
+  -lem               print a Lem translated version of the specification
+  -ocaml             print an Ocaml translated version of the specification
+  -skip_constraints  skip constraint resolution in type-checking (*Not recommended*)
+  -lem_lib           provide additional library to open in Lem output
+  -ocaml_lib         provide additional library to open in Ocaml output
+  -v                 print version
+  -o                 select output filename prefix
+  -help              Display this list of options
+  --help             Display this list of options
+
+
+Usage
+
+./sail test.sail foo.sail -o spec -lem_ast -ocaml
+
+Will generate the files spec.lem and spec.ml in the current directory
+
+It is not recommended to try to read the generated Lem ast file, as it is a very verbose
+representation of the AST. 
+
+IN PROGRESS COMMANDS: -lem -ocaml
+The resulting output of these commands may well be untype checkable Lem or OCaml
+
+
+DIRECTORY STRUCTURE
 
 Sail sources and binaries are to be found in the directories of
 bitbucket/l2 (to be renamed when we make sail public in a
@@ -21,14 +80,9 @@ bitbucket/sail respository (hopefully)
 Top level directories
 src/            ML implementation of Sail frontend, Sail executable, subdirectories
 language/       Ott definitions of source language, pdfs as well
-l3-to-l2/       Directory for student to define l3-to-l2 translation, abandoned?
-
-Relevant make commands:
-make            Builds Sail executable
-make test       As above, also builds interpreter, and runs test suite
-make power      As above (except running) and  builds executable interpreting power binary
-make clean      Cleans src and language
-
+mips/           Sail definition of a MIPS specification
+risc-v/         abandoned very partial attempt at RISC V specification
+l3-to-l2/       abandoned but not GC-ed directory
 
 language directory
 l2_parse.ott    Grammar of Sail generated by parser, superset of source language
@@ -75,16 +129,10 @@ util.ml
 
 Relevant make commands:
 make            Builds Sail executable (does not remake language files automatically)
-make test       As above, also builds interpreter, and runs test suite
-make power      As above (except running) and  builds executable interpreting power binary
-make test_power As above, runs power binary found in idl/power/binary
+make interpreter Builds sail interpeter
+make run_mips.native Builds an executable sequential interpreter for MIPS Elf binaries
 make clean      
 
-Using sail executable
-./sail.native -h   % Lists command line flags
-./sail.native test.sail -lem_ast % typical usage to generate a lem_ast file test.lem
-./sail.native test.sail -verbose % resulting sail is not typecheckable
-
 lem_interp directory
 interp.lem              interpreter implementation
 interp_ast.lem          symlink to language/l2.lem
@@ -94,13 +142,3 @@ interp_lib.lem          implementation of sail library functions
 pretty_interp.ml        pretty printing for interperter forms
 run_interp.ml           interactive implementation for running interpreter with simple memory and registers
 
-
-test directory
-idempotence.sh          script to test the pretty printer, but files might not pass type checking for predictable reasons
-pattern.sail            part of test suite, testing pattern match
-power.sail              extract of subset of power instructions: NOT JUST USED FOR TESTING
-regbits.sail            part of test suite, testing register declarations
-run_power.ml            framework to read memory, and run power in interpreter
-run_tests.ml            framework for running test suite
-testN.sail              various test suite files, based on past bugs
-vectors.sail            part of test suite, testing vector operations