Fix links

docs/effects/conclusions.rst

@@ -13,17 +13,17 @@ paper [1]_.
 Some libraries and programs which use ``Effects`` can be found in the
 following places:
 
--  http://github.com/edwinb/SDL-idris — some bindings for the SDL media
+-  https://github.com/edwinb/SDL-idris — some bindings for the SDL media
    library, supporting graphics in particular.
 
--  http://github.com/edwinb/idris-demos — various demonstration
+-  https://github.com/edwinb/idris-demos — various demonstration
    programs, including several examples from this tutorial, and a “Space
    Invaders” game.
 
 -  https://github.com/SimonJF/IdrisNet2 — networking and socket
    libraries.
 
--  http://github.com/edwinb/Protocols — a high level communication
+-  https://github.com/edwinb/Protocols — a high level communication
    protocol description language.
 
 The inspiration for the ``Effects`` library was Bauer and Pretnar’s
@@ -37,32 +37,32 @@ foundations are also well-studied see [5]_, [6]_, [7]_, [8]_.
 .. [1] Edwin Brady. 2013. Programming and reasoning with algebraic
        effects and dependent types. SIGPLAN Not. 48, 9 (September
        2013), 133-144. DOI=10.1145/2544174.2500581
-       http://doi.acm.org/10.1145/2544174.2500581
+       https://dl.acm.org/citation.cfm?doid=2544174.2500581
 
 .. [2] Andrej Bauer, Matija Pretnar, Programming with algebraic
        effects and handlers, Journal of Logical and Algebraic Methods
        in Programming, Volume 84, Issue 1, January 2015, Pages
        108-123, ISSN 2352-2208,
