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; Tue, 13 Dec 1994 02:57:05 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA01027; Mon, 12 Dec 1994 19:48:05 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA01023; Mon, 12 Dec 1994 19:47:59 -0700 Received: from auk.cl.cam.ac.uk (user drs1004 (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 13 Dec 1994 02:43:13 +0000 To: info-hol@leopard.cs.byu.edu Subject: New Release: TkHolWorkbench.0.1b Date: Tue, 13 Dec 1994 02:43:07 +0000 From: Donald Syme Message-Id: <"swan.cl.cam.:267500:941213024316"@cl.cam.ac.uk> Well, here it is - the results of my first 2 months of PhD work at Cambridge. I will be supporting and developing this package further during my time here. ...Announcing... TkHolWorkbench 0.1b (including TkTheoryViewer, TkHolShell, TkTRS and TkGoalProof) Donald Syme The Computer Laboratory Cambridge University email: Donald.Syme@cl.cam.ac.uk 1. TkHolWorkbench 1.1. What is it? TkHolWorkbench is a set of GUI tools and packages for HOL, implemented using the Tk toolkit. The TkHolWorkbench tools aim to be lightweight, user friendly, robust and extensible. This, however, is a first (beta) release, so take these promises with a grain of salt. Part of the idea of this release is to generate feedback on what people really want from a HOL GUI, not not to convert everyone over to using an underdeveloped interface. If you let me know how the packages could be changed to actually be useful, I'd be glad. TkHolWorkbench is available via ftp from: Site: ftp.cl.cam.ac.uk Directory: hvg/contrib/TkHolWorkbench/TkHolWorkbench.0.1b.tgz The file is 0.6 MB. Uncompressed it is 2 MB, though if you're not running on a sun4 1.2. TkHolWorkbench - For New and Old HOL users A GUI is a theoretically great tool for new users to learn HOL. This preliminary release does not allow users to access all functionality via a GUI interface, but it should still lessen the steepness of the HOL learning curve. I would be interested to hear feedback from any new HOL users who try out the system. In an effort to encourage people to move switch interfaces, TkHolWorkbench provides "familiar" functionality to old HOL users, such as a shell like interface. This means you can switch to using TkHolWorkbench without significantly changing the way you work. I'm interested, of course, to hear if TkHolWorkbench proves useful to old HOL users, but I am also interested in hearing from you if TkHolWorkbench turns out to be *inferior* to your current work environment. I would imagine this would apply particularly to people who use "emacs" to control HOL and might not want to move out of that integrated environment. 1.3. Standard Programs in TkHolWorkbench Three programs come standard with the TkHolWorkbench: "tkholshell", "tktheoryviewer" and "tkholwb". tkholshell: A simple shell interface to HOL, very similar to what you get if you run HOL from an xterm. However, as bonuses you get command history, plus you can run multiple shells acessing the one HOL session. tktheoryviewer: Lets you view theories and navigate around the theory heirarchy. Most importantly, it lets you search through theories for the theorems and definitions you need. "tktheoryviewer" is a great way to look around other people's libraries, for example the "reals" or "more_arithmetic" libraries. tkholwb: All the functionality of tktheoryviewer and tkholshell and more. Create new HOL theories, prove theorems and produce a script file which will do all this automatically. Having TkHolShells available to work with means that any functionality not presently in the GUI can still be accessed. And even being able to have more than one shell accessing a HOL session can be handy. 1.4. TkHolWorkbench - Flexible architecture The architecture of TkHolWorkbench is of independent but cooperating packages. A collection of packages run together forms a program. Users may, without too much trauma, write their own packages and add run them in combination with either TkTheoryViewer or TkTheoryEditor. An example (skeleton) package is included with this release to help enable this. Each of the "programs" described above is really a simple shell script which combines a number of "packages" (Tcl code libraries) and creates some top windows. Thus, it is trivial to add new libraries, specify extra top windows, stop some libraries from ever being looked at and so on. For example, if you decide you don't like TkGoalProof, and never perform goal directed proofs anyway, you can run: tkholwb -stoppackage TkGoalProof and the package won't be loaded. To include your own package is as simple as: tkholwb -package ~/MyPackage -win MyPackageWin I am open to offers from people interested in becoming co-developers of TkHolWorkbench. I am also interested in hearing as much feedback as possible on what people find useful in the different tools, as well as bugs and suggestions of improvements. I am also interested in communicating with other people developing Tk-based or other user interfaces to HOL and other theorem provers. 2. More on the TkHolWorkbench Packages 2.1. TkTheoryViewer TkTheoryViewer is a GUI theory browser for HOL. It is most useful for investigating theory heirarchies and displaying often used theories for reference. TkTheoryViewer can display the theorems, definitions and axioms for any theories loaded into the underlying HOL session. For hol88 users, theorems can be displayed in either plain text or rich text formats. Plain text is like the normal HOL output format, whereas rich text uses symbols, fonts and colours to display theorems in a more readable fashion. TkTheoryViewer works with both hol88 and hol90. Rich text formatting of theorems is only available with hol88 systems built with AKCL, but will eventually be available with all HOL systems. 2.2. TkTRS (TRS = Theorem Retrieval System) TkHolWorkbench also comes with the TkTRS package, which is an interface to Richard Boulton's Theorem Retrieval System (trs) library. TkTRS is a tool for searching across theories for useful theorems and definitions. The results are displayed in result windows and, in hol88, the theorems may again be displayed rich text format. TkTRS works with both hol88 and hol90. The TkTRS source code includes a rough port of the trs library to hol90. See USAGE.tktheoryviewer for details on how to run tktheoryviewer. In general it will be a matter of running .../TkHolWorkbench/bin/tktheoryviewer -hol 2.3. TkHolShell 2.4. Putting It All Together - TkHolWorkbench (tkholwb) TkHolWorkbench is not only the name of the set of programs and tools described by this README, but is also the name (as tkholwb) of the program that runs all the packages in TkHolWorkbench together. TkHolWorkbench provides all the functionality found in TkTheoryViewer. In addition, it provides access to theory editing functions, such as specifying new parents, loading libraries and so on. It also provides script management facilities for managing the production a script which will recreate the HOL theory at a later date. See USAGE.tkholwb for details on how to run tktheoryviewer. In general it will be a matter of typing .../TkHolWorkbench/bin/tkholwb -hol 3. AVAILABILITY The latest versions of all the programs in the TkHolWorkbench suite can always be found at: ftp://ftp.cl.cam.ac.uk/hvg/contrib/TkHolWorkbench/... You will need a copy of either hol88 or hol90 on your system. If you are using a private (dumped) copy of hol90 incorporating your favourite libraries, you may use that with the TkHolWorkbench programs by specifying the executable ith a -hol switch on the command line. See USAGE fo more details. 4. INSTALLATION See ./INSTALL for details. 5. USAGE See ./USAGE.* for more details. There are loads of command line switches that can be given to control how TkHolWorkbench progams startup. Hol90 users will need to provide the flag tkholwb -hol hol90 tkholshell -hol hol90 tktheoryviewer -hol hol90 Here hol90 can be your favourite hol90 executable, with libraries loaded in. 6. BUGS AND PROBLEMS This is a first, alpha release. There will be problems, especially with different configurations and window managers. Mail me with these ones especially. Patches to code are particularly welcome. I am doing a 3 year PhD. at Cambridge, and plan to maintain these tools and extend them during my time here. This is not my major PhD. work, however, merely a time consuming sidetrack. 7. SUGGESTIONS, FUTURE WORK AND PATCHES I am keen to involve others, particularly in writing new packages to add to the TkHolWorkbench suite. Ultimately I would like to see interface components come standard with each HOL library/extension. In the modern world good work deserves a good interface. I am also interested in supporting similar interfaces to other theorem proving systems. Nearly all the TkHol code should be portable to other theorem provers. A pilot project with Isabelle would be the likely first step.