update readme

Author: flupe

README.md

@@ -3,19 +3,37 @@
 An [Agda] backend to generate [MetaCoq] λ□ (LambdaBox) programs
 for further (verified) extraction to WASM or Rust.
 The backend builds off Agda 2.7.0.1.
+Compatible with Coq 8.19.0, MetaCoq 1.3.1 and CertiCoq 0.9.
 
 [Agda]: https://github.com/agda/agda
 [MetaCoq]: https://metacoq.github.io/
 
+To install the backend, setup GHC (tested with `9.10.1`) and cabal.
+
+```
+git clone git@github.com:omelkonian/agda2lambox.git
+cd agda2lambox
+cabal install
+```
+
+This will take a while, as it has to (recursively) clone the Agda repo 
+and compile from source.
+
+Then you're good to go.
+
+```
+agda2lambox [AGDAFLAGS] [--out-dir DIR] [--typed] FILE
+```
+
 ## Setup
 
-Compatible with Coq 8.19.0, MetaCoq 1.3.1 and CertiCoq 0.9.
+The backend generates `.v` and `.txt` files that contain the extracted λ□ environment.
+To check what's generated, setup CertiCoq and compile the minimal Coq prelude.
 
 ```
 opam pin add certicoq 0.9+8.19
 coq_makefile -f _CoqProject -o CoqMakefile
 make -f CoqMakefile
-cabal run agda2lambox -- --out-dir build -itest test/Nat.agda
 ```
 
 ## Status