use HTTPS URL instead of HTTP URL when possible

Author: MilanKral

Diff for: CITATION.md

@@ -17,7 +17,7 @@ If you use `Idris` in your work we would prefer it if you would use the followin
   pages = {552--593},
   numpages = {42},
   doi = {10.1017/S095679681300018X},
-  URL = {http://journals.cambridge.org/article_S095679681300018X},
+  URL = {https://journals.cambridge.org/article_S095679681300018X},
 }
 ```
 

Diff for: CONTRIBUTING.md

@@ -6,9 +6,9 @@ Here are a few guidelines that we would like contributors to follow so that we c
 
 ## Getting Started
 
-1. Make sure you are familiar with [Git](http://git-scm.com/book).
+1. Make sure you are familiar with [Git](https://git-scm.com/book).
 1. Make sure you have a [GitHub account](https://github.com/signup/free).
-1. Make sure you are familiar with: [Idris](http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf).
+1. Make sure you are familiar with: [Idris](https://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf).
 1. Make sure you can install Idris:
   * [Mac OS X](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-OS-X-using-Homebrew)
   * [Ubuntu](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Ubuntu)
@@ -72,7 +72,7 @@ We do not want you wasting your time nor duplicating somebody's work!
 
 ## Making Changes
 
-Idris developers and hackers try to adhere to something similar to the [successful git branching model](http://nvie.com/posts/a-successful-git-branching-model/).
+Idris developers and hackers try to adhere to something similar to the [successful git branching model](https://nvie.com/posts/a-successful-git-branching-model/).
 The steps are described below.
 
 ### New contributors
@@ -175,8 +175,8 @@ To help increase the chance of your pull request being accepted:
 * Idris FAQs: [Official](https://idris.readthedocs.io/en/latest/faq/faq.html); [Unofficial](https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ);
 * [Idris Manual](https://github.com/idris-lang/Idris-dev/wiki/Manual);
 * [Idris Tutorial](https://idris.readthedocs.io/en/latest/tutorial/index.html);
-* [Idris News](http://www.idris-lang.org/news/);
-* [other Idris docs](http://www.idris-lang.org/documentation/).
+* [Idris News](https://www.idris-lang.org/news/);
+* [other Idris docs](https://www.idris-lang.org/documentation/).
 * [Using Pull Requests](https://help.github.com/articles/using-pull-requests)
 * [General GitHub Documentation](https://help.github.com/).
 

Diff for: Makefile

@@ -56,7 +56,7 @@ linecount:
 
 #Note: this doesn't yet link to Hackage properly
 doc: dist/setup-config
-	$(CABAL) haddock --hyperlink-source --html --hoogle --html-location="http://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"
+	$(CABAL) haddock --hyperlink-source --html --hoogle --html-location="https://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"
 
 lib_doc:
 	$(MAKE) -C libs IDRIS=../../dist/build/idris/idris doc

Diff for: README.md

@@ -4,11 +4,11 @@
 [![Appveyor build](https://ci.appveyor.com/api/projects/status/xi8yu81oy1134g7o/branch/master?svg=true)](https://ci.appveyor.com/project/idrislang/idris-dev)
 [![Documentation Status](https://readthedocs.org/projects/idris/badge/?version=latest)](https://readthedocs.org/projects/idris/?badge=latest)
 [![Hackage](https://img.shields.io/hackage/v/idris.svg)](https://hackage.haskell.org/package/idris)
-[![Stackage LTS](http://stackage.org/package/idris/badge/lts)](http://stackage.org/lts/package/idris)
-[![Stackage Nightly](http://stackage.org/package/idris/badge/nightly)](http://stackage.org/nightly/package/idris)
+[![Stackage LTS](https://stackage.org/package/idris/badge/lts)](https://stackage.org/lts/package/idris)
+[![Stackage Nightly](https://stackage.org/package/idris/badge/nightly)](https://stackage.org/nightly/package/idris)
 [![IRC](https://img.shields.io/badge/IRC-%23idris-1e72ff.svg?style=flat)](https://www.irccloud.com/invite?channel=%23idris&hostname=irc.freenode.net&port=6697&ssl=1)
 
-Idris (http://idris-lang.org/) is a general-purpose functional programming
+Idris (https://idris-lang.org/) is a general-purpose functional programming
 language with dependent types.
 
 ## Installation Guides.
@@ -28,7 +28,7 @@ Idris has support for external code generators. Supplied with the distribution
 is a C code generator to compile executables, and a JavaScript code generator
 with support for node.js and browser JavaScript.
 
-More information about [code generators can be found on the wiki](http://idris.readthedocs.io/en/latest/reference/codegen.html).
+More information about [code generators can be found on the wiki](https://idris.readthedocs.io/en/latest/reference/codegen.html).
 
 ## More Information
 

Diff for: appveyor.yml

@@ -5,7 +5,7 @@ init:
 
     mkdir C:\ghc
 
-    Invoke-WebRequest "http://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"
+    Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"
 
     7z x C:\ghc\ghc.tar.xz -oC:\ghc
 

Diff for: azure-pipelines.yml

@@ -68,7 +68,7 @@ jobs:
         choco install 7zip.portable -y --no-progress
         choco install msys2 -y --no-progress --params "/InstallDir=C:/msys64/"
         mkdir C:\ghc
-        Invoke-WebRequest "http://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"
+        Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"
         7z x C:\ghc\ghc.tar.xz -oC:\ghc
         7z x C:\ghc\ghc.tar -oC:\ghc
       displayName: "Setting up environment"

Diff for: benchmarks/pidigits/pidigits.idr

@@ -3,7 +3,7 @@ import Data.Vect
 
 {- Toy program that outputs the n first digits of Pi.
 
-   Inspired from http://www.haskell.org/haskellwiki/Shootout/Pidigits.
+   Inspired from https://www.haskell.org/haskellwiki/Shootout/Pidigits.
    The original ns and str lazy lists have been replaced by strict functions.
 
    Memory usage seems to be excessive. One of the branches of str is tail recursive, and

Diff for: docs/LICENSE

@@ -7,4 +7,4 @@ rights to Documentation for Idris.
 
 More information concerning the CC0 can be found online at:
 
-    http://creativecommons.org/publicdomain/zero/1.0/
+    https://creativecommons.org/publicdomain/zero/1.0/

Diff for: docs/Makefile

@@ -9,7 +9,7 @@ BUILDDIR      = _build
 
 # User-friendly check for sphinx-build
 ifeq ($(shell which $(SPHINXBUILD) >/dev/null 2>&1; echo $$?), 1)
-$(error The '$(SPHINXBUILD)' command was not found. Make sure you have Sphinx installed, then set the SPHINXBUILD environment variable to point to the full path of the '$(SPHINXBUILD)' executable. Alternatively you can add the directory with the executable to your PATH. If you don't have Sphinx installed, grab it from http://sphinx-doc.org/)
+$(error The '$(SPHINXBUILD)' command was not found. Make sure you have Sphinx installed, then set the SPHINXBUILD environment variable to point to the full path of the '$(SPHINXBUILD)' executable. Alternatively you can add the directory with the executable to your PATH. If you don't have Sphinx installed, grab it from https://www.sphinx-doc.org/)
 endif
 
 # Internal variables.

Diff for: docs/README.md

@@ -1,7 +1,7 @@
 # Documentation for the Idris Language.
 
 
-This manual has been prepared using ReStructured Text and the [Sphinx Documentation Generator](http://sphinx-doc.org) for future inclusion on [Read The Docs](http://www.readthedocs.org).
+This manual has been prepared using ReStructured Text and the [Sphinx Documentation Generator](https://www.sphinx-doc.org) for future inclusion on [Read The Docs](https://www.readthedocs.org).
 
 ## Dependencies
 
@@ -12,7 +12,7 @@ To build the manual the following dependencies must be met. We assume that you h
 Python should be installed by default on most systems.
 Sphinx can be installed either through your hosts package manager or using pip/easy_install.
 
-*Note* [ReadTheDocs](http://www.readthedocs.org) works with Sphinx
+*Note* [ReadTheDocs](https://www.readthedocs.org) works with Sphinx
  `v1.2.2`. If you install a more recent version of sphinx then
  'incorrectly' marked up documentation may get passed the build system
  of readthedocs and be ignored. In the past we had several code-blocks
@@ -45,7 +45,7 @@ rights to Documentation for Idris.
 
 More information concerning the CC0 can be found online at:
 
-    http://creativecommons.org/publicdomain/zero/1.0/
+    https://creativecommons.org/publicdomain/zero/1.0/
 
 
 When contributing material to the manual please bear in mind that the work will be licensed as above.

Diff for: docs/effects/conclusions.rst

@@ -51,7 +51,7 @@ foundations are also well-studied see [5]_, [6]_, [7]_, [8]_.
        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://link.springer.com/chapter/10.1007%2F978-3-642-10672-9_9
+       https://link.springer.com/chapter/10.1007%2F978-3-642-10672-9_9
 
 
 .. [4] Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in

Diff for: docs/effects/index.rst

@@ -25,7 +25,7 @@ A tutorial on the `Effects` package in `Idris`.
    Idris Community* has waived all copyright and related or neighbouring
    rights to Documentation for Idris.
 
-   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+   More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
 
 .. toctree::
    :maxdepth: 1

Diff for: docs/effects/introduction.rst

@@ -3,7 +3,7 @@ Introduction
 ************
 
 Pure functional languages with dependent types such as `Idris
-<http://www.idris-lang.org/>`_ support reasoning about programs directly
+<https://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:

Diff for: docs/faq/faq.rst

@@ -37,7 +37,7 @@ Is there some documentation for the standard lib? List of functions?
 =====================================================================
 
 API documentation for the shipped packages is listed on `the
-documentation page <http://www.idris-lang.org/documentation/>`_.
+documentation page <https://www.idris-lang.org/documentation/>`_.
 
 Unfortunately, the default prelude and shipped packages for `Idris`
 are not necessarily complete with regards to documentation.  Other
@@ -310,7 +310,7 @@ better and it will make sense to revisit this. For now, however, Idris will not
 be offering arbitrary Unicode symbols in operators.
 
 This seems like an instance of `Wadler's
-Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
+Law <https://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
 
 This answer is based on Edwin Brady's response in the following
 `pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`_.

Diff for: docs/guides/index.rst

@@ -12,7 +12,7 @@ Tutorials submitted by community members.
    Idris Community* has waived all copyright and related or neighboring
    rights to Documentation for Idris.
 
-   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+   More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
 
 
 .. toctree::

Diff for: docs/guides/theorem-prover.rst

@@ -22,7 +22,7 @@ We will be given the following prompt, in future releases the version string wil
          ____    __     _
         /  _/___/ /____(_)____
         / // __  / ___/ / ___/     Version 0.9.18.1
-      _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
+      _/ // /_/ / /  / (__  )      https://www.idris-lang.org/
      /___/\__,_/_/  /_/____/       Type :? for help
 
     Idris is free software with ABSOLUTELY NO WARRANTY.

Diff for: docs/guides/type-providers-ffi.rst

@@ -3,7 +3,7 @@ Type Providers in Idris
 ***********************
 
 `Type providers in Idris
-<http://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`__
+<https://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`__
 are simple enough, but there are a few caveats to using them that it
 would be worthwhile to go through the basic steps. We also go over
 foreign functions, because these will often be used with type

Diff for: docs/index.rst

@@ -13,7 +13,7 @@ Documentation for the Idris Language
    Idris Community* has waived all copyright and related or neighboring
    rights to Documentation for Idris.
 
-   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+   More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
 
 
 .. toctree::

Diff for: docs/listing/idris-prompt-helloworld.txt

@@ -2,7 +2,7 @@ $ idris hello.idr
      ____    __     _
     /  _/___/ /____(_)____
     / // __  / ___/ / ___/     Version 1.3.2
-  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
+  _/ // /_/ / /  / (__  )      https://www.idris-lang.org/
  /___/\__,_/_/  /_/____/       Type :? for help
 
 Type checking ./hello.idr

Diff for: docs/listing/idris-prompt-interp.txt

@@ -2,7 +2,7 @@ $ idris interp.idr
      ____    __     _
     /  _/___/ /____(_)____
     / // __  / ___/ / ___/     Version 1.3.2
-  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
+  _/ // /_/ / /  / (__  )      https://www.idris-lang.org/
  /___/\__,_/_/  /_/____/       Type :? for help
 
 Type checking ./interp.idr

Diff for: docs/listing/idris-prompt-start.txt

@@ -2,7 +2,7 @@ $ idris
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 1.3.2
- _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
+ _/ // /_/ / /  / (__  )      https://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help
 
 Idris>

Diff for: docs/make.bat

@@ -65,7 +65,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 for: docs/proofs/index.rst

@@ -13,7 +13,7 @@ A tutorial on theorem proving in Idris.
    Idris Community* has waived all copyright and related or neighboring
    rights to Documentation for Idris.
 
-   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+   More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
 
 .. toctree::
    :maxdepth: 1

Diff for: docs/proofs/interactive.rst

@@ -129,7 +129,7 @@ On running , two global names are created, ``plusredZ_Z`` and
 
     .  /  _/___/ /____(_)____
        / // __  / ___/ / ___/     Version 1.2.0
-     _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
+     _/ // /_/ / /  / (__  )      https://www.idris-lang.org/
     /___/\__,_/_/  /_/____/       Type :? for help
 
     Idris is free software with ABSOLUTELY NO WARRANTY.

Diff for: docs/reference/erasure.rst

@@ -254,7 +254,7 @@ Benchmarks
 ==========
 
 -  source: https://github.com/ziman/idris-benchmarks
--  results: http://ziman.functor.sk/erasure-bm/
+-  results: https://ziman.functor.sk/erasure-bm/
 
 It can be clearly seen that asymptotics are improved by erasure.
 
@@ -499,4 +499,4 @@ References
 
 .. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive
            families need not store their indices
-           <http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849>`__
+           <https://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849>`__

Diff for: docs/reference/index.rst

@@ -14,7 +14,7 @@ This will tell you how Idris works, for using it you should read the Idris Tutor
    Idris Community* has waived all copyright and related or neighboring
    rights to Documentation for Idris.
 
-   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+   More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
 
 
 .. toctree::

Diff for: docs/reference/language-extensions.rst

@@ -9,7 +9,7 @@ Type Providers
 
 Idris type providers are a way to get the type system to reflect
 observations about the world outside of Idris. Similarly to `F# type
-providers <http://msdn.microsoft.com/en-us/library/vstudio/hh156509.aspx>`__,
+providers <https://msdn.microsoft.com/en-us/library/vstudio/hh156509.aspx>`__,
 they cause effectful computations to run during type checking, returning
 information that the type checker can use when checking the rest of the
 program. While F# type providers are based on code generation, Idris
@@ -32,5 +32,5 @@ to the user.
 Example Idris type providers can be seen at `this
 repository <https://github.com/david-christiansen/idris-type-providers>`__.
 More detailed descriptions are available in David Christiansen's `WGP
-'13 paper <http://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
+'13 paper <https://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
 thesis <http://itu.dk/people/drc/david-christiansen-thesis.pdf>`__.

Diff for: docs/reference/partial-evaluation.rst

@@ -8,7 +8,7 @@ of functions with arguments annotated as ``%static``.
 
 (This is an implementation of the partial evaluator described in `this
 ICFP 2010
-paper <http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
+paper <https://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
 Please refer to this for more precise definitions of what follows.)
 
 Partial evaluation is switched off by default since Idris 1.0. It can
@@ -207,7 +207,7 @@ Specialising Interpreters
 A particularly useful situation where partial evaluation becomes
 effective is in defining an interpreter for a well-typed expression
 language, defined as follows (see the `Idris tutorial, section
-4 <http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf>`__
+4 <https://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf>`__
 for more details on how this works):
 
 ::

Diff for: docs/reference/type-directed-search.rst

@@ -4,7 +4,7 @@ Type Directed Search ``:search``
 
 Idris' ``:search`` command searches for terms according to their
 approximate type signature (much like
-`Hoogle <http://www.haskell.org/hoogle/>`__ for Haskell). For
+`Hoogle <https://www.haskell.org/hoogle/>`__ for Haskell). For
 example::
 
     Idris> :search e -> List e -> List e

Diff for: docs/reference/uniqueness-types.rst

@@ -13,7 +13,7 @@ ideally while giving up as little high level conveniences as possible.
 
 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
+<https://wiki.clean.cs.ru.nl/Clean>`__ programming language, and
 ownership types and borrowed pointers in the `Rust
 <https://www.rust-lang.org/>`__ programming language.
 

Diff for: docs/st/index.rst

@@ -14,7 +14,7 @@ the `Control.ST` library in `Idris`.
    Idris Community* has waived all copyright and related or neighbouring
    rights to Documentation for Idris.
 
-   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+   More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
 
 .. toctree::
    :maxdepth: 1

Diff for: docs/st/introduction.rst

@@ -3,7 +3,7 @@ Overview
 ********
 
 Pure functional languages with dependent types such as `Idris
-<http://www.idris-lang.org/>`_ support reasoning about programs directly
+<https://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.