Merge pull request #380 from chrrasmussen/add-docs-about-dirs

Add documentation for sourcedir/builddir/outputdir

docs/source/backends/custom.rst

@@ -31,7 +31,7 @@ Now create a file containing
     compile : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
             ClosedTerm -> (outfile : String) -> Core (Maybe String)
     compile defs tmpDir outputDir term file = do coreLift $ putStrLn "I'd rather not."
-                                    pure $ Nothing
+                                                 pure $ Nothing
 
     execute : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
     execute defs tmpDir term = do coreLift $ putStrLn "Maybe in an hour."
@@ -70,3 +70,12 @@ It will not be overly eager to actually compile any code with the new backend th
     $ ./build/exec/lazy-idris2 --cg lazy Hello.idr -o hello
     I'd rather not.
     $
+
+About the directories
+---------------------
+
+The code generator can assume that both ``tmpDir`` and ``outputDir`` exist. ``tmpDir``
+is intended for temporary files, while ``outputDir`` is the location to put the desired
+output files. By default, ``tmpDir`` and ``outputDir`` point to the same directory
+(``build/exec``). The directories can be set from the package description (See Section
+:ref:`ref-sect-packages`) or via command line options (Listed in ``idris2 --help``).

docs/source/reference/packages.rst

@@ -39,9 +39,9 @@ The added fields are:
 + ``brief = "<text>"``, a string literal containing a brief description
   of the package.
 
-+ ``version = "<text>""``, a version string to associate with the package.
++ ``version = "<text>"``, a version string to associate with the package.
 
-+ ``readme = "<file>""``, location of the README file.
++ ``readme = "<file>"``, location of the README file.
 
 + ``license = "<text>"``, a string description of the licensing
   information.
@@ -57,6 +57,16 @@ The added fields are:
 
 + ``bugtracker = "<url>"``, the location of the project's bug tracker.
 
+Directories
+-----------
+
++ ``sourcedir = "<dir>"``, the directory to look for Idris source files.
+
++ ``builddir = "<dir>"``, the directory to put the checked modules and
+  the artefacts from the code generator.
+
++ ``outputdir = "<dir>"``, the directory where the code generator should
+  output the executable.
 
 Common Fields
 -------------
@@ -68,11 +78,11 @@ Other common fields which may be present in an ``ipkg`` file are:
   identifier. the iPKG format also takes a quoted version that accepts
   any valid filename.
 
-  Executables are placed in ``build/exec``, relative to the top level
-  source directory.
+  Executables are placed in ``build/exec`` by default. The location can
+  be changed by specifying the ``outputdir`` field.
 
 + ``main = <module>``, which takes the name of the main module, and
-  must be present if the executable field is present.
+  must be present if the ``executable`` field is present.
 
 + ``opts = "<idris options>"``, which allows options to be passed to
   Idris.