From 43c5075f6e032e00b837982cdf07acbab5b74f3d Mon Sep 17 00:00:00 2001 From: Jan de Muijnck-Hughes Date: Sat, 23 May 2020 19:57:50 +0100 Subject: [PATCH 1/2] Use reST directives to make warnings and TODOs explicit in the documentation. --- docs/source/reference/envvars.rst | 4 +++- docs/source/tutorial/miscellany.rst | 10 ++++++---- docs/source/tutorial/theorems.rst | 6 ++++-- docs/source/tutorial/views.rst | 4 +++- docs/source/typedd/typedd.rst | 4 +++- docs/source/updates/updates.rst | 7 +++++-- 6 files changed, 24 insertions(+), 11 deletions(-) diff --git a/docs/source/reference/envvars.rst b/docs/source/reference/envvars.rst index a044b1d0b..582b9447e 100644 --- a/docs/source/reference/envvars.rst +++ b/docs/source/reference/envvars.rst @@ -4,4 +4,6 @@ Environment Variables ********************* -[TODO: Fill in the environment variables recognised by Idris 2] +.. todo:: + + Fill in the environment variables recognised by Idris 2 diff --git a/docs/source/tutorial/miscellany.rst b/docs/source/tutorial/miscellany.rst index bd1d65bd9..2f8aba3e9 100644 --- a/docs/source/tutorial/miscellany.rst +++ b/docs/source/tutorial/miscellany.rst @@ -81,9 +81,9 @@ number as 0), we could write: .. code-block:: idris - fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat - fibonacci {lag} Z = lag - fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n + fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat + fibonacci {lag} Z = lag + fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``, and will return the 5th fibonacci number. Note that while this works, this is not the @@ -114,7 +114,9 @@ any other character). Cumulativity ============ -[NOT YET IN IDRIS 2] +.. warning:: + + NOT YET IN IDRIS 2 Since values can appear in types and *vice versa*, it is natural that types themselves have types. For example: diff --git a/docs/source/tutorial/theorems.rst b/docs/source/tutorial/theorems.rst index e5a11e637..268ec6192 100644 --- a/docs/source/tutorial/theorems.rst +++ b/docs/source/tutorial/theorems.rst @@ -126,7 +126,7 @@ To see more detail on what's going on, we can replace the recursive call to ``plusReducesZ`` with a hole: .. code-block:: idris - + plusReducesZ (S k) = cong S ?help Then inspecting the type of the hole at the REPL shows us: @@ -361,7 +361,9 @@ total, a function ``f`` must: Directives and Compiler Flags for Totality ------------------------------------------ -[NOTE: Not all of this is implemented yet for Idris 2] +.. warning:: + + Not all of this is implemented yet for Idris 2 By default, Idris allows all well-typed definitions, whether total or not. However, it is desirable for functions to be total as far as possible, as this diff --git a/docs/source/tutorial/views.rst b/docs/source/tutorial/views.rst index a9fe7fc57..4840050cf 100644 --- a/docs/source/tutorial/views.rst +++ b/docs/source/tutorial/views.rst @@ -4,7 +4,9 @@ Views and the “``with``” rule ***************************** -[NOT UPDATED FOR IDRIS 2 YET] +.. warning:: + + NOT UPDATED FOR IDRIS 2 YET Dependent pattern matching ========================== diff --git a/docs/source/typedd/typedd.rst b/docs/source/typedd/typedd.rst index 905d72f63..bd966c7ae 100644 --- a/docs/source/typedd/typedd.rst +++ b/docs/source/typedd/typedd.rst @@ -453,4 +453,6 @@ In ``ATM.idr``, add: Chapter 15 ---------- -TODO +.. todo:: + + This chapter. diff --git a/docs/source/updates/updates.rst b/docs/source/updates/updates.rst index 1a7d1a4c1..815217a36 100644 --- a/docs/source/updates/updates.rst +++ b/docs/source/updates/updates.rst @@ -428,8 +428,11 @@ used with care. Too many hints can lead to a large search space! Totality and Coverage --------------------- -``%default covering`` is now the default status [Actually still TODO, but -planned soon!] +``%default covering`` is now the default statusk + +.. note:: + + Actually still TODO, but planned soon! Build artefacts --------------- From 3e810b1de73e8c16858849c5996ccb4263508467 Mon Sep 17 00:00:00 2001 From: Jan de Muijnck-Hughes Date: Sat, 23 May 2020 20:03:36 +0100 Subject: [PATCH 2/2] Add venv for rtd docs to .gitignore. --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 53c2314e3..2eedd56ad 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ +idris2docs_venv *~ *.ibc *.ttc