Advanced Operation of the Proofscape ISE#
These instructions are for users who want to change the configuration of the ISE, or run it with a different graph database back-end. To simply run and use PISE, follow Basic Operation of the Proofscape ISE.
The deploy directory#
If you have run the ISE at least once (following the steps under Basic Operation of the Proofscape ISE),
then under your PFSC_ROOT directory you will find a subdirectory
called deploy. If not, it’s a good idea to make this directory manually now,
as it will be involved in advanced operations of PISE.
$ cd PFSC_ROOT
$ mkdir deploy
Configuration#
For home use#
If you are running PISE at home, for personal use, then you
can make configuration settings in the file PFSC_ROOT/deploy/pfsc.conf, so go
ahead and form that file now, if you have not already.
$ cd PFSC_ROOT/deploy
$ touch pfsc.conf
To set any variable, put a line in your pfsc.conf file of the form shown
in Listing 79.
VARIABLE_NAME=VALUE
Define as many or as few variables as you wish. Each variable has a default setting. Define exactly one variable per line.
Selected variable table#
While the complete list of configuration variables available in PISE is quite long, at this time only a few of the more relevant variables are documented here.
Variable name |
Description |
|---|---|
|
Number of milliseconds before autosave after last change in editor panels. Set to zero to turn off autosave. Default: Example: |
|
Policy for reloading open files from disk, when the app regains focus. Explanation: If you are editing source files in PISE, and then alt-tab away, it’s possible that you make changes to those same files, using another editor application. This variable controls how PISE behaves when you alt-tab back to it, and it discovers that the version of these files on disk differs from the version open in PISE. Possible values:
Default: Example: |
|
Policy for saving open files when the app loses focus. Explanation: If you are editing source files in PISE, and then alt-tab away, this controls whether PISE will automatically save all open files at this time. Possible values:
Default: Example: |
|
Set certain libpaths to be automatically trusted. Explanation: Any libpath equal to, or extending, any of the ones named here will be automatically trusted, meaning the user does not have to first grant trust through PISE. (See Trust settings.) Whether a module is trusted controls things like rendering of links and images in
Annotations,
and execution of Value: Comma-separated list of Absolute libpaths, each being at least two segments long. Example: |
For operation on the web#
If you are operating an instance of PISE on the web, you should familiarize
yourself with all of the config vars in the config.py file of pise/server,
and set these as environment variables before starting up your server processes.
The Graph Database#
pise-server uses a graph database to store indexing information. This
describes the connections between the various entities you define in pfsc
modules. For example, when you right-click a node in a proof diagram and
find available expansions, it’s the graph database (GDB) that’s supplying
this information.
The GDB that ships with the pise Docker image is RedisGraph,
which is an in-memory database. It’s lightweight, and should be adequate
for casual users. Background saves triggered after every write operation
dump the contents of the database to disk, so that everything is still there
the next time you start up the application.
However, using an in-memory database implies certain inherent limitations.
The amount of material you can index is limited by your computer’s available
memory. For casual applications this shouldn’t be a problem. For example,
indexing version 0.23.0 of the gh.toepproj.lit repo requires about
a third of a megabyte. That means you’d have to index 3000 times as much
material before the database would occupy 1 GB of memory.
Still, if you want to use a different GDB system, it’s easy to do. The
pise-server software speaks both Cypher and Gremlin, so it’s ready to
work in conjunction with a wide selection of GDB systems, such as Neo4j,
OrientDB, JanusGraph, and more.
Attention
Whichever GDB system you choose, it’s up to you to ensure you have a license to use it. Most vendors at least offer a free option for personal, home use. Many license their system permissively (such as under Apache 2.0). However, in all cases you must read the vendor’s website carefully, and go by what they say, not by anything you read here.
Essentially, all it takes to use a different GDB system with pise-server
is two steps:
Ensure the GDB is up and running.
Tell
pise-serverhow to connect to it.
The easiest way to achieve both of these things at once is to start up the
whole system using docker compose.
In the sections below, we guide you through writing yaml files for use
with docker compose, which you should save under The deploy directory.
Using JanusGraph#
Attention
Do not use any graph database system without a license. Visit the vendor’s website to learn more.
To use Proofscape with JanusGraph, you can save the following file as
PFSC_ROOT/deploy/pfsc_w_janusgraph.yaml, being sure to substitute your
chosen ``PFSC_ROOT`` directory both in this path and where
it occurs within the file.
version: "3.5"
services:
janusgraph:
image: "janusgraph/janusgraph:0.6.0"
pise:
image: "proofscape/pise:latest"
depends_on:
- janusgraph
ports:
- "7372:7372"
volumes:
- "PFSC_ROOT:/proofscape"
environment:
GRAPHDB_URI: ws://janusgraph:8182/gremlin
Note
Under its default configuration, JanusGraph operates as an in-memory database. If your goal is to achieve persistence to disk, you will need to configure JanusGraph accordingly. Instructions can be found in their docs.
Next, follow the instructions under Starting up.
Using Neo4j#
Attention
Do not use any graph database system without a license. Visit the vendor’s website to learn more.
To use Proofscape with Neo4j, you can save the following file as
PFSC_ROOT/deploy/pfsc_w_neo4j.yaml, being sure to substitute your
chosen ``PFSC_ROOT`` directory both in this path and in the three places where
it occurs in the file.
version: "3.5"
services:
neo4j:
image: "neo4j:4.0.6"
volumes:
- "PFSC_ROOT/graphdb/nj/data:/data"
- "PFSC_ROOT/graphdb/nj/logs:/logs"
environment:
NEO4J_AUTH: none
pise:
image: "proofscape/pise:latest"
depends_on:
- neo4j
ports:
- "7372:7372"
volumes:
- "PFSC_ROOT:/proofscape"
environment:
GRAPHDB_URI: bolt://neo4j:7687
Next, follow the instructions under Starting up.
Starting up#
Once you have saved a docker compose yaml file, you can start up the system.
(First: If you are currently running the ISE as described earlier in this
guide, you should stop it now!)
Then, in the PFSC_ROOT/deploy directory, start the system with
docker compose -f YAML_FILE up
substituting the name of the yaml file you saved, for YAML_FILE.
You should see output in the terminal indicating the state of the servers you
are running. When they are stable, navigate your web browser to localhost:7372
to load the ISE.
Shutting down#
When you are finished using the ISE, you can shut the system down by returning to the terminal where you started it up, hitting Ctrl-C, then running
docker compose -f YAML_FILE down
to clean up all resources.
Alternatively, the system can be started in detached mode, using
docker compose -f YAML_FILE up -d
(note the -d switch at the end), and then Ctrl-C is not necessary,
just the docker compose down command.