Better command line handling, with subcommands.

GNUmakefile

@@ -16,7 +16,7 @@ doc:
 
 #### Unit tests and sanity check #############################################
 
-LAMBDAPI     = dune exec -- lambdapi --lib-root lib
+LAMBDAPI     = dune exec -- lambdapi check --lib-root lib
 OK_TESTFILES = $(sort $(wildcard tests/OK/*.dk tests/OK/*.lp))
 KO_TESTFILES = $(sort $(wildcard tests/KO/*.dk tests/KO/*.lp))
 

README.md

@@ -8,30 +8,35 @@ in the [documentation](doc/DOCUMENTATION.md).
 Installation via [Opam](http://opam.ocaml.org/)
 ---------------------
 
+We will only publish a new version of `lambdapi` Opam pacakge when the
+development has reached a more stable test. For now, we advise you to
+pin the development repository to get the latest bug fixes.
+
 ```bash
-opam install lambdapi
+opam pin add lambdapi https://github.com/Deducteam/lambdapi.git
 ```
-
 Dependencies and compilation
 ----------------------------
 
 Lambdapi requires a Unix-like system. It should work on Linux as well as on
 MacOS. It might also be possible to make it work on Windows with Cygwin or
 with "bash on Windows".
 
-List of dependencies:
+List of dependencies (for version numbers refer to `lambdapi.opam`):
  - GNU make
- - [ocaml](https://ocaml.org/) >= 4.04.1
- - [dune](https://dune.build/) >= 1.2.0
- - odoc (for documentation only)
- - [bindlib](https://github.com/rlepigre/ocaml-bindlib) >= 5.0.0
- - [earley](https://github.com/rlepigre/ocaml-earley) >= 2.0.0
- - [timed](https://github.com/rlepigre/ocaml-timed) >= 1.0
+ - [ocaml](https://ocaml.org/) (at least 4.04.1 and at most 4.07.1)
+ - [dune](https://dune.build/)
+ - [odoc](https://github.com/ocaml/odoc) (for documentation only)
+ - [bindlib](https://github.com/rlepigre/ocaml-bindlib)
+ - [earley](https://github.com/rlepigre/ocaml-earley)
+ - [timed](https://github.com/rlepigre/ocaml-timed)
  - [menhir](http://gallium.inria.fr/~fpottier/menhir/)
- - yojson >= 1.6.0
- - cmdliner
- - ppx\_inline\_test
- - [why3](http://why3.lri.fr/) >= 1.2.0
+ - [yojson](https://github.com/ocaml-community/yojson)
+ - [cmdliner](https://erratique.ch/logiciel/cmdliner)
+ - [why3](http://why3.lri.fr/)
+
+**Note on OCaml versions:** more recent versions of OCaml will be supported
+soon, once the new parsing technology that we are using has stabilized.
 
 **Note on the use of Why3:** the command `why3 config --detect` must be run to
 update the Why3 configuration when a new prover is installed (including on the
@@ -41,7 +46,7 @@ Using Opam, a suitable OCaml environment can be setup as follows.
 ```bash
 opam switch 4.05.0
 eval `opam config env`
-opam install dune odoc menhir yojson cmdliner bindlib.5.0.0 timed.1.0 earley.2.0.0 ppx_inline_test why3.1.2.0
+opam install dune odoc menhir yojson cmdliner bindlib.5.0.0 timed.1.0 earley.2.0.0 why3.1.2.0
 why3 config --detect
 ```
 

doc/DOCUMENTATION.md

@@ -25,8 +25,6 @@ Table of contents
 
  - [Tactics](sections/tactics.md)
 
- - [API](sections/api.md)
-
  - [Structure of directories and files](sections/structure.md)
 
  - [Implementation choices](sections/implementation.md)

doc/sections/install.md

@@ -1,15 +1,20 @@
-Installation via Opam
----------------------
+Installation via [Opam](http://opam.ocaml.org/)
+-----------------------------------------------
 
-See http://opam.ocaml.org/.
+The version of `lambdapi` that is directly available through Opam (with the
+command `opam install lambdapi`) is currently outdated. We will only publish
+a new version of `lambdapi` Opam pacakge when the development has reached a
+more stable test. For now, we advise you to pin the development repository to
+get the latest bug fixes.
 
 ```bash
-opam install lambdapi
+opam pin add lambdapi https://github.com/Deducteam/lambdapi.git
 ```
 
 The installation of `lambdapi` gives you:
  - a main executable named `lambdapi` in your `PATH`,
- - an OCaml library called `lambdapi`,
- - an LSP-compatible server called `lp-lsp` in your `PATH`,
+ - an OCaml library called `lambdapi.core` (system internals),
+ - an OCaml library called `lambdapi.pure` (pure interface),
+ - an OCaml library called `lambdapi.lsp` (LSP server),
  - a `lambdapi` mode for `Vim` (optional),
  - a `lambdapi` mode for `emacs` (optional).

doc/sections/module.md

@@ -25,8 +25,8 @@ library root.  The typical case is when a library (or package) is still  under
 development. In that case,  what we can do is map the development folder under
 the library root, similarly to what would happen when mounting a volume in our
 file system. There are two ways of doing that, the first one being to used the
-`--map <MOD_PATH>:<DIR>` command line option.  However, the best way is to use
-a package configuration file.
+`--map-dir MOD:DIR` command line option.  However, the best way is to use a
+package configuration file.
 
 #### Package configuration file
 
@@ -40,8 +40,8 @@ contain the following fields (an example is given below for the syntax):
  - `root_path` gives the module path under which the library is to be  placed.
    Assuming that our configuration file is at `<REPO_ROOT>/lambdapi.pkg`, this
    means that `<REPO_ROOT>/a/b/c.lp` will get module path `<ROOT_PATH>.a.b.c`.
-   In other words this is amounts to giving `--map <ROOT_PATH>:<REPO_ROOT>` on
-   the command line.
+   In other words this is amounts to giving `--map-dir <ROOT_PATH>:<REPO_ROOT>`
+   on the command line.
 
 In the future,  more useful meta data will be added to the configuration file,
 for example the name of the author, version number, dependencies, ...