Notes to include in documentation. ---------------------------------- ******** Suggestion for outline of improved documentation. Terminology: I suggest "proof mode" should become "proof script mode", aka "the proof script mode of Proof General". We should be careful here, e.g. present docs speak of buffers in proof mode, etc, but no buffer is directly in that mode, which is confusing to the users, at least! 1. Introduction Description 1.1 1.2 Feature list, xref'd to later chaps. 1.2 Supported Proof Assistants, xref'd too. Support for new instances, xref'd to later chaps. 2. Basics of script management 2.1 What a proof script is 2.2 Locked region and queue region 2.3 Script processing commands 2.4 Toolbar commands 2.5 Other commands 2.4 Walkthrough example [maybe in appendix?] 3. Script management with multiple files 3.1 Proof General's view of processed files 3.2 Switching between proof scripts 3.2 Retracting across files [ 3.3 Re-synchronizing with the proof assistant - if added ] 5. Customizing Proof General 5.1 Setting user options, what they are: proof-splash-inhibit etc. 5.2 Using proof assistant on another machine 5.3 Examining configuration settings (xref'd later) 6. LEGO Proof General 6.1 LEGO commands 6.2 LEGO customizations 7. Coq Proof General 7.1 Coq commands 7.2 Coq customizations 8. Isabelle Proof General 8.1 Isabelle commands 8.2 Isabelle customizations 8.3 Notes about multiple files 9. Adapting Proof General to New Provers 9.1 Files and directories. Skeleton code. 9.2 Settings for proof scripts 9.3 Settings for proof shell -- Special annotations 10. Internals of Proof General. 10.1 Proof script mode: - fontification hacks - spans in locked region 10.2 Proof shell mode - proof-action-list - proof-shell-exec-loop - proof-shell-output-filter - eager annotations 11. Credits and history APPENDIX A. Obtaining and installing the software B. Known bugs C. Future ideas and plans ******** Why is C-c C-b useful? Could just use the file to read it one go (will we have a command to do this other than via the process?). BUT it's nice because it stops exactly where a proof fails, so you can continue development from there. ********* Suggestions for improving web pages after Rod reading them: - slideshow rather than single screen shot - separate feature list - explain what a proof script is and what script management buys you Get Dave a laptop to demo on. ********* Support for fume-function. fume-func is a handy package which makes a menu from the function declarations in a buffer. Proof General configures fume-func so that you can quickly jump to particular proofs in a script buffer. If you want to use fume-func, you may need to enable it for yourself. It is distributed with XEmacs (and FSF GNU Emacs) but by not enabled by default. To enable it you should find the file fume-func.el and follow the instructions there. If you have XEmacs 20.4, what you need to do is this: ...... If you have any other version of Emacs, you should check the fume-func.el file ********* Isabelle with multiple files. Proper multiple file support only works for .ML files which are read via the theory loader, with use_thy. If you want to load .ML files which aren't associated with theories, it's best to use a dummy theory, see [Reference to Isabelle manual] ********** ***************************************************************** Notes for writing a paper describing Proof General ------------------------------------------------- Thesis/introduction =================== As programming languages have evolved, environments for developing and debugging programs have also improved. However, discounting various "visual" programming languages, a program is usually still a piece of text which can be directly edited by a programmer, a situation which hasn't changed since the early days when VDUs replaced punched cards. Similarly, whilst the history of languages for proof assistants is much shorter, we believe that a proof script, describing the operations needed to construct a proof, will remain the fundamental form of input for proof systems. ... - interactive proof assistants geared to developing proof scripts interactively, but may not come with integrated editing support. Problem of shell-like interaction is that input has to be tediously reassembled after or during proof to get a successful proof script. - script management [refs] aims to make this process easier. Aspects of design ================= - Generic. Fits inside Emacs architecture. (Compare with comint). - Extensive use of Emacs Customization mechanism to make it easy to set/inspect configuration as well as user-options. - Script management with multiple files Seen one proof assistant, use them all ====================================== - Same interface for different underlying systems - Compare: web technology, where "browsing" works for different protocols: http, ftp, etc - Anyone can use Proof General to browse and replay proofs from other systems, without needing to know how to invoke the system, etc. - However, proof script language and output remains particular to each prover. It would be another (interesting) project to attempt to map input and output into an interchange format for proof systems. A Specification for a proof assistant interface =============================================== The settings to instantiate Proof General can be seen as a set of requirements for a proof assistant interface.