Skip to content

Commit

Permalink
Updated gh-pages
Browse files Browse the repository at this point in the history
  • Loading branch information
gares committed Nov 28, 2024
1 parent fd887d8 commit e215ffd
Show file tree
Hide file tree
Showing 43 changed files with 17,440 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 e215ffd

Please sign in to comment.