1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-15 06:13:26 +03:00
Idris2/docs
2021-11-17 10:50:49 +00:00
..
source [ doc ] Fix a complain of not being in a toctree 2021-11-17 10:50:49 +00:00
LICENSE Copy more files over from Idris2 2020-05-20 11:23:04 +01:00
make.bat replace HTTP links with HTTPS 2020-05-27 14:50:05 +02:00
Makefile Copy more files over from Idris2 2020-05-20 11:23:04 +01:00
README.md docs: fix grammar 2020-12-16 10:02:34 +00:00
requirements.txt Check docs in CI 2021-02-04 14:59:14 +00:00

Documentation for the Idris Language.

This manual has been prepared using ReStructured Text and the Sphinx Documentation Generator for future inclusion on Read The Docs.

Dependencies

To build the manual, the following dependencies must be met. We assume that you have standard build automation tools already installed i.e. make.

Sphinx-Doc

Python should be installed by default on most systems. Sphinx can be installed either through your hosts package manager or using pip/easy_install. Recommended way is to use virtual environment for building documentation.

Note ReadTheDocs 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 disappear because of that.

The ReadTheDocs theme can be installed in virtual environment using pip as follows:

python3 -m venv idris2docs_venv
source idris2docs_venv/bin/activate
pip install --upgrade pip
pip install sphinx_rtd_theme

LaTeX

LaTeX can be installed either using your systems package manager or directly from TeXLive.

Build Instructions

cd docs
make html
make latexpdf

Contributing

The documentation for Idris has been published under the Creative Commons CC0 License. As such to the extent possible under law, /The 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:

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.