9bffc19 · Idris-dev · git.iko.soy

CITATION.md+1−1

compare with master

unifiedsplit

@@ -17,7 +17,7 @@ If you use `Idris` in your work we would prefer it if you would use the followin

17 pages = {552--593},

18 numpages = {42},

19 doi = {10.1017/S095679681300018X},

20− URL = {http://journals.cambridge.org/article_S095679681300018X},

20+ URL = {https://journals.cambridge.org/article_S095679681300018X},

21}

22```

23

CONTRIBUTING.md+5−5

@@ -6,9 +6,9 @@ Here are a few guidelines that we would like contributors to follow so that we c

6

7## Getting Started

8

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).

101. 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).

121. Make sure you can install Idris:

13 * [Mac OS X](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-OS-X-using-Homebrew)

14 * [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!

72

73## Making Changes

74

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/).

76The steps are described below.

77

78### New contributors

@@ -175,8 +175,8 @@ To help increase the chance of your pull request being accepted:

175* Idris FAQs: [Official](https://idris.readthedocs.io/en/latest/faq/faq.html); [Unofficial](https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ);

176* [Idris Manual](https://github.com/idris-lang/Idris-dev/wiki/Manual);

177* [Idris Tutorial](https://idris.readthedocs.io/en/latest/tutorial/index.html);

178−* [Idris News](http://www.idris-lang.org/news/);

178+* [Idris News](https://www.idris-lang.org/news/);

179−* [other Idris docs](http://www.idris-lang.org/documentation/).

179+* [other Idris docs](https://www.idris-lang.org/documentation/).

180* [Using Pull Requests](https://help.github.com/articles/using-pull-requests)

181* [General GitHub Documentation](https://help.github.com/).

182

Makefile+1−1

@@ -56,7 +56,7 @@ linecount:

56

57#Note: this doesn't yet link to Hackage properly

58doc: 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"

60

61lib_doc:

62 $(MAKE) -C libs IDRIS=../../dist/build/idris/idris doc

README.md+4−4

@@ -4,11 +4,11 @@

4[![Appveyor build](https://ci.appveyor.com/api/projects/status/xi8yu81oy1134g7o/branch/master?svg=true)](https://ci.appveyor.com/project/idrislang/idris-dev)

5[![Documentation Status](https://readthedocs.org/projects/idris/badge/?version=latest)](https://readthedocs.org/projects/idris/?badge=latest)

6[![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)

7+[![Stackage LTS](https://stackage.org/package/idris/badge/lts)](https://stackage.org/lts/package/idris)

8−[![Stackage Nightly](http://stackage.org/package/idris/badge/nightly)](http://stackage.org/nightly/package/idris)

8+[![Stackage Nightly](https://stackage.org/package/idris/badge/nightly)](https://stackage.org/nightly/package/idris)

9[![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)

10

11−Idris (http://idris-lang.org/) is a general-purpose functional programming

11+Idris (https://idris-lang.org/) is a general-purpose functional programming

12language with dependent types.

13

14## Installation Guides.

@@ -28,7 +28,7 @@ Idris has support for external code generators. Supplied with the distribution

28is a C code generator to compile executables, and a JavaScript code generator

29with support for node.js and browser JavaScript.

30

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).

32

33## More Information

34

appveyor.yml+1−1

@@ -5,7 +5,7 @@ init:

5

6 mkdir C:\ghc

7

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"

9

10 7z x C:\ghc\ghc.tar.xz -oC:\ghc

11

azure-pipelines.yml+1−1

@@ -68,7 +68,7 @@ jobs:

68 choco install 7zip.portable -y --no-progress

69 choco install msys2 -y --no-progress --params "/InstallDir=C:/msys64/"

70 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"

72 7z x C:\ghc\ghc.tar.xz -oC:\ghc

73 7z x C:\ghc\ghc.tar -oC:\ghc

74 displayName: "Setting up environment"

benchmarks/pidigits/pidigits.idr+1−1

@@ -3,7 +3,7 @@ import Data.Vect

3

4{- Toy program that outputs the n first digits of Pi.

5

6− Inspired from http://www.haskell.org/haskellwiki/Shootout/Pidigits.

6+ Inspired from https://www.haskell.org/haskellwiki/Shootout/Pidigits.

7 The original ns and str lazy lists have been replaced by strict functions.

8

9 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.

7

8More information concerning the CC0 can be found online at:

9

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

9

10# User-friendly check for sphinx-build

11ifeq ($(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/)

13endif

14

15# Internal variables.

docs/README.md+3−3

@@ -1,7 +1,7 @@

1# Documentation for the Idris Language.

2

3

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).

5

6## Dependencies

7

@@ -12,7 +12,7 @@ To build the manual the following dependencies must be met. We assume that you h

12Python should be installed by default on most systems.

13Sphinx can be installed either through your hosts package manager or using pip/easy_install.

14

15−*Note* [ReadTheDocs](http://www.readthedocs.org) works with Sphinx

15+*Note* [ReadTheDocs](https://www.readthedocs.org) works with Sphinx

16 `v1.2.2`. If you install a more recent version of sphinx then

17 'incorrectly' marked up documentation may get passed the build system

18 of readthedocs and be ignored. In the past we had several code-blocks

@@ -45,7 +45,7 @@ rights to Documentation for Idris.

45

46More information concerning the CC0 can be found online at:

47

48− http://creativecommons.org/publicdomain/zero/1.0/

48+ https://creativecommons.org/publicdomain/zero/1.0/

49

50

51When 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]_.

51 Programming Languages and Systems (APLAS '09), Zhenjiang Hu

52 (Ed.). Springer-Verlag, Berlin, Heidelberg,

53 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

55

56

57.. [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`.

25 Idris Community* has waived all copyright and related or neighbouring

26 rights to Documentation for Idris.

27

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/

29

30.. toctree::

31 :maxdepth: 1

docs/effects/introduction.rst+1−1

@@ -3,7 +3,7 @@ Introduction

3************

4

5Pure 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

7in the type system, promising that we can *know* a program will run

8correctly (i.e. according to the specification in its type) simply

9because 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?

37=====================================================================

38

39API 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/>`_.

41

42Unfortunately, the default prelude and shipped packages for `Idris`

43are 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

310be offering arbitrary Unicode symbols in operators.

311

312This 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.

314

315This answer is based on Edwin Brady's response in the following

316`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.

12 Idris Community* has waived all copyright and related or neighboring

13 rights to Documentation for Idris.

14

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/

16

17

18.. 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

22 ____ __ _

23 / _/___/ /____(_)____

24 / // __ / ___/ / ___/ Version 0.9.18.1

25− _/ // /_/ / / / (__ ) http://www.idris-lang.org/

25+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/

26 /___/\__,_/_/ /_/____/ Type :? for help

27

28 Idris is free software with ABSOLUTELY NO WARRANTY.

docs/guides/type-providers-ffi.rst+1−1

@@ -3,7 +3,7 @@ Type Providers in Idris

3***********************

4

5`Type providers in Idris

6−<http://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`__

6+<https://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`__

7are simple enough, but there are a few caveats to using them that it

8would be worthwhile to go through the basic steps. We also go over

9foreign functions, because these will often be used with type

docs/index.rst+1−1

@@ -13,7 +13,7 @@ Documentation for the Idris Language

13 Idris Community* has waived all copyright and related or neighboring

14 rights to Documentation for Idris.

15

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/

17

18

19.. toctree::

docs/listing/idris-prompt-helloworld.txt+1−1

@@ -2,7 +2,7 @@ $ idris hello.idr

2 ____ __ _

3 / _/___/ /____(_)____

4 / // __ / ___/ / ___/ Version 1.3.2

5− _/ // /_/ / / / (__ ) http://www.idris-lang.org/

5+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/

6 /___/\__,_/_/ /_/____/ Type :? for help

7

8Type checking ./hello.idr

docs/listing/idris-prompt-interp.txt+1−1

@@ -2,7 +2,7 @@ $ idris interp.idr

2 ____ __ _

3 / _/___/ /____(_)____

4 / // __ / ___/ / ___/ Version 1.3.2

5− _/ // /_/ / / / (__ ) http://www.idris-lang.org/

5+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/

6 /___/\__,_/_/ /_/____/ Type :? for help

7

8Type checking ./interp.idr

docs/listing/idris-prompt-start.txt+1−1

@@ -2,7 +2,7 @@ $ idris

2 ____ __ _

3 / _/___/ /____(_)____

4 / // __ / ___/ / ___/ Version 1.3.2

5− _/ // /_/ / / / (__ ) http://www.idris-lang.org/

5+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/

6/___/\__,_/_/ /_/____/ Type :? for help

7

8Idris>

docs/make.bat+1−1

@@ -65,7 +65,7 @@ if errorlevel 9009 (

65 echo.may add the Sphinx directory to PATH.

66 echo.

67 echo.If you don't have Sphinx installed, grab it from

68− echo.http://sphinx-doc.org/

68+ echo.https://www.sphinx-doc.org/

69 exit /b 1

70)

71

docs/proofs/index.rst+1−1

@@ -13,7 +13,7 @@ A tutorial on theorem proving in Idris.

13 Idris Community* has waived all copyright and related or neighboring

14 rights to Documentation for Idris.

15

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/

17

18.. toctree::

19 :maxdepth: 1

docs/proofs/interactive.rst+1−1

@@ -129,7 +129,7 @@ On running , two global names are created, ``plusredZ_Z`` and

129

130 . / _/___/ /____(_)____

131 / // __ / ___/ / ___/ Version 1.2.0

132− _/ // /_/ / / / (__ ) http://www.idris-lang.org/

132+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/

133 /___/\__,_/_/ /_/____/ Type :? for help

134

135 Idris is free software with ABSOLUTELY NO WARRANTY.

docs/reference/erasure.rst+2−2

@@ -254,7 +254,7 @@ Benchmarks

254==========

255

256- source: https://github.com/ziman/idris-benchmarks

257−- results: http://ziman.functor.sk/erasure-bm/

257+- results: https://ziman.functor.sk/erasure-bm/

258

259It can be clearly seen that asymptotics are improved by erasure.

260

@@ -499,4 +499,4 @@ References

499

500.. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive

501 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

14 Idris Community* has waived all copyright and related or neighboring

15 rights to Documentation for Idris.

16

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/

18

19

20.. toctree::

docs/reference/language-extensions.rst+2−2

@@ -8,7 +8,7 @@ Type Providers

8

9Idris type providers are a way to get the type system to reflect

10observations 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>`__,

12they cause effectful computations to run during type checking, returning

13information that the type checker can use when checking the rest of the

14program. While F# type providers are based on code generation, Idris

@@ -31,7 +31,7 @@ to the user.

31Example Idris type providers can be seen at `this

32repository <https://github.com/david-christiansen/idris-type-providers>`__.

33More 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.

35thesis <http://itu.dk/people/drc/david-christiansen-thesis.pdf>`__.

36

37Elaborator Reflection

docs/reference/partial-evaluation.rst+2−2

@@ -8,7 +8,7 @@ of functions with arguments annotated as ``%static``.

8

9(This is an implementation of the partial evaluator described in `this

10ICFP 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>`__.

12Please refer to this for more precise definitions of what follows.)

13

14Partial evaluation is switched off by default since Idris 1.0. It can

@@ -207,7 +207,7 @@ Specialising Interpreters

207A particularly useful situation where partial evaluation becomes

208effective is in defining an interpreter for a well-typed expression

209language, 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>`__

211for more details on how this works):

212

213::

docs/reference/type-directed-search.rst+1−1

@@ -4,7 +4,7 @@ Type Directed Search ``:search``

4

5Idris' ``:search`` command searches for terms according to their

6approximate type signature (much like

7−`Hoogle <http://www.haskell.org/hoogle/>`__ for Haskell). For

7+`Hoogle <https://www.haskell.org/hoogle/>`__ for Haskell). For

