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.

$ mkdir deploy


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.

Listing 79 Format for defining a variable in pfsc.conf#

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



Number of milliseconds before autosave after last change in editor panels.

Set to zero to turn off autosave.

Default: 5000



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:

  • auto: Silently overwrite the in-app version with the on-disk version.

  • none: Silently overwrite the on-disk version with the in-app version, upon next save. (Dangerous!)

  • compare: Bring up a comparison dialog, and make the user decide which version to keep.

Default: compare



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:

  • 0: Do not save all on app blur.

  • 1: Do save all on app blur.

Default: 1



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 build code in Display Widgets.

Value: Comma-separated list of Absolute libpaths, each being at least two segments long.

Example: PFSC_TRUSTED_LIBPATHS=gh.MyGitHubUsername,gh.MyFriendsGitHubUsername

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


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:

  1. Ensure the GDB is up and running.

  2. 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. 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#


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"
    image: "janusgraph/janusgraph:0.6.0"
    image: "proofscape/pise:latest"
      - janusgraph
      - "7372:7372"
      - "PFSC_ROOT:/proofscape"
      GRAPHDB_URI: ws://janusgraph:8182/gremlin


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#


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"
    image: "neo4j:4.0.6"
      - "PFSC_ROOT/graphdb/nj/data:/data"
      - "PFSC_ROOT/graphdb/nj/logs:/logs"
      NEO4J_AUTH: none
    image: "proofscape/pise:latest"
      - neo4j
      - "7372:7372"
      - "PFSC_ROOT:/proofscape"
      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.