Skip to content

Commit

Permalink
Updated gh-pages
Browse files Browse the repository at this point in the history
gares committed Jan 13, 2025

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
1 parent 09b3500 commit a32106d
Showing 40 changed files with 17,858 additions and 1 deletion.
59 changes: 59 additions & 0 deletions _sources/about.rst.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
About
=====

This page is both an introspection and self documentation for this documentation stack.

Prerequisites
-------------

Before building this documentation, make sure to have ``sphinx`` installed:

.. code-block:: console
pip install sphinx
pip install in-place
To match the visuals used in the community (*e.g.* https://coq.inria.fr/distrib/current/refman/):

.. code-block:: console
pip install sphinx-rtd-theme
On debian based systems, one can use the package manager:

.. code-block:: console
apt install sphinx-doc
apt install python3-sphinx-rtd-theme
pip install in-place
Extensions
----------

This documentation can make use of the following plugins:

.. code-block:: python
extensions = [
'sphinx.ext.intersphinx',
'sphinx.ext.githubpages'
]
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.

Building
--------

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

Instead, use the ``doc-sphinx`` target of the source tree's root's ``Makefile`` to build the documentation:

.. code-block:: python
make doc-build
Or, to build and publish the documentation to github pages:

.. code-block:: python
make doc-publish
22 changes: 22 additions & 0 deletions _sources/index.rst.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
.. Elpi documentation master file, created by
sphinx-quickstart on Thu Jun 16 10:59:15 2022.
You can adapt this file completely to your liking, but it should at least
contain the root `toctree` directive.
Welcome to Elpi's documentation!
================================

.. .. toctree:
.. :maxdepth: 2
.. :caption: Contents:
..
.. about
.. playground
.. toctree::
:maxdepth: 2
:caption: API:

elpi <elpi/index.html#http://>
elpi-option-legacy-parser <elpi-option-legacy-parser/index.html#http://>

Loading

0 comments on commit a32106d

Please sign in to comment.