Skip to content

Commit f3e560f

Browse files
committed
Deploying to gh-pages from @ e905c06 🚀
1 parent f2d60de commit f3e560f

File tree

276 files changed

+18534
-516
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

276 files changed

+18534
-516
lines changed

_sources/about.rst.txt

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
About
2+
=====
3+
4+
This page is both an introspection and self documentation for this documentation stack.
5+
6+
Prerequisites
7+
-------------
8+
9+
Before building this documentation, make sure to have ``sphinx`` installed:
10+
11+
.. code-block:: console
12+
13+
pip install sphinx
14+
pip install in-place
15+
16+
To match the visuals used in the community (*e.g.* https://coq.inria.fr/distrib/current/refman/):
17+
18+
.. code-block:: console
19+
20+
pip install sphinx-rtd-theme
21+
22+
On debian based systems, one can use the package manager:
23+
24+
.. code-block:: console
25+
26+
apt install sphinx-doc
27+
apt install python3-sphinx-rtd-theme
28+
pip install in-place
29+
30+
Extensions
31+
----------
32+
33+
This documentation can make use of the following plugins:
34+
35+
.. code-block:: python
36+
37+
extensions = [
38+
'sphinx.ext.intersphinx',
39+
'sphinx.ext.githubpages'
40+
]
41+
42+
Namely, ``intersphinx`` (https://www.sphinx-doc.org/en/master/usage/extensions/intersphinx.html) can generate links to the documentation of objects in external projects, either explicitly through the external role, or as a fallback resolution for any other cross-reference, and, ``githubpages`` (https://www.sphinx-doc.org/en/master/usage/extensions/githubpages.html#module-sphinx.ext.githubpages) which creates a ``.nojekyll`` file on generated HTML directory to publish the document on GitHub Pages.
43+
44+
Building
45+
--------
46+
47+
``sphinx`` comes with its own helpers to build the documentation but are not meant to be used directly, see :doc:`playground` section for injection points.
48+
49+
Instead, use the ``doc-sphinx`` target of the source tree's root's ``Makefile`` to build the documentation:
50+
51+
.. code-block:: python
52+
53+
make doc-build
54+
55+
Or, to build and publish the documentation to github pages:
56+
57+
.. code-block:: python
58+
59+
make doc-publish

_sources/index.rst.txt

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
.. Elpi documentation master file, created by
2+
sphinx-quickstart on Thu Jun 16 10:59:15 2022.
3+
You can adapt this file completely to your liking, but it should at least
4+
contain the root `toctree` directive.
5+
6+
Welcome to Elpi's documentation!
7+
================================
8+
9+
.. .. toctree:
10+
.. :maxdepth: 2
11+
.. :caption: Contents:
12+
..
13+
.. about
14+
.. playground
15+
16+
.. toctree::
17+
:maxdepth: 2
18+
:caption: API:
19+
20+
elpi <elpi/index.html#http://>
21+
elpi-option-legacy-parser <elpi-option-legacy-parser/index.html#http://>
22+

0 commit comments

Comments
 (0)