diff --git a/CITATION.md b/CITATION.md
index 61b29049d..9331dbc84 100644
--- a/CITATION.md
+++ b/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 --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 71fd267ee..237c3da41 100644
--- a/CONTRIBUTING.md
+++ b/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 --git a/Makefile b/Makefile
index 974e3d7d0..2d269abeb 100644
--- a/Makefile
+++ b/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 --git a/README.md b/README.md
index 8878328f3..d0759fc5b 100644
--- a/README.md
+++ b/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 --git a/appveyor.yml b/appveyor.yml
index 96220f7f6..2c1d6bd49 100644
--- a/appveyor.yml
+++ b/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 --git a/azure-pipelines.yml b/azure-pipelines.yml
index 6f82f755b..243f45625 100644
--- a/azure-pipelines.yml
+++ b/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 --git a/benchmarks/pidigits/pidigits.idr b/benchmarks/pidigits/pidigits.idr
index 97cbbdd61..167982ca5 100644
--- a/benchmarks/pidigits/pidigits.idr
+++ b/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 --git a/docs/LICENSE b/docs/LICENSE
index d1580a419..897ab8f97 100644
--- a/docs/LICENSE
+++ b/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 --git a/docs/Makefile b/docs/Makefile
index 21b2726bd..9baab9d92 100644
--- a/docs/Makefile
+++ b/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 --git a/docs/README.md b/docs/README.md
index 15511d3af..bdce2e24c 100644
--- a/docs/README.md
+++ b/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 --git a/docs/effects/conclusions.rst b/docs/effects/conclusions.rst
index 7018c9387..c167b416a 100644
--- a/docs/effects/conclusions.rst
+++ b/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 --git a/docs/effects/index.rst b/docs/effects/index.rst
index a7c2ed695..921fb9458 100644
--- a/docs/effects/index.rst
+++ b/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 --git a/docs/effects/introduction.rst b/docs/effects/introduction.rst
index ec3b481dd..3b09eff9c 100644
--- a/docs/effects/introduction.rst
+++ b/docs/effects/introduction.rst
@@ -3,7 +3,7 @@ Introduction
************
Pure functional languages with dependent types such as `Idris
-`_ support reasoning about programs directly
+`_ 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 --git a/docs/faq/faq.rst b/docs/faq/faq.rst
index 916415bc8..b1e9d00a5 100644
--- a/docs/faq/faq.rst
+++ b/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 `_.
+documentation page `_.
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 `__ in action.
+Law `__ in action.
This answer is based on Edwin Brady's response in the following
`pull request `_.
diff --git a/docs/guides/index.rst b/docs/guides/index.rst
index 22a654a4b..12ff25d10 100644
--- a/docs/guides/index.rst
+++ b/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 --git a/docs/guides/theorem-prover.rst b/docs/guides/theorem-prover.rst
index ba35ac347..5fe0e6795 100644
--- a/docs/guides/theorem-prover.rst
+++ b/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 --git a/docs/guides/type-providers-ffi.rst b/docs/guides/type-providers-ffi.rst
index 21b9702de..655622451 100644
--- a/docs/guides/type-providers-ffi.rst
+++ b/docs/guides/type-providers-ffi.rst
@@ -3,7 +3,7 @@ Type Providers in Idris
***********************
`Type providers in Idris
-`__
+`__
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 --git a/docs/index.rst b/docs/index.rst
index 9bccefc68..0453e10de 100644
--- a/docs/index.rst
+++ b/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 --git a/docs/listing/idris-prompt-helloworld.txt b/docs/listing/idris-prompt-helloworld.txt
index 2e3b241f9..43f6ba396 100644
--- a/docs/listing/idris-prompt-helloworld.txt
+++ b/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 --git a/docs/listing/idris-prompt-interp.txt b/docs/listing/idris-prompt-interp.txt
index aa82a8f10..e3760453c 100644
--- a/docs/listing/idris-prompt-interp.txt
+++ b/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 --git a/docs/listing/idris-prompt-start.txt b/docs/listing/idris-prompt-start.txt
index c40b86eed..43cbf530c 100644
--- a/docs/listing/idris-prompt-start.txt
+++ b/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 --git a/docs/make.bat b/docs/make.bat
index 566f3c82d..9c772a944 100644
--- a/docs/make.bat
+++ b/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 --git a/docs/proofs/index.rst b/docs/proofs/index.rst
index a4db17a47..2287275ab 100644
--- a/docs/proofs/index.rst
+++ b/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 --git a/docs/proofs/interactive.rst b/docs/proofs/interactive.rst
index 67c29bf47..aaadc0fe9 100644
--- a/docs/proofs/interactive.rst
+++ b/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 --git a/docs/reference/erasure.rst b/docs/reference/erasure.rst
index 275dfff12..7f44c5a74 100644
--- a/docs/reference/erasure.rst
+++ b/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
- `__
+ `__
diff --git a/docs/reference/index.rst b/docs/reference/index.rst
index b9dc2a71b..1c0e21d9a 100644
--- a/docs/reference/index.rst
+++ b/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 --git a/docs/reference/language-extensions.rst b/docs/reference/language-extensions.rst
index cfdf9a5c1..e4d6f8170 100644
--- a/docs/reference/language-extensions.rst
+++ b/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 `__,
+providers `__,
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 `__.
More detailed descriptions are available in David Christiansen's `WGP
-'13 paper `__ and `M.Sc.
+'13 paper `__ and `M.Sc.
thesis `__.
diff --git a/docs/reference/partial-evaluation.rst b/docs/reference/partial-evaluation.rst
index f7c5fc9ff..ee2160102 100644
--- a/docs/reference/partial-evaluation.rst
+++ b/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 `__.
+paper `__.
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 `__
+4 `__
for more details on how this works):
::
diff --git a/docs/reference/type-directed-search.rst b/docs/reference/type-directed-search.rst
index 21cb7736c..38864cc04 100644
--- a/docs/reference/type-directed-search.rst
+++ b/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 `__ for Haskell). For
+`Hoogle `__ for Haskell). For
example::
Idris> :search e -> List e -> List e
diff --git a/docs/reference/uniqueness-types.rst b/docs/reference/uniqueness-types.rst
index 1fc568604..2ef2c0b82 100644
--- a/docs/reference/uniqueness-types.rst
+++ b/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
`__ in the `Clean
-`__ programming language, and
+`__ programming language, and
ownership types and borrowed pointers in the `Rust
`__ programming language.
diff --git a/docs/st/index.rst b/docs/st/index.rst
index fd9b6774e..da0a478b2 100644
--- a/docs/st/index.rst
+++ b/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 --git a/docs/st/introduction.rst b/docs/st/introduction.rst
index 2ee9828cb..ecaf83747 100644
--- a/docs/st/introduction.rst
+++ b/docs/st/introduction.rst
@@ -3,7 +3,7 @@ Overview
********
Pure functional languages with dependent types such as `Idris
-`_ support reasoning about programs directly
+`_ 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.
diff --git a/docs/tutorial/conclusions.rst b/docs/tutorial/conclusions.rst
index fdfdccf07..34d6fc1cf 100644
--- a/docs/tutorial/conclusions.rst
+++ b/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://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
@@ -25,7 +25,7 @@ dependent types in general, can be obtained from various sources:
https://github.com/idris-lang/Idris-dev.
- Existing projects on the ``Idris Hackers`` web space:
- http://idris-hackers.github.io.
+ https://idris-hackers.github.io.
- Various papers (e.g. [1]_, [2]_, and [3]_). Although these mostly
describe older versions of Idris.
@@ -36,14 +36,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
.. [2] 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
.. [3] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your
inefficient engine: using partial evaluation to improve
@@ -51,4 +51,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/tutorial/index.rst b/docs/tutorial/index.rst
index 92be8ced9..507c740b0 100644
--- a/docs/tutorial/index.rst
+++ b/docs/tutorial/index.rst
@@ -15,7 +15,7 @@ existing functional programming language such as Haskell or OCaml.
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 --git a/docs/tutorial/introduction.rst b/docs/tutorial/introduction.rst
index f89d523e5..208d50dae 100644
--- a/docs/tutorial/introduction.rst
+++ b/docs/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/tutorial/miscellany.rst b/docs/tutorial/miscellany.rst
index 72d09fe81..9825b5f27 100644
--- a/docs/tutorial/miscellany.rst
+++ b/docs/tutorial/miscellany.rst
@@ -560,7 +560,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/tutorial/syntax.rst b/docs/tutorial/syntax.rst
index 09ed8d9a6..d560c7fc5 100644
--- a/docs/tutorial/syntax.rst
+++ b/docs/tutorial/syntax.rst
@@ -196,16 +196,16 @@ syntax rule, we can even go as far as:
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
.. [2] 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
.. [3] Edwin Brady and Kevin Hammond. 2010. Correct-by-Construction
Concurrency: Using Dependent Types to Verify Implementations of
Effectful Resource Usage Protocols. Fundam. Inf. 102, 2 (April
- 2010), 145-176. http://dl.acm.org/citation.cfm?id=1883636
+ 2010), 145-176. https://dl.acm.org/citation.cfm?id=1883636
diff --git a/idris.cabal b/idris.cabal
index a31c02b59..cfb75b4e7 100644
--- a/idris.cabal
+++ b/idris.cabal
@@ -4,7 +4,7 @@ License: BSD3
License-file: LICENSE
Author: Edwin Brady
Maintainer: Edwin Brady
-Homepage: http://www.idris-lang.org/
+Homepage: https://www.idris-lang.org/
Bug-reports: https://github.com/idris-lang/Idris-dev/issues
Stability: Beta
@@ -16,7 +16,7 @@ Description: Idris is a general purpose language with full dependent types.
meaning that some aspects of a program's behaviour can be
specified precisely in the type. The language is closely
related to Epigram and Agda. There is a tutorial at
- .
+ .
Features include:
.
* Full, first class, dependent types with dependent pattern matching
diff --git a/libs/contrib/Data/Combinators.idr b/libs/contrib/Data/Combinators.idr
index 28d2805b7..887d99b44 100644
--- a/libs/contrib/Data/Combinators.idr
+++ b/libs/contrib/Data/Combinators.idr
@@ -26,13 +26,13 @@ infixl 9 ...
(...) = (.) . (.)
||| Warbler, as named in "To Mock a Mockingbird".
-||| See http://code.jsoftware.com/wiki/Vocabulary/tilde
+||| See https://code.jsoftware.com/wiki/Vocabulary/tilde
||| Equivalent to `join` on the Reader monad (`(->) e` in Haskell)
reflex : (a -> a -> b) -> (a -> b)
reflex f x = f x x
||| Phoenix, according to Data.Aviary.
-||| See http://code.jsoftware.com/wiki/Vocabulary/fork.
+||| See https://code.jsoftware.com/wiki/Vocabulary/fork.
||| Equivalent to `liftA2` on the Reader monad (`(->) e` in Haskell)
fork2 : (b -> c -> d) -> (a -> b) -> (a -> c) -> (a -> d)
fork2 f g h x = f (g x) (h x)
diff --git a/libs/contrib/Language/JSON.idr b/libs/contrib/Language/JSON.idr
index 714b741a0..07c5687d7 100644
--- a/libs/contrib/Language/JSON.idr
+++ b/libs/contrib/Language/JSON.idr
@@ -1,4 +1,4 @@
-||| The JSON language, as described at http://json.org/
+||| The JSON language, as described at https://json.org/
module Language.JSON
import Language.JSON.Lexer
diff --git a/libs/prelude/IO.idr b/libs/prelude/IO.idr
index 292472e7d..824b2965c 100644
--- a/libs/prelude/IO.idr
+++ b/libs/prelude/IO.idr
@@ -80,7 +80,7 @@ foreign_prim f fname (FFun arg sc) env
||| Idris compiler backend in use. For the default C backend, see the
||| documentation for `FFI_C`.
|||
-||| For more details, please consult [the Idris documentation](http://docs.idris-lang.org/en/latest/reference/ffi.html).
+||| For more details, please consult [the Idris documentation](https://idris.readthedocs.io/en/latest/reference/ffi.html).
|||
||| @ f an FFI descriptor, which is specific to the compiler backend.
||| @ fname the name of the foreign function
diff --git a/man/idris.1 b/man/idris.1
index e7fe456f8..55f63566b 100644
--- a/man/idris.1
+++ b/man/idris.1
@@ -113,7 +113,7 @@ should not necessarily be seen as production ready nor for industrial use.
.SH SEE ALSO
-+ The IDRIS web site (http://idris-lang.org/
++ The IDRIS web site (https://idris-lang.org/
+ The IRC channel #idris, on chat.freenode.net
diff --git a/src/Idris/CmdOptions.hs b/src/Idris/CmdOptions.hs
index ed1dd9f1c..d132e916d 100644
--- a/src/Idris/CmdOptions.hs
+++ b/src/Idris/CmdOptions.hs
@@ -71,7 +71,7 @@ runArgParser = do opts <- execParser $ info parser
PP.empty,
PP.text "More details over Idris can be found online here:",
PP.empty,
- PP.indent 4 (PP.text "http://www.idris-lang.org/")]
+ PP.indent 4 (PP.text "https://www.idris-lang.org/")]
execArgParserPure :: [String] -> ParserResult [Opt]
execArgParserPure args = preProcOpts <$> execParserPure (prefs idm) (info parser idm) args
diff --git a/src/Idris/ModeCommon.hs b/src/Idris/ModeCommon.hs
index a9ff941ed..0a86171c9 100644
--- a/src/Idris/ModeCommon.hs
+++ b/src/Idris/ModeCommon.hs
@@ -167,7 +167,7 @@ loadInputs inputs toline -- furthest line to read in input source files
banner = " ____ __ _ \n" ++
" / _/___/ /____(_)____ \n" ++
" / // __ / ___/ / ___/ Version " ++ getIdrisVersion ++ "\n" ++
- " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
+ " _/ // /_/ / / / (__ ) https://www.idris-lang.org/ \n" ++
" /___/\\__,_/_/ /_/____/ Type :? for help \n" ++
"\n" ++
"Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++
diff --git a/test/pkg001/test-pkg.ipkg b/test/pkg001/test-pkg.ipkg
index ac2b2c3e2..bc8ade729 100644
--- a/test/pkg001/test-pkg.ipkg
+++ b/test/pkg001/test-pkg.ipkg
@@ -12,6 +12,6 @@ license = BSD3 but see LICENSE for more information
brief = "This is a test package."
readme = README.md
version = 1234
-homepage = http://www.idris-lang.org
-sourceloc = http://ww.github.com/idris-lang/Idris-Dev
-bugtracker = http://ww.github.com/idris-lang/Idris-Dev/issues
+homepage = https://www.idris-lang.org
+sourceloc = https://www.github.com/idris-lang/Idris-Dev
+bugtracker = https://www.github.com/idris-lang/Idris-Dev/issues