jape.org.uk
| Host Site Selector |
|---|
| jape.comlab.ox.ac.uk |
| jape.org.uk |
(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.
(July 2005) You can now visit the Jape Community Wiki
The Windows implementation is now compiled rather than interpreted. This means it's faster, though a little larger, than before. It's also possible (if you want to hurt like me) to build it on a standalone Windows machine.
The Windows/Solaris/Linux installation process is now somewhat simpler and more reliable than hitherto.
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.
(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.
Jape is a work in progress.