Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 13 Apr 1995 14:55:08 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA153389144; Thu, 13 Apr 1995 07:19:04 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA153339102; Thu, 13 Apr 1995 07:18:22 -0600 Received: from albatross.cl.cam.ac.uk (user drs1004 (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 13 Apr 1995 14:15:06 +0100 X-Mailer: exmh version 1.5.2 12/21/94 To: info-hol@leopard.cs.byu.edu Cc: stuart@dcs.gla.ac.uk Subject: TkHolWorkbench 0.2 now available Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Thu, 13 Apr 1995 14:14:59 +0100 From: Donald Syme Message-Id: <"swan.cl.cam.:056940:950413131515"@cl.cam.ac.uk> TkHolWorkbench 0.2 is now available for ftp. This version is identical to TkHolWorkbench 0.2 (beta) patch 7. Thanks to Michael Norrish, Mike Benjamin, Wai Wong, Mats Larsson, Rob Shaw, Paul Curzon and Mark Staples for taking the time to report bugs and problems in the beta release. The list of bug fixes since TkHolWorkbench 0.2b patch 0 is shown below. Site: ftp.cl.cam.ac.uk Choose one of: hvg/contrib/TkHolWorkbench/TkHolWorkbench.0.2.tar.gz hvg/contrib/TkHolWorkbench/TkHolWorkbench.0.2.WithoutTclTk.tar.gz hvg/contrib/TkHolWorkbench/TkHolWorkbench.0.2.WithoutTclTkExpect.tar.gz (The latter files are smaller files if you already have Tcl/Tk and/or Expect installed on your system. You may discover this by trying to run the programs "wish" (for tcl/tk) and "expectk" (for Expect).) At Cambridge TkHolWorkbench may be run by executing /usr/groups/hol/interfaces/TkHolWorkbench/bin/tkholhelper Version 0.2bp7 (released Tue Apr 4 17:37 BST 1995): - When a type was defined using TkDefineType, the wrong theorem and definition names were appearing in the TkTheoryViewer. A more general notification scheme has now been introduced to fix this. - The SearchResults windows now have a close button. So do the result window from TkDefineType and the script window from TkGoalProof. - The help text in each of the "Options" windows now resizes properly. - An empty definition/theorem/axiom no longer appears at the top of a list of such objects in TkTheoryViewer. This was happening when the list itsel was meant to be completely empty. Thanks to Michael Norrish for reporting this bug. - Backups in TkGoalProof past the first goal now allow you to re-edit the original goal. This now works for both hol88 and hol90. - Added assumption numbering (and option) and assumption ordering (first on top/first on bottom) (and option). - Reintroduced automatic HOL_ERR checking for most computations in hol90. Why did I ever take this out? - Added automatic CHANGED_TAC around each tactic that is applied so an error is raised if the goal does not change. There is an option to turn this off. Version 0.2bp6: - Fixed initial expansion of the theory tree. The tree was being computed but not drawn. Also made default initial expansion depth 0. Also made the list of theories at which to prune the initial expansion a configuration option. Version 0.2bp5: - you can now specify the initial expansion depth both as an option under the "Options" menu and as a command line option: tkholhelper -theoryTreeInitialExpand 1 - Normally you would exit by pressing Ctrl-D or using "exit()" from the hol90 prompt. You can now exit from TkTheoryViewer as well in case the stdin/stdout isn't working. Version 0.2bp4: - Fixed bug added accidently in 0.2bp3. Version 0.2bp3: - Added store_thm to the functions modified so the interface can track changes to the theory files. Version 0.2bp1: - Only the goal window now expands when a TkGoalProof window is resized. - Fixed bug with "Reset" on option menu. This cleared the option database when it shouldn't have. - Added tactic history list/menu to TkGoalProof - TkTheoryViewer parents frame no longer resurrects itself even when it has been collapsed when a theory changes. - "shell" widgets (Tcl and Hol) now support selection and pasting better. Initial focus on shells also works better. Pasting into text widgets is also a little less flaky. - Fixed some bugs with feedback lines and blocking windows. When executng commands from the HOL command line, the windows will in general now block. Also the focus is grabbed when the application is busy. - Added feedback lines to most top-level windows. - Mail reports can now use "mail" and not just MH "send". Mail reports are now a decent size as well. - Added a menu entry to mail a bug report (an explicit Tcl error is no longer necessary). - Fixed most packing problems with the TkTheoryViewer window. Collapsed boxes should now not take up more space than they ought after the mai nwindow has been expanded.