replace HTTP links with HTTPS

docs/make.bat

@@ -21,7 +21,7 @@ if errorlevel 9009 (
 	echo.may add the Sphinx directory to PATH.
 	echo.
 	echo.If you don't have Sphinx installed, grab it from
-	echo.http://sphinx-doc.org/
+	echo.https://www.sphinx-doc.org/
 	exit /b 1
 )
 

docs/source/faq/faq.rst

@@ -57,5 +57,5 @@ You can find more details in Section :ref:`updates-index`.
 Where can I find more answers?
 ==============================
 
-The `Idris 1 FAQ <http://docs.idris-lang.org/en/latest/faq/faq.html>`_ is
+The `Idris 1 FAQ <https://docs.idris-lang.org/en/latest/faq/faq.html>`_ is
 mostly still relevant.

docs/source/tutorial/conclusions.rst

@@ -10,7 +10,7 @@ dependent types in general, can be obtained from various sources:
 *  `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_
    by Edwin Brady, available from `Manning <https://www.manning.com>`_.
 
-*  The Idris web site (http://www.idris-lang.org/) and by asking
+*  The Idris web site (https://www.idris-lang.org/) and by asking
    questions on the mailing list.
 
 *  The IRC channel ``#idris``, on
@@ -30,7 +30,7 @@ dependent types in general, can be obtained from various sources:
 
 *  Existing projects on the ``Idris Hackers`` web space:
    
-   * http://idris-hackers.github.io.
+   * https://idris-hackers.github.io.
 
 *  Various papers (e.g. [#BradyHammond2012]_, [#Brady]_, and [#BradyHammond2010]_).  Although these mostly
    describe older versions of Idris.
@@ -41,14 +41,14 @@ dependent types in general, can be obtained from various sources:
        Aspects of Declarative Languages (PADL'12), Claudio Russo and
        Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,
        242-257. DOI=10.1007/978-3-642-27694-1_18
-       http://dx.doi.org/10.1007/978-3-642-27694-1_18
+       https://dx.doi.org/10.1007/978-3-642-27694-1_18
 
 .. [#Brady] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
        dependent types. In Proceedings of the 5th ACM workshop on
        Programming languages meets program verification (PLPV
        '11). ACM, New York, NY, USA,
        43-54. DOI=10.1145/1929529.1929536
-       http://doi.acm.org/10.1145/1929529.1929536
+       https://doi.acm.org/10.1145/1929529.1929536
 
 .. [#BradyHammond2010] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your
        inefficient engine: using partial evaluation to improve
@@ -56,4 +56,4 @@ dependent types in general, can be obtained from various sources:
        15th ACM SIGPLAN international conference on Functional
        programming (ICFP '10). ACM, New York, NY, USA,
        297-308. DOI=10.1145/1863543.1863587
-       http://doi.acm.org/10.1145/1863543.1863587
+       https://doi.acm.org/10.1145/1863543.1863587

docs/source/tutorial/interactive.rst

@@ -252,5 +252,5 @@ for other editors can be added in a relatively straightforward manner
 by using ``idris2 -–client``.
 More sophisticated support can be added by using the IDE protocol (yet to
 be documented for Idris 2, but which mostly extends to protocol documented for 
-`Idris 1 <http://docs.idris-lang.org/en/latest/reference/ide-protocol.html>`_.
+`Idris 1 <https://docs.idris-lang.org/en/latest/reference/ide-protocol.html>`_.
 

docs/source/tutorial/interfaces.rst

@@ -658,4 +658,4 @@ parameter used to find an implementation.
 .. [#ConorRoss] Conor McBride and Ross Paterson. 2008. Applicative programming
        with effects. J. Funct. Program. 18, 1 (January 2008),
        1-13. DOI=10.1017/S0956796807006326
-       http://dx.doi.org/10.1017/S0956796807006326
+       https://dx.doi.org/10.1017/S0956796807006326

docs/source/tutorial/introduction.rst

@@ -6,7 +6,7 @@ Introduction
 
 In conventional programming languages, there is a clear distinction
 between *types* and *values*. For example, in `Haskell
-<http://www.haskell.org>`_, the following are types, representing
+<https://www.haskell.org>`_, the following are types, representing
 integers, characters, lists of characters, and lists of any value
 respectively:
 
@@ -49,7 +49,7 @@ Intended Audience
 
 This tutorial is intended as a brief introduction to the language, and
 is aimed at readers already familiar with a functional language such
-as `Haskell <http://www.haskell.org>`_ or `OCaml <http://ocaml.org>`_.
+as `Haskell <https://www.haskell.org>`_ or `OCaml <https://ocaml.org>`_.
 In particular, a certain amount of familiarity with Haskell syntax is
 assumed, although most concepts will at least be explained
 briefly. The reader is also assumed to have some interest in using

docs/source/tutorial/miscellany.rst

@@ -136,7 +136,7 @@ But what about the type of ``Type``? If we ask Idris it reports:
     Type : Type 1
 
 If ``Type`` were its own type, it would lead to an inconsistency due to
-`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
+`Girard’s paradox <https://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
 so internally there is a *hierarchy* of types (or *universes*):
 
 .. code-block:: idris

docs/source/tutorial/theorems.rst

@@ -456,4 +456,4 @@ argument.
        control. In Proceedings of the 17th ACM SIGPLAN-SIGACT
        symposium on Principles of programming languages (POPL
        '90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714
-       http://doi.acm.org/10.1145/96709.96714
+       https://doi.acm.org/10.1145/96709.96714