Developers' Notes about Documentation ------------------------------------- * Plan for outline of improved documentation. (Completed) 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 [da] 1.1 Quick start guide 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 [da] 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. Advanced script management [done] 3.1 Proof General's view of processed files 3.2 Switching between proof scripts 3.3 Retracting across files 3.4 Handy hints and tips (e.g. C-c C-b stuff?) 3.5 Using the proof shell [ 3.6 Re-synchronizing with the proof assistant - if added ] 4. Customizing Proof General [da] 4.1 Setting user options, what they are: proof-splash-inhibit etc. 4.2 Using proof assistant on another machine 4.3 Examining configuration settings (xref'd later) 5. LEGO Proof General [done] 5.1 LEGO commands 5.2 LEGO customizations 6. Coq Proof General [anon] 6.1 Coq commands 6.2 Coq customizations 7. Isabelle Proof General [da] 7.1 Isabelle commands 7.2 Isabelle customizations 7.3 Notes about multiple files 8. Adapting Proof General to New Provers [da] 8.1 Files and directories. Skeleton code. 8.2 Settings for proof scripts 8.3 Settings for proof shell -- Special annotations 9. Internals of Proof General. [tms] 9.1 Proof script mode: - fontification hacks - spans in locked region 9.2 Proof shell mode - proof-action-list - proof-shell-exec-loop - proof-shell-output-filter - eager annotations 10. Credits and history [done] APPENDIX A. Obtaining and installing the software [da] B. Known bugs [done] C. Future ideas and plans [da] ********* Support for Function Menus 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 func-menu.el and follow the instructions there. At the time of writing, the current version of XEmacs is 20.4 and it has these instructions: (require 'func-menu) (define-key global-map 'f8 'function-menu) (add-hook 'find-file-hooks 'fume-add-menubar-entry) (define-key global-map "\C-cl" 'fume-list-functions) (define-key global-map "\C-cg" 'fume-prompt-function-goto) (define-key global-map '(shift button3) 'mouse-function-menu) (define-key global-map '(meta button1) 'fume-mouse-function-goto) 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. Example of API design guidlines =============================== 1. Use a different prompt for continued lines during input communication. Helps parsing output.