Elpi sphinx documentation preview

[jwintz]

Hi,

Here is a preview for Elpi's sphinx based documentation to be: https://dream.inria.fr/elpi/

The Test Bed (https://dream.inria.fr/elpi/playground.html#test-bed) is so far only applied to 3 elpi test source files. Will list exhaustively all examples for validation before merging upstream.

For the reference, here are listed current sources for about and playground doc sources.

Before merging all proof of concepts repositories from Inria's Gitlab to Github, everything lies here:

• https://gitlab.inria.fr/jwintz/elpi
• https://gitlab.inria.fr/jwintz/elpi-vs-code-extension

TODO:

• Apply elpi syntax highlighting
• Embed dune build $(DUNE_OPTS) @doc output
• Add a regexp based validation mechanism
• Connection with gh-pages, through sphinx.ext.githubpages

---

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:

   pip install sphinx
   pip install in-place

To match the visuals used in the community (e.g. https://coq.inria.fr/distrib/current/refman/):

   pip install sphinx-rtd-theme

Extensions

This documentation can make use of the following plugins:

   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:

    make doc-sphinx

---

Playground

This page will be used to test hooks in order to run elpi on code snippets and inject its output within sphinx documentation sources.

Prerequisites

Before running the hooks, make sure to have elpi built locally:

   eval $(opam env)
   make build

It doesn't hurt to check that dune runs the locally built elpi correctly:

   dune exec elpi -- -h

Syntax

Elpi code blocks to be evaluated and injection from docs/base to docs/source are conventionally denoted in reStructuredText as .. elpi:: FILE and turned into:

.. literalinclude:: ../../tests/sources/chr.elpi
   :linenos:
   :language: elpi

The injection engine will:

• Retrieve all .. elpi:: directives for any rst source
• Change them into literalinclude in the generated source with relevant options
• Run dune exec elpi -- -test FILE on the FILE containing the elpi snippet, test or example.
• Capture its output (stdout & stderr)
• Create respective .. code-block:: console just after it to inject the captured console output

Result should look as follows:

   Parsing time: 0.000

   Compilation time: 0.004
   File "/home/jwintz/Development/elpi/tests/sources/chr.elpi", line 7, column 60, character 133: Warning: constant term has no declared type.
   File "/home/jwintz/Development/elpi/tests/sources/chr.elpi", line 11, column 8, character 319: Warning: constant len has no declared type. Did you mean std.length ?
   File "/home/jwintz/Development/elpi/tests/sources/chr.elpi", line 28, column 28, character 761: Warning: constant compatible has no declared type.

   Typechecking time: 0.154
   compat [term c1 (uvar frozen--501 []), term c0 (uvar frozen--502 [])] |- frozen--494 [
    c1, c0] arr (uvar frozen--495 [c0, c1]) (arr (uvar frozen--496 [c0, c1]) (uvar frozen--497 [])) , [
    term c3 (uvar frozen--499 []), term c2 (uvar frozen--498 [])] |- frozen--494 [
    c2, c3] arr (uvar frozen--498 []) (arr (uvar frozen--499 []) (uvar frozen--500 []))
   NEW [X0 = X1, X2 = X3] arr (X4 c0 c1) (arr (X5 c0 c1) X6) = arr X1 (arr X3 X7)
   1
   compat [term c0 bool] |- frozen--507 [c0] uvar frozen--508 [] , [term c1 (uvar frozen--509 [])] |- frozen--507 [c1] nat
   NEW [bool = X8] X9 = nat
   2
   compat [term c0 bool] |- frozen--514 [c0] uvar frozen--515 [] , [term c1 (uvar frozen--515 [])] |- frozen--514 [c1] nat
   NEW [bool = X10] X10 = nat
   compat [term c0 bool] |- frozen--520 [c0] uvar frozen--521 [] , [term c1 nat] |- frozen--520 [c1] nat
   NEW [bool = nat] X11 = nat

   Success:

   Time: 0.001

   Constraints:
    {c0} : term c0 bool ?- term (X12 c0) nat  /* suspended on X12 */ {c0 c1} : term c1 X13, term c0 X13 ?- term (X14 c1 c0) (arr X13 (arr X13 X6))  /* suspended on X14 */

   State:

Test Bed

.. elpi:: ../../tests/sources/accumulated.elpi

.. elpi:: ../../tests/sources/ackermann.elpi

.. elpi:: ../../tests/sources/chr.elpi

[gares]

awesome!

The main missing thing w.r.t. what we discussed is a

.. elpi:: file
   :assert: regexp

which would fail if the captured output does not match (and possibly be able to repeat this directive)

[jwintz]

Final preview before submitting MR on feature/doc: http://dream.inria.fr/elpi.

• https://gitlab.inria.fr/jwintz/elpi/-/commit/e7a3399e5674d3c639fcf190ac0a069abc056014
• https://gitlab.inria.fr/jwintz/elpi/-/commit/8ee20ba5db4f499306c6c12c531c5559ed373497

• Apply elpi syntax highlighting
• Embed dune build $(DUNE_OPTS) @doc output
• Add a regexp based validation mechanism
• Connection with gh-pages, through sphinx.ext.githubpages
• Search engine Ok (does not index the ocaml doc)

NOTE:

If neither distrib neither doc is specified, dune-release publishes both

• Github pages can be published using make gh-pages
• Whenever using dune-release publish change to dune-release publish distrib -> Update make release target defintion, please review

[jwintz]

Merge requested: #152.

[gares]

the preview looks good, but the test is somewhat wrong. The injection when the regex does not match should fail, and the command to build the doc exit non zero, hence the ci job fail. here it seems the injection successfully prints an error, which makes sense but is not how I plan to use the feature: I do not want to review the doc looking for red boxes.

I'll review the pr tomorrow, thanks!

[jwintz]

Alright, I didn't get the intent for the assertion at first.

So if it is a matter of integration through the examples, we can surely disseminate sys.exit(code) statements in the injection engine.

Also, sanity checks do not pass on the PR, which seems to be related to the artefacts' binaries we added on Friday for deployment. Not sure how to deal with that, as the branches seem to be in sync, I'll leave this to you.