From 7816c6c5e99fb652486abc5ea05ccc61a91000b5 Mon Sep 17 00:00:00 2001 From: Boyd Stephen Smith Jr Date: Mon, 25 May 2020 21:31:58 -0500 Subject: [PATCH 1/3] Fix formatting Someone had LaTeX on the brain instead of RST --- docs/source/app/exceptionsstate.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/app/exceptionsstate.rst b/docs/source/app/exceptionsstate.rst index d95bf0014..5525e46c5 100644 --- a/docs/source/app/exceptionsstate.rst +++ b/docs/source/app/exceptionsstate.rst @@ -64,7 +64,7 @@ and is not required at run-time, as explicitly stated in the types of These use an ``auto``-implicit to pass around a ``State`` with the relevant ``tag`` implicitly, so we refer to states by tag alone. In ``helloCount`` earlier, we used an empty type -\texttt{Counter} as the tag: +``Counter`` as the tag: .. code-block:: idris From 7e23c844a85d98295c9c6779401b37a6e06c1ebe Mon Sep 17 00:00:00 2001 From: Boyd Stephen Smith Jr Date: Mon, 25 May 2020 21:32:33 -0500 Subject: [PATCH 2/3] Mention `make install` README.md has that step, but this section of the documentation was missing it. --- docs/source/tutorial/starting.rst | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/docs/source/tutorial/starting.rst b/docs/source/tutorial/starting.rst index 2d7738227..cfcc871d1 100644 --- a/docs/source/tutorial/starting.rst +++ b/docs/source/tutorial/starting.rst @@ -40,9 +40,11 @@ follows:: make bootstrap-racket -This will, by default, install into ``${HOME}/.idris2``. You can change this -by editing the options in ``config.mk``. For example, -to install into ``/usr/local``, you can edit the ``PREFIX`` as follows:: +Once you've successfully bootstrapped with any of the above commands, you can +install with the command ``make install``. This will, by default, install into +``${HOME}/.idris2``. You can change this by editing the options in +``config.mk``. For example, to install into ``/usr/local``, you can edit the +``PREFIX`` as follows:: PREFIX ?= /usr/local From 38876800ca3bec9e9df5698a9a23024fea0f57af Mon Sep 17 00:00:00 2001 From: Boyd Stephen Smith Jr Date: Mon, 25 May 2020 21:35:23 -0500 Subject: [PATCH 3/3] Mention %access specifically (The first failure I got when trying to compile Idris 1.3.1 code with Idris2.) --- docs/source/updates/updates.rst | 3 +++ 1 file changed, 3 insertions(+) diff --git a/docs/source/updates/updates.rst b/docs/source/updates/updates.rst index 57beebad5..c55ffb3db 100644 --- a/docs/source/updates/updates.rst +++ b/docs/source/updates/updates.rst @@ -334,6 +334,9 @@ There are several ``%language`` pragmas in Idris 1, which define various experimental extensions. None of these are available in Idris 2, although extensions may be defined in the future. +Also removed was the ``%access`` pragma for default visibility, use visibility +modifiers on each declaration instead. + ``let`` bindings ----------------