git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4797 from MilanKral/https

use HTTPS URL instead of HTTP URL when possible

commit9bffc1945572e6c0e25a88e57964d4e50b675376 authorNiklas Larsson <metaniklas@gmail.com> dateSat 21 Dec 2019, 13:41 (7 years ago) parent01dd51c35757f9
45 files changed+69−69
compare with master
unifiedsplit
CITATION.md+1−1 CONTRIBUTING.md+5−5 Makefile+1−1 README.md+4−4 appveyor.yml+1−1 azure-pipelines.yml+1−1 benchmarks/pidigits/pidigits.idr+1−1 docs/LICENSE+1−1 docs/Makefile+1−1 docs/README.md+3−3 docs/effects/conclusions.rst+1−1 docs/effects/index.rst+1−1 docs/effects/introduction.rst+1−1 docs/faq/faq.rst+2−2 docs/guides/index.rst+1−1 docs/guides/theorem-prover.rst+1−1 docs/guides/type-providers-ffi.rst+1−1 docs/index.rst+1−1 docs/listing/idris-prompt-helloworld.txt+1−1 docs/listing/idris-prompt-interp.txt+1−1 docs/listing/idris-prompt-start.txt+1−1 docs/make.bat+1−1 docs/proofs/index.rst+1−1 docs/proofs/interactive.rst+1−1 docs/reference/erasure.rst+2−2 docs/reference/index.rst+1−1 docs/reference/language-extensions.rst+2−2 docs/reference/partial-evaluation.rst+2−2 docs/reference/type-directed-search.rst+1−1 docs/reference/uniqueness-types.rst+1−1 docs/st/index.rst+1−1 docs/st/introduction.rst+1−1 docs/tutorial/conclusions.rst+5−5 docs/tutorial/index.rst+1−1 docs/tutorial/introduction.rst+2−2 docs/tutorial/miscellany.rst+1−1 docs/tutorial/syntax.rst+3−3 idris.cabal+2−2 libs/contrib/Data/Combinators.idr+2−2 libs/contrib/Language/JSON.idr+1−1 libs/prelude/IO.idr+1−1 man/idris.1+1−1 src/Idris/CmdOptions.hs+1−1 src/Idris/ModeCommon.hs+1−1 test/pkg001/test-pkg.ipkg+3−3
CITATION.md+1−1
@@ -17,7 +17,7 @@ If you use `Idris` in your work we would prefer it if you would use the followin
1717 pages = {552--593},
1818 numpages = {42},
1919 doi = {10.1017/S095679681300018X},
20− URL = {http://journals.cambridge.org/article_S095679681300018X},
20+ URL = {https://journals.cambridge.org/article_S095679681300018X},
2121}
2222```
2323
CONTRIBUTING.md+5−5
@@ -6,9 +6,9 @@ Here are a few guidelines that we would like contributors to follow so that we c
66
77## Getting Started
88
9−1. Make sure you are familiar with [Git](http://git-scm.com/book).
9+1. Make sure you are familiar with [Git](https://git-scm.com/book).
10101. Make sure you have a [GitHub account](https://github.com/signup/free).
11−1. Make sure you are familiar with: [Idris](http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf).
11+1. Make sure you are familiar with: [Idris](https://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf).
12121. Make sure you can install Idris:
1313 * [Mac OS X](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-OS-X-using-Homebrew)
1414 * [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!
7272
7373## Making Changes
7474
75−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/).
75+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/).
7676The steps are described below.
7777
7878### New contributors
@@ -175,8 +175,8 @@ To help increase the chance of your pull request being accepted:
175175* Idris FAQs: [Official](https://idris.readthedocs.io/en/latest/faq/faq.html); [Unofficial](https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ);
176176* [Idris Manual](https://github.com/idris-lang/Idris-dev/wiki/Manual);
177177* [Idris Tutorial](https://idris.readthedocs.io/en/latest/tutorial/index.html);
178−* [Idris News](http://www.idris-lang.org/news/);
179−* [other Idris docs](http://www.idris-lang.org/documentation/).
178+* [Idris News](https://www.idris-lang.org/news/);
179+* [other Idris docs](https://www.idris-lang.org/documentation/).
180180* [Using Pull Requests](https://help.github.com/articles/using-pull-requests)
181181* [General GitHub Documentation](https://help.github.com/).
182182
Makefile+1−1
@@ -56,7 +56,7 @@ linecount:
5656
5757#Note: this doesn't yet link to Hackage properly
5858doc: dist/setup-config
59− $(CABAL) haddock --hyperlink-source --html --hoogle --html-location="http://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"
59+ $(CABAL) haddock --hyperlink-source --html --hoogle --html-location="https://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"
6060
6161lib_doc:
6262 $(MAKE) -C libs IDRIS=../../dist/build/idris/idris doc
README.md+4−4
@@ -4,11 +4,11 @@
44[![Appveyor build](https://ci.appveyor.com/api/projects/status/xi8yu81oy1134g7o/branch/master?svg=true)](https://ci.appveyor.com/project/idrislang/idris-dev)
55[![Documentation Status](https://readthedocs.org/projects/idris/badge/?version=latest)](https://readthedocs.org/projects/idris/?badge=latest)
66[![Hackage](https://img.shields.io/hackage/v/idris.svg)](https://hackage.haskell.org/package/idris)
7−[![Stackage LTS](http://stackage.org/package/idris/badge/lts)](http://stackage.org/lts/package/idris)
8−[![Stackage Nightly](http://stackage.org/package/idris/badge/nightly)](http://stackage.org/nightly/package/idris)
7+[![Stackage LTS](https://stackage.org/package/idris/badge/lts)](https://stackage.org/lts/package/idris)
8+[![Stackage Nightly](https://stackage.org/package/idris/badge/nightly)](https://stackage.org/nightly/package/idris)
99[![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)
1010
11−Idris (http://idris-lang.org/) is a general-purpose functional programming
11+Idris (https://idris-lang.org/) is a general-purpose functional programming
1212language with dependent types.
1313
1414## Installation Guides.
@@ -28,7 +28,7 @@ Idris has support for external code generators. Supplied with the distribution
2828is a C code generator to compile executables, and a JavaScript code generator
2929with support for node.js and browser JavaScript.
3030
31−More information about [code generators can be found on the wiki](http://idris.readthedocs.io/en/latest/reference/codegen.html).
31+More information about [code generators can be found on the wiki](https://idris.readthedocs.io/en/latest/reference/codegen.html).
3232
3333## More Information
3434
appveyor.yml+1−1
@@ -5,7 +5,7 @@ init:
55
66 mkdir C:\ghc
77
8− 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"
8+ 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"
99
1010 7z x C:\ghc\ghc.tar.xz -oC:\ghc
1111
azure-pipelines.yml+1−1
@@ -68,7 +68,7 @@ jobs:
6868 choco install 7zip.portable -y --no-progress
6969 choco install msys2 -y --no-progress --params "/InstallDir=C:/msys64/"
7070 mkdir C:\ghc
71− 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"
71+ 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"
7272 7z x C:\ghc\ghc.tar.xz -oC:\ghc
7373 7z x C:\ghc\ghc.tar -oC:\ghc
7474 displayName: "Setting up environment"
benchmarks/pidigits/pidigits.idr+1−1
@@ -3,7 +3,7 @@ import Data.Vect
33
44{- Toy program that outputs the n first digits of Pi.
55
6− Inspired from http://www.haskell.org/haskellwiki/Shootout/Pidigits.
6+ Inspired from https://www.haskell.org/haskellwiki/Shootout/Pidigits.
77 The original ns and str lazy lists have been replaced by strict functions.
88
99 Memory usage seems to be excessive. One of the branches of str is tail recursive, and
docs/LICENSE+1−1
@@ -7,4 +7,4 @@ rights to Documentation for Idris.
77
88More information concerning the CC0 can be found online at:
99
10− http://creativecommons.org/publicdomain/zero/1.0/
10+ https://creativecommons.org/publicdomain/zero/1.0/
docs/Makefile+1−1
@@ -9,7 +9,7 @@ BUILDDIR = _build
99
1010# User-friendly check for sphinx-build
1111ifeq ($(shell which $(SPHINXBUILD) >/dev/null 2>&1; echo $$?), 1)
12−$(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/)
12+$(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/)
1313endif
1414
1515# Internal variables.
docs/README.md+3−3
@@ -1,7 +1,7 @@
11# Documentation for the Idris Language.
22
33
4−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).
4+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).
55
66## Dependencies
77
@@ -12,7 +12,7 @@ To build the manual the following dependencies must be met. We assume that you h
1212Python should be installed by default on most systems.
1313Sphinx can be installed either through your hosts package manager or using pip/easy_install.
1414
15−*Note* [ReadTheDocs](http://www.readthedocs.org) works with Sphinx
15+*Note* [ReadTheDocs](https://www.readthedocs.org) works with Sphinx
1616 `v1.2.2`. If you install a more recent version of sphinx then
1717 'incorrectly' marked up documentation may get passed the build system
1818 of readthedocs and be ignored. In the past we had several code-blocks
@@ -45,7 +45,7 @@ rights to Documentation for Idris.
4545
4646More information concerning the CC0 can be found online at:
4747
48− http://creativecommons.org/publicdomain/zero/1.0/
48+ https://creativecommons.org/publicdomain/zero/1.0/
4949
5050
5151When contributing material to the manual please bear in mind that the work will be licensed as above.
docs/effects/conclusions.rst+1−1
@@ -51,7 +51,7 @@ foundations are also well-studied see [5]_, [6]_, [7]_, [8]_.
5151 Programming Languages and Systems (APLAS '09), Zhenjiang Hu
5252 (Ed.). Springer-Verlag, Berlin, Heidelberg,
5353 95-110. DOI=10.1007/978-3-642-10672-9_9
54− http://link.springer.com/chapter/10.1007%2F978-3-642-10672-9_9
54+ https://link.springer.com/chapter/10.1007%2F978-3-642-10672-9_9
5555
5656
5757.. [4] Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in
docs/effects/index.rst+1−1
@@ -25,7 +25,7 @@ A tutorial on the `Effects` package in `Idris`.
2525 Idris Community* has waived all copyright and related or neighbouring
2626 rights to Documentation for Idris.
2727
28− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
28+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
2929
3030.. toctree::
3131 :maxdepth: 1
docs/effects/introduction.rst+1−1
@@ -3,7 +3,7 @@ Introduction
33************
44
55Pure functional languages with dependent types such as `Idris
6−<http://www.idris-lang.org/>`_ support reasoning about programs directly
6+<https://www.idris-lang.org/>`_ support reasoning about programs directly
77in the type system, promising that we can *know* a program will run
88correctly (i.e. according to the specification in its type) simply
99because it compiles. Realistically, though, things are not so simple:
docs/faq/faq.rst+2−2
@@ -37,7 +37,7 @@ Is there some documentation for the standard lib? List of functions?
3737=====================================================================
3838
3939API documentation for the shipped packages is listed on `the
40−documentation page <http://www.idris-lang.org/documentation/>`_.
40+documentation page <https://www.idris-lang.org/documentation/>`_.
4141
4242Unfortunately, the default prelude and shipped packages for `Idris`
4343are 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
310310be offering arbitrary Unicode symbols in operators.
311311
312312This seems like an instance of `Wadler's
313−Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
313+Law <https://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
314314
315315This answer is based on Edwin Brady's response in the following
316316`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`_.
docs/guides/index.rst+1−1
@@ -12,7 +12,7 @@ Tutorials submitted by community members.
1212 Idris Community* has waived all copyright and related or neighboring
1313 rights to Documentation for Idris.
1414
15− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
15+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
1616
1717
1818.. toctree::
docs/guides/theorem-prover.rst+1−1
@@ -22,7 +22,7 @@ We will be given the following prompt, in future releases the version string wil
2222 ____ __ _
2323 / _/___/ /____(_)____
2424 / // __ / ___/ / ___/ Version 0.9.18.1
25− _/ // /_/ / / / (__ ) http://www.idris-lang.org/
25+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/
2626 /___/\__,_/_/ /_/____/ Type :? for help
2727
2828 Idris is free software with ABSOLUTELY NO WARRANTY.
docs/guides/type-providers-ffi.rst+1−1
@@ -3,7 +3,7 @@ Type Providers in Idris
33***********************
44
55`Type providers in Idris
6−<http://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`__
6+<https://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`__
77are simple enough, but there are a few caveats to using them that it
88would be worthwhile to go through the basic steps. We also go over
99foreign functions, because these will often be used with type
docs/index.rst+1−1
@@ -13,7 +13,7 @@ Documentation for the Idris Language
1313 Idris Community* has waived all copyright and related or neighboring
1414 rights to Documentation for Idris.
1515
16− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
16+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
1717
1818
1919.. toctree::
docs/listing/idris-prompt-helloworld.txt+1−1
@@ -2,7 +2,7 @@ $ idris hello.idr
22 ____ __ _
33 / _/___/ /____(_)____
44 / // __ / ___/ / ___/ Version 1.3.2
5− _/ // /_/ / / / (__ ) http://www.idris-lang.org/
5+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/
66 /___/\__,_/_/ /_/____/ Type :? for help
77
88Type checking ./hello.idr
docs/listing/idris-prompt-interp.txt+1−1
@@ -2,7 +2,7 @@ $ idris interp.idr
22 ____ __ _
33 / _/___/ /____(_)____
44 / // __ / ___/ / ___/ Version 1.3.2
5− _/ // /_/ / / / (__ ) http://www.idris-lang.org/
5+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/
66 /___/\__,_/_/ /_/____/ Type :? for help
77
88Type checking ./interp.idr
docs/listing/idris-prompt-start.txt+1−1
@@ -2,7 +2,7 @@ $ idris
22 ____ __ _
33 / _/___/ /____(_)____
44 / // __ / ___/ / ___/ Version 1.3.2
5− _/ // /_/ / / / (__ ) http://www.idris-lang.org/
5+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/
66/___/\__,_/_/ /_/____/ Type :? for help
77
88Idris>
docs/make.bat+1−1
@@ -65,7 +65,7 @@ if errorlevel 9009 (
6565 echo.may add the Sphinx directory to PATH.
6666 echo.
6767 echo.If you don't have Sphinx installed, grab it from
68− echo.http://sphinx-doc.org/
68+ echo.https://www.sphinx-doc.org/
6969 exit /b 1
7070)
7171
docs/proofs/index.rst+1−1
@@ -13,7 +13,7 @@ A tutorial on theorem proving in Idris.
1313 Idris Community* has waived all copyright and related or neighboring
1414 rights to Documentation for Idris.
1515
16− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
16+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
1717
1818.. toctree::
1919 :maxdepth: 1
docs/proofs/interactive.rst+1−1
@@ -129,7 +129,7 @@ On running , two global names are created, ``plusredZ_Z`` and
129129
130130 . / _/___/ /____(_)____
131131 / // __ / ___/ / ___/ Version 1.2.0
132− _/ // /_/ / / / (__ ) http://www.idris-lang.org/
132+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/
133133 /___/\__,_/_/ /_/____/ Type :? for help
134134
135135 Idris is free software with ABSOLUTELY NO WARRANTY.
docs/reference/erasure.rst+2−2
@@ -254,7 +254,7 @@ Benchmarks
254254==========
255255
256256- source: https://github.com/ziman/idris-benchmarks
257−- results: http://ziman.functor.sk/erasure-bm/
257+- results: https://ziman.functor.sk/erasure-bm/
258258
259259It can be clearly seen that asymptotics are improved by erasure.
260260
@@ -499,4 +499,4 @@ References
499499
500500.. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive
501501 families need not store their indices
502− <http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849>`__
502+ <https://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849>`__
docs/reference/index.rst+1−1
@@ -14,7 +14,7 @@ This will tell you how Idris works, for using it you should read the Idris Tutor
1414 Idris Community* has waived all copyright and related or neighboring
1515 rights to Documentation for Idris.
1616
17− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
17+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
1818
1919
2020.. toctree::
docs/reference/language-extensions.rst+2−2
@@ -8,7 +8,7 @@ Type Providers
88
99Idris type providers are a way to get the type system to reflect
1010observations about the world outside of Idris. Similarly to `F# type
11−providers <http://msdn.microsoft.com/en-us/library/vstudio/hh156509.aspx>`__,
11+providers <https://msdn.microsoft.com/en-us/library/vstudio/hh156509.aspx>`__,
1212they cause effectful computations to run during type checking, returning
1313information that the type checker can use when checking the rest of the
1414program. While F# type providers are based on code generation, Idris
@@ -31,7 +31,7 @@ to the user.
3131Example Idris type providers can be seen at `this
3232repository <https://github.com/david-christiansen/idris-type-providers>`__.
3333More detailed descriptions are available in David Christiansen's `WGP
34−'13 paper <http://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
34+'13 paper <https://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
3535thesis <http://itu.dk/people/drc/david-christiansen-thesis.pdf>`__.
3636
3737Elaborator Reflection
docs/reference/partial-evaluation.rst+2−2
@@ -8,7 +8,7 @@ of functions with arguments annotated as ``%static``.
88
99(This is an implementation of the partial evaluator described in `this
1010ICFP 2010
11−paper <http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
11+paper <https://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
1212Please refer to this for more precise definitions of what follows.)
1313
1414Partial evaluation is switched off by default since Idris 1.0. It can
@@ -207,7 +207,7 @@ Specialising Interpreters
207207A particularly useful situation where partial evaluation becomes
208208effective is in defining an interpreter for a well-typed expression
209209language, defined as follows (see the `Idris tutorial, section
210−4 <http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf>`__
210+4 <https://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf>`__
211211for more details on how this works):
212212
213213::
docs/reference/type-directed-search.rst+1−1
@@ -4,7 +4,7 @@ Type Directed Search ``:search``
44
55Idris' ``:search`` command searches for terms according to their
66approximate type signature (much like
7−`Hoogle <http://www.haskell.org/hoogle/>`__ for Haskell). For
7+`Hoogle <https://www.haskell.org/hoogle/>`__ for Haskell). For
88example::
99
1010 Idris> :search e -> List e -> List e
docs/reference/uniqueness-types.rst+1−1
@@ -13,7 +13,7 @@ ideally while giving up as little high level conveniences as possible.
1313
1414They are inspired by linear types, `Uniqueness Types
1515<https://en.wikipedia.org/wiki/Uniqueness_type>`__ in the `Clean
16−<http://wiki.clean.cs.ru.nl/Clean>`__ programming language, and
16+<https://wiki.clean.cs.ru.nl/Clean>`__ programming language, and
1717ownership types and borrowed pointers in the `Rust
1818<https://www.rust-lang.org/>`__ programming language.
1919
docs/st/index.rst+1−1
@@ -14,7 +14,7 @@ the `Control.ST` library in `Idris`.
1414 Idris Community* has waived all copyright and related or neighbouring
1515 rights to Documentation for Idris.
1616
17− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
17+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
1818
1919.. toctree::
2020 :maxdepth: 1
docs/st/introduction.rst+1−1
@@ -3,7 +3,7 @@ Overview
33********
44
55Pure functional languages with dependent types such as `Idris
6−<http://www.idris-lang.org/>`_ support reasoning about programs directly
6+<https://www.idris-lang.org/>`_ support reasoning about programs directly
77in the type system, promising that we can *know* a program will run
88correctly (i.e. according to the specification in its type) simply
99because it compiles.
docs/tutorial/conclusions.rst+5−5
@@ -7,7 +7,7 @@ Further Reading
77Further information about Idris programming, and programming with
88dependent types in general, can be obtained from various sources:
99
10−- The Idris web site (http://www.idris-lang.org/) and by asking
10+- The Idris web site (https://www.idris-lang.org/) and by asking
1111 questions on the mailing list.
1212
1313- The IRC channel ``#idris``, on
@@ -25,7 +25,7 @@ dependent types in general, can be obtained from various sources:
2525 https://github.com/idris-lang/Idris-dev.
2626
2727- Existing projects on the ``Idris Hackers`` web space:
28− http://idris-hackers.github.io.
28+ https://idris-hackers.github.io.
2929
3030- Various papers (e.g. [1]_, [2]_, and [3]_). Although these mostly
3131 describe older versions of Idris.
@@ -36,14 +36,14 @@ dependent types in general, can be obtained from various sources:
3636 Aspects of Declarative Languages (PADL'12), Claudio Russo and
3737 Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,
3838 242-257. DOI=10.1007/978-3-642-27694-1_18
39− http://dx.doi.org/10.1007/978-3-642-27694-1_18
39+ https://dx.doi.org/10.1007/978-3-642-27694-1_18
4040
4141.. [2] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
4242 dependent types. In Proceedings of the 5th ACM workshop on
4343 Programming languages meets program verification (PLPV
4444 '11). ACM, New York, NY, USA,
4545 43-54. DOI=10.1145/1929529.1929536
46− http://doi.acm.org/10.1145/1929529.1929536
46+ https://doi.acm.org/10.1145/1929529.1929536
4747
4848.. [3] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your
4949 inefficient engine: using partial evaluation to improve
@@ -51,4 +51,4 @@ dependent types in general, can be obtained from various sources:
5151 15th ACM SIGPLAN international conference on Functional
5252 programming (ICFP '10). ACM, New York, NY, USA,
5353 297-308. DOI=10.1145/1863543.1863587
54− http://doi.acm.org/10.1145/1863543.1863587
54+ https://doi.acm.org/10.1145/1863543.1863587
docs/tutorial/index.rst+1−1
@@ -15,7 +15,7 @@ existing functional programming language such as Haskell or OCaml.
1515 Idris Community* has waived all copyright and related or neighboring
1616 rights to Documentation for Idris.
1717
18− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
18+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
1919
2020
2121.. toctree::
docs/tutorial/introduction.rst+2−2
@@ -6,7 +6,7 @@ Introduction
66
77In conventional programming languages, there is a clear distinction
88between *types* and *values*. For example, in `Haskell
9−<http://www.haskell.org>`_, the following are types, representing
9+<https://www.haskell.org>`_, the following are types, representing
1010integers, characters, lists of characters, and lists of any value
1111respectively:
1212
@@ -49,7 +49,7 @@ Intended Audience
4949
5050This tutorial is intended as a brief introduction to the language, and
5151is aimed at readers already familiar with a functional language such
52−as `Haskell <http://www.haskell.org>`_ or `OCaml <http://ocaml.org>`_.
52+as `Haskell <https://www.haskell.org>`_ or `OCaml <https://ocaml.org>`_.
5353In particular, a certain amount of familiarity with Haskell syntax is
5454assumed, although most concepts will at least be explained
5555briefly. The reader is also assumed to have some interest in using
docs/tutorial/miscellany.rst+1−1
@@ -560,7 +560,7 @@ But what about the type of ``Type``? If we ask Idris it reports:
560560 Type : Type 1
561561
562562If ``Type`` were its own type, it would lead to an inconsistency due to
563−`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
563+`Girard’s paradox <https://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
564564so internally there is a *hierarchy* of types (or *universes*):
565565
566566.. code-block:: idris
docs/tutorial/syntax.rst+3−3
@@ -196,16 +196,16 @@ syntax rule, we can even go as far as:
196196 Aspects of Declarative Languages (PADL'12), Claudio Russo and
197197 Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,
198198 242-257. DOI=10.1007/978-3-642-27694-1_18
199− http://dx.doi.org/10.1007/978-3-642-27694-1_18
199+ https://dx.doi.org/10.1007/978-3-642-27694-1_18
200200
201201.. [2] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
202202 dependent types. In Proceedings of the 5th ACM workshop on
203203 Programming languages meets program verification (PLPV
204204 '11). ACM, New York, NY, USA,
205205 43-54. DOI=10.1145/1929529.1929536
206− http://doi.acm.org/10.1145/1929529.1929536
206+ https://doi.acm.org/10.1145/1929529.1929536
207207
208208.. [3] Edwin Brady and Kevin Hammond. 2010. Correct-by-Construction
209209 Concurrency: Using Dependent Types to Verify Implementations of
210210 Effectful Resource Usage Protocols. Fundam. Inf. 102, 2 (April
211− 2010), 145-176. http://dl.acm.org/citation.cfm?id=1883636
211+ 2010), 145-176. https://dl.acm.org/citation.cfm?id=1883636
idris.cabal+2−2
@@ -4,7 +4,7 @@ License: BSD3
44License-file: LICENSE
55Author: Edwin Brady
66Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>
7−Homepage: http://www.idris-lang.org/
7+Homepage: https://www.idris-lang.org/
88Bug-reports: https://github.com/idris-lang/Idris-dev/issues
99
1010Stability: Beta
@@ -16,7 +16,7 @@ Description: Idris is a general purpose language with full dependent types.
1616 meaning that some aspects of a program's behaviour can be
1717 specified precisely in the type. The language is closely
1818 related to Epigram and Agda. There is a tutorial at
19− <http://www.idris-lang.org/documentation>.
19+ <https://www.idris-lang.org/documentation>.
2020 Features include:
2121 .
2222 * Full, first class, dependent types with dependent pattern matching
libs/contrib/Data/Combinators.idr+2−2
@@ -26,13 +26,13 @@ infixl 9 ...
2626(...) = (.) . (.)
2727
2828||| Warbler, as named in "To Mock a Mockingbird".
29−||| See http://code.jsoftware.com/wiki/Vocabulary/tilde
29+||| See https://code.jsoftware.com/wiki/Vocabulary/tilde
3030||| Equivalent to `join` on the Reader monad (`(->) e` in Haskell)
3131reflex : (a -> a -> b) -> (a -> b)
3232reflex f x = f x x
3333
3434||| Phoenix, according to Data.Aviary.
35−||| See http://code.jsoftware.com/wiki/Vocabulary/fork.
35+||| See https://code.jsoftware.com/wiki/Vocabulary/fork.
3636||| Equivalent to `liftA2` on the Reader monad (`(->) e` in Haskell)
3737fork2 : (b -> c -> d) -> (a -> b) -> (a -> c) -> (a -> d)
3838fork2 f g h x = f (g x) (h x)
libs/contrib/Language/JSON.idr+1−1
@@ -1,4 +1,4 @@
1−||| The JSON language, as described at http://json.org/
1+||| The JSON language, as described at https://json.org/
22module Language.JSON
33
44import Language.JSON.Lexer
libs/prelude/IO.idr+1−1
@@ -80,7 +80,7 @@ foreign_prim f fname (FFun arg sc) env
8080||| Idris compiler backend in use. For the default C backend, see the
8181||| documentation for `FFI_C`.
8282|||
83−||| For more details, please consult [the Idris documentation](http://docs.idris-lang.org/en/latest/reference/ffi.html).
83+||| For more details, please consult [the Idris documentation](https://idris.readthedocs.io/en/latest/reference/ffi.html).
8484|||
8585||| @ f an FFI descriptor, which is specific to the compiler backend.
8686||| @ fname the name of the foreign function
man/idris.1+1−1
@@ -113,7 +113,7 @@ should not necessarily be seen as production ready nor for industrial use.
113113
114114.SH SEE ALSO
115115
116−+ The IDRIS web site (http://idris-lang.org/
116++ The IDRIS web site (https://idris-lang.org/
117117
118118+ The IRC channel #idris, on chat.freenode.net
119119
src/Idris/CmdOptions.hs+1−1
@@ -71,7 +71,7 @@ runArgParser = do opts <- execParser $ info parser
7171 PP.empty,
7272 PP.text "More details over Idris can be found online here:",
7373 PP.empty,
74− PP.indent 4 (PP.text "http://www.idris-lang.org/")]
74+ PP.indent 4 (PP.text "https://www.idris-lang.org/")]
7575
7676execArgParserPure :: [String] -> ParserResult [Opt]
7777execArgParserPure args = preProcOpts <$> execParserPure (prefs idm) (info parser idm) args
src/Idris/ModeCommon.hs+1−1
@@ -167,7 +167,7 @@ loadInputs inputs toline -- furthest line to read in input source files
167167banner = " ____ __ _ \n" ++
168168 " / _/___/ /____(_)____ \n" ++
169169 " / // __ / ___/ / ___/ Version " ++ getIdrisVersion ++ "\n" ++
170− " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
170+ " _/ // /_/ / / / (__ ) https://www.idris-lang.org/ \n" ++
171171 " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++
172172 "\n" ++
173173 "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++
test/pkg001/test-pkg.ipkg+3−3
@@ -12,6 +12,6 @@ license = BSD3 but see LICENSE for more information
1212brief = "This is a test package."
1313readme = README.md
1414version = 1234
15−homepage = http://www.idris-lang.org
16−sourceloc = http://ww.github.com/idris-lang/Idris-Dev
17−bugtracker = http://ww.github.com/idris-lang/Idris-Dev/issues
15+homepage = https://www.idris-lang.org
16+sourceloc = https://www.github.com/idris-lang/Idris-Dev
17+bugtracker = https://www.github.com/idris-lang/Idris-Dev/issues