Add revisions to README

README.org

@@ -6,6 +6,12 @@
 </a>
 #+end_html
 
+#+begin_html
+<a href="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment"><img
+src="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment/badge.svg"
+alt="pages-build-deployment" /></a>
+#+end_html
+
 #+begin_html
 <a href="https://github.com/anoma/juvix/tags">
 <img alt="" src="https://img.shields.io/github/v/release/anoma/juvix?include_prereleases" />
@@ -18,12 +24,6 @@
 </a>
 #+end_html
 
-#+begin_html
-<a href="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment"><img
-src="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment/badge.svg"
-alt="pages-build-deployment" /></a>
-#+end_html
-
 #+begin_html
 <a href="https://github.com/anoma/juvix">
 <img align="right" width="300" height="300" alt="Juvix Mascot" src="assets/seating-mascot.051c86a.svg" />
@@ -35,57 +35,86 @@ alt="pages-build-deployment" /></a>
 
 Juvix is a research programming language created by [[https://heliax.dev/][Heliax]] as a first step toward creating more robust and reliable alternatives for formally verified smart contracts than existing languages. The Juvix language is constantly evolving, open-source, functional, and statically typed with special support for compiling [[https://anoma.network/blog/validity-predicates/][validity predicates]] to the =C= language, which can be deployed to various distributed ledgers including [[https://anoma.net/][Anoma]].
 
-The Juvix programming language allows developers to write programs with a high degree of assurance that they will meet specific standards. This is due to the fact that several static analyses are performed during compilation, including, for example, scope, termination, arity, and type checking. As a result, functional programs, especially validity predicates, can be written with greater confidence that they will be free of runtime errors.
-
-The language features:
-
-- unicode syntax
-- parametric polymorphism
-- inductive and parametric data types
-- higher-order functions
-- implicit arguments
-- holes in programs
-- axioms for non-computable terms
-
-Additionally, the foreign and compile blocks syntax enable developers to compile a program to different backends including the =C= language. The Juvix module system further permits splitting programs into several modules to build libraries which can be later documented by generating HTML files based on the codebase, see for example, [[https://anoma.github.io/juvix-stdlib/][the Juvix standard library's website]]. For futher details, please refer to [[https://anoma.github.io/juvix/][the Juvix book]] which includes our [[https://anoma.github.io/juvix/introduction/changelog.html][latest updates]].
+The Juvix language and related tools are documented in [[https://anoma.github.io/juvix/][the Juvix book]].
 
-** [[https://github.com/anoma/juvix/tree/main/examples/milestone][Examples of programs written in Juvix]]
+** [[https://github.com/anoma/juvix/tree/main/examples/milestone][First examples of programs written in Juvix]]
 
-The following links are clickable versions of their corresponding Juvix programs. The HTML output can be generated by running =juvix html --recursive FileName.juvix=.
+The following links are clickable versions of their corresponding Juvix programs. The HTML output is generated by running =juvix html --recursive FileName.juvix=.
 
 - [[https://docs.juvix.org/examples/html/Fibonacci/Fibonacci.html][Fibonacci.juvix]]
 - [[https://docs.juvix.org/examples/html/Collatz/Collatz.html][Collatz.juvix]]
 - [[https://docs.juvix.org/examples/html/TicTacToe/CLI/CLI.TicTacToe.html][TicTacToe.juvix]]
 - [[https://docs.juvix.org/examples/html/ValidityPredicates/SimpleFungibleToken.html][SimpleFungibleToken.juvix]]
 
-The [[https://anoma.github.io/juvix-stdlib/][Juvix standard library]] contains common functions that can be used in Juvix programs.
+The [[https://anoma.github.io/juvix-stdlib/][Juvix standard library]] contains
+common functions that can be used in Juvix programs.
 
 ** Quick Start
 
-To install Juvix, you can download its sources using
-[[http://git-scm.com/][Git]] from the
-[[https://github.com/anoma/juvix.git][Github repository]]. Then, the
-program can be downloaded and installed with the following commands. You
-will need to have [[https://haskellstack.org][Stack]] installed.
+*** Installing Juvix on MacOS
+
+The easiest way to install Juvix on MacOS is by using
+[[https://brew.sh][Homebrew]]. Run the following commands on your machine.
+
+To install the [[https://github.com/anoma/homebrew-juvix][homebrew-juvix tap]], run:
+
+#+begin_src shell
+brew tap anoma/juvix
+#+end_src
+
+To install Juvix, run:
+
+#+begin_src shell
+brew install juvix
+#+end_src
+
+After installing Juvix, you might want to try our doctor to check your system
+setup:
+
+#+begin_src shell
+juvix doctor
+#+end_src
+
+Helpful information on the shell can also be obtained by running:
+
+#+begin_src shell
+brew info juvix
+#+end_src
+
+*** Building Juvix from the sources
+
+To install Juvix from the sources, you must download the
+[[https://github.com/anoma/juvix.git][Github repository]]. Then, the program can
+be installed with the following commands. We assume have
+[[https://haskellstack.org][Stack]] installed.
 
 #+begin_src shell
 git clone --recursive https://github.com/anoma/juvix.git
 cd juvix
 stack install
 #+end_src
 
-If the installation succeeds, you must be able to run the Juvix
-command from any location. To get the complete list of commands, please
-run =juvix --help=.
+If the installation succeeds, you must be able to run the Juvix command from any
+location. To get the complete list of commands, please run =juvix --help=.
+
+On MacOS, you can alternatively run the following command for Homebrew. The flag
+=--HEAD= used below is optional, mostly to build the latest version of Juvix in
+the =main= branch on Github.
+
+#+begin_src shell
+brew install --build-from-source --HEAD juvix --verbose
+#+end_src
 
 ** Usage Example
 
 In the following example a Juvix file is compiled using the C backend. The
-result is compiled to WASM using [[https://llvm.org][Clang]] and then executed using [[https://wasmer.io][wasmer]].
+result is compiled to WASM using [[https://llvm.org][Clang]] and then executed
+using [[https://wasmer.io][wasmer]].
 
 NB: Set the =WASI_SYSROOT_PATH= environment variable to the root of the WASI
-sysroot. See [[https://anoma.github.io/juvix/getting-started/dependencies.html][Installing dependencies]] for instructions on how to install the
-sysroot.
+sysroot. See
+[[https://anoma.github.io/juvix/getting-started/dependencies.html][Installing
+dependencies]] for instructions on how to install the sysroot.
 
 #+begin_src shell
 cd tests/positive/MiniC/HelloWorld
@@ -95,9 +124,57 @@ wasmer Input.wasm
 
 You should see the output: =hello world!=
 
-** The Juvix Book
+** The Juvix programming language
 
-The Juvix language and related tools are documented in [[https://anoma.github.io/juvix/][the Juvix book]].
+Juvix allows us to write programs with a high degree of assurance. The Juvix
+compiler runs several static analyses during the compilation phase to guarantee
+no runtime errors. Analyses permormed during this phase include scope,
+termination, arity, and type checkiqng. As a result, functional programs,
+especially validity predicates, can be written with greater confidence that they
+will be free of runtime errors.
+
+Some of the language features in Juvix include:
+
+- unicode syntax
+- parametric polymorphism
+- inductive and parametric data types
+- higher-order functions
+- implicit arguments
+- holes in expressions
+- axioms for non-computable terms
+
+Additionally, the foreign and compile blocks syntax enable developers to compile
+a program to different backends including the =C= language. The Juvix module
+system further permits splitting programs into several modules to build
+libraries which can be later documented by generating HTML files based on the
+codebase, see for example, [[https://anoma.github.io/juvix-stdlib/][the Juvix
+standard library's website]]. For futher details, please refer to
+[[https://anoma.github.io/juvix/][the Juvix book]] which includes our
+[[https://anoma.github.io/juvix/introduction/changelog.html][latest updates]].
+
+** Coming soon
+
+For the language:
+
+- lambda expressions
+- =let= expressions
+- tail call optimization
+- inference for mutually recursive functions
+- compilation to circuits
+- coverage checking (i.e. exhaustiveness and useless clauses)
+
+For the emacs mode:
+
+- jump back to errors
+
+For the compiler:
+
+- Init command
+- New documentation tool. Currently available as an internal command:
+
+    #+begin_src shell
+       juvix internal doc MyFile.juvix
+    #+end_src
 
 ** Community