Library Basics#
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.
Repos#
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 .pfsc,
and “rST files” (or “reStructuredText files”), which have extension .rst.
We’ll talk more about the role played by each file type in later sections.
Libpaths#
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 libpath segment is a string of characters obeying the following rules:
Composed of alphanumerics and underscores
Case-sensitive
Cannot begin with a number
Does not begin with an underscore, except for certain special segments reserved for system use
The segments
true,false, andnullare illegal (to avoid collisions in Proofscape-flavored JSON).
Thus, a libpath may look something like this:
I.like.pi_3_14
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.
Absolute libpaths#
Syntactically, absolute libpaths occur in only two places in Proofscape modules: Imports, and Dependency declarations.
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:
gh: GitHubbb: BitBucketlh: localhosttest: (used in testing)
Libpaths starting with gh or 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.
Important
Underscores (_) in owner and repo libpath segments translate to
hyphens (-) in owner and repo names at GitHub and BitBucket.
For example, 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
from lh libpaths are not portable.
Finally, the test host segment is simply used for testing the
Proofscape software.
Relative libpaths#
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
called Pf declares as its target the node Thm.C (see, for example A deduction with a target),
then 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 Thm in Thm.C)
must point to an object that was either defined in, or imported into the
module (see Imports).
Modules#
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
pfscorrstfile. 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”).
Note
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.
Submodules#
If module B is defined immediately under non-terminal module A – meaning that the filesystem
representation of B lives in the directory representing A – then B is said to be
a submodule of A.
If module B is defined anywhere under non-terminal module A – meaning that the filesystem
representation of B lives in any directory at or below the one representing A – then B is
said to be a descendant of A, and A an ancestor of B.
(If you prefer, descendants can be defined inductively in terms of submodules.)
In particular, submodules are descendants.
Filenames#
The names you choose for your .pfsc and .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
./dir1/dir2/dir3/foo.pfsc, or./dir1/dir2/dir3/bar.rst
has absolute libpath
host.owner.repo.dir1.dir2.dir3.foo, orhost.owner.repo.dir1.dir2.dir3.bar, respectively.
Note that the file extensions .pfsc and .rst are dropped, when we move to a libpath.
Important
Because file extensions are dropped, .pfsc and .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.pfsc and foo.rst in the same directory.
Meanwhile, a non-terminal module whose dunder file has relative filesystem path
./dir1/dir2/dir3/__.pfsc
has absolute libpath
host.owner.repo.dir1.dir2.dir3.
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 host.owner.repo
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 is a place where certain important definitions can be made. For example, this is where you can declare the other repos on which the given one depends. See Dependency declarations.
Versions#
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, and general word-smithing.
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:
host.owner.repo@version.further.segments.go.here
or it can be appended at the tail end, again using an @ symbol, and resulting in a
tail-versioned libpath, which looks like this:
host.owner.repo.further.segments.go.here@version
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 couple of times when they 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.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.
Dependency declarations#
Proofscape projects are meant to be able to benefit from each other, and therefore you are able to make Imports from other repos into your own. In order to do that, you have to declare the version number at which you are taking each external repo.
You do this by defining a dependency declarations object in The root module.
This is simply an object, assigned to the name deps, in which each key is the absolute
libpath of a repo, and the value is a version string indicating
the version at which you are taking that repo.
For example, a project importing from two of the Toeplitz Project repos might define a dependency declaration like this:
deps = {
"gh.toepproj.lit": "v0.23.1",
"gh.toepproj.ex": "v0.24.0",
}
Version strings#
Numbered versions#
Most of the time, you will be importing a numbered release of another repo, meaning
you are taking it at a specific, numbered version. For example, in Listing 38,
we are taking gh.toepproj.lit at version 0.23.1, and gh.toepproj.ex at version 0.24.0.
In order to do this, we use a string starting with a v (for “version”) as in
"v0.23.1" or "v0.24.0".
The general format of a numbered version string is:
vMAJOR.MINOR.PATCH
Work in progress#
At other times, you may be simultaneously developing two or more Proofscape repos, with one
importing from another. When you want to import from another repo in its current, working state,
as it stands on disk on your computer, then you import it at a version called "WIP", for
“work in progress”. In a dependency declaration, that should look something like this:
deps = {
"gh.example.MyProject": "WIP",
}