Initial documentation of back ends

docs/backends/chez.rst

@@ -0,0 +1,47 @@
+**************************
+Chez Scheme Code Generator
+**************************
+
+The Chez Scheme code generator is the default, or it can be accessed via a REPL
+command:
+
+::
+
+    Main> :set cg chez
+
+By default, therefore, to run Idris programs you will need to install
+`Chez Scheme <https://www.scheme.com/>`_. Chez Scheme is open source, and
+available via most OS package managers.
+
+You can compile an expression ``expr`` of type ``IO ()`` to an executable as
+follows, at the REPL:
+
+::
+
+    Main> :c execname expr
+
+...where ``execname`` is the name of the executable file. This will generate
+the following:
+
+* A shell script ``build/exec/execname`` which invokes the program
+* A subdirectory ``build/exec/execname_app`` which contains all the data necessary
+  to run the program. This includes the Chez Scheme source (``execname.ss``),
+  the compiled Chez Scheme code (``execname.so``) and any shared libraries needed
+  for foreign function definitions.
+
+The executable ``execname`` is relocatable to any subdirectory, provided that
+``execname_app`` is also in the same subdirectory.
+
+You can also execute an expression directly:
+
+::
+
+    Main> :exec expr
+
+Again, ``expr`` must have type ``IO ()``. This will generate a temporary
+executable script ``_tmpchez`` in the ``build/exec`` directory, and execute
+that.
+
+Chez Scheme is the default code generator, so if you invoke ``idris2`` with the
+``-o execname`` flag, it will generate an executable script
+``build/exec/execname``, again with support files in ``build/exec/execname_app``.

docs/backends/index.rst

@@ -0,0 +1,47 @@
+************************
+Compiling to Executables
+************************
+
+.. note::
+
+   The documentation for Idris has been published under the Creative
+   Commons CC0 License. As such to the extent possible under law, *The
+   Idris Community* has waived all copyright and related or neighboring
+   rights to Documentation for Idris.
+
+   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+
+Idris 2 (the language) is designed to be independent of any specific code
+generator. Still, since the point of writing a program is to be able to run it,
+it's important to know how to do so! By default, Idris compiles to executables
+via `Chez Scheme <https://www.scheme.com/>`_.
+
+You can compile to an executable as follows, at the REPL:
+
+::
+
+     Main> :c execname expr
+
+...where ``execname`` is the name of the executable file to generate, and
+``expr`` is the Idris expression which will be executed. ``expr`` must have
+type ``IO ()``. This will result in an executable file ``execname``, in a
+directory ``build/exec``, relative to the current working directory.
+
+You can also execute expressions directly:
+
+::
+
+    Main> :exec expr
+
+Again, ``expr`` must have type ``IO ()``.
+
+There are two code generators provided in Idris 2, and (later) there will be
+a system for plugging in new code generators for a variety of targets. The
+default is to compile via Chez Scheme, with an alternative via Racket.
+
+.. toctree::
+   :maxdepth: 1
+
+   chez
+   racket
+

docs/backends/racket.rst

@@ -0,0 +1,11 @@
+*********************
+Racket Code Generator
+*********************
+
+The Racket code generator is accessed via a REPL command:
+
+::
+
+    Main> :set cg racket
+
+[More details TODO]

docs/index.rst

@@ -23,6 +23,7 @@ and yet to be updated, so use with caution!
    :maxdepth: 1
 
    tutorial/index
+   backends/index
    updates/updates
    typedd/typedd
    app/index