From a587987a431e325de9d4e7f8e52a5a09746f974b Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 26 Nov 1999 12:51:56 +0000 Subject: Renamed file --- doc/notes.txt | 196 ------------------------------------------------------ etc/doc-notes.txt | 196 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 196 insertions(+), 196 deletions(-) delete mode 100644 doc/notes.txt create mode 100644 etc/doc-notes.txt diff --git a/doc/notes.txt b/doc/notes.txt deleted file mode 100644 index 0cf83b88..00000000 --- a/doc/notes.txt +++ /dev/null @@ -1,196 +0,0 @@ -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. - - diff --git a/etc/doc-notes.txt b/etc/doc-notes.txt new file mode 100644 index 00000000..0cf83b88 --- /dev/null +++ b/etc/doc-notes.txt @@ -0,0 +1,196 @@ +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. + + -- cgit v1.2.3