From 9f78f1cddcfaf2365135ac20c0a3e8c788e7768a Mon Sep 17 00:00:00 2001 From: Milan Kral Date: Wed, 27 May 2020 14:50:05 +0200 Subject: [PATCH] replace HTTP links with HTTPS --- docs/make.bat | 2 +- docs/source/faq/faq.rst | 2 +- docs/source/tutorial/conclusions.rst | 10 +++++----- docs/source/tutorial/interactive.rst | 2 +- docs/source/tutorial/interfaces.rst | 2 +- docs/source/tutorial/introduction.rst | 4 ++-- docs/source/tutorial/miscellany.rst | 2 +- docs/source/tutorial/theorems.rst | 2 +- 8 files changed, 13 insertions(+), 13 deletions(-) diff --git a/docs/make.bat b/docs/make.bat index 6247f7e23..6fcf05b4b 100644 --- a/docs/make.bat +++ b/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 ) diff --git a/docs/source/faq/faq.rst b/docs/source/faq/faq.rst index 74ee20529..82fab0b41 100644 --- a/docs/source/faq/faq.rst +++ b/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 `_ is +The `Idris 1 FAQ `_ is mostly still relevant. diff --git a/docs/source/tutorial/conclusions.rst b/docs/source/tutorial/conclusions.rst index 3157f3844..4d60f022d 100644 --- a/docs/source/tutorial/conclusions.rst +++ b/docs/source/tutorial/conclusions.rst @@ -10,7 +10,7 @@ dependent types in general, can be obtained from various sources: * `Type-Driven Development with Idris `_ by Edwin Brady, available from `Manning `_. -* 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 diff --git a/docs/source/tutorial/interactive.rst b/docs/source/tutorial/interactive.rst index 62a7bb379..f535feae0 100644 --- a/docs/source/tutorial/interactive.rst +++ b/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 `_. +`Idris 1 `_. diff --git a/docs/source/tutorial/interfaces.rst b/docs/source/tutorial/interfaces.rst index 70e57f15c..13601a9ae 100644 --- a/docs/source/tutorial/interfaces.rst +++ b/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 diff --git a/docs/source/tutorial/introduction.rst b/docs/source/tutorial/introduction.rst index 904cc91b3..403b05c96 100644 --- a/docs/source/tutorial/introduction.rst +++ b/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 -`_, the following are types, representing +`_, 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 `_ or `OCaml `_. +as `Haskell `_ or `OCaml `_. 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 diff --git a/docs/source/tutorial/miscellany.rst b/docs/source/tutorial/miscellany.rst index 2f8aba3e9..c0f45d67f 100644 --- a/docs/source/tutorial/miscellany.rst +++ b/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 `_, +`Girard’s paradox `_, so internally there is a *hierarchy* of types (or *universes*): .. code-block:: idris diff --git a/docs/source/tutorial/theorems.rst b/docs/source/tutorial/theorems.rst index 268ec6192..ebf0599d8 100644 --- a/docs/source/tutorial/theorems.rst +++ b/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