Basic Operation of the Proofscape ISE#

Quickstart#

For those who already have Docker and know how to use it, you can run PISE in one line. After making the ~/proofscape directory, just run:

docker run --rm \
  --name=pise \
  -p 7372:7372 \
  -v ~/proofscape:/proofscape \
  alpinemath/pise:latest

Give the server a moment to start up, and then navigate your browser to localhost:7372.

Caution

The command given above will write to the directory ~/proofscape on your computer, so don’t run it unless you’re sure!

Full Instructions#

Running the Proofscape ISE is easy. After following the steps on this page, you can start it up with the click of a button in Docker Desktop, or at the command line if you prefer.

Preparation#

These preparatory steps only have to be performed once, before the first time you run the ISE.

  1. Install Docker Desktop, if you haven’t already.

  2. Choose a place in your filesystem for Proofscape to live. We recommend ~/proofscape, but you can choose any directory you want. For the remainder of this guide, we will refer to the directory you choose as PFSC_ROOT.

    When making your choice, bear in mind that all of your Proofscape content repos will live under PFSC_ROOT/lib. So, be sure to choose a convenient location.

    If the PFSC_ROOT directory doesn’t exist yet, make it now.

  3. Pull the Docker image, by opening a terminal and entering the command:

    docker pull alpinemath/pise:latest
    

    The image may take several minutes to download, depending on the speed of your internet connection.

Running the ISE#

Once you’ve performed the Preparation steps listed above, you can run the Proofscape ISE app. You can either do this from the terminal, or from Docker Dashboard. Choose whichever you prefer, and follow the steps in the corresponding section below.

From the Terminal#

Start the app by entering the following command in the terminal, making sure to substitute your chosen directory for ``PFSC_ROOT``:

docker run --rm \
  --name=pise \
  -p 7372:7372 \
  -v PFSC_ROOT:/proofscape \
  alpinemath/pise:latest

You should see some logging output. When you see a line containing INFO success: pfsc_web entered RUNNING state, you can navigate your web browser to localhost:7372 and the Proofscape ISE should load. We recommend using either Firefox or Chrome.

From Docker Dashboard#

If instead you prefer to start the app from Docker Dashboard, you can proceed as follows:

  1. From the Docker whale menu, select “Dashboard”.

  2. In the Dashboard, select the “Images” tab (on the left).

  3. Under local images, find alpinemath/pise:latest.

  4. Hover over the row for alpinemath/pise:latest, and click the “Run” button on the right.

  5. Click “Optional Settings”.

  6. For Container Name, enter pise

  7. Under Ports, in the “Local Host” box on the left, enter 7372

  8. Under Volumes, in the “Host Path” box on the left, click the ... symbol, and select the directory you chose to be PFSC_ROOT.

  9. Again under Volumes, in the “Container Path” box on the right, enter /proofscape

  10. Click the “Run” button to start the app.

The Dashboard should now automatically go back to the “Containers / Apps” tab, and you should see pise in the list of running containers. It should have a green box next to it, indicating that it’s running.

Hover your mouse over the row for the pise container, and you should see a set of buttons on the right. The first button looks like an arrow pointing out of a box, and if you hover it says “OPEN IN BROWSER”. Click this button, and the Proofscape ISE should load in your web browser.

If you prefer to open the ISE manually, you can always type localhost:7372 in any web browser’s address bar. We recommend using either Firefox or Chrome.

Stopping and Restarting the ISE#

When you’re finished using the ISE, you may want to stop the application just to free up memory on your computer. If you use it frequently, you may prefer to keep it running all the time.

From the Terminal#

If you started the ISE from the terminal using the command given in the previous section, you can now stop it by going back to the terminal and pressing Ctrl-C.

If you prefer to keep the app running all the time, then it is better to start it in “detached” mode, using:

docker run --rm -d \
  --name=pise \
  -p 7372:7372 \
  -v PFSC_ROOT:/proofscape \
  alpinemath/pise:latest

(note the added -d in the first line).

When the app is running in detached mode, it can be stopped with:

docker stop pise

From Docker Dashboard#

To stop the ISE app from Docker Dashboard, hover your mouse over the row for the pise container in the “Containers/Apps” tab, and find the “Stop” button on the right. Click this to stop the app.

The “Stop” button now becomes a “Start” button you can use to restart the app any time you want.

There is also a “Delete” button (trash can icon). While there is no need to click this, there is also no need to be afraid of it. This will not delete your work. It just deletes the stopped app container. If you haven’t used the ISE for a long time and want to clean up your Dashboard, feel free to click this delete button. If you then want to start the app again, you’ll have to once again follow the instructions under Running the ISE.

Upgrading#

From time to time, a new version of the Docker image will be released. By default, PISE is configured to check for updates automatically, and it will alert you when a new version is available. If you want, you can turn this feature off (from the “PISE” menu), and simply check for updates manually, by visiting https://hub.docker.com/r/alpinemath/pise.

When it’s time to upgrade, you can follow these steps:

  1. If you’re currently working in PISE, first save all your work, close everything, and quit.

  2. Stop the PISE docker container, if it’s currently running.

  3. Go to the command line, and remove the existing image and pull the new one, with:

    docker rmi alpinemath/pise:latest
    docker pull alpinemath/pise:latest
    

That’s it. Now you can follow the instructions in Running the ISE to get back up and runnning again.