`rst` files#

Files with .rst extension, which can be called “rST files,” or “reStructuredText files” are one type of file in which you can define Proofscape modules (the other being pfsc files).

Historically, Proofscape supported only pfsc files for a long time, before rst files were eventually introduced so that you could have a handy way to define Sphinx pages. However, these files are not some kind of second-class citizen; every rst file defines a first-class Proofscape module, just like any pfsc file does. (This is one reason why it’s important to maintain the conceptual distinction between a file and a module.)

What an `rst` file does in Proofscape#

The main job of an rst file in Proofscape is the same as its job in any HTML Sphinx project: to define a single page of HTML. It uses reStructuredText to create section headings, lists, tables, asides, boldface and italics, etc., as well as to enrich the page with one or more tables of contents (which can be in-page, and/or in a sidebar).

However, in Proofscape, the basic rST language is extended by certain custom roles and directives, allowing you to do two extra things, beyond just defining a page of HTML:

The pfsc directive allows you to embed the syntax of pfsc files within an rst file, meaning you can do everything here that you can do in a pfsc file.
Other roles and directives (covered under Sphinx Pages) allow you to define Widgets in your HTML page, just as you can do in Annotations.

The Sphinx page#

The HTML page defined by an rst file is another one of the basic Data Types of Proofscape, and it is called a Sphinx page.

Just as deductions, annotations, and the other Proofscape data types have names, every Sphinx page has a name; however, you do not choose it. The name of every Sphinx page is _page. This becomes relevant when determining the libpath of a Sphinx page.

The `pfsc` directive#

rST files are made able to interact with the other objects defined in Proofscape via the rST extension mechanism of roles and directives.

Most of these custom roles and directives allow you to define Widgets in Sphinx pages, just as you can in annotations, and their syntax is covered in Sphinx Pages.

However, there is one custom directive, the pfsc directive, which is fundamental to understanding how rST files fit into the Proofscape library, so we cover that here.

In the body of a pfsc directive you can place arbitrary pfsc module syntax. Usage therefore looks something like this:

.. pfsc::

    # Anything you can write in a ``pfsc`` file can go here.
    # E.g.:

    from some.module import Pf as Pf3

    deduc X1 of Pf3.A20 {
        asrt A {
            en = "This provides some clarification."
        }
        meson = "Pf3.A20 by A"
    }

Most importantly, this provides a way to perform Imports in rst files. By importing objects under a pfsc directive, you can then reference those objects when you define widgets, using the various widget roles and directives.

It also means that any Proofscape data type (deduction, annotation, etc.) that can be defined at the top-level of a .pfsc file can also be defined in the body of a pfsc directive inside an .rst file.

You can use as many pfsc directives as you want, within a single .rst file. They are evaluated in the order given.

Libpaths#

Sphinx pages#

Sphinx pages can only be defined in terminal modules (see Modules), with filenames like index.rst or foo.rst, and, as a data type, each Sphinx page always has the name _page (see above), so a Sphinx page will always have an absolute libpath such as:

host.owner.repo.index._page, or
host.owner.repo.dir1.dir2.dir3.index._page, or
host.owner.repo.dir1.dir2.dir3.foo._page,

etc.

Widgets#

Widgets defined within a Sphinx page are thought of as elements of the page, and therefore their libpaths extend that of the page. For example, a widget named w01 inside a Sphinx page might have libpath host.owner.repo.dir1.dir2.dir3.foo._page.w01.

Other objects#

Any objects defined under a pfsc directive in an rst file are siblings of the Sphinx page the file defines. They are top-level entities of the module, just as _page is. Thus, an rst file defining the Sphinx page host.owner.repo.dir1.dir2.dir3.foo._page could also define a deduction with libpath host.owner.repo.dir1.dir2.dir3.foo.Thm.

rst files#

What an rst file does in Proofscape#