From 58a0f196da301ccf56e280ca4bd28abd35e0a75a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=81ukasz=20Czajka?=
 <62751+lukaszcz@users.noreply.github.com>
Date: Tue, 7 Feb 2023 19:12:44 +0100
Subject: [PATCH] Documentation: how to compile Juvix programs (#1813)

---
 docs/org/SUMMARY.org                    |  2 --
 docs/org/howto/compilation.org          | 41 +++++++++++++++++++++++++
 docs/org/reference/examples.org         |  1 -
 docs/org/reference/language/README.org  |  2 --
 docs/org/reference/language/modules.org | 20 ++++++------
 5 files changed, 51 insertions(+), 15 deletions(-)
 create mode 100644 docs/org/howto/compilation.org

diff --git a/docs/org/SUMMARY.org b/docs/org/SUMMARY.org
index 85c8bd73c..0ed5814c6 100644
--- a/docs/org/SUMMARY.org
+++ b/docs/org/SUMMARY.org
@@ -30,8 +30,6 @@
   - [[./reference/language/modules.md][Modules]]
   - [[./reference/language/comments.md][Comments]]
   - [[./reference/language/axioms.md][Axioms]]
-  - [[./reference/language/compileblocks.md][Compile blocks]]
-  - [[./reference/language/foreign.md][Foreign blocks]]
 - [[./reference/examples.md][Example programs]]
 - [[./reference/benchmarks.md][Benchmarks]]
 - [[./reference/tooling/README.md][Tooling]]
diff --git a/docs/org/howto/compilation.org b/docs/org/howto/compilation.org
new file mode 100644
index 000000000..3d0f88ed7
--- /dev/null
+++ b/docs/org/howto/compilation.org
@@ -0,0 +1,41 @@
+
+* Compiling simple programs
+
+A Juvix file must declare a module whose name corresponds exactly to the name of the file. For example, a file =Hello.juvix= must declare a module =Hello=:
+#+begin_example
+-- Hello world example. This is a comment.
+module Hello;
+
+-- Import the standard library prelude, including the function 'printStringLn'
+open import Stdlib.Prelude;
+
+main : IO;
+main := printStringLn "Hello world!";
+
+end;
+#+end_example
+A file compiled to an executable must define the zero-argument function =main= of type =IO= which is evaluated when running the program.
+
+To compile the file =Hello.juvix= type =juvix compile Hello.juvix=. Typing =juvix compile --help= will list all options to the =compile= command.
+
+* Compilation targets
+
+Since version 0.3 Juvix supports three compilation targets. The targets are specified with the =-t= option: =juvix compile -t target file.juvix=.
+
+1. =native=. This is the default. Produces a native 64bit executable for your machine.
+2. =wasm32-wasi=. Produces a WebAssembly binary which uses the WASI runtime.
+3. =geb=. Produces a [[https://anoma.github.io/geb/][GEB]] input file.
+
+* Juvix projects
+
+A _Juvix project_ is a collection of Juvix modules inside one main
+project directory containing a =juvix.yaml= metadata file. The name of
+each module must coincide with the path of the file it is defined in,
+relative to the project's root directory. For example, if the file is
+=root/Data/List.juvix= then the module must be called =Data.List=,
+assuming =root= is the project's directory.
+
+To check that Juvix is correctly detecting your project's root, you
+can run the command =juvix dev root File.juvix=.
+
+See also: [[../reference/language/modules.md][Modules Reference]].
diff --git a/docs/org/reference/examples.org b/docs/org/reference/examples.org
index 87d522bd1..a071f86ed 100644
--- a/docs/org/reference/examples.org
+++ b/docs/org/reference/examples.org
@@ -6,4 +6,3 @@ The following links are clickable versions of their corresponding Juvix programs
 - [[https://docs.juvix.org/examples/html/PascalsTriangle/PascalsTriangle.html][PascalsTriangle.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]]
diff --git a/docs/org/reference/language/README.org b/docs/org/reference/language/README.org
index a3219dc7d..a2d732c36 100644
--- a/docs/org/reference/language/README.org
+++ b/docs/org/reference/language/README.org
@@ -3,5 +3,3 @@
   - [[./modules.md][Modules]]
   - [[./comments.md][Comments]]
   - [[./axioms.md][Axioms]]
-  - [[./compileblocks.md][Compile blocks]]
-  - [[./foreign.md][Foreign blocks]]
diff --git a/docs/org/reference/language/modules.org b/docs/org/reference/language/modules.org
index d6e57e2af..50e933a11 100644
--- a/docs/org/reference/language/modules.org
+++ b/docs/org/reference/language/modules.org
@@ -2,9 +2,8 @@
 
 ** Defining a module
 
-A module is of the following form. The =module= keyword stars the declaration of
-a module followed by its name and its body. The module declaration ends after
-seeing the =end= keyword.
+The =module= keyword stars the declaration of a module followed by its
+name and body. The module declaration ends with the =end= keyword.
 
 #+begin_example
 -- ModuleName.juvix
@@ -13,15 +12,16 @@ module ModuleName;
 end;
 #+end_example
 
-A _Juvix project_ is a collection of Juvix modules inside one main project
-folder containing a metadata file named =juvix.yaml=. Each Juvix file has to
-define a _module_ of the same name. The name of the module must coincide with
-the path of the its file respect to its project. For example, if the file is
-=root/Data/List.juvix= then the module must be called =Data.List=, assuming
-=root= is the project's folder.
+A _Juvix project_ is a collection of Juvix modules inside one main
+project folder containing a metadata file named =juvix.yaml=. Each
+Juvix file has to define a _module_ of the same name. The name of the
+module must coincide with the path of the its file relative to its
+project's root directory. For example, if the file is
+=root/Data/List.juvix= then the module must be called =Data.List=,
+assuming =root= is the project's folder.
 
 To check that Juvix is correctly detecting your project's root, one can run the
-command =juvix internal root File.juvix=.
+command =juvix dev root File.juvix=.
 
 # - Inside a module, other (sub) modules can be declared.