8example::

9

10 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.

13

14They are inspired by linear types, `Uniqueness Types

15<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

17ownership types and borrowed pointers in the `Rust

18<https://www.rust-lang.org/>`__ programming language.

19

docs/st/index.rst+1−1

@@ -14,7 +14,7 @@ the `Control.ST` library in `Idris`.

14 Idris Community* has waived all copyright and related or neighbouring

15 rights to Documentation for Idris.

16

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/

18

19.. toctree::

20 :maxdepth: 1

docs/st/introduction.rst+1−1

@@ -3,7 +3,7 @@ Overview

3********

4

5Pure 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

7in the type system, promising that we can *know* a program will run

8correctly (i.e. according to the specification in its type) simply

9because it compiles.

docs/tutorial/conclusions.rst+5−5

@@ -7,7 +7,7 @@ Further Reading

7Further information about Idris programming, and programming with

8dependent types in general, can be obtained from various sources:

9

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

11 questions on the mailing list.

12

13- The IRC channel ``#idris``, on

@@ -25,7 +25,7 @@ dependent types in general, can be obtained from various sources:

25 https://github.com/idris-lang/Idris-dev.

26

27- Existing projects on the ``Idris Hackers`` web space:

28− http://idris-hackers.github.io.

28+ https://idris-hackers.github.io.

