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#

pfsc-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, at time of writing, indexing the full gh.alpinemath.histarch repo requires about a quarter of a megabyte. That means you’d have to index 4000 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 pfsc-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) so that you can use it in just about any way you wish. However, in all cases you must read the vendor’s website carefully, and go by what they say, not by anything we say here.

Essentially, all it takes to use a different GDB system with pfsc-server is two steps:

  1. Ensure the GDB is up and running.

  2. Tell pfsc-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.

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: "alpinemath/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: "alpinemath/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:

  • pfsc-server

  • redis

UNDER CONSTRUCTION…….