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 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:

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 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:

  • gh: GitHub

  • bb: BitBucket

  • lh: localhost

  • test: (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 pfsc or rst file. 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 __.pfsc inside 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 __.pfsc file, 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, or

  • host.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 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.

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.

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 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@version in 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.