The fundamental concepts of the Proofscape library – repos, libpaths, modules, etc. – are tightly coupled, and it is hard to define any of them without mentioning the others. This page tries to introduce them in a logical order.
Concretely, a Proofscape project is usually referred to as a “Proofscape repo,” because it
takes the form of a git repository. Within the repo are directories containing a few different
types of file, mostly consisting of “Proofscape files,” which have extension
and “rST files” (or “reStructuredText files”), which have extension
We’ll talk more about the role played by each file type in later sections.
In the Proofscape library, every entity (be it module, deduction, node, annotation, etc.) has an address, called a library path, or libpath for short. A libpath consists of segments separated by dots. Each segment is a string of alphanumerics and underscores, and is case-sensitive. It cannot begin with a number, and, except for certain special segments reserved for system use, does not begin with an underscore. Thus, a libpath may look something like this:
Each libpath is either absolute or relative. Absolute libpaths, as their name suggests, describe an entity’s location within the entire universe of possible Proofscape repos. Relative libpaths locate Proofscape entities relative to the module in which they appear.
Syntactically, absolute libpaths occur in only a couple of places in Proofscape modules, mainly in Imports. (They also occur when defining the versions at which one repo imports from another, a topic we cover later.)
The first three segments of an absolute libpath are called the host, owner, and repo segments. The host segment can only take on one of a small set of possible values:
test: (used in testing)
Libpaths starting with
bb are like URLs, in that they are
universally unique identifiers for Proofscape entities. They refer to objects
defined in Proofscape repos hosted at GitHub or BitBucket, under owners and
repos given, of course, by the owner and repo segments of the libpath.
_) in owner and repo libpath segments translate to
-) in owner and repo names at GitHub and BitBucket.
gh.pfsc_example.auth_tut is the libpath of the repo
hosted at https://github.com/pfsc-example/auth-tut.
The basic motivation for this rule is that GitHub usernames allow hyphens, but do not allow underscores. Furthermore, at least anecdotally, hyphens seem to be more conventional than underscores in repo names.
Strictly speaking, we needn’t have translated underscores to hyphens in repo names, or even in BitBucket owner names (where underscores are allowed); however, this would have made the rule harder to remember.
Libpaths starting with
lh are not universal, but instead simply point into
the directory structure of a local Proofscape installation. This offers
a lot of freedom, but also must be used carefully, because modules importing
lh libpaths are not portable.
test host segment is simply used for testing the
Except for the few places in Proofscape modules where absolute libpaths are required,
all other libpaths are interpreted as relative to the context in which they are used.
For example, if a deduction
Pf declares as its target the node
Thm.C (see, for example A deduction with a target),
Thm.C is being used as a relative libpath.
When you write a Proofscape module (see below), you must always ensure that relative libpaths can be
resolved, i.e. that the system can determine which object you are trying to point to.
For a relative libpath to be resolvable, its first segment (like
must point to an object that was either defined in, or imported into the
module (see Imports).
The various Data Types (deductions, annotations, etc.) that you can define in Proofscape are defined by what you write inside of the files in a Proofscape repo. Meanwhile the files and directories themselves define what we call Proofscape modules.
A Proofscape module is an abstract entity which is essentially a namespace: a place where you can define things, and give them names. A module also has its own name and libpath.
Modules can often harmlessly be confused with files, but really modules and files are not the same thing. A file is a concrete object that lives in your computer’s file system. A module is abstract, and, while it is often represented by a single file, it is also sometimes represented by a file and a directory in combination. These two forms of representation correspond to two types of module, which we call terminal and non-terminal.
A terminal module can have no further modules defined under it. It only defines contents. A non-terminal module can have one or more other modules defined under it. A non-terminal module may also, optionally, define its own contents.
The precise form of the file system representation of each type of module is as follows:
A terminal module is represented by a
rstfile. The contents of the module (deductions, annotations, Sphinx page, etc.) are defined in this file.
A non-terminal module is represented by a directory with a file called
__.pfscinside of it. Any modules defined under this one are also defined in or under this directory. The contents of the module, if any, are defined in the
__.pfscfile, which may be referred to as the module’s “dunder file” (the term “dunder” is borrowed from Python, and is short for “double underscore”).
Some aspects of Proofscape, such as its module system, were deliberately modeled after corresponding aspects of the Python programming language. If you’re familiar with Python, you may have already noticed some similarities in the module system. You’ll see another example when we talk about Imports.
B is defined immediately under non-terminal module
A – meaning that the filesystem
B lives in the directory representing
A – then
B is said to be
a submodule of
B is defined anywhere under non-terminal module
A – meaning that the filesystem
B lives in any directory at or below the one representing
A – then
said to be a descendant of
A an ancestor of
(If you prefer, descendants can be defined inductively in terms of submodules.)
In particular, submodules are descendants.
The names you choose for your
.rst files must consist entirely of
alphanumerics and underscores, and, except for dunder files
__.pfsc, must begin
with a letter (not a number or an underscore).
The names of the directories representing non-terminal modules must follow the same rules.
Libpaths for repos and modules#
Each Proofscape repo has a libpath, which is simply the three-segment absolute libpath
host.owner.repo that points to it, as indicated above.
Within a given repo
host.owner.repo, the libpath of each module corresponds directly to its
filesystem path, relative to the repo root directory. If we write the root directory as
., then a terminal module with relative filesystem path
has absolute libpath
Note that the file extensions
.rst are dropped, when we move to a libpath.
Because file extensions are dropped,
.rst files share a common namespace.
Therefore you are not allowed to have a file of each type with the same stem, within a given directory.
For example, you cannot have both
foo.rst in the same directory.
Meanwhile, a non-terminal module whose dunder file has relative filesystem path
has absolute libpath
The root module#
Every Proofscape repo must define a dunder file
__.pfsc in its root directory.
The file itself is called the repo’s root file, while the module it defines is called
the repo’s root module.
According to the rules stated above,
the absolute libpath of the root module is the same three-segment libpath
which we said was associated with the repo itself. This is the only time we will describe
two entities as having the same libpath. In a sense, only the repo’s root module really has
a libpath, while “the libpath of the repo” is really just a shorthand for “the libpath of the
repo’s root module”.
The root module of a given Proofscape repo will be important for things like declaring other repos on which the first one depends, as we will cover in a later section.
A Proofscape repo is expected to evolve, and be serially released under version numbers, like any software project. This is important because, when you release a Proofscape repo, others can build off of it by importing entities you have defined. If you published a proof in the form of a Proofscape deduction, I might import it and write an annotation that talks about that proof. If you then make subsequent changes, I still need to be able to import the version that I originally wrote about.
The three components – major, minor, and patch – of semver version numbers apply to Proofscape repos in intuitive ways. For example, a major increment should accompany breaking changes, like moving a deduction to a different libpath, or restructuring a deduction so that it no longer defines the same set of nodes; a minor increment should accompany the addition of new material; a patch increment should accompany fixes to typos and other minor errors.
Accordingly, an absolute libpath becomes a truly unique identifier when it has a version number
attached. There are two ways to attach a version number to a libpath. It can be appended
to the repo segment using an
@ symbol, resulting in a repo-versioned libpath, which
looks like this:
or it can be appended at the tail end, again using an
@ symbol, and resulting in a
tail-versioned libpath, which looks like this:
While it’s important to understand this, when working in PISE, the Proofscape Integrated Study Environment, you will only rarely need to work with versioned libpaths directly. A few times when version numbers will come up are as follows:
If you want to load a repo at a given version, you need to enter
host.owner.repo@versionin the text box in the library sidebar.
When defining your project’s dependencies in The root module, you have to declare the version at which you are taking each repo.
The content-loading URLs you can copy from the “PISE” menu contain (a special representation of) repo-versioned libpaths, but you don’t really need to know about this, since these URLs are automatically generated for you anyway.