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 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-server
how 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
.
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, you can make that directory manually now.
This is a good place to store yaml
files for use with docker compose
.
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.
Server processes#
When you start up the proofscape
Docker container, there are two server
processes running inside of it:
pise-server
redis
UNDER CONSTRUCTION…….