News
- 2009 September 2 --
Mac OS X 10.6 (Snow Leopard) and Tarski's World
There is an incompatibility between Tarski's World 6.x and Mac OS 10.6 (a.k.a. Snow Leopard). We plan to release a new version of Tarski's World as soon as possible, but there is a workaround. The issue is that Tarski's World assumes that Java 1.4.2 is installed, and Snow Leopard does not include this version of Java. The workaround is to fool Snow Leopard into believing that 1.4.2 is present, without actually installing it. Use of an administrator account is required to install this workaround. (Under Accounts in System Preferences, the account would have the Allow user to administer this computer box checked.) Here's what to do:
- Open the Terminal application found in /Applications/Utilities
- Paste the following one-line command into the window, and type return or enter.
sudo ln -shfv CurrentJDK /System/Library/Frameworks/JavaVM.framework/Versions/1.4.2
Notes:- This comand creates a file called 1.4.2 in the folder /System/Library/Frameworks/JavaVM.framework/Versions/. This is where Tarski's World expects to find Java 1.4.2, and the file indicates that it is present. When Tarski's World looks for what it needs, it will then be directed to CurrentJDK.
- sudo executes commands as an administrator. To elevate your privileges to that of an administrator, you will need to provide your password. (If you do not have access to an administrator account, you will have to ask someone who does to install this workaround.)
- If you have never used the sudo command before, you might see a warning, which you should read and understand.
- More information about these commands can be found by typing man sudo, man ln, or man man into the Terminal window.
- Launch Tarski's World, which should now work.
- If Tarski's World does not now work, please open the Console application (also in /Applications/Utilities), and send us any messages from Tarski's World that appear there.
- Quit Terminal.
- 2007 August --
LPL 2.5 available for download
LPL 2.5 consists of: Boole 2.5, Fitch 2.5, Submit 2.5, Tarski's World 6.5
Submit 2.5 works for Mac OS X 10.4 and Java 2 Standard Edition (J2SE) 5.0.
Fitch 2.5 for Mac OS X fixes a problem where constructing a subproof sometimes caused Fitch to freeze and become unusable.
- 2007 March --
Submit issue for Mac OS X 10.4 and J2SE 5.0
Submit 2.4.4 (and earlier) for Mac OS X 10.4 is incompatible with Java 2 Standard Edition (J2SE) 5.0. Submit will quit when sending a submission to be graded. Until there is a fix for this problem, the workaround is to run:
/Applications/Utilities/Java/J2SE 5.0/Java Preferences
and in the section that says "Java Application Runtime Settings", drag J2SE 1.4.2 (or the latest version prior to 1.5) to be at the top of the list. (This is in the lower part of the window, where a list is shown, not in the upper part where there are items with radio buttons.) Save the preferences, and then try Submit again.This has the effect that all Java applications on your system will use the older version of Java. Likely this will have no noticable effect. (Those programs using an even older version of Java, prior to the update, will continue to do so.) An issue might arise if you install an application that requires the new version of Java. In this case we can only suggest that you change the preference before running that application (or before running Submit, if you prefer).
- 2006 November -- LPL 2.4.3 released
LPL 2.4.3 consists of: Boole 2.4.2, Fitch 2.4.2, Submit 2.4.2, Tarski's World 6.4 (and Tarski's World 5.7)
- 2006 September -- Tarski's World 6.3 bug
There is a bug in Tarski's World 6.3 which prevents it from opening files containing blank lines. Until we complete the preparat ion of a new version, the work around is to downgrade to Tarski's World 6.2.
- 2006 March -- LPL 2.4.1 released
Windows LPL 2.4.1 consists of: Boole 2.4.1, Fitch 2.4.1, Submit 2.4.1, Tarski's World 6.2 (and Tarski's World 5.7)
Macintosh LPL 2.4.1 consists of: Boole 2.4, Fitch 2.4, Submit 2.4, Tarski's World 6.2 (and Tarski's World 5.7)
- Windows LPL 2.4.1 applications handle better non-Western characters in the filesystem.
- Mac LPL 2.4.1 installer fixes problems with installing on some non-English Mac OS.
- Tarski's World 6.2 fixes a printing bug in 6.1
- 2005 September 19 -- LPL 2.4 released
LPL 2.4 consists of: Boole 2.4, Fitch 2.4, Submit 2.4, Tarski's World 6.1 (and Tarski's World 5.7)
- Submit 2.4 fixes a problem in Submit 2.3 that produced a complaint from the Grade Grinder about a phantom "Empty file in submission" when first run. (Typically, quitting and restarting Submit 2.3 made the problem go away.)
- Tarski's World 5.7 is able to read and write files that are compatible with Tarski's World 5.6 and Tarski's World 6.x
- Tarski's World 6.1 fixes a number of bugs in 6.0
- 2005 September 1 -- Several downloads have been made available:
- Submit 2.1 is available as a separate download for users encountering difficulties with Submit 2.3, such as Grade Grinder complaints of "Empty file in submission".
- Boole 2.4 for Mac OS X 10.4 (Tiger) is available. It fixes a Boole on Macintosh Tiger-only problem, described below on July 14 2005.
- 2005 July 14 -- A problem has been discovered with Boole 2.0-2.3 on Mac OS X 10.4 (Tiger) that causes the Boole window not to update.
Resizing the window restores updating of the window and blinking of the text cursor, but the problem may recur.
Another workaround is to run Boole (Classic); this requires the Classic (Mac OS 9) environment, which may be installed in Tiger using the original system discs.
- 2004 November 23 -- Problem with the University of Chicgo Grade Grinder fixed.
We recommend returning your preferences to use Load Balancing. This will result in a faster response, since this always submits to the least busy Grade Grinder.
- 2004 November 22 -- University of Chicago Grade Grinder down.
Users may have idfficulty connecting to the Grade Grinder because of problems at the University of Chicago. As a temporary workaround, use Submit's preferences to choose to direct submissions to the Stanford server.
- 2004 September 29 --- The Grade Grinder has been updated.
Users may notice two significant differences in behavior with this release.
- Improved grading of Fitch proofs.
Instead of simply reporting that a step does not check out, together with the formula contained in that step, we now report the inference rule, and if possible a more detailed reason for the failure (essentially repeating the message from Fitch's status line for this step.)
We have added a message reporting the number of lines in the proof, which will always be included. This is primarily intended to help instructors to grade proofs where students have either used a Con rule to complete the proof of a goal when this is permitted, but have used it to validate non-trivial inferences (E.g. to complete the whole proof in one step.)
- The Grade Grinder will now include a message when a submission is made by a user who has been registered for more than six months.
- Improved grading of Fitch proofs.
- 2004 March 3 --- New versions of all of the LPL software released.
- A serious bug in Fitch which cased some files to be saved in a corrupt state, has been fixed.
- Fitch, Boole and Submit running under Windows XP were all subject to a bug in the Windows Java VM which caused crashes and the loss of data under some circumstances when saving files. This has been fixed (our applications, not the Windows VM)
- Tarski's World can now open files created by later versions of the application.
- 2004 January 27 --- A significant bug in the Fitch 2.1 Taut
Con procedure has been reported.
This soundness bug causes Taut Con to incorrectly report some inferences involving equality as valid.
We have fixed the Grade Grinder, and are preparing a new version of Fitch for download.
The effect of this is that some users may see Fitch reporting Taut Con steps as valid, while Grade Grinder disagrees. If this happens to you, then you need to change your proof, since the Grade Grinder is correct.
- 2004 January 27 --- Issues with AOL mailboxes.
America Online (AOL) appear to be blocking mail from servers at cornell.edu and pitt.edu. Several of our users are forwarding mail from their pitt.edu and cornell.edu addresses, and are therefore not receiving grade reports or other mail.
A temporary workaround would be to not forward mail from pitt.edu and cornell.edu to aol.com.
We can do nothing about this situation. Until this issue is resolved between Cornell and Pitt and AOL, users forwarding mail from those sites to AOL will continue to be impacted.
- 2004 January 19 --- New versions of all of the LPL software released.
In addition to improved support on Mac OS X and Windows XP, all users will notice a number of improvements and bug fixes. We recommend that all users upgrade to the new versions of the software.
- 2004 January 9 --- The Grade Grinder has been updated.
Users may notice two differences in behavior with this new release.
- The Grade Grinder now uses a new theorem prover, called Gentzen,
to check the solutions to some exercises, and all applications of the
Con rules in submitted Fitch proofs.
In principle, there should be no differences in behavior with the introduction of the new theorem prover, but in practice there undoubtedly will be some. On the positive side, we believe that Gentzen fixes some bugs in the old theorem prover, and therefore will be more reliable in its reporting in some cases. Of course, its possible that there are undiscovered bugs in Gentzen which will result in incorrect reporting of results, though we currently know of none. We do know that Gentzen has different performance characteristics than the old theorem prover, and therefore we expect, and have observed, that different "hard" conjectures timeout between the two systems. That is, some solutions which were too hard to check using the old system which will now be correctly graded, and vice versa.
There is now the possibility that users will see discrepancies between the results returned by the Con rules in Fitch and the Grade Grinder, because of bugs in either prover and/or performance characteristics. These discrepancies will disappear if users upgrade to Fitch 2.1, which we expect to make available for download on or before January 19 2004.
- The Grade Grinder now supports the "personality" feature implemented as a Submit 2.x preference. This allows users of submit to have some control over the exclamations that are included in the report of a correct exercise.
- The Grade Grinder now uses a new theorem prover, called Gentzen,
to check the solutions to some exercises, and all applications of the
Con rules in submitted Fitch proofs.
- 2002 December 13 --- A significant bug in Fitch 1.3's
Tautological Consequence (Taut Con) rule has been reported.
Fitch 1.3 sometimes incorrectly reports some Taut con steps involving quantified formulae as valid.
We have fixed the Grade Grinder, and are in the process of preparing a new version of Fitch for download.
The effect of this is that some users may see Fitch reporting Taut Con steps as valid, while Grade Grinder disagrees. If this happens to you, then you need to change your proof, since the Grade Grinder is correct.