29

30- Various papers (e.g. [1]_, [2]_, and [3]_). Although these mostly

31 describe older versions of Idris.

@@ -36,14 +36,14 @@ dependent types in general, can be obtained from various sources:

36 Aspects of Declarative Languages (PADL'12), Claudio Russo and

37 Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,

38 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

40

41.. [2] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full

42 dependent types. In Proceedings of the 5th ACM workshop on

43 Programming languages meets program verification (PLPV

44 '11). ACM, New York, NY, USA,

45 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

47

48.. [3] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your

49 inefficient engine: using partial evaluation to improve

@@ -51,4 +51,4 @@ dependent types in general, can be obtained from various sources:

51 15th ACM SIGPLAN international conference on Functional

52 programming (ICFP '10). ACM, New York, NY, USA,

53 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.

15 Idris Community* has waived all copyright and related or neighboring

16 rights to Documentation for Idris.

17

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/

19

20

21.. toctree::

docs/tutorial/introduction.rst+2−2

@@ -6,7 +6,7 @@ Introduction

6

7In conventional programming languages, there is a clear distinction

8between *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

10integers, characters, lists of characters, and lists of any value

11respectively:

12

@@ -49,7 +49,7 @@ Intended Audience

49

50This tutorial is intended as a brief introduction to the language, and

51is 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>`_.

53In particular, a certain amount of familiarity with Haskell syntax is

54assumed, although most concepts will at least be explained

55briefly. 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:

560 Type : Type 1

561

562If ``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>`_,

564so internally there is a *hierarchy* of types (or *universes*):

565

566.. code-block:: idris

docs/tutorial/syntax.rst+3−3

@@ -196,16 +196,16 @@ syntax rule, we can even go as far as:

196 Aspects of Declarative Languages (PADL'12), Claudio Russo and

197 Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,

198 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

200

201.. [2] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full

202 dependent types. In Proceedings of the 5th ACM workshop on

203 Programming languages meets program verification (PLPV

204 '11). ACM, New York, NY, USA,

205 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

207

208.. [3] Edwin Brady and Kevin Hammond. 2010. Correct-by-Construction

209 Concurrency: Using Dependent Types to Verify Implementations of

210 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

4License-file: LICENSE

5Author: Edwin Brady

6Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>

7−Homepage: http://www.idris-lang.org/

7+Homepage: https://www.idris-lang.org/

8Bug-reports: https://github.com/idris-lang/Idris-dev/issues

9

10Stability: Beta

@@ -16,7 +16,7 @@ Description: Idris is a general purpose language with full dependent types.

16 meaning that some aspects of a program's behaviour can be

17 specified precisely in the type. The language is closely

18 related to Epigram and Agda. There is a tutorial at

19− <http://www.idris-lang.org/documentation>.

19+ <https://www.idris-lang.org/documentation>.

20 Features include:

21 .

22 * Full, first class, dependent types with dependent pattern matching

libs/contrib/Data/Combinators.idr+2−2

@@ -26,13 +26,13 @@ infixl 9 ...

26(...) = (.) . (.)

27

28||| 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

30||| Equivalent to `join` on the Reader monad (`(->) e` in Haskell)

31reflex : (a -> a -> b) -> (a -> b)

32reflex f x = f x x

33

34||| Phoenix, according to Data.Aviary.

35−||| See http://code.jsoftware.com/wiki/Vocabulary/fork.

35+||| See https://code.jsoftware.com/wiki/Vocabulary/fork.

36||| Equivalent to `liftA2` on the Reader monad (`(->) e` in Haskell)

37fork2 : (b -> c -> d) -> (a -> b) -> (a -> c) -> (a -> d)

38fork2 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/

2module Language.JSON

3

4import Language.JSON.Lexer

libs/prelude/IO.idr+1−1

@@ -80,7 +80,7 @@ foreign_prim f fname (FFun arg sc) env

80||| Idris compiler backend in use. For the default C backend, see the

81||| documentation for `FFI_C`.

82|||

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).

84|||

85||| @ f an FFI descriptor, which is specific to the compiler backend.

86||| @ 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.

113

114.SH SEE ALSO

115

116−+ The IDRIS web site (http://idris-lang.org/

116++ The IDRIS web site (https://idris-lang.org/

117

118+ The IRC channel #idris, on chat.freenode.net

119

src/Idris/CmdOptions.hs+1−1

@@ -71,7 +71,7 @@ runArgParser = do opts <- execParser $ info parser

71 PP.empty,

72 PP.text "More details over Idris can be found online here:",

73 PP.empty,

74− PP.indent 4 (PP.text "http://www.idris-lang.org/")]

74+ PP.indent 4 (PP.text "https://www.idris-lang.org/")]

75

76execArgParserPure :: [String] -> ParserResult [Opt]

77execArgParserPure 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

167banner = " ____ __ _ \n" ++

168 " / _/___/ /____(_)____ \n" ++

169 " / // __ / ___/ / ___/ Version " ++ getIdrisVersion ++ "\n" ++

170− " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

170+ " _/ // /_/ / / / (__ ) https://www.idris-lang.org/ \n" ++

171 " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++

172 "\n" ++

173 "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

12brief = "This is a test package."

13readme = README.md

14version = 1234

15−homepage = http://www.idris-lang.org

15+homepage = https://www.idris-lang.org

16−sourceloc = http://ww.github.com/idris-lang/Idris-Dev

16+sourceloc = https://www.github.com/idris-lang/Idris-Dev

17−bugtracker = http://ww.github.com/idris-lang/Idris-Dev/issues

17+bugtracker = https://www.github.com/idris-lang/Idris-Dev/issues