From 2ec923d4f386812d7be451caa7f61a56471c217e Mon Sep 17 00:00:00 2001
From: Niklas Larsson <niklas@mm.st>
Date: Sun, 14 Jun 2020 19:04:43 +0200
Subject: [PATCH] Add documentation

---
 docs/source/backends/custom.rst | 72 +++++++++++++++++++++++++++++++++
 docs/source/backends/index.rst  |  1 +
 2 files changed, 73 insertions(+)
 create mode 100644 docs/source/backends/custom.rst

diff --git a/docs/source/backends/custom.rst b/docs/source/backends/custom.rst
new file mode 100644
index 000000000..877b2c2b5
--- /dev/null
+++ b/docs/source/backends/custom.rst
@@ -0,0 +1,72 @@
+**********************************
+Building Idris 2 with new backends
+**********************************
+
+The way to extend Idris 2 with new backends is to use it as
+a library. The module ``Idris.Driver`` exports the function
+``mainWithCodegens``, that takes a list of ``(String, Codegen)``,
+starting idris with these codegens in addition to the built-in ones.
+
+Getting started
+===============
+
+To use Idris 2 as a library you need to install it with (the ipkg file
+is at the top level of the Idris2 repo)
+
+::
+
+    idris2 --build idris2api.ipkg
+    idris2 --install idris2api.ipkg
+
+Now create a file containing
+
+.. code-block:: idris
+
+    module Main
+
+    import Core.Context
+    import Compiler.Common
+    import Idris.Driver
+
+    compile : Ref Ctxt Defs -> (execDir : String) ->
+            ClosedTerm -> (outfile : String) -> Core (Maybe String)
+    compile defs dir term file = do coreLift $ putStrLn "I'd rather not."
+                                    pure $ Nothing
+
+    execute : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
+    execute defs dir term = do coreLift $ putStrLn "Maybe in an hour."
+
+    lazyCodegen : Codegen
+    lazyCodegen = MkCG compile execute
+
+    main : IO ()
+    main = mainWithCodegens [("lazy", lazyCodegen)]
+
+Build it with
+
+::
+
+    $ idris2 -p idris2 -p contrib -p network Lazy.idr -o lazy-idris2
+
+Now you have an idris2 with an added backend.
+
+::
+
+    $ ./build/exec/lazy-idris2
+        ____    __     _         ___
+        /  _/___/ /____(_)____   |__ \
+        / // __  / ___/ / ___/   __/ /     Version 0.2.0-d8c7f08bd
+    _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
+    /___/\__,_/_/  /_/____/   /____/      Type :? for help
+
+    Welcome to Idris 2.  Enjoy yourself!
+    With codegen for: lazy
+    Main>
+
+It will not be overly eager to actually compile any code with the new backend though
+
+::
+
+    $ ./build/exec/lazy --cg lazy Hello.idr -o hello
+    I'd rather not.
+    $
diff --git a/docs/source/backends/index.rst b/docs/source/backends/index.rst
index 6005c57ee..dc355d796 100644
--- a/docs/source/backends/index.rst
+++ b/docs/source/backends/index.rst
@@ -60,3 +60,4 @@ or via the `IDRIS2_CG` environment variable.
    chez
    racket
    gambit
+   custom