Jape

Binary Distributions for Linux, Windows, and OS/X

Installing an OS/X Distribution

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 10.8 it is necessary to reassure the system that you know what you are doing the first time you run it. If the DAFT (Dealing with Apple Frustrations Tax) were merely monetary then we might be prepared to buy the right to sign Jape. (see Recent News of 17th December 2012)

Installing a Windows or Linux Distribution

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.

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 you should make sure you have a recent java installation installed, then right-click on the jar file, and select the Open with ... java ... menu entry.

Windows and Windows Shortcuts

The Windows distribution sometimes lags superficially behind the Linux and OS/X distributions because of problems with the (OCAML) tool chain on Windows. An up-to-date distribution will be found here. It has been tested on 32 bit Windows XP, and 64 bit Windows 7.

((Note added by BS: 5th May 2014. As far as I can tell the installer now makes appropriate shortcuts to the executable jar file, but the shortcut-making machinery is architecture-dependent. If you have any difficulty with shortcuts made by the installer, or if the installer appears to become unresponsive, then please let me know -- giving precise details of the operating system and architecture of the machine you are using. On Windows 7 I have evidence that making a shortcut (right-click>make shortcut) to the Jape.jar file in the installation distribution gives a working shortcut.))

Recent News

(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)

(5th April 2014) (v7_d11) Fixed a potentially confusing error message reporting lack of a selected conclusion in some theories. (BS)

(17 December 2012) (v7_d10) It seems that, on OS/X 10.8 (Mountain Lion), Gatekeeper used to insist that Jape is some sort of toxin that might mess up your lovely Mountain Lion.

The build in jape_v7_d10_g.dmg should solve that problem; though all Lions will continue to moan the first time you run Jape.

Many thanks to James Baker of Cambridge University for doing the critical research. This will be incorporated into all future distributions. (Bernard Sufrin)

(27 July 2012) v7_d10 is the latest release. Mousewheel scrolling has been added, and the appearance of ''givens'' in proofs of a derived rule is more suggestive of them being clickable. (29 July) The 32-bit installation was compiled on a 32-bit Ubuntu 12.04 and was tested there and on a 32-bit Ubuntu 11.10 but not elsewhere. Please let me know if it fails to function on other 32-bit Linux installations. (Bernard Sufrin)

(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)

(March 2012) v7_d6_4a is a binary distribution for Linux and for Snow Leopard and Lion OS/X that corrects a very slight bug in the transitive-style display of proofs and derivations. The bug affected only two theories: the trfunctions variant of functional programming, and the operational semantics of the lambda calculus. (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)

Announcements and Tips

Bernard has developed a lightweight multiplatform Unicode-capable editor suitable for Jape theories. This is intended for people who find emacs or jedit too heavy or clumsy when working with Unicode.

Manuals

Resources

Contact

Email information about bugs, omissions and infelicities to



Old News

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