-       http://dx.doi.org/10.1016/j.jlamp.2014.02.001.
-       (http://www.sciencedirect.com/science/article/pii/S2352220814000194)
+       http://math.andrej.com/wp-content/uploads/2012/03/eff.pdf
+
 
 .. [3] Ben Lippmeier. 2009. Witnessing Purity, Constancy and
        Mutability. In Proceedings of the 7th Asian Symposium on
        Programming Languages and Systems (APLAS '09), Zhenjiang Hu
        (Ed.). Springer-Verlag, Berlin, Heidelberg,
        95-110. DOI=10.1007/978-3-642-10672-9_9
-       http://dx.doi.org/10.1007/978-3-642-10672-9_9
+       http://link.springer.com/chapter/10.1007%2F978-3-642-10672-9_9
+
 
 .. [4] Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in
        action. SIGPLAN Not. 48, 9 (September 2013),
        145-158. DOI=10.1145/2544174.2500590
-       http://doi.acm.org/10.1145/2544174.2500590
+       https://dl.acm.org/citation.cfm?doid=2544174.2500590
 
 .. [5] Martin Hyland, Gordon Plotkin, John Power, Combining effects:
        Sum and tensor, Theoretical Computer Science, Volume 357,
        Issues 1–3, 25 July 2006, Pages 70-99, ISSN 0304-3975,
-       http://dx.doi.org/10.1016/j.tcs.2006.03.013.
-       (http://www.sciencedirect.com/science/article/pii/S0304397506002659)
+       (https://www.sciencedirect.com/science/article/pii/S0304397506002659)
 
 .. [6] Paul Blain Levy. 2004. Call-By-Push-Value: A
        Functional/Imperative Synthesis (Semantics Structures in

docs/effects/introduction.rst

@@ -3,7 +3,7 @@ Introduction
 ************
 
 Pure functional languages with dependent types such as `Idris
-<http://idris-lang.org/>`_ support reasoning about programs directly
+<http://www.idris-lang.org/>`_ support reasoning about programs directly
 in the type system, promising that we can *know* a program will run
 correctly (i.e. according to the specification in its type) simply
 because it compiles. Realistically, though, things are not so simple:

docs/effects/state.rst

@@ -83,7 +83,7 @@ effectful program ``f`` has a type of the following form:
 
 .. code-block:: idris
 
-    f : (x1 : a1) -> (x2 : a2) -> ... -> Eff t effs 
+    f : (x1 : a1) -> (x2 : a2) -> ... -> Eff t effs
 
 That is, the return type gives the effects that ``f`` supports
 (``effs``, of type ``List EFFECT``) and the type the computation
@@ -419,7 +419,7 @@ underlying type ``EffM``:
 
     EffM : (m : Type -> Type) -> (t : Type)
             -> (List EFFECT)
-            -> (t -> List EFFECT) -> Type 
+            -> (t -> List EFFECT) -> Type
 
 This is more general than the types we have been writing so far. It is
 parameterised over an underying computation context ``m``, a
@@ -443,15 +443,15 @@ operations which can change the set of available effects are:
   possible.
 
 While powerful, this can make uses of the ``EffM`` type hard to read.
-Therefore the library provides an overloaded function ``Eff`` 
+Therefore the library provides an overloaded function ``Eff``
 There are the following three versions:
 
 .. code-block:: idris
 
     SimpleEff.Eff : (t : Type) -> (input_effs : List EFFECT) -> Type
-    TransEff.Eff  : (t : Type) -> (input_effs : List EFFECT) -> 
+    TransEff.Eff  : (t : Type) -> (input_effs : List EFFECT) ->
                                   (output_effs : List EFFECT) -> Type
-    DepEff.Eff    : (t : Type) -> (input_effs : List EFFECT) -> 
+    DepEff.Eff    : (t : Type) -> (input_effs : List EFFECT) ->
                                   (output_effs_fn : x -> List EFFECT) -> Type
 
 So far, we have used only the first version, ``SimpleEff.Eff``, which
@@ -521,7 +521,9 @@ the ``new`` function, though this is beyond the scope of this tutorial.
 .. [3] Edwin Brady. 2013. Programming and reasoning with algebraic
        effects and dependent types. SIGPLAN Not. 48, 9 (September
        2013), 133-144. DOI=10.1145/2544174.2500581
-       http://doi.acm.org/10.1145/2544174.2500581
+       http://dl.acm.org/citation.cfm?doid=2544174.2500581
+
+
 
 .. |image| image:: ../image/effects-tree.png
                    :width: 500px

docs/faq/faq.rst

@@ -150,7 +150,7 @@ names ``Float`` and ``Double`` to represent floating point numbers of
 size 32 and 64 respectivly.  Newer languages such as Rust and Julia
 have begun to follow the naming scheme described in `IEE Standard for
 Floating-Point Arithmetic (IEEE 754)
-<http://en.wikipedia.org/wiki/IEEE_floating_point>`_. This describes
+<https://en.wikipedia.org/wiki/IEEE_floating_point>`_. This describes
 single and double precision numbers as ``Float32`` and ``Float64``;
 the size is described in the type name.
 

docs/reference/erasure.rst

@@ -29,7 +29,7 @@ and we can use irrelevance-related methods to achieve erasure.
 However, sometimes we want to erase *indices* and this is where the
 traditional approaches stop being useful, mainly for reasons described
 in the `original proposal
-<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations#prop-is-cumbersome-coq>`__.
+<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations>`__.
 
 .. code-block:: idris
 

docs/reference/uniqueness-types.rst

@@ -15,7 +15,7 @@ They are inspired by linear types, `Uniqueness Types
 <https://en.wikipedia.org/wiki/Uniqueness_type>`__ in the `Clean
 <http://wiki.clean.cs.ru.nl/Clean>`__ programming language, and
 ownership types and borrowed pointers in the `Rust
-<http://www.rust-lang.org/>`__ programming language.
+<https://www.rust-lang.org/>`__ programming language.
 
 Some things we hope to be able to do eventually with uniqueness types
 include:

docs/tutorial/conclusions.rst

@@ -7,7 +7,7 @@ Further Reading
 Further information about Idris programming, and programming with
 dependent types in general, can be obtained from various sources:
 
--  The Idris web site (http://idris-lang.org/) and by asking
+-  The Idris web site (http://www.idris-lang.org/) and by asking
    questions on the mailing list.
 
 -  The IRC channel ``#idris``, on

docs/tutorial/interactive.rst

@@ -20,7 +20,7 @@ hole, and even a basic proof search mechanism. In this
 section, we explain how these features can be exploited by a text
 editor, and specifically how to do so in `Vim
 <https://github.com/idris-hackers/idris-vim>`_. An interactive mode
-for `Emacs <https://github.com/idris-hackers/idris-emacs>`_ is also
+for `Emacs <https://github.com/idris-hackers/idris-mode>`_ is also
 available.
 
 

docs/tutorial/testing.rst

@@ -23,8 +23,8 @@ does not aggregate test results.
 
 For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.
 
+.. name: Math/NumOps.idr
 .. code-block:: idris
-   :caption: Math/NumOps.idr
 
     module Maths.NumOps
 
@@ -36,8 +36,8 @@ For example, lets take the following list of functions that are defined in a mod
 
 A simple test module, with a qualified name of ``Test.NumOps`` can be declared as
 
+.. name: Math/TestOps.idr
 .. code-block:: idris
-   :caption: Math/TestOps.idr
 
     module Test.NumOps