Running a local copy of ProofDesigner

Download the jar wget http://www.cs.amherst.edu/~djv/pd/ProofDesigner.jar
Create html file with contents:

<HTML>
<HEAD>
<TITLE>Proof Designer</TITLE>
<SCRIPT language="JavaScript">
function showHTML() {
        outputWindow = window.open("", "", arguments[0]);
        outputWindow.document.open();
        var n = arguments.length;
        for (var i = 1; i < n; i++) {
                outputWindow.document.writeln(arguments[i]);
        }
        outputWindow.document.close();
}
</SCRIPT>
</HEAD>
<BODY>
<APPLET codebase="http://localhost:8000/"
archive="ProofDesigner.jar" code="ProofDesigner.class"
width="200" height="50" mayscript>
<PARAM name="symbolface" value="Lucida Sans">
<PARAM name="fontsize" value="12">
</APPLET>
</BODY>
</HTML>

Install icedtea-web for the Java applet to run
Start a server in the directory.

For anyone facing difficulties running applets in browser, it is because for the last four years or so NPAPI and what enables Java applets has been disabled in browsers such as Firefox and Chrome.

Also:

icedtea-web is not available for every platform
you need the JRE (Java Runtime Environment) to run applets
and in the JRE's settings (wherever it is in your system that you'll find the Java Control Panel), you need to allow your localhost as an exception for this to run

So, assuming you know what NodeJS is (and how to install it), and you are open with using an old browser to access a pretty unique piece of software, feel free to read the steps I took to make it work today (July 2020).

Keeping in mind that running applets in browser is now considered a security risk, that using old browsers is a security risk, and that following directions online blindly is also a risk, here is what I did for MacOS 10.14 (Mojave) if that helps anyone:

I followed the first two steps of this guide (downloading the JAR and creating the html page), but I changed the port of localhost to 8080 (thus getting codebase="http://localhost:8080/") and named the html file pd.html
I retrieved a version of Firefox which still uses NPAPI and allows for Java applets to run (52.0esr), by going to Mozilla's releases for that version and downloading the right version for my computer (in my case on MacOs 10.14, this one)
I saved that version of Firefox somewhere other than my usual install, because I want to use it only for Proof Designer
In order to retain that version one must make sure that it does not update, so I quickly went to Firefox preferences and under Advanced -> Update disabled auto-update

(for reference, on MacOS I also used LittleSnitch to block outgoing requests to mozilla's servers to prevent an update, if you have an equivalent for your platform that might help)

I installed the JRE for Java 8 for my platform (for example from Oracle)
I configured the JRE in the Java Control Panel (in MacOs under System Preferences -> Java) by going to the Security tab and adding a site to the exception list: http://localhost:8080/pd.html

Then, to serve the file pd.html to my localhost without much hassle I used whatever version of node I had (currently 10) and installed globally http-server by running npm install http-server -g. After going to the directory where the JAR and the HTML files are together, I could locally serve my files by running http-server ..
This means I could use a browser to access http://localhost:8080/

Now, using the Firefox 52esr and going to http://localhost:8080/pd.html, I was finally able to load the applet.

Keep in mind that the "Help" links in the applet won't work unless you've also downloaded the rest of the Proof Designer website (which you might want to do since it seems unmaintained), but otherwise you can find the help at the original website anytime.

Also worth noting that downloading everything locally isn't required to make this procedure theoretically work (just add the original website to the list of exceptions and use an old browser), but having everything locally might ensure you get to run it in the future if the website is down.

Hope that helps any other reader of "How to Prove it", which is a fantastic book by the way.

P.P.S: if you really know what you're doing, a one-liner to download the website without external links is wget --recursive --domains amherst.edu --page-requisites --html-extension --convert-links --no-clobber https://www.cs.amherst.edu/~djvelleman/pd/, and then if you use http-server from the root of the folder containing pd.html an add the whole localhost as an exception then you should get the exact website locally.

samrat/running_pd.org

Running a local copy of ProofDesigner

ckuma commented Jul 18, 2020 •

edited

Loading

samrat/running_pd.org

Running a local copy of ProofDesigner

ckuma commented Jul 18, 2020 • edited Loading

ckuma commented Jul 18, 2020 •

edited

Loading