git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2066 from jfdm/doc/sphinx-version-fixes

Sphinx 1.2 series compatibility fixes.

commitd0b8bb50e455d9c0f80e6940058fe0c5e5cec1ba authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateFri 27 Mar 2015, 16:43 (12 years ago) parent1dec451df9c178
7 files changed+21−13
compare with master
unifiedsplit
docs/README.md+7−1 docs/effects/simpleeff.rst+1−2 docs/index.rst+1−1 docs/tutorial/interp.rst+2−1 docs/tutorial/modules.rst+4−2 docs/tutorial/starting.rst+1−1 docs/tutorial/typesfuns.rst+5−5
docs/README.md+7−1
@@ -10,7 +10,13 @@ To build the manual the following dependencies must be met. We assume that you h
1010### Sphinx-Doc
1111
1212Python should be installed by default on most systems.
13−Sphinx can be installed wither through your hosts package manager or using pip/easy_install.
13+Sphinx can be installed either through your hosts package manager or using pip/easy_install.
14+
15+*Note* [ReadTheDocs](http://www.readthedocs.org) works with Sphinx
16+ `v1.2.2`. If you install a more recent version of sphinx then
17+ 'incorrectly' marked up documentation may get passed the build system
18+ of readthedocs and be ignored. In the past we had several code-blocks
19+ disappear because of that.
1420
1521### LaTeX
1622
docs/effects/simpleeff.rst+1−2
@@ -274,8 +274,7 @@ correct:
274274
275275 guess : Int -> { [STDIO] } Eff ()
276276
277−For reference, the code for ``guess`` is given in Listing
278−:ref:`eff-game`.
277+For reference, the code for ``guess`` is given below:
279278
280279.. _eff-game:
281280.. code-block:: idris
docs/index.rst+1−1
@@ -76,7 +76,7 @@ Learning Effects
7676 effects/conclusions
7777 effects/summary
7878
79−.. _proofs::
79+.. _proofs:
8080
8181###############
8282Theorem Proving
docs/tutorial/interp.rst+2−1
@@ -266,8 +266,9 @@ integer, giving 0 if the input is invalid. An example run of this
266266program at the Idris interactive environment is:
267267
268268
269+.. _factrun:
269270.. literalinclude:: ../listing/idris-prompt-interp.txt
270− :name: factrun
271+
271272
272273Aside: ``cast``
273274~~~~~~~~~~~~~~~
docs/tutorial/modules.rst+4−2
@@ -10,7 +10,7 @@ module, a list of ``import`` statements giving the other modules which
1010are to be imported, and a collection of declarations and definitions of
1111types, classes and functions. For example, the listing below gives a
1212module which defines a binary tree type ``BTree`` (in a file
13−``btree.idr``):;
13+``btree.idr``):
1414
1515.. code-block:: idris
1616
@@ -32,8 +32,9 @@ module which defines a binary tree type ``BTree`` (in a file
3232 toTree [] = Leaf
3333 toTree (x :: xs) = insert x (toTree xs)
3434
35+
3536Then, this gives a main program (in a file
36−``bmain.idr``) which uses the ``bst`` module to sort a list::
37+``bmain.idr``) which uses the ``bst`` module to sort a list:
3738
3839.. code-block:: idris
3940
@@ -45,6 +46,7 @@ Then, this gives a main program (in a file
4546 main = do let t = toTree [1,8,2,7,9,3]
4647 print (btree.toList t)
4748
49+
4850The same names can be defined in multiple modules. This is possible
4951because in practice names are *qualified* with the name of the module.
5052The names defined in the ``btree`` module are, in full:
docs/tutorial/starting.rst+1−1
@@ -86,5 +86,5 @@ checking a file, if successful, creates a bytecode version of the file
8686(in this case ``hello.ibc``) to speed up loading in future. The
8787bytecode is regenerated if the source file changes.
8888
89+.. _run1:
8990.. literalinclude:: ../listing/idris-prompt-helloworld.txt
90− :name: run1
docs/tutorial/typesfuns.rst+5−5
@@ -221,8 +221,8 @@ declaration for a function ``f`` *can* be omitted if:
221221
222222- ``f`` appears in the right hand side of the top level definition
223223
224−- The type of ``f`` can be completely determined from its first
225− application
224+- The type of ``f`` can be completely determined from its first application
225+
226226
227227So, for example, the following definitions are legal:
228228
@@ -948,10 +948,10 @@ analysis of intermediate expressions to avoid the need to write
948948auxiliary functions, and is also used internally to implement pattern
949949matching ``let`` and lambda bindings. It will *only* work if:
950950
951−- Each branch *matches* a value of the same type, and *returns* a value
952− of the same type.
951+- Each branch *matches* a value of the same type, and *returns* a
952+ value of the same type.
953953
954−- The type of the result is “known”. i.e. the type of the expression
954+- The type of the result is "known". i.e. the type of the expression
955955 can be determined *without* type checking the ``case``-expression
956956 itself.
957957