Site last edited on 26 October 2019 at 18:57, (BS)
To install an OS/X distribution you should open the .dmg
file, thereby mounting the distribution volume. The just copy Jape.app
to an applications folder and examples to a convenient place before
dismounting the distribution volume. It seems that, because Jape is an unsigned application, on OS/X 10.7 (and subsequent versions) it is necessary
to reassure the system that you know what you are doing the first time you run it. This may require
you to temporarily adjust your security & privacy settings (on the General tab) to allow
applications downloaded from "anywhere" to run, or to give specific permission for Jape to run. If the DAFT
(Dealing with Apple Frustrations Tax) were merely monetary then we might be
prepared to buy the right to sign Jape.
To install a Linux or Windows distribution you should run the Install...jape.jar file
it comes in using the appropriate platform method for
running a jar file. Installation takes no more than 15 seconds on a lightly-loaded machine.
On machines with either of these operating systems you should make sure
you have an appropriately recent java (jre or jdk) installed beforehand.
It is never appropriate for you to unpack the
.jar file, but it turns out that certain file-archiving software on
these operating systems tell the operating system that .jar
files are archives, and that opening means unpacking. On a Linux
machine the way round this is to java -jar Install...jape.jar
from a terminal window. On a Windows machine right-click on the
jar file, and select the Open with ... java ... menu entry.
We regret that we are only able to build 64-bit distributions for Windows, for I only have access to a 64-bit Windows 7 installation. I would be interested to learn of successful operation of the 64-bit distribution on Windows 8, and of of successful builds for 32 bit and/or XP installations.
As far as we can tell the installer now makes appropriate shortcuts to the executable jar file, but the shortcut-making machinery is architecture-dependent and can be fragile. If you have any difficulty with shortcuts made by the installer, or if the installer appears to become unresponsive, then please let us know -- giving precise details of the operating system and architecture of the machine you are using. On Windows 7 we have evidence that making a shortcut (right-click>make shortcut) to the Jape.jar file in the installation distribution gives a working shortcut.
(April 2018) Added Materials to support Bernard's Oxford 10-lecture "Introduction to Formal Proof" course at Oxford.(BS)
(March 2017) Revised natural deduction manual. (RB)
(2nd November 2014) (v7_d14) 32-bit Linux distribution added. (BS)
(1st October 2014) (v7_d14) Proof engine can now reload proofs over N-ary relations properly. (RB)
(17th April 2014) (v7_d13) Better help menu; theories can add their own help in the proof window. (BS)
(5th April 2014) (v7_d12) Fixed two more confusing error messages consequent on double-clicking in inappropriate places. (BS)
(July 2012) The public domain name for this site is now japeforall.org.uk. (Bernard Sufrin)
(July 2012) There's a Facebook group for Jape, called "Jape". Ask to join. As I write this I see that there's also a Facebook page for (Bernard Sufrin)
(September 2011) The domain name jape.org.uk was kidnapped while its registration was being transferred between Bernard and Richard. We are not minded to pay the kidnappers' ransom; so until we can find another euphonious domain name, we will maintain this, slowly-changing, site. (Bernard Sufrin)
Bernard developed (in about 1995) a lightweight multiplatform Unicode-capable editor suitable for Jape theories as well as general text. This was intended for people who found emacs or jedit too heavy or clumsy when working with Unicode. The editing landscape has changed a lot since then, but Bernard still uses Dred! Documentation is here, and Linux/Windows and OS/X versions are available.
(November 2009) Tiger vs. Leopard. As a convenience, I've put the Tiger build together with examples in the file BUILDS/v7_d6_4/TigerJapeWithExamples.zip. To useit: unzip it somewhere, then doubleclick the Jape.app the resulting Jape directory contains, then click on File/Open new theory ..., then navigate to the theory you want to use. (Bernard Sufrin)
(16th March 2009) Tiger versus Leopard. It seems that it is possible to build Jape on Mac OS 10.4 (Tiger) with a modern version of OCaml. Bernard Sufrin did it. The version you get also runs on 10.5 (Leopard). If you have trouble running Jape on Tiger, take the current binary distribution and replace Jape.app with the Tiger-built version.
(2nd Feb 2009) Mac OS X stuff again (sigh!). Jeff Lindstrom pointed out that (a) Jape doesn't run on OS X 10.4 and (b) it doesn't even build on 10.4. I'm working on the problem. Meantime, there's a new how-to-build file for OS X which acknowledges the problem and at least tells you what to do with JarBundler.
(20th Jan 2009, v7_d6_4) When I updated from Java 1.4 to 1.5 I tried to go polymorphic (Java generic). This introduced some bugs into the disproof mechanism, which I didn't notice till I started teaching it this winter (two years after the event). I fixed most of those bugs, but there's still one on Mac OS X: drags can sort of stop halfway through their life. It has to do with the mouse wheel: if you move it during a drag (easy to do!) then the drag stops halfway and oh dear Jape can't recover. I've reported the bug to Apple.
(5th Jan 2009, v7_d6_3) When writing files, Jape didn't hint that saved proof files should end with .jp and postscript copies of a proof should end with .ps. Now it does. It took so much hackery that I decided to release it. Still includes the 10.5 release 2 hack/bugfix for OS X (see below). The OS X release is v7_d6_3a, because I realised I'd made a mistake in the first version, and corrected it.
(3rd Dec 2008, v7_d6_2) For some reason, Java includes a close box in a dialog(ue) window. This is bonkers, hard to deal with, and it used to cause Jape to become very confused. Jape now doesn't allow the user to close a dialog(ue) box unless either there is a single OK button, or there's a Cancel button: in the first case close means OK; in the second it means Cancel. In all other cases (I hope) you get a moany response. Also fixed some infelicities in greyening/blackening formulae in box-and-line proofs. This release will work on MacOS X -- i.e. it includes the 10.5 release 2 hack/bugfix. There are also some changes to the Natural Deduction Conjectures panel: I took out some redundant brackets to emphasise the need to indentify principal operators. (Moan to Richard if it screws up your teaching.)
(9th Oct 2008, v7_d6_1_10point5r2) Mac OS X. If, like me, you've installed Java 10.5 release 2, then recent Jape releases (v7_d6 and v7_d6_1) have stopped working. It seems Apple have screwed something up in the Java launching mechanism (see this Apple support discussion). This special release, just for Mac OS X victims like me, hacks round that problem.
(20th May 2008, v7_d6_1) Linux, Windows and Mac OS X. Corrected more bugs in Hoare logic encoding (the same as in February, actually, but just in more places). And a slight improvement in selection: it will now allow a single text selection to direct a command, instead of insisting that you select the formula as well.
(18th Feb 2008, v7_d6) Linux, Windows and Mac OS X (including Leopard). Corrected some source bugs, so put up a corrected source distribution (if you took it between 13th Feb and 18th, sorry but you'll have to get it again).
(13th Feb 2008, v7_d6) Minor bug fixes in Hoare logic, plus a way of stopping multiple hypothesis selections in theories that can't understand it (e.g. sets). Ready now for Mac OS X (including Leopard) and Windows; Linux real soon now.
(1st Dec 2007) PROBLEMS WITH JAVA ON MAC OS X 10.5 (Leopard). I can't build a properly-working Jape GUI on Leopard -- so no bug fixes for Mac for a while.
(13th Sept 2007, v7_d5_1) Better treatment of conjectured rules and theorems (see RELEASENOTES). And universal binary for the Mac faithful.
(7th Sept 2007, v7_d4_13) Bug fixes: reloading proofs doesn't reset STRUCTURERULE settings unless it has to; now reads CRLF files separators correctly on non-Windows boxes. (Not compiled for Mac PowerPC)
(24th May 2007, v7_d4_12) For Intel Mac users only (same as v7_d4_12, but compiled for the Intel processor).
(15th August 2005, v7.d4.11) bugfixes to do with rerunning proofs of derived rules (thanks to Stefano Mannino, Genova, for the bug report), and incorporated Stefano's bug fix to the Java interface.
(25th April 2005) Another glitch in the Unix installer removed. Expect a period of silence!
(17th April 2005) Dred -- a lightweight editor suitable for editing Jape theory files has been released.
(2nd April 2005) A glitch in the Unix installer and a couple more garbled theoryfiles have been corrected. Engine and GUI same as in the 20050330 release.
(30 March 2005) Small theory corrections. Three theory files needed small corrections, and this didn't seem to warrant making a new distribution. Download the tar archive corrections-to-v7_d4_6.tgz from the 20050322 folder and unpack it in the installation directory after you install Jape.
(22 March 2005) New Release. This release (v7.d4.6) brings Jape in line with Richard's forthcoming book. A very nasty bug (blush!) in the natural deduction encoding (I2L.jt) has been fixed. (You could evade the privacy condition on quantifier rules.) The Hoare Logic section has been improved, and the drag-n-drop interface to multiplicative theories has been resuscitated.
(May 2004) Jape theory files now use Unicode. You may use any of the conventional Unicode encodings (UTF8, UTF16, ...). Support for transcoding existing theories in the old Konstanz or Laura encodings is provided in the release.
We've released the Jape source. Don't ask why it took so long; definitely don't ask why the engine is such a complicated mess; just enjoy the liberty to browse through our dirty washing. And contribute, if you wish, to tidying it up. We'd like it if you sent your improvements back to us to be incorporated in future releases, of course. (We may soon put Jape on an open-source site; we haven't decided which; advice welcome.)
The Jape implementation has been ported (by Richard Bornat) from SML of New Jersey to OCAML, and all versions now use the same front-end, namely Richard's Java-written GUI.
Implementations are currently available for Mac OS X, Linux (x86), and Windows (2K, NT, XP). We used to distribute for Solaris, but we ran out of machines on which we could build.
The distributions are around 1MB in size. Java is built into MacOSX; for other OSs you will need to have a functioning Java 2 implementation (preferably Sun's JDK or JRE, version 1.5.0 or later) before you can do the installation. Once you have one of these, installation is done by executing a jar file -- a one-command operation on Unixoid systems and a one-click operation on Windows.