Home

Proof General - Engineering & Computer Science

image

Contents

1. 14 67 proof ernorsfate ani lee EAE 38 proof find theoremS 2 2 osos 15 proof frob locked end ees sessssn 24 proof goto command end s esses 12 proof goto command start sess 12 proof goto end of locked sus 12 proof goto pouBt bbs E que PED 14 proof helps pd 15 proof interrupt prOCesS uote ev RE x 15 o A Re ceeds ERES E 16 PEOOF 1SSUC SAVE ccs ii ques 16 proof layout windOoWS 2 239 Gcc mex esp 35 proof l cked face uud lle da RIBERA 38 proof minibuffer cmd c 2xi eee 9r e res 15 proof mouse track insert utiss 13 pEoof prf iiliucsg doge eb rer ERR ER OPES 15 proof process buffer sess esse 14 proof queue face ii pk n po v AP Pace ed ans 38 proof retract B ffer 2 2 4 sees den moms 14 proof retract until point interactive 14 proof shell exit o rice 16 pro of shell restart cm RR RR CRETA 16 proof shell start i 2 oie si exert ur eee 16 proof tacticals name f ce sees 39 proof toggle active scripting 11 proof undo and delete last successful command E EP 14 proof undo last successful command 13 proof warning fa6e ca prr reads 38 U unicode tokens rotate glyph backward 20 unicode tokens rotate glyph forward 20 unicode tokens token insert 28 68 Proof General Variable and User Option Index Variable and User Option Index
2. The right hand mouse button provides this convenient way to copy subterms from the goals buffer using the function pg goals yank subterm pg goals yank subterm event Command Copy the subterm indicated by the mouse click event This function should be bound to a mouse button in the Proof General goals buffer The event is used to find the smallest subterm around a point The subterm is copied to the kill ring and immediately yanked copied into the current buffer at the current cursor position 20 Proof General In case the current buffer is the goals buffer itself the yank is not performed Then the subterm can be retrieved later by an explicit yank BR Chapter 4 Advanced Script Management and Editing 21 4 Advanced Script Management and Editing If you are working with large proof developments you may want to know about the advanced script management and editing features of Proof General covered in this chapter Large developments may contain files with many long proofs Proof General provides functions that let you hide completed proofs from view temporarily Large proof developments are typically spread across various files which depend on each other in some way Proof General knows enough about the dependencies to allow script management across multiple files With large developments particularly users may occasionally need to escape from script management in case Proof General loses synchronization with the pro
3. If your prover generates output which is recognized as tracing output in Proof General you may need to know about a special provision for interrupting the prover process If the trace output is voluminous perhaps looping it may be difficult to interrupt with the ordinary C c C c proof interrupt process or the corresponding button menu In this case you should try Emacs s quit key C g This will cause a quit in any current editing commands as usual Chapter 2 Basic Script Management 17 but during tracing output it will also send an interrupt signal to the prover Hopefully this will stop the tracing output and Emacs should catch up after a short delay Here s an explanation of the reason for this special provision When large volumes of output from the prover arrive quickly in Emacs as typically is the case during tracing especially tracing looping tactics Emacs may hog the CPU and spend all its time updating the display with the trace output This is especially the case when features like output fontification and X Symbol display are active If this happens ordinary user input in Emacs is not processed and it becomes difficult to do normal editing The root of the problem is that Emacs runs in a single thread and pending process output is dealt with before pending user input Whether or not you see this problem depends partly on the processing power of your machine or CPU available to Emacs when the prover is running One way to
4. C coq mode hooks c onc 260 idee nee rude 21 I isa mode hooks voraces sede EXER E 27 isabelle web page lu ide 51 L L go mode hooks 4 re Ree ewan 27 LEO EAS 221624 6i uses e bna dA E RIA Eis 45 lego www home page o cw sees Bra RR 45 P PA completion table esencia 30 PA sCript indent odo cepi cue maa 31 PA x symbol enable8 2122i 222 Geko LAT 36 PE input ring SYZ0 2 262 GA bb bp REA 37 proof allow undo in read only 36 proof assistant home page esses 39 proof auto action when deactivating scripting ich E a Web et a bap derer isla 38 69 proof disappearing proofs s s 21 proof electric terminator enable 36 proof experimental features 25 proof follow mode sirsie zm ed pied eos 37 proof general debug since RIPE ERE 37 proof goal with hole regexp 29 proof goal with hole result 20 proof keep response history 3T proof multiple frames enable 35 proof one command per line 37 proof output fontify enable sci e e 36 proof prog name asK 4 3 dub ene 37 proof prog name guess eese 37 proof query file save when activating SCrUPCING seori ermi ee PT ETYM PER E 36 proof rsh commamd 2 lxrcmeile ced ee sted 38 proof script command separator 38 proof script indent 22 2x nadir nn 12 proof splash enable
5. Proof General has support for proof by pointing as described in the document e BKS97 Yves Bertot Thomas Kleymann Schreiber and Dilip Sequeira Implementing Proof by Pointing without a Structure Editor LFCS Technical Report ECS LFCS 97 368 Also published as Rapport de recherche de INRIA Sophia Antipolis RR 3286 62 Proof General History of Proof General 63 History of Proof General It all started some time in 1994 There was no Emacs interface for LEGO Back then Emacs militants worked directly with the Emacs shell to interact with the LEGO system David Aspinall convinced Thomas Kleymann that programming in Emacs Lisp wasn t so difficult after all In fact Aspinall had already implemented an Emacs interface for Isabelle with bells and whistles called Isamode Soon after the package lego mode was born Users were able to develop proof scripts in one buffer Support was provided to automatically send parts of the script to the proof process The last official version with the name lego mode 1 9 was released in May 1995 The interface project really took off the ground in November 1996 Yves Bertot had been working on a sophisticated user interface for the Coq system CtCoq based on the generic environment Centaur He visited the Edinburgh LEGO group for a week to transfer proof by pointing technology Even though proof by pointing is an inherently structure conscious algorithm within a week Yves Bertot Dilip Sequeira and
6. 69 Keystroke Index 42225429 COR RERO RA IRA RAP 71 Concept Index 2222 rh raw y RR AR AAA T8 Proof General
7. One of the symbols locked follow followdown ignore If locked point sticks to the end of the locked region If follow point moves just when needed to display the locked region end If followdown point if necessary to stay in write able region If ignore point is never moved after movement commands or on errors If you choose ignore you can find the end of the locked using M x proof goto end of locked The default value is locked 38 Proof General proof auto action when deactivating scripting User Option If retract or process do that when deactivating scripting With this option set to retract or process when scripting is turned off in a partly processed buffer the buffer will be retracted or processed automatically With this option unset nil the user is questioned instead Proof General insists that only one script buffer can be partly processed all others have to be completely processed or completely unprocessed This is to make sure that handling of multiple files makes sense within the proof assistant NB A buffer is completely processed when all non whitespace is locked coloured blue a buffer is completely unprocessed when there is no locked region The default value is nil proof script command separator User Option String separating commands in proof scripts For example if a proof assistant prefers one command per line then this string should be set to a newline Otherwise it should be
8. To store these symbols in files you need to use a particular coding for example UTF 8 In fact Modern Emacsen can handle a multitude of different coding systems and will try to automatically detect an appropriate one consult the Emacs documentation for more details Proof General includes two special mechanisms for assisting with input The first is Maths Menu originally by Dave Love which simply adds a menu for inserting common mathematical symbols Proof General gt Options gt Unicode Maths Menu This only works in GNU Emacs and whether or not the symbols display in the menus depends on the font used to display the menus which depends on the Emacs version toolkit and platform The second mechanism has been written specially for Proof General to provide some backward compatibility with X Symbol This is the Unicode Tokens minor mode Proof General gt Options gt Unicode Tokens The aim of this mode is to allow displaying of ASCII tokens as Unicode strings This allows a file to be stored in perfectly portable plain ASCII encoding but be displayed and edited with real symbols When the file is visited the ASCII tokens are replaced by Unicode strings when it is saved the reverse happens For this to be reliable you need to provide tokens for all the Unicode symbols you don t want to appear in the saved file if any are not encoded Emacs will try to save them in a richer encoding such as UTF 8 You also need to make
9. is a useful mouse binding for copying the highlighted command under the mouse N Chapter 2 Basic Script Management 13 C button1 proof mouse track insert proof mouse track insert event Command Copy highlighted command under mouse event to point Ignore comments If there is no command under the mouse behaves like mouse track insert Read the documentation in Emacs to find out about the normal behaviour of proof mouse track insert if you don t already know what it does 2 6 Script processing commands Here are the commands for asserting and retracting portions of the proof script together with their default key bindings Sometimes assertion and retraction commands can only be issued when the queue is empty You will get an error message Proof Process Busy if you try to assert or retract when the queue is being processed C c C n proof assert next command interactive C c C u proof undo last successful command C c C BS proof undo and delete successful command C c C RET proof goto point C c C b proof process buffer G c C F proof retract buffer C c terminator character proof electric terminator toggle The last command proof electric terminator toggle is triggered using the character which terminates proof commands for your proof assistant s script language For LEGO and Isabelle use C c for Coq use C c This not really a script processing command Instead if enabled it causes subsequent key presses of or
10. DA dde 49 C608 Lucesacor baa er d Se ahs Ian dicis als dus 50 CHO B Eoi kdo ae O 49 A mre vare deg BR ae d Pr ens 50 o ec Pm 13 CAGHGHBS ia Eu pO ERA aac ER Td ace 13 C6 U E ueieLPRRPT4da Aia 14 CAOS ii ia A e ad A da 12 uo A 14 49 CASCO used bb ihi ae uu edu de ei gets 14 ero EP CODICE 13 C C CED esc iat CORDE NRI PEU Eee 14 GHG CPR Em 13 OG CREE ddd tabla taeda reu e 13 CAG OE nuit isque DR a oe od hg edad dank ds 14 60 id Sacro bd E Tia ies 13 CG CST es sa hemi eds IR eee Ga ie opis 14 Coq version is V8 0 modista e de ee ees 47 Gcoq version 1s V8 1 id 47 M Maid this id ak 24 72 Proof General Concept Index Concept Index A active scripting buffer eese eer nee 11 Dy 5 AsSertiOn vierta oo cerda bd 10 23 B bl e tert sueta np ph oa de Vos 10 buffer display customization 34 C Comitan tee bd beds 63 GOLOUE adr cit oe Bh cad la e EE tento Ead 14 2 completion 22 cei eee LE lere dee eraen a 30 OIC Meir nd red bade tenet ot 63 Customization llle n 33 D Dedicated windows 0s eee eee ee 35 display customization sess 34 E Editing region i2 er pnr a 10 Emacs customization library 33 F Peat utes n ieneskhil wbiveEe a 4 fil variables 223 3 2564 Deezer amd 41 tonb Jockes cia an alado 27 mames EMT 34 AMADE sassen ceca a adan des 29 A nemen es 29 Turiction men sure tcn Eminem kel
11. David von Oheimb helped to develop the generic version of his X Symbol addition which he originally provided for Isabelle A new instantiation of Proof General is being worked on for Plastic a proof assistant being developed at the University of Durham Old News for 3 1 Proof General 3 1 released March 2000 is a bug fix improvement over version 3 0 There are some minor cosmetic improvements but large changes have been held back to ensure stability This release solves a few minor problems which came to light since the final testing stages for History of Proof General 65 3 0 It also solves some compatibility problems so now it works with various versions of Emacs which we hadn t tested with before non mule GNU Emacs certain Japanese Emacs versions We re also pleased to announce HOL Proof General a new instance of Proof General for HOL98 This is supplied as a technology demonstration for HOL users in the hope that somebody from the HOL community will volunteer to adopt it and become a maintainer and developer Otherwise work on HOL Proof General will not continue Apart from that there are a few other small improvements Check the CHANGES file in the distribution for full details The HOL98 support and much of the work on Proof General 3 1 was undertaken by David Aspinall while he was visiting ETL Osaka Japan supported by the British Council and ETL Old News for 3 2 Proof General 3 2 introduced several new featu
12. Interrupting during trace output 0 0 0 tainga dea wa aa aAa aa aaa rn 16 3 Subterm Activation and Proof by Pointing 19 3 1 Goals buffer commands 00000 c cece ee enn tee hh han 19 4 Advanced Script Management and Editing 21 4 1 Visibility of completed proofs 00 eee cece tenet tenets 21 4 2 Switching between proof scripts 00 ce eee eee hh 21 4 3 View of processed lle iia eiua ied quu ra ete eduardo RA DE TR Fade 22 4 4 Retracting across files iode eee er tete gc eee a ORC UE RD Roe eee Rd 23 4 5 Asserting across files sslsilsluessllelllels ehh hh hh 23 4 6 Automatic multiple file handling 0 0 cece eee 23 4 7 Escaping script management sseseeeelee ehh hh hn 23 4 8 Editing features uu seca ii A b gne gine para Ead eoa ca cd 24 4 9 Experimental features serors ciririnrss kirii ai ehh hh 25 li Proof General 5 Support for other Packages 9 oe Rr mnn 27 b l Syntax bighliehtine srs ae eei pott dulce dba ERR amd due alas REPRE ga eh 27 5 2 X Symbol SUPPO tasasi sa atid I ade tel odds pee eR edd dade 27 5 3 Unicode Support udo esee ia ter oe do ob bar ede doe deed ee gw aes 28 5 4 Imenu and Speedbar and Function Menu 0 cee eee eee e teen nees 29 5 5 Support for outline mode 0 cee seh 30 5 6 Support for Completion metida daw EROR Reo PU AGRE ee pees 30 Bal Support for GAPS sacha ii tt qul
13. Rotate the character before point in the current code page by N steps If no character is found at the new codepoint no change is made This function may only work reliably for GNU Emacs gt 23 Unfortunately the precise set of symbol glyphs that are available to you will depend in compli cated ways on your operating system Emacs version installed font sets and even command line options used to start Emacs Describing the full range of possibilities or giving recommen dations is beyond the scope of this manual please search and contribute to the Proof General wiki at http proofgeneral inf ed ac uk wiki for more details To edit the strings used to display tokens or the collection of short cuts you can edit the file PA unicode tokens el or customize the two main variables it contains PA token name alist and PA shortcut alist E g for Isabelle M x customize variable isar token name alist RET provides an interface to the tokens and M x customize variable isar shortcut alist an interface to the shortcuts 5 4 Imenu and Speedbar and Function Menu The Emacs packages imenu Index Menu and func menu Function Menu each provide a menu built from the names of entities e g theorems definitions etc declared in a buffer This allows easy navigation within the file Proof General configures both packages automatically so that you can quickly jump to particular proofs in a script buffer Developers note the automatic
14. assumes that the only files processed are the ones it has sent to the proof assistant itself Moreover it conservatively assumes that there is a linear dependency between files in the order they were processed If you only have automatic multiple file handling you ll find that any files loaded directly by the proof assistant are not locked when you visit them in Proof General Moreover if you retract a file it may retract more than is strictly necessary because it assumes a linear dependency For further technical details of the ways multiple file scripting is configured see Handling multiple files in the Adapting Proof General manual 4 7 Escaping script management Occasionally you may want to review the dialogue of the entire session with the proof assistant or check that it hasn t done something unexpected Experienced users may also want to directly communicate with the proof assistant rather than sending commands via the minibuffer see Section 2 7 Proof assistant commands page 14 Although the proof shell is usually hidden from view it is run in a buffer which provides the usual full editing and history facilities of Emacs shells see the package comint el distributed with your version of Emacs You can switch to it using the menu Proof General gt Buffers gt Shell Warning you can probably cause confusion by typing in the shell buffer Proof General may lose track of the state of the proof assistant Output fro
15. component files and the names and positions of the functions or other named subunits in each file Grouping the related files makes it possible to search or replace through all the files with one command Recording the function names and positions makes possible the M command which finds the definition of a function by looking up which of the files it is in Some instantiations of Proof General currently LEGO and Coq are supplied with external programs legotags and cogtags for making tags tables For example invoking coqtags v produces a file TAGS for all files v in the current directory Invoking cogtags find name v produces a file TAGS for all files ending in v in the current directory structure Once a tag table has been made for your proof developments you can use the Emacs tags mechanisms to find tags and complete symbols from tags table One useful key binding you might want to make is to set the usual tags completion key M tab to run tag complete symbol to use completion from names in the tag table To set this binding in Proof General script buffers put this code in your emacs file add hook proof mode hook lambda local set key meta tab tag complete symbol Since this key binding interferes with a default binding that users may already have customized or may be taken by the window manager Proof General doesn t do this automatically Apart from complet
16. configuration is done with the settings proof goal with hole regexp and proof save with hole regexp Better configuration may be made manually with several other settings see the Adapting Proof General manual for further details To use Imenu select the option Proof General gt Options gt Index Menu This adds an Index menu to the main menu bar for proof script buffers You can also use M x imenu for keyboard driven completion of tags built from names in the buffer To use Function Menu distributed only with XEmacs use M x function menu To enable it by default each time you visit a proof script file i e avoid typing M x function menu you should find the file unc menu e1 and follow the instructions there Speedbar displays a file tree in a separate window on the display allowing quick navigation Middle double clicking or pressing on a file icon opens up to display tags definitions theorems etc within the file Middle double clicking on a file or tag jumps to that file or tag To use Speedbar use Tools gt Display Speedbar for GNU Emacs or 30 Proof General Proof General gt Advanced gt Speedbar for XEmacs If you prefer the old fashioned way M x speedbar does the same job For more information about Speedbar see http cedet sourceforge net speedbar shtml 5 5 Support for outline mode Proof General configures Emacs variables outline regexp and outline heading end regexp so that
17. customization setting lego www home page At present there is no easy way to save changes to other configuration variables across sessions other than by edit ing the source code In future versions of Proof General we plan to make all configuration settings editable in Customize by shadowing the settings as prover specific ones using the PA mechanism 40 Proof General Chapter 7 Hints and Tips 41 7 Hints and Tips Apart from the packages officially supported in Proof General many other features of Emacs are useful when using Proof General even though they need no specific configuration for Proof General It is worth taking a bit of time to explore the Emacs manual to find out about them Here we provide some hints and tips for a couple of Emacs features which users have found valuable with Proof General Further contributions to this chapter are welcomed 7 1 Adding your own keybindings Proof General follows Emacs convention for file modes in using prefix key bindings for its own functions which is why some of the default keyboard short cuts are quite lengthy Some users may prefer to add additional key bindings for shorter sequences This can be done interactively with the command M x local set key or for longevity by adding code like this to your emacs or xemacs init el file eval after load proof script progn define key proof mode map control n proof assert next command interactive def
18. in a taller pane on the left A prefix argument will prevent the horizontal split and result in three windows spanning the full width of the Emacs frame For multiple frame mode this function obeys the setting of pg response eagerly raise which see 6 4 User options Here is the complete set of user options for Proof General apart from the three display options mentioned above User options can be set via the customization system already mentioned via the old fashioned M x edit options mechanism or simply by adding setq s to your emacs file The first approach is strongly recommended Unless mentioned all of these settings can be changed dynamically without needing to restart Emacs to see the effect But you must use customize to be sure that Proof General reconfigures itself properly proof splash enable User Option If non nil display a splash screen when Proof General is loaded The default value is t 36 Proof General proof electric terminator enable User Option If non nil use electric terminator mode If electric terminator mode is enabled pressing a terminator will automatically issue proof assert next command for convenience to send the command straight to the proof process If the command you want to send already has a terminator character you don t need to delete the terminator character first Just press the terminator somewhere nearby Electric The default value is nil proof tool
19. in inverse video if you don t have a colour display before you see a window containing text like this theory Walkthrough which reflects the command just executed In this case of this first command it is hard to see the orange pink stage because the command is processed very quickly on most machines But in general processing commands can take an arbitrary amount of time or not terminate at all For this reason Proof General maintains a queue of commands which are sent one by one from the proof script As Isabelle successfully processes commands in the queue they will turn from the orange pink colour into blue The blue regions indicate text that has been read by the prover and should not be edited for this reason it is made read only by default e Next type on a new line theorem my theorem A amp B gt B amp A The goal we have set ourselves to prove should be displayed in the goals buffer e Now type proof assume A amp C This will update the goals buffer But whoops That was the wrong command we typed C instead of B e Press C c C BS to pretend that didn t happen Note BS means the backspace key This key press sends an undo command to Isabelle and deletes the assume command from the proof script If you just want to undo without deleting you can type C c C u instead or use the toolbar navigation button e Instead let s try assume A B Which is better e From this assumption we can get
20. option proof multiple frames enable User Option Whether response and goals buffers have separate frames If non nil Emacs will make separate frames screen windows for the goals and response buffers by altering the Emacs variable special display regexps The default value is nil Multiple frames work best when proof delete empty windows is off and proof three window mode is on Finally there are two commands available which help to switch between buffers or refresh the window layout These are on the menu Proof General gt Buffers proof display some buffers Command Display the reponse trace goals or shell buffer rotating A fixed number of repetitions of this command switches back to the same buffer Also move point to the end of the response buffer if it s selected If in three window or multiple frame mode display two buffers The idea of this function is to change the window gt buffer mapping without adjusting window layout proof layout windows amp optional nohorizontalsplit Command Refresh the display of windows according to current display mode For single frame mode this uses a canonical layout made by splitting Emacs windows verti cally in equal proportions You can then adjust the proportions by dragging the separating bars In three pane mode the canonical layout is to split both horizontally and vertically to display the prover responses in two panes on the right hand side and the proof script
21. path for Proof General and add auto loads and modes for the supported assistants The default names for proof assistant binaries may work on your system If not you will need to set the appropriate variables The easiest way to do this and most other customization of Proof General is via the Customize mechanism see the menu item Proof General gt Advanced gt Customize gt Name of Assistant gt Prog Name The Proof General menu is available from script buffers after Proof General is loaded To load it manually type M x load library RET proof RET If you do not want to use customize simply add a line like this setq coq prog name usr bin coqtop emacs to your emacs file A 5 Notes for syssies Here are some more notes for installing Proof General in more complex ways Only attempt things in this section if you really understand what you re doing Byte compilation Compilation of the Emacs lisp files improves efficiency but can sometimes cause compatibil ity problems especially if you use more than one version of Emacs with the same elc files Furthermore we develop Proof General with source files so may miss problems with the byte compiled versions If you discover problems using the byte compiled elc files which aren t present using the source el files please report them to us You can compile Proof General by typing make in the directory where you installed it Site wide installation If you are insta
22. pese 29 FU ERAT RR 1 G POC iia Ria eee ie 63 BOAl ood a ee Ver epus 10 goal save sequences eeeeeeeee KEET 10 goals butler A O 11 Greek letters oe ctr edet rer petes 27 28 H l sLOPy 223 6eheterese epe ien NOME E Ya eds 63 HOL Proof General o ooooooooomomooo 53 DEDU es chav dss de ri a tpr aad Canoe ed 29 Indentation 2 2 2 pods ee cee ae ewes S 35 index metu used aida pies erbe enden 29 Input TIBE oi editi peek 24 35 Isabelle commands 0 0 cc cee eee ences 49 73 Isabelle customizations lille esses 51 Isabelle logie ius eri sinto rede ERR RR Eds 51 Isabelle Proof General 000000000 cue 49 K key Sequences reser ereeE EXE e 5 keybindi gs r iai PEE RPeP REIS PER RP es 41 L LEGO Proof General 22er ERR EI 45 Lego Mode e tii aio Wd 1 63 Locked region eiereenibeenkre kae hr 10 logical symbols escrir arem ek 27 28 M t alhtenances sass seeds fei hes REIR euius 1 mathematical symbols 00 27 28 Metronic ren uev ERE Ped n atr 5 Multiple Elle RIP ee ED T 21 multiple fr mes o 2cclsc Rl Rete em 34 multiple windows emer mex bebe ee 34 outline mode clip astas dls ape ea kgs 30 P pink tert osoei rrr nE E E E rea 10 prefix argument o4 ver e see eas sees 13 proof assistant es ise iecur ti ER ER RE CER 3 proof by pointing sere rr I1 63 Proof General 22b bbs ae achete ads 3 Proof General Kit 2 22 2
23. rather than the two buffer mode where they are switched between It also prevents Emacs automatically resizing windows between proof steps If you use several frames the same Emacs in several windows on the screen you can force a frame to stick to showing the goals or response buffer The default value is nil Sometimes during script management there is no response from the proof assistant to some command In this case you might like the empty response window to be hidden so you have more room to see the proof script The setting proof delete empty windows helps you do this proof delete empty windows User Option If non nil automatically remove windows when they are cleaned For example at the end of a proof the goals buffer window will be cleared if this flag is set it will automatically be removed If you want to fix the sizes of your windows you may want to set this variable to nil to avoid windows being deleted automatically If you use multiple frames only the windows in the currently selected frame will be automatically deleted The default value is nil Chapter 6 Customizing Proof General 35 This option only has an effect when you have set proof three window mode If you are working on a machine with a window system you can use Emacs to manage several frames on the display to keep the goals buffer displayed in a fixed place on your screen and in a certain font for example A convenient way to do this is via the user
24. set to a space The default value is proof rsh command User Option Shell command prefix to run a command on a remote host For example ssh bigjobs Would cause Proof General to issue the command ssh bigjobs isabelle to start Isabelle remotely on our large compute server called bigjobs The protocol used should be configured so that no user interaction passwords or whatever is required to get going For proper behaviour with interrupts the program should also communicate signals to the remote host The default value is nil 6 5 Changing faces The fonts and colours that Proof General uses are configurable If you alter faces through the customize menus or the command M x customize face only the particular kind of display in use colour window system monochrome window system console will be affected This means you can keep separate default settings for each different display environment where you use Proof General As well as the faces listed below Proof General may use the regular font lock faces eg font lock keyword face font lock variable name face etc for fontifying the proof script or proof assistant output These can be altered to your taste just as easily but note that changes will affect all other modes which use them proof queue face Face Face for commands in proof script waiting to be processed proof locked face Face Face for locked region of proof script processed commands proo
25. test is to start an Emacs shell with M x shell and type a command such as yes which produces output indefinitely Now see if you can interrupt the process Warning on slower machines especially this can cause lockups so use a fresh Emacs 18 Proof General Chapter 3 Subterm Activation and Proof by Pointing 19 3 Subterm Activation and Proof by Pointing This chapter describes what you can do from inside the goals buffer providing support for these features exists for your proof assistant As of Proof General 3 0 it only exists for LEGO If you would like to see subterm activation support for Proof General in another proof assistant please petition the developers of that proof assistant to provide it 3 1 Goals buffer commands When you are developing a proof the input focus Emacs cursor is usually on the script buffer Therefore Proof General binds mouse buttons for commands in the goals buffer to avoid the need to move the cursor between buffers The mouse bindings are these button2 pg goals button action C button2 proof undo and delete last successful command button3 pg goals yank subterm Where button2 indicates the middle mouse button and button3 indicates the right hand mouse button The idea is that you can automatically construct parts of a proof by clicking Using the middle mouse button asks the proof assistant to try to do a step in the proof based on where you click If you don t like the command which
26. to automatically activate proof assert next command interactive for convenience Rather than use a file command inside the proof assistant to read a proof script a good reason to use C c C b proof process buffer is that with a faulty proof script e g a script you are adapting to prove a different theorem Proof General will stop exactly where the proof script fails showing you the error message and the last processed command So you can easily continue development from exactly the right place in the script Here is the full set of script processing commands proof assert next command interactive Command Process until the end of the next unprocessed command after point If inside a comment just process until the start of the comment proof undo last successful command Command Undo last successful command at end of locked region In fact this is an unnecessary restriction imposed by the original design of Proof General There is nothing to stop future versions of Proof General allowing the queue region to be extended or shrunk whilst the prover is processing it Proof General 3 0 already relaxes the original design by allowing successive assertion commands without complaining 14 Proof General proof undo and delete last successful command Command Undo and delete last successful command at end of locked region Useful if you typed completely the wrong command Also handy for proof by pointing in case the last proof by po
27. to the cursor that appears before it If you simply want to retract the whole file in one go you can use the key C c C r which corresponds to the up arrow on the toolbar which will automatically move the cursor to the top of the file e Now improve the goal name for example theorem and_commutes A amp B gt B amp A You can swiftly replay the rest of the buffer now with C c C b or the down arrow on the toolbar e At the end of the buffer you may insert the command end to complete the theory Notice that if you right click on one of the highlighted regions in the blue area you will see a context menu for the region This includes a show hide option for folding a proof as well as some editing commands for copying the region or rearranging its order in the processed text move up move down These latter commands occasionally help you reorder text without needing to reprove it although they risk breaking the proof Finally once you are happy with your theory you should save the file with C x C s before moving on to edit another file or exiting Emacs If you forget to do this Proof General or Emacs will surely prompt you sooner or later 2 2 Proof scripts A proof script is a sequence of commands which constructs definitions declarations theories and proofs in a proof assistant Proof General is designed to work with text based interactive proof assistants where the mode of working is usually a dialogue bet
28. tree including all of the elisp and documentation along with our low level list of things to do sources for the images some make files used to generate the release itself from our CVS repository and some test files Developers interested in accessing our CVS repository directly should contact da pg support inf ed ac uk A 2 Installing Proof General from tarball Copy the distribution to some directory mydir Unpack it there For example cd mydir gunzip ProofGeneral version tar gz tar xpf ProofGeneral version tar If you downloaded the version called latest you ll find it unpacks to a numeric version number Proof General will now be in some subdirectory of mydir The name of the subdirectory will depend on the version number of Proof General For example it might be ProofGeneral 2 0 It s convenient to link it to a fixed name ln sf ProofGeneral 2 0 ProofGeneral Now put this line in your emacs file load file mydir ProofGeneral generic proof site el A 3 Installing Proof General from RPM package To install an RPM package you need to be root Then type rpm Uvh ProofGeneral latest noarch rpm Now add the line load file usr share emacs ProofGeneral generic proof site el to your emacs or the site wide initialisation file site start el 58 Proof General A 4 Setting the names of binaries The load file command you have added will load proof site which sets the Emacs load
29. was inserted into the script you can use the control key with the middle button to undo the step and delete it from your script Note that proof by pointing may construct several commands in one go These are sent back to the proof assistant altogether and appear as a single step in the proof script However if the proof is later replayed without using PBP the proof by pointing constructions will be considered as separate proof commands as usual pg goals button action event Command Construct a proof by pointing command based on the mouse click event This function should be bound to a mouse button in the Proof General goals buffer The event is used to find the smallest subterm around a point A position code for the subterm is sent to the proof assistant to ask it to construct an appropriate proof command The command which is constructed will be inserted at the end of the locked region in the proof script buffer and immediately sent back to the proof assistant If it succeeds the locked region will be extended to cover the proof by pointing command just as for any proof command the user types by hand Proof by pointing uses markup describing the term structure of the concrete syntax output by the proof assistant This markup is useful in itself it allows you to explore the structure of a term using the mouse the smallest subexpression that the mouse is over is highlighted and easily copy subterms from the output to a proof script
30. work across multiple files It was time to come up with a better name than just proof mode David Aspinall suggested Proof General and set about reorganizing the file structure to disentangle the Proof General project from LEGO at last He cooked up some images and bolted on a toolbar so a naive user can replay proofs without knowing a proof assistant language or even Emacs hot keys He also designed some web pages and wrote most of this manual Despite views of some detractors we demonstrated that an interface both friendly and powerful can be built on top of Emacs Proof General 2 0 was the first official release of the improved program made in December 1998 Version 2 1 was released in August 1999 It owas used at the Types Summer School held in Giens France in September 1999 see http www sop inria fr types project types sum school html About 50 students learning Coq Isabelle and LEGO used Proof General for all three systems This experience provided invaluable feedback and encouragement to make the improvements that went into Proof General 3 0 64 Proof General Old News for 3 0 Proof General 3 0 released November 1999 has many improvements over 2 x releases First there are usability improvements The toolbar was somewhat impoverished before It now has twice as many buttons and includes all of the useful functions used during proof which were previously hidden on the menu or even only available as key presses Key bin
31. xemacs node Easy Customization 6 3 Display customization By default Proof General displays two buffers during scripting in a split window on the display One buffer is the script buffer The other buffer is either the goals buffer e g isabelle goals or the response buffer isabelle response Proof General switches between these last two automatically Proof General allows several ways to customize this default display model by splitting the Emacs frames in different ways and maximising the amount of information shown or by using multiple frames The customization options are explained below they are also available on the menu Proof General gt Options gt Display and you can save your preferred default If your screen is large enough you may prefer to display all three of the interaction buffers at once This is useful for example to see output from the proof find theorems command at the same time as the subgoal list Set the user option proof three window enable to make Proof General keep both the goals and response buffer displayed proof three window enable User Option Whether response and goals buffers have dedicated windows If non nil Emacs windows displaying messages from the prover will not be switchable to display other windows This option can help manage your display Setting this option triggers a three buffer mode of interaction where the goals buffer and response buffer are both displayed
32. 1 See Chapter 8 LEGO Proof General page 45 for more details e Coq Proof General for Coq Version 6 3 7 x 8 x See Chapter 9 Coq Proof General page 47 for more details e Isabelle Proof General for Isabelle2005 and Isabelle2007 See Chapter 10 Isabelle Proof General page 49 and documentation supplied with Isabelle for more details e HOL Proof General for HOL98 HOL4 See Chapter 11 HOL Proof General page 53 for more details e Shell Proof General for shell scripts not really a proof assistant See Chapter 12 Shell Proof General page 55 for more details Proof General is designed to be generic so if you know how to write regular expressions you can make e Your Proof General for your favourite proof assistant For more details of how to make Proof General work with another proof assistant see the accompanying manual Adapting Proof General The exact list of Proof Assistants supported may vary according to the version of Proof General you have and its local configuration only the standard instances documented in this manual are listed above Note that there is some variation between the features supported by different instances of Proof General The main variation is proof by pointing which is only supported in LEGO at the moment For advanced features like this some extensions to the output routines of the proof assistant are required typically If you like Proof General please help us by asking the imple me
33. 2 20 pida 1 proof Script citadino 9 Proof script indentation isses esses 35 proof script Modes iiie bee br irea 10 Q Query program NaMe o res le tipki A utatu res 35 Queue region ercon ieran rnr as eg es ll 10 R Remote host 22b te a sade oa E yee 35 Remote shell222245 bei ROI esOTex ede PIS 35 response b lfer 2ez sa RE RR ue 11 Retraction uz duo pese e ira a 10 23 Running proof assistant remotely 35 74 SAVE Caged Ig Xe ae We E Saber deo eda ee PEE EIE EE 10 script DUfler ire 10 script management veyed tiene b 4 eee ese de 63 SCHIPUNG i A 9 Shell lose ee nbl MERO ETE 23 shell butler uses A Lc nS RE D Shell Proof General 0 000s eee eee 55 Speedbatr n seeded doe e E Pee Rd 29 Strict fead Only ser rr 35 Structure edito ita webct ia dl bed 63 Switching between proof scripts 21 symbols i sebeenreR e 21 28 T TAGS EEEE RETE 31 three buffer interaction o oooooooomomoo 34 Toolbar button enablers o oooooooooooo 35 Toolbar disabling 22r data 35 Proof General Toolbar follow mode 00c cece ene enee 95 U Undo in read only region 004 35 User Options merou lerem n n9 bee PEERS 35 Using Customize oe cerrEI RE ErepIrrR EE 33 V Visibility of proofs sea sedeo PORePHER EYE 21 W Why use Proof General 000 0000 4 X A oymbols id rent E Oeo erede 27 28 Table o
34. B and A by the trivial step which splits the assumption using an elimination step then obtain B and A e Finally we establish the goal by the trivial step again which triggers an introduction rule then show B amp A After this proof step the message from Isabelle indicates that the proof has succeeded so we can conclude the proof with the qed command e Finally type qed This last command closes the proof and saves the proved theorem Moving the mouse pointer over the locked region now reveals that the entire proof has been aggregated into a single segment if you did this before you would see highlighting of each command separately This reflects the fact that Isabelle has thrown away the history of the proof so if we want to undo now the whole proof must be retracted e Suppose we decide to call the theorem something more sensible Move the cursor up into the locked region somewhere between theorem and qed enter C c C RET Chapter 2 Basic Script Management 9 You see that the locked segment for the whole proof is now unlocked and uncoloured it is transferred back into the editing region The command C c C RET moves the end of the locked region to the cursor position or as near as possible above or below it sending undoing commands or proof commands as necessary In this case the locked region will always be moved back to the end of the theory line since that is the closest possible position
35. Hide all completed proofs in the buffer proof disappearing proofs User Option Non nil causes Proof General to hide proofs as they are completed The default value is nil 4 2 Switching between proof scripts Basic modularity in large proof developments can be achieved by splitting proof scripts across various files Let s assume that you are in the middle of a proof development You are working on a soundness proof of Hoare Logic in a file called HSound 1 It depends on a number of other The suffix may depend of the specific proof assistant you are using e g LEGO s proof script files have to end with faq 22 Proof General files which develop underlying concepts e g syntax and semantics of expressions assertions imperative programs You notice that the current lemma is too difficult to prove because you have forgotten to prove some more basic properties about determinism of the programming language Or perhaps a previous definition is too cumbersome or even wrong At this stage you would like to visit the appropriate file say sos 1 and retract to where changes are required Then using script management you want to develop some more basic theory in sos 1 Once this task has been completed possibly involving retraction across even earlier files and the new development has been asserted you want to switch back to HSound 1 and replay to the point you got stuck previously Some hours or days later
36. P C Callaghan durham ac uk gt Coq Proof General was written by Healfdene Goguen with later contributions from Patrick Loiseleur It is now maintained by Pierre Courtieu lt courtieu lri fr gt Isabelle Proof General was written and is being maintained by David Aspinall lt David AspinallGed ac uk gt It has benefited greatly from tweaks and suggestions by Markus Wenzel lt wenzelm informatik tu muenchen de gt who wrote Isabelle Isar Proof General and added Proof General support inside Isabelle David von Oheimb supplied the original patches for X Symbol support which improved Proof General significantly Christoph Wedler the author of X Symbol has provided much useful support in adapting his package for PG The generic base for Proof General was developed by Kleymann Sequeira Goguen and Aspinall It follows some of the ideas used in Project CROAP The project to implement a proof mode for LEGO was initiated in 1994 and coordinated until October 1998 by Thomas Kleymann becoming generic along the way In October 1998 the project became Proof General and has been managed by David Aspinall since then This manual was written by David Aspinall and Thomas Kleymann Some words found their way here from the user documentation of LEGO mode prepared by Dilip Sequeira Healfdene Goguen supplied some text for Coq Proof General Since Proof General 2 0 this manual has been maintained and improved by David Aspinall Pierre Courtieu and Markus Wenzel co
37. Proof General Organize your proofs User Manual for Proof General 3 7 January 2008 proofgeneral inf ed ac uk David Aspinall and Thomas Kleymann with P Courtieu H Goguen D Sequeira M Wenzel This manual and the program Proof General are Copyright 1998 2008 Proof General team LFCS Edinburgh Permission is granted to make and distribute verbatim copies of this manual provided the copy right notice and this permission notice are preserved on all copies This manual documents Proof General Version 3 7 for use with XEmacs 21 5 28 and GNU Emacs 22 1 1 or later versions subject to Emacs API changes Proof General is distributed under the terms of the GNU General Public License GPL please check the accompanying file COPYING for more details Visit Proof General on the web at http proofgeneral inf ed ac uk ProofGeneral texi v 9 1 2008 01 31 19 41 17 da Exp Preface 1 Preface Welcome to Proof General This preface has some news about the current release future plans and acknowledgements to those who have helped along the way The appendix History of Proof General page 63 contains old news about previous releases and notes on the development of Proof General Proof General has a home page at http proofgeneral inf ed ac uk Visit this page for the latest version of this manual other documentation system downloads etc Latest news for version 3 7 Proof General version 3 7 collects together a cu
38. Thomas Kleymann managed to implement a first prototype of proof by pointing in the Emacs interface for LEGO BKS97 Perhaps we could reuse even more of the CtCoq system It being a structure editor did no longer seem to be such an obstacle Moreover to conveniently use proof by pointing in actual developments one would need better support for script management In 1997 Dilip Sequeira implemented script management in our Emacs interface for LEGO following the recipe in B T98 Inspired by the project CROAP the implementation made some effort to be generic A working prototype was demonstrated at UITP 97 In October 1997 Healfdene Goguen ported lego mode to Coq Part of the generic code in the lego package was outsourced and made more generic in a new package called proof Dilip Sequeira provided some LEGO specific support for handling multiple files and wrote a few manual pages The system was reasonably robust and we shipped out the package to friends In June 1998 David Aspinall reentered the picture by providing an instantiation for Isabelle Actually our previous version wasn t quite as generic as we had hoped Whereas LEGO and Coq are similar systems in many ways Isabelle was really a different beast Fierce re engineering and various usability improvements were provided by Aspinall and Kleymann to make it easier to instantiate to new proof systems The major technical improvement was a truly generic extension of script management to
39. a ac AAA Rp cede beu 31 6 Customizing Proof General esos o Rh xen 33 0 1 Basic OpUlODS e eee os rape egit o ids ve o RURAL os Rx ad ed UE d 33 0 2 How to CUSTOMIZO i5 exer aa RAE ENERO RR CURE OR RUE RR 33 6 3 Display customization inercia daa ended eR stand RARI e e 34 GA Teropong 2 553 d re EID de ln b S alana a Ep a ee E te de re ah o e 35 0 5 Changing facs ius cata nt ta A oor dod M RR AAA BoE pede RU a Rl C dec 38 6 6 Tweaking configuration settings 0 cece hh hh 39 T Hints and Lips xr REESE xaasmkG RR 41 7 1 Adding your own keybindings 0 0 eee cece ete hn 41 12 Using fle variables idad eke ie ad Ge bea RUP NERA phat edo ee ded de 41 To Usine abbreviations supina be rae A Dd pe Das Br e Use dU ra d one 42 S LEGO Proof General n rr Rx ERROR 45 8 1 LEGO specihe commands esee emo see t hone o e on Reg 45 82 LEGO TABS 4 2 Eee ident doti domat rud d ecd m Ran RA ae 45 8 3 LEGO customizations 24 414 ee EATER eto ned qu edu ed acd men edu ed aed ee 45 9 Coq Proof General eee hn 47 9 1 Coq specific commands ooo 47 9 2 Coqg specific variables ecu ci a hie id MUR EL COTRA RR de 47 9 3 Editing multiple proofs issssseseseleesslll n ene hh 4T 9 4 User loaded tactics ssssssssssesesleellel hh hh rh 48 9 5 Holes feature eaa cede ate er eh UA toting deck Ead dad ead du ded eee 48 10 Isabelle Proof General ooooooooooooocooooo 49 10 1 Isabelle c
40. ant we write PA for these names In this chapter we only consider the generic settings ones which apply to all proof assistants globally or individually The support for a particular proof assistant may provide extra indi vidual customization settings not available in other proof assistants See the chapters covering each assistant for details of those settings 6 1 Basic options Proof General has some common options which you can toggle directly from the menu Proof General gt Options The effect of changing one of these options will be seen immediately or in the next proof step The window control options on this menu are described shortly See Section 6 3 Display customization page 34 To save the current settings for these options only use the Save Options command in the submenu Proof General gt Options gt Save Options or M x customize save customized The options on this sub menu are also available in the complete user customization options group for Proof General For this you need to know a little bit about how to customize in Emacs 6 2 How to customize Proof General uses the Emacs customization library to provide a friendly interface You can access all the customization settings for Proof General via the menu Proof General gt Advanced gt Customize Using the customize facility is straightforward You can select the setting to customize via the menus or with M x customize variable When you ha
41. assumes that the proof script has a series of proofs which look something like this goal mythm is G save theorem mythm interspersed with comments definitions and the like Of course the exact syntax and termi nology will depend on the proof assistant you use The name mythm can appear in a menu for the proof script to help quickly find a proof see Section 5 4 Imenu and Speedbar and Function Menu page 29 Chapter 2 Basic Script Management 11 2 3 3 Active scripting buffer You can edit as many script buffers as you want simultaneously but only one buffer at a time can be used to process a proof script incrementally this is the active scripting buffer The active scripting buffer has a special indicator the word Scripting appears in its mode line When you use a scripting command it will automatically turn a buffer into the active scripting mode You can also do this by hand via the menu command Toggle Scripting or the key C c C s C c C s proof toggle active scripting When active scripting mode is turned on several things may happen to get ready for scripting exactly what happens depends on which proof assistant you are using and some user settings First the proof assistant is started if it is not already running Second a command is sent to the proof assistant to change directory to the directory of the current buffer If the current buffer corresponds to a file this is the directory the file lives in This is in
42. bar enable User Option If non nil display Proof General toolbar for script buffers The default value is t PA x symbol enable User Option Whether to use x symbol in Proof General for this assistant If you activate this variable whether or not you really get x symbol support depends on whether your proof assistant supports it and whether X Symbol is installed in your Emacs The default value is nil proof output fontify enable User Option Whether to fontify output from the proof assistant If non nil output from the proof assistant will be highlighted in the goals and response buffers This is providing font lock keywords have been set for the buffer modes The default value is t proof strict read only User Option Whether Proof General is strict about the read only region in buffers If non nil an error is given when an attempt is made to edit the read only region If nil Proof General is more relaxed but may give you a reprimand The default value is strict proof allow undo in read only User Option Whether Proof General allows text undo in the read only region If non nil undo will allow altering of processed text default behaviour before Proof General 3 7 If nil undo history is cut at first edit of processed text NB the history manipulation only works on GNU Emacs The default value is nil proof toolbar use button enablers User Option If non nil toolbars buttons may be enabled disabled automati
43. bol mode to turn on and off X Symbol display in the scripting buffer as you would when using X Symbol for other modes or indeed as for any other Emacs minor mode However this way of turning on and off symbols will only affect the current script BR 28 Proof General buffer and will not change the status of any symbol configuration for the prover input output some proof assistants such as Isabelle have switches for enabling symbol output To make sure that symbol output is switched on or off for the prover as a whole use the menu option mentioned above or its underlying command M x proof x symbol toggle Notice that for proper symbol support the proof assistant needs to have a special token language or a special character set to use symbols In this case the proof assistant will output and accept as input tokens like longrightarrow which display as the corresponding symbols However for proof assistants which do not have such token support we can use fake symbol support quite effectively displaying ordinary ASCII character sequences such as gt with symbols For more information about the X Symbol package please visit its home page at http x symbol sourceforge net 5 3 Unicode support Proof General inherits support for displaying Unicode and any other fonts from the underlying Emacs program If you are lucky your system will be able to use or synthesise a font that provides a rich set of mathematical symbols
44. cally Toolbar buttons can be automatically enabled disabled according to the context Set this variable to nil if you don t like this feature or if you find it unreliable The default value is t proof query file save when activating scripting User Option If non nil query user to save files when activating scripting Often activating scripting or executing the first scripting command of a proof script will cause the proof assistant to load some files needed by the current proof script If this option is non nil the user will be prompted to save some unsaved buffers in case any of them corresponds to a file which may be loaded by the proof assistant You can turn this option off if the save queries are annoying but be warned that with some proof assistants this may risk processing files which are out of date with respect to the loaded buffers The default value is t Chapter 6 Customizing Proof General 37 PA script indent User Option If non nil enable indentation code for proof scripts The default value is t proof one command per line User Option If non nil format for newlines after each proof command in a script This option is not fully functional at the moment The default value is nil proof prog name ask User Option If non nil query user which program to run for the inferior process The default value is nil proof prog name guess User Option If non nil use proof guess command line to guess proof pro
45. case any scripting commands refer to files in the same directory as the script The third thing that may happen is that you are prompted to save some unsaved buffers This is in case any scripting commands may read in files which you are editing Finally some proof assistants may automatically read in files which the current file depends on implicitly In Isabelle for example there is an implicit dependency between a ML script file and a thy theory file which defines its theory If you have a partly processed scripting buffer and use C c C s or you attempt to use script processing in a new buffer Proof General will ask you if you want to retract what has been proved so far Scripting incomplete in buffer myproof 1 retract or if you want to process the remainder of the active buffer Completely process buffer myproof 1 instead before you can start scripting in a new buffer If you refuse to do either Proof General will give an error message Cannot have more than one active scripting buffer To turn off active scripting the buffer must be completely processed all blue or completely unprocessed There are two reasons for this First it would certainly be confusing if it were possible to split parts of a proof arbitrarily between different buffers the dependency between the commands would be lost and it would be tricky to replay the proof Second we want to interface with file management in the proof assistant Proof General assumes that a p
46. dings have been re organized users of previous versions may notice The menu has been redesigned and coordinated with the toolbar and now gives easy access to more of the features of Proof General Previously several features were only likely to be discovered by those keen enough to read this manual Second there are improvements extensions and bug fixes in the generic basis Proofs which are unfinished and not explicitly closed by a save type command are supported by the core if they are allowed by the prover The design of switching the active scripting buffer has been streamlined The management of the queue of commands waiting to be sent to the shell has been improved so there are fewer unnecessary Proof Process Busy messages The support for scripting with multiple files was improved so that it behaves reliably with Isabelle99 file reading messages can be communicated in both directions now The proof shell filter has been optimized to give hungry proof assistants a better share of CPU cycles Proof by pointing has been resurrected even though LEGO s implementation is incomplete it seems worth maintain ing the code in Proof General so that the implementors of other proof assistants are encouraged to provide support For one example we can certainly hope for support in Coq since the CtCoq proof by pointing code has been moved into the Coq kernel lately We need a volunteer from the Coq community to help to do this An importan
47. ds in a file with the extension pgsh and load up Proof General Now use the toolbar to send each line of the file to your tool and have the output displayed clearly in another window Much easier and more pleasant for your audience to watch If you wish you may adjust the value of proof prog name in pgshell el to launch your program rather than the shell interpreter We welcome feedback and suggestions concerning this subsidiary provision in Proof General Please recommend it to your colleagues e g the model checking crew 56 Proof General Appendix A Obtaining and Installing 57 Appendix A Obtaining and Installing Proof General has its own home page hosted at Edinburgh Visit this page for the latest news A 1 Obtaining Proof General You can obtain Proof General from the URL http proofgeneral inf ed ac uk The distribution is available in three forms e A source tarball http proofgeneral inf ed ac uk ProofGeneral devel latest tar gz e A Linux RPM package for any architecture http proofgeneral inf ed ac uk ProofGeneral latest noarch rpm e A developer s tarball http proofgeneral inf ed ac uk ProofGeneral devel latest tar gz Both the source tarball and the RPM package include the generic elisp code and code for LEGO Coq Isabelle and other provers Also included are installation instructions reproduced in brief below and this documentation The developer s tarball contains our full source
48. e ML code Command termination via is an optional feature of Isar syntax Neither Isabelle nor Proof General require semicolons to do their job The following command allows to get rid of command terminators in existing texts isar strip terminators Command Remove explicit Isabelle Isar command terminators from the buffer Chapter 10 Isabelle Proof General 51 10 2 Logics and Settings The prover specific menu the same on both Isabelle variants of Proof General offers a way to select the invoked object logic and also access to numerous settings of Isabelle If you look at the menu Isabelle gt Logics gt you should see the list of logics available to Isabelle This menu is generated from the output of the command isatool findlogics so you should check that Proof General can find the isatool program for it to operate correctly Similarly the documentation menu is partly generated from isatool doc The logics menu is refreshed dynamically so you can select any newly built heap images in the same Emacs session However notice that the choices are greyed out while Isabelle is actually runnning you can only switch to a new logic if you first exit Isabelle similarly to Proof General Isabelle operates with only one logic at a time The prover specific menu also contains a Settings submenu which allows you to configure things such as the behaviour of Isabelle s term pretty printer display of types sor
49. e script buffer The goals buffer has facility for proof by pointing e The response buffer displays other output from the proof assistant for example error mes sages or informative messages The response buffer is displayed whenever Proof General puts a new message in it e The trace buffer is a special version of the response buffer It may be used to display unusual debugging output from the prover for example tracing proof tactics or rewriting procedures This buffer is also displayed whenever Proof General puts a new message in it although it may be quickly replaced with the response or goals buffer in two buffer mode Normally Proof General will automatically reveal and hide the goals and response buffers as nec essary during scripting However there are ways to customize the way the buffers are displayed see Section 6 3 Display customization page 34 The menu Proof General gt Buffers provides a convenient way to display or switch to a Proof General buffer the active scripting buffer the goal or response buffer the tracing buffer or the shell buffer Another command on this menu Clear Responses clears the response and tracing buffer 2 5 Script editing commands Proof General provides a few functions for editing proof scripts The generic functions mainly consist of commands to navigate within the script Specific proof assistant code may add more to these basics Indentation is controlled by the user option proof scri
50. ents for new versions of provers in particular Coq 7 and new versions of emacs in particular XEmacs 21 4 One new feature is control over visibility of completed proofs See Section 4 1 Visibility of completed proofs page 21 Another new feature is the tracking of theorem dependencies inside Isabelle A context sensitive menu right button on proof scripts provides facility for browsing the ancestors and child theorems of a theorem and highlighting them The idea of this feature is that it can help you untangle and rearrange big proof scripts by seeing which parts are interdependent The implementation is provisional and not documented yet in the body of this manual It only works for the classic version of Isabelle99 2 Old News for 3 4 Proof General 3 4 adds improvements and also compatibility fixes for new versions of Emacs in particular for GNU Emacs 21 which adds the remaining pretty features that have only been available to XEmacs users until now the toolbar and X Symbol support One major improvement has been to provide better support for synchronization with Coq proof scripts now Coq Proof General should be able to retract and replay most Coq proof scripts reliably Credit is due to Pierre Courtieu who also updated the documentation in this manual As of version 3 4 Proof General is distributed under the GNU General Public License GPL Compared with the previous more restrictive license this means the program can no
51. enu Electric terminator sends commands to the proof assistant as you type them The exact key binding is based on the terminator used for your proof assistant but you can always check the menu if you re not sure Electric terminator mode is popular but not enabled by default because of the principle of least surprise Moreover in Isabelle the semicolon terminators are strictly optional so proof scripts are usually written without them to avoid clutter Without electric terminator you can trigger processing the text up to the current position of the point with the key C c C RET or just up to the next command with C c C n We show the rest of the example in Isabelle with semi colons but you can miss them out Coq on the other hand requires a full stop terminator at the end of each line If you want to use electric terminator you can customize Proof General to enable it everytime if you want See Chapter 6 Customizing Proof General page 33 For this option customization is particularly easy just use the menu item Proof General gt Options to select some common options and Proof General gt Options gt Save Options to save your choices 8 Proof General At the moment you type the semicolon the theory command will be sent to Isabelle behind the scenes First there is a short delay while Isabelle is launched you may see a welcome message Then you may notice that the command briefly is given an orange pink background or shown
52. essing and retraction or undoing Assertion causes commands from the editing region to be transferred to the queue region and sent one by one to the proof process If the command is accepted it is transferred to the locked region but if an error occurs it is signalled to the user and the offending command is transferred back to the editing region together with any remaining commands in the queue Assertion corresponds to processing proof commands and makes the locked region grow Retraction causes commands to be transferred from the locked region to the editing region again via the queue region and the appropriate undo commands to be sent to the proof process Retraction corresponds to undoing commands and makes the locked region shrink For details of the commands available for doing assertion and retraction See Section 2 6 Script processing commands page 13 2 3 2 Goal save sequences A proof script contains a sequence of commands used to prove one or more theorems As commands in a proof script are transferred to the locked region they are aggregated into segments which constitute the smallest units which can be undone Typically a segment consists of a declaration or definition or all the text from a goal command to the corresponding save command or the individual commands in the proof of an unfinished goal As the mouse moves over the the region the segment containing the pointer will be highlighted Proof General therefore
53. eviously imported modules Therefore reasserting the extended module declaration really only processes the newly imported modules Using the LEGO Proof General you never ever need to use administrative LEGO commands such as Forget ForgetMark KillRef Load Make Reload and Undo again 8 1 LEGO specific commands In addition to the commands provided by the generic Proof General as discussed in the previous sections the LEGO Proof General provides a few extensions In proof scripts there are some abbreviations for common commands C c C a C i intros C c C a C I Intros C c C a C R Refine 8 2 LEGO tags You might want to ask your local system administrator to tag the directories lib_Prop lib_Type and lib_TYPE of the LEGO library See Section 5 7 Support for tags page 31 for further details on tags 8 3 LEGO customizations We refer to chapter Chapter 6 Customizing Proof General page 33 for an introduction to the customisation mechanism In addition to customizations at the generic level for LEGO you can also customize lego tags User Option The directory of the tags table for the lego library The default value is usr lib lego lib Type lego www home page Variable Lego home page URL l And please don t even think of including those in your LEGO proof script 46 Proof General Chapter 9 Coq Proof General 4T 9 Coq Proof General C
54. f Contents Preface 2225 PR 1 Latest news for version 3 7 00 cece cee tenet ten ete hh hh hh 1 Iu c pe LUUD il ici TIE 1 1 Introducing Proof General eere eee 3 1 1 Installing Proof General oooccooocccococc hh hh 3 1 2 Quick start gulde eid Eae tae dad bene dad MAb RULES E aaa ead Bee 3 1 3 Featuresvof Proof General 3 022344 cp east pec bb UR ERR RUE eoe ge 4 1 4 Supported proof assistants isses hh hh 5 1 5 Prerequisites for this manual o ooccccoccccccnccccrncccr e Ea 5 1 6 Organization of this mantial 9 202000 snnt ee eed ewe Bee Penge ee es 6 2 Basic Script Management leen T 2 1 Walkthrough example in Isabelle 0000 nee 7 2 2 Prool SCripts 4244 aeaaea a aae uri tdt ue prete don sped Re agen dta ee Chee 9 2 9 SeripU butlers 1e dia qu ake Ru RU RERCR Cd peed alee diy Hawa Mn c Dl a RE d 10 2 3 1 Locked queue and editing regions 00 ee cece rr 10 2 3 2 Goal save sequences iucunde ee ad endure ERU IA uo oS RACE DR ie 10 23 3 cdXetive scripting DU ii rete eoe Eb Veo one to o Rae RR Rad 11 2 4 Summary of Proof General bufferS o oocooooccocoococooor ss 11 2 5 Seript editing commands ssc sexa hd cd RI od PRA eC ned A a 12 2 6 Script processing commands 0c cece seh aia han 13 2 7 Proof assistant commands eriscepidii piiriin kia a ENA EESE hh hne 14 2 8 Toolbar commands esscr rini aria iE E EEA A E E 16 2 9
55. f error face Face Face for error messages from proof assistant proof warning face Face Face for warning messages Warning messages can come from proof assistant or from Proof General itself Chapter 6 Customizing Proof General 39 proof debug message face Face Face for debugging messages from Proof General proof declaration name face Face Face for declaration names in proof scripts Exactly what uses this face depends on the proof assistant proof tacticals name face Face Face for names of tacticals in proof scripts Exactly what uses this face depends on the proof assistant proof eager annotation face Face Face for important messages from proof assistant The slightly bizarre name of the last face comes from the idea that while large amounts of output are being sent from the prover some messages should be displayed to the user while the bulk of the output is hidden The messages which are displayed may have a special annotation to help Proof General recognize them and this is an eager annotation in the sense that it should be processed as soon as it is observed by Proof General 6 6 Tweaking configuration settings This section is a note for advanced users Configuration settings are the per prover customizations of Proof General These are not in tended to be adjusted by the user But occasionally you may like to test changes to these settings to improve the way Proof General works You may want to do this w
56. f the Proof General project is to provide powerful environments and tools for interactive proof Proof General has been Emacs based so far and uses heavy per prover customisation The new Proof General Kit project proposes that proof assistants use a standard XML based protocol for interactive proof dubbed PGIP PGIP will enable middleware for interactive proof tools and interface components Rather than configuring Proof General for your proof assistant you will need to configure your proof assistant to understand PGIP There is a similarity however the design of PGIP was based heavily on the Emacs Proof General framework At the time of writing the Proof General Kit software is in a prototype stage We have a prototype Proof General plugin for the Eclipse IDE and a prototype version of a PGIP enabled Isabelle There is also a middleware component for co ordinating proof written in Haskell the Proof General Broker Further collaborations are sought for more developments especially the PGIP enabling of other provers For more details see the Proof General Kit webpage Help us to help you organize your proofs Credits The original developers of the basis of Proof General were e David Aspinall 2 Proof General e Healfdene Goguen e Thomas Kleymann and e Dilip Sequeira LEGO Proof General the successor of lego mode was written by Thomas Kleymann and Dilip Sequeira It is presently maintained by David Aspinall and Paul Callaghan
57. g name This option is compatible with proof prog name ask No effect if proof guess command line is nil The default value is nil proof tidy response User Option Non nil indicates that the response buffer should be cleared often The response buffer can be set either to accumulate output or to clear frequently With this variable non nil the response buffer is kept tidy by clearing it often typically between successive commands just like the goals buffer Otherwise the response buffer will accumulate output from the prover The default value is t proof keep response history User Option Whether to keep a browsable history of responses With this feature enabled the buffers used for prover responses will have a history that can be browsed without processing undoing in the prover Changes to this variable take effect after restarting the prover The default value is nil pg input ring size User Option Size of history ring of previous successfully processed commands The default value is 32 proof general debug User Option Non nil to run Proof General in debug mode This changes some behaviour e g markup stripping and displays debugging messages in the response buffer To avoid erasing messages shortly after they re printed set proof tidy response to nil This is only useful for PG developers The default value is nil proof follow mode User Option Choice of how point moves with script processing commands
58. hen a proof assistant has a flexible proof script language in which one can define new tactics or even operations and you want Proof General to recognize some of these which the default settings don t mention So please feel free to try adjusting the configuration settings and report to us if you find better default values than the ones we have provided The configuration settings appear in the customization group prover config or via the menu Proof General gt Internals gt Prover Config One basic example of a setting you may like to tweak is proof assistant home page Variable Web address for information on proof assistant Used for Proof General s help menu Most of the others are more complicated For more details of the settings see Adapting Proof General for full details To browse the settings you can look through the customization groups prover config proof script and proof shell The group proof script contains the con figuration variables for scripting and the group proof shel11 contains those for interacting with the proof assistant Unfortunately although you can use the customization mechanism to set and save these vari ables saving them may have no practical effect because the default settings are mostly hard wired into the proof assistant code Ones we expect may need changing appear as proof as sistant specific configurations For example proof assistant home page is set in the LEGO code from the value of the
59. ibe function C h v describe variable 1 6 Organization of this manual This manual covers the user level view and customization of Proof General The accompanying Adapting Proof General manual considers adapting Proof General to new proof assistants and documents some of the internals of Proof General Three appendices of this manual contain some details about obtaining and installing Proof General and some known bugs The contents of these final chapters is also covered in the files INSTALL and BUGS contained in the distribution Refer to those files for the latest information The manual concludes with some references and indexes See the table of contents for full details Chapter 2 Basic Script Management 7 2 Basic Script Management This chapter is an introduction to using the script management facilities of Proof General We begin with a quick walkthrough example then describe the concepts and functions in more detail 2 1 Walkthrough example in Isabelle Here s a short example in Isabelle to see how script management is used The file you are asked to type below is included in the distribution as isar Example thy If you re not using Isabelle substitute some lines from a simple proof for your proof assistant or consult the example file supplied with Proof General for your prover called something like foo example foo for a proof assistant Foo This walkthrough is keyboard based but you could easily
60. ine key proof mode map control b proof undo last successful command This lisp fragment adds bindings for every buffer in proof script mode the Emacs keymap is called proof mode map To just affect one prover use a keymap name like isar mode map and evaluate after the library isar has been loaded To find the names of the functions you may want to bind look in this manual or query current bindings interactively with C h k This command describe key works for menu operations as well also use it to discover the current key bindings which you re losing by declarations such as those above By default C n is next line and C b is backward char command neither are really needed if you have working cursor keys If you re using XEmacs and your keyboard has a super modifier on my PC keyboard it has a Windows symbol and is next to the control key you can freely bind keys on that modifier globally since none are used by default Use lisp like this global set key super 1 x symbol INSERT lambda global set key super n x symbol INSERT notsign global set key super a x symbol INSERT logicaland global set key super o x symbol INSERT logicalor global set key super f x symbol INSERT universal1 global set key super t x symbol INSERT existential1 global set key super A x symbol INSERT biglogicaland global set key super e x symbol INSERT equivalence global set key super
61. inting command took the proof in a direction you don t like Notice that the deleted command is put into the Emacs kill ring so you can use the usual yank and similar commands to retrieve the deleted text proof goto point Command Assert or retract to the command at current position Calls proof assert until point or proof retract until point as appropriate proof process buffer Command Process the current or script buffer and maybe move point to the end proof retract buffer Command Retract the current buffer and maybe move point to the start proof electric terminator toggle arg Command Toggle proof electric terminator enable With arg turn on iff ARG gt O This function simply uses customize set variable to set the variable It was constructed with proof deftoggle fn proof assert until point interactive Command Process the region from the end of the locked region until point Default action if inside a comment is just process as far as the start of the comment proof retract until point interactive amp optional delete region Command Tell the proof process to retract until point If invoked outside a locked region undo the last successfully processed command If called with a prefix argument delete region non nil also delete the retracted region from the proof script As experienced Emacs users will know a prefix argument is a numeric argument supplied by some key sequence typed before a command
62. into four categories e state changing commands which need Back to be backtracked e state changing tactics which need Undo to be backtracked e state preserving commands which do not need to be backtracked e state preserving tactics which do not need to be backtracked We give an example of existing commands that fit each category e coq user state preserving commands example Print e coq user state changing commands example Require e coq user state changing tactics example Intro e coq user state preserving tactics example Idtac This variables are regexp string lists See their documentations in emacs C h v coq user for details on how to set them in your emacs file Here is a simple example setq coq user state changing commands MyHint MyRequire setq coq user state preserving commands gt Show s Mydata The regexp character sequence s means one or more whitespaces See the Emacs doc umentation of regexp quote for the syntax and semantics WARNING you need to restart Emacs to make the changes to these variables effective In case of losing synchronization the user can use C c C z to move the locked region to the proper position proof frob locked end see Section 4 7 Escaping script management page 23 or C c C v to re issue an erroneously back tracked tactic without recording it in the script 9 5 Holes feature Holes are an experimental feature for complex expressio
63. ion there are several other operations on tags One common one is replacing identifiers across all files using tags query replace For more information on how to use tags See Info file xemacs node Tags To use tags for completion at the same time as the completion mechanism mentioned already you can use the command M x add completions from tags table add completions from tags table Command Add completions from the current tags table 32 Proof General Chapter 6 Customizing Proof General 33 6 Customizing Proof General There are two ways of customizing Proof General it can be customized for a user s preferences using a particular proof assistant or it can be customized by a developer to add support for a new proof assistant The latter kind of customization we call instantiation or adapting See the Adapting Proof General manual for how to do this Here we cover the user level customization for Proof General There are two kinds of user level settings in Proof General e Settings that apply globally to all proof assistants e those that can be adjusted for each proof assistant individually The first sort have names beginning with proof The second sort have names which begin with a symbol corresponding to the proof assistant for example isa coq etc The symbol is the root of the mode name See Section 1 2 Quick start guide page 3 for a table of the supported modes To stand for an arbitrary proof assist
64. it and insert the line load proof general home generic proof site el into your emacs file where proof general home is the top level directory that was created when Proof General was unpacked For much more information See Appendix A Obtaining and Installing page 57 1 2 Quick start guide Once Proof General is correctly installed the corresponding Proof General mode will be invoked automatically when you visit a proof script file for your proof assistant for example Prover Extensions Mode LEGO E lego mode Coq ww coq mode Isabelle thy isar mode Phox phx phox mode HOL98 sml ho198 mode ACL2 acl acl2 mode Twelf elf twelf mode Plastic dd plastic mode Lambda CLAM lcm lclam mode CCC CCC ccc mode PG Shell pgsh pgshell mode the exact list of Proof Assistants supported may vary according to the version of Proof General and its local configuration You can also invoke the mode command directly e g type M x lego mode to turn a buffer into a lego script buffer A proof assistant is a computerized helper for developing mathematical proofs For short we sometimes call it a prover although we always have in mind an interactive system rather than a fully automated theorem prover 2A proof script is a sequence of commands which constructs a proof usually stored in a file 4 Proof General You ll find commands to process the proof script are available from the toolbar menu
65. kages Proof General makes some configuration for other Emacs packages which provide various useful facilities that can make your editing more effective Sometimes this configuration is purely at the proof assistant specific level and so not necessarily available and sometimes it is made using Proof General settings When adding support for a new proof assistant we suggest that these other packages are sup ported as a convention The packages currently supported are font lock x symbol func menu outline mode completion and etags 5 1 Syntax highlighting Proof script buffers are decorated or fontified with colours bold and italic fonts etc according to the syntax of the proof language and the settings for font lock keywords made by the proof assistant specific portion of Proof General Moreover Proof General usually decorates the output from the proof assistant also using font lock In XEmacs fontification is automatically turned on To automatically switch on fontification in GNU Emacs 20 4 you may need to engage M x global font lock mode The old mecha nism of adding hooks to the mode hooks lego mode hooks coq mode hooks etc is no longer recommended it should not be needed in latest Emacs versions which have more flexible cus tomization Fontification for output is controlled by a separate switch in Proof General Set proof output fontify enable to nil if you don t want the output from your proof assistant to be f
66. key sequence You can supply a specific number by typing with the digits or a universal prefix of C u See See Info file xemacs node Arguments for more details Several Proof General commands like proof retract until point interactive may accept a prefix argument to adjust their behaviour somehow 2 7 Proof assistant commands There are several commands for interacting with the proof assistant and Proof General which do not involve the proof script Here are the key bindings and functions G c CHL proof display some buffers C c C p proof prf C c C t proof ctxt C c C h proof help G C f proof find theorems C c C w pg response clear displays G c C c proof interrupt process C c C v proof minibuffer cmd C c C s proof shell start C c C x proof shell exit Chapter 2 Basic Script Management 15 proof display some buffers Command Display the reponse trace goals or shell buffer rotating A fixed number of repetitions of this command switches back to the same buffer Also move point to the end of the response buffer if it s selected If in three window or multiple frame mode display two buffers The idea of this function is to change the window gt buffer mapping without adjusting window layout proof prf Command Show the current proof state Issues a command to the assistant based on proof showproof command proof ctxt Command Show the current context Issues a command to the assistant based on proof c
67. ll replay simply as a single step proof and you will need to convert from the interactive to batch form as usual if you wish to obtain batch proofs Also note that Proof General does not contain an SML parser so there can be problems if you write complex ML in proof scripts HOL Proof General may work with variants of HOL other than HOL98 but is untested Proba bly a few of the settings would need to be changed in a simple way to cope with small differences in output between the systems Please let us know if you modify the HOL98 version for another variant of HOL Perhaps somebody from the HOL community is willing to adopt HOL Proof General and support and improve it Please volunteer 54 Proof General Chapter 12 Shell Proof General 55 12 Shell Proof General This instance of Proof General is not really for proof assistants at all but simply provided as a handy way to use a degenerate form of script management with other tools Suppose you have a software tool of some kind with a command line interface and you want to demonstrate several example uses of it perhaps at a conference But the command lines for your tool may be quite complicated so you do not want to type them in live Instead you just want to cut and paste from a pre recorded list But watching somebody cut and paste commands into a window is almost as tedious as watching them type those commands Shell Proof General comes to the rescue Simply record your comman
68. lling Proof General site wide you can put the components in the standard di rectories of the filesystem if you prefer providing the variables in proof site el are adjusted accordingly see Proof General site configuration in Adapting Proof General for more details Make sure that the generic and assistant specific elisp files are kept in subdirectories coq isa lego of proof home directory so that the autoload directory calculations are cor rect To prevent every user needing to edit their own emacs files you can put the load file command to load proof site el into site start el or similar Consult the Emacs docu mentation for more details if you don t know where to find this file Removing support for unwanted provers You cannot run more than one instance of Proof General at a time so if you re using Coq visiting an ML file will not load Isabelle Proof General and the buffer remains in fundamental mode If there are some assistants supported that you never want to use you can adjust the variable proof assistants in proof site el to remove the extra autoloads This is advisable in case the extensions clash with other Emacs modes for example Verilog mode for v files clashes with Coq mode See Proof General site configuration in Adapting Proof General for more details of how to adjust the proof assistants setting Instead of altering proof assistants a simple way t
69. lly Ideally the completion table would be set from the running process according to the identifiers available are within the particular context of a script file But until this is available this table may be set to contain a number of standard identifiers available for your proof assistant The setting PA completion table holds the list of identifiers for a proof assistant The function proof add completions adds these into the completion database PA completion table Variable List of identifiers to use for completion for this proof assistant Completion is activated with c ret If this table is empty or needs adjusting please make changes using customize variable and post suggestions at http proofgeneral inf ed ac uk trac The completion facility uses a library completion el which usually ships with XEmacs and GNU Emacs and supplies the complete function complete Command Fill out a completion of the word before point Point is left at end Consecutive calls rotate through all possibilities Prefix args C u leave point at the beginning of the completion not the end a number rotate through the possible completions by that amount 0 same as 1 insert previous completion See the comments at the top of completion el for more info Chapter 5 Support for other Packages 31 5 7 Support for tags An Emacs tags table is a description of how a multi file system is broken up into files It lists the names of the
70. m the assistant is only fully monitored when Proof General is in control of the shell When in control Proof General watches the output from the proof assistant to guess when a file is loaded or when a proof step is taken or undone What happens when you type in the shell buffer directly depends on how complete the communication is between Proof General and the prover which depends on the particular instantiation of Proof General If synchronization is lost you have two options to resynchronize If you are lucky it might suffice to use the key 24 Proof General C c C z proof frob locked end This command is disabled by default to protect novices using it accidently If proof frob locked end does not work you will need to restart script management altogether see Section 2 7 Proof assistant commands page 14 proof frob locked end Command Move the end of the locked region backwards to regain synchronization Only for use by consenting adults This command can be used to repair synchronization in case something goes wrong and you want to tell Proof General that the proof assistant has processed less of your script than Proof General thinks You should only use it to move the locked region to the end of a proof command 4 8 Editing features To make editing proof scripts more productive Proof General provides some additional editing commands One facility is the input ring of previously processed commands This allows a conve
71. med local contexts cases C C a h f Shows all local facts C c C a hd Shows inner syntax of the current theory context for types and terms 50 Proof General C c C ahm Shows proof methods available in current theory context C c C aho Shows all available commands of Isabelle s outer syntax C c C aht Shows theorems stored in the current theory node C c C a C s Invoke sledgehammer on first subgoal C c C a C m Find theorems containing given arguments prompt in minibuffer Invokes the thms containing command Arguments are separated by white space as usual in Isar C c C a C f Find theorems containing argument in form C c C f Find theorems either of the above The following shortcuts insert control sequences into the text modifying the appearance of individual symbols single letters mathematical entities etc the X Symbol package will provide immediate visual feedback C c C a b Inserts lt bold gt C c C a C b Inserts lt loc gt C c C a C u Inserts lt sup gt superscript character C C a C 1 Inserts lt sub gt subscript character C c C au Inserts lt bsup gt lt esup gt superscript string C c C al Inserts lt bsub gt lt esub gt subscript string C c C a C i Inserts lt isub gt identifier subscript letter C c C a C r Inserts lt raw gt raw LaTeX text C c C a C a Inserts text anti quotation C c C a C x Inserts ML inlin
72. mmas are proved or their proofs aborted they are popped off a stack Coq Proof General supports this feature of Coq Top level commands entered while in a proof are well backtracked If new lemmas are started Coq Proof General lets the user work on the proof of the new lemma and when the lemma is finished it falls back to the previous one This is supported to any nesting depth that Coq allows Warning Using Coq commands for navigating inside the different proofs Resume and especially Suspend are not supported backtracking will break syncronization Special note The old feature that moved nested proofs outside the current proof is disabled 48 Proof General 9 4 User loaded tactics Another feature that Coq allows is the extension of the grammar of the proof assistant by new tactic commands This feature interacts with the proof script management of Proof General because Proof General needs to know when a tactic is called that alters the proof state When the user tries to retract across an extended tactic in a script the algorithm for calculating how far to undo has a default behavior that is not always accurate in proof mode do Undo Coq Proof General does not currently support dynamic tactic extension in Coq this is desirable but requires assistance from the Coq core Instead we provide a way to add tactic and command names in the emacs file Four Configurable variables allows to register personal new tactics and commands
73. mmulative set of improvements to Proof General 3 5 There are compatibility fixes for newer Emacs versions and particularly for GNU Emacs credit is due to Stefan Monnier for an intense period of debugging and patching The options menu has been simplified and extended and the display management is improved and repaired for Emacs API changes There are some other usability improvements some after feedback from use at TYPES Summer Schools Many new features have been added to enhance Coq mode thanks to Pierre Courtieu and several improvements made for Isabelle thanks to Makarius Wenzel Stefan Berghofer and Tjark Weber Support has been added for the useful Emacs packages Speedbar and Index Menu both usually distributed with Emacs Compatible versions of the Emacs packages X Symbol for mathemat ical symbols in place of ASCII sequences Math Menu for Unicode symbols and MMM Mode for multiple modes in one buffer are bundled with Proof General A new Unicode Tokens package has been added which will replace X Symbol eventually Proof General 3 7 is available in RPM package format which includes pre compiled code for GNU Emacs or XEmacs and desktop integration on freedesktop org compliant desktops including for example many recent Linux distributions See the CHANGES file in the distribution for more complete details of changes since version 3 5 and the appendix History of Proof General page 63 for old news Future The aim o
74. n editing It is inspired from other tools like Pcoq http www sop inria fr lemme pcoq index htm1 The principle is simple holes are pieces of text that can be filled by different means The new coq command insertion menu system makes use of the holes system Almost all holes operations are available in the Coq holes menu Note Holes make use of the Emacs abbreviation mechanism it will work without problem if you don t have an abbrev table defined for Coq in your config files C h v abbrev file name to see the name of the abbreviation file If you already have such a table it won t be automatically overwritten so that you keep your own abbreviations But you must read the abbrev file given in PG Coq sources to be able to use the command insertion menus You can do the following to merge your abbreviations with ProofGeneral s abbreviations M x read abbrev file then select the file named coq abbrev el in the ProofGeneral coq directory At Emacs exit you will be asked if you want to save abbrevs answer yes Chapter 10 Isabelle Proof General 49 10 Isabelle Proof General Isabelle Proof General supports major generic features of Proof General including integration with Isabelle s theory loader for proper automatic multiple file handling Support for tags and proof by pointing is missing In this version support for the old style classic Isabelle theory files has been removed in Isabelle2007 only Isar style theory files are sup
75. nient way of repeating an earlier command or a small edit of it The feature is reminiscent of history mechanisms provided in shell terminals and the implementation is borrowed from the Emacs Comint package The input ring only contains commands which have been successfully pro cessed coloured blue Duplicated commands are only entered once The size of the ring is set by the variable pg input ring size M p pg previous matching input from input M n pg next matching input from input pg previous input arg Command Cycle backwards through input history saving input pg next input arg Command Cycle forwards through input history pg previous matching input regexp n Command Search backwards through input history for match for regexp Previous history elements are earlier commands With prefix argument n search for Nth previous match If n is negative find the next or Nth next match pg next matching input regexp n Command Search forwards through input history for match for regexp Later history elements are more recent commands With prefix argument n search for Nth following match If n is negative find the previous or Nth previous match pg previous matching input from input n Command Search backwards through input history for match for current input Previous history elements are earlier commands With prefix argument n search for Nth previous match If n is negative search forwards for the Nth following match
76. ntors of your favourite proof assistant to support Proof General as much as possible 1 5 Prerequisites for this manual This manual assumes that you understand a little about using Emacs for example switching between buffers using C x b and understanding that a key sequence like C x b means control with x followed by b A key sequence like M z means meta with z Meta may be labelled on your keyboard The manual also assumes you have a basic understanding of your proof assistant and the language and files it uses for proof scripts But even without this Proof General is not useless you can 6 Proof General use the interface to replay proof scripts for any proof assistant without knowing how to start it up or issue commands etc This is the beauty of a common interface mechanism To get more from Proof General and adapt it to your liking it helps to know a little bit about how Emacs lisp packages can be customized via the Customization mechanism It s really easy to use For details see Section 6 2 How to customize page 33 See Info file xemacs node Easy customization for documentation in XEmacs To get the absolute most from Proof General to improve it or to adapt it for new provers you ll need to know a little bit of Emacs lisp Emacs is self documenting so you can begin from C h and find out everything Here are some useful commands C h i info C h m describe mode C h b describe bindings C h f descr
77. ntributed some sections The Proof General project has benefited from indirect funding by EPSRC Applications of a Type Theory Based Proof Assistant in the late 1990s and The Integration and Interaction of Multiple Mathematical Reasoning Processes EP E005713 1 RA0084 in 2006 8 the EC the Co ordination Action Types and previous related projects and the support of the LFCS Version 3 1 was prepared whilst David Aspinall was visiting ETL Japan supported by the British Council For Proof General 3 7 Graham Dutton assisted with the project management system and web pages For testing and feedback for older versions of Proof General thanks go to Rod Burstall Martin Hofmann and James McKinna and some of those who continued to help with the latest 3 x series named next During the development of Proof General 3 x releases many people helped provide testing and other feedback including the Proof General maintainers Paul Callaghan Pierre Courtieu and Markus Wenzel Stefan Berghofer Gerwin Klein and other folk who tested pre releases or sent bug reports and patches including Cuihtlauac Alvarado Lennart Beringer Pascal Brisset James Brotherston Martin Buechi Lucas Dixon Matt Fairtlough Ivan Filippenko Kim Hyung Ho Mark A Hillebrand Greg O Keefe Pierre Lescanne John Longley Stefan Monnier Tobias Nipkow Leonor Prensa Nieto David von Oheimb Lawrence Paulson Paul Roziere Randy Pol lack Robert R Schneck Norbert Schi
78. o disable support for some prover is to delete the relevant directories from the PG installation For example to remove support for Coq delete the coq directory in the Proof General home directory Appendix B Bugs and Enhancements 59 Appendix B Bugs and Enhancements For an up to date description of bugs and other issues please consult the bugs file included in the distribution BUGS If you discover a problem which isn t mentioned in BUGS please use the search facility on our Trac tracking system at http proofgeneral inf ed ac uk trac If you cannot find the problem mentioned please add a ticket giving a careful description of how to repeat your problem and saying exactly which versions of all Emacs and theorem prover you are using If you have some suggested enhancements to request or contribute please also use the tracking system at http proofgeneral inf ed ac uk trac for this 60 Proof General References 61 References A short overview of the Proof General system is described in the note e Asp00 David Aspinall Proof General A Generic Tool for Proof Development Tools and Algorithms for the Construction and Analysis of Systems Proc TACAS 2000 LNCS 1785 Script management as used in Proof General is described in the paper e BT98 Yves Bertot and Laurent Th ry A generic approach to building user interfaces for theorem provers Journal of Symbolic Computation 25 7 pp 161 194 February 1998
79. of assistant Proof General provides you with several escape mechanisms if you want to do this 4 1 Visibility of completed proofs Large developments may consist of large files with many proofs To help see what has been proved without the detail of the proof itself Proof General can hide portions of the proof script Two different kinds of thing can be hidden comments and what Proof General designates as the body of proofs You can toggle the visibility of a proof script portion by using the context sensitive menu triggered by clicking the right mouse button on a completed proof or the key C c v which runs pg toggle visibility You can also select the disappearing proofs mode from the menu Proof General gt Options gt Disappearing Proofs This automatically hides each the body of each proof portion as it is completed by the proof assistant Two further menu commands in the main Proof General menu Show all and Hide all apply to all the completed portions in the buffer Notice that by design this feature only applies to completed proofs after they have been processed by the proof assistant When files are first visited in Proof General no information is stored about proof boundaries The relevant elisp functions and settings are mentioned below pg toggle visibility Command Toggle visibility of region under point pg show all proofs Command Display all completed proofs in the buffer pg hide all proofs Command
80. of scripts including syntax hilight ing and a menu to jump to particular goals definitions or declarations Special editing functions send lines of proof script to the proof assistant or undo previous proof steps For more details see Section 2 5 Script editing commands page 12 and Section 2 6 Script processing commands page 13 Chapter 1 Introducing Proof General 5 e Toolbar and menus A script buffer has a toolbar with navigation buttons for processing parts of the proof script A menu provides further functions for operations in the proof assistant as well as customization of Proof General For more details see Section 2 8 Toolbar commands page 16 Section 2 7 Proof assistant commands page 14 and Chapter 6 Customizing Proof General page 33 e Proof by pointing Proof General has support for proof by pointing and similar features Proof by pointing allows you to click on a subterm of a goal to be proved and automatically apply an appro priate proof rule or tactic Proof by pointing is specific to the proof assistant and logic in use therefore it is configured mainly on the proof assistant side If you would like to see proof by pointing support for Proof General in a particular proof assistant petition the developers of the proof assistant to provide it 1 4 Supported proof assistants Proof General comes ready customized for several proof assistants including these e LEGO Proof General for LEGO Version 1 3
81. ommands vicio odas ida dea dead 49 10 2 Logics and SIMS cs e te e aa ta ae eked da dona a 51 10 3 Isabelle customizations 0oooooccocccc hh hh hh 51 ll HOL Proof General 2 usuu usar no Dnm tea RC RD Gd e oen 53 12 Shell Proof General vc ecu RUE RR tno C dex 55 Appendix A Obtaining and Installing 57 A 1 Obtaining Proof General ooccccooccccooccr ehh hh 57 A 2 Installing Proof General from tarball 000 0 cece cece eens 57 A 3 Installing Proof General from RPM package 0 000 cece eee eee 57 A 4 Setting the names of binaries 000 c cece cece hh 58 Ab Notes LOM SYSSICS p id aa Bes 58 Byte COMPA Mint eee tte bsc Bo te eee gal RR a quere od V e te Ge RURAL 58 Site wide installation 0 cece cece net tnt etn hee 58 Removing support for unwanted PIOVEOTS oooooooroorr ehh 58 Appendix B Bugs and Enhancements 59 Re erences socorrista 61 History of Proof General ous 2o uhr AAA 63 Old News for 3 0 sasra aoe fa aa tn EAER de helene ne oo ea rogo tenes 64 Old News TOT ul dc ec ask teeter durare m oreo Ced Soke DRE Rp gne uad ug ae dein AG 64 Old News for 3 2 enseri dag eR eR Ig dd babet SG e ia 65 Old News LOT 3d taa ida asd eee es mtr urbc asi dr Neu lata 66 Old News tor 3 E Seca clea tence ee ad ebrei Sate odd ud peu ed eat tx 66 Function and Command Index ees 67 Variable and User Option Index Lees
82. ontext command proof help Command Show a help or information message from the proof assistant Typically a list of syntax of commands available Issues a command to the assistant based on proof info command proof find theorems arg Command Search for items containing given constants Issues a command based on arg to the assistant using proof find theorems command The user is prompted for an argument pg response clear displays Command Clear Proof General response and tracing buffers You can use this command to clear the output from these buffers when it becomes overly long Particularly useful when proof tidy response is set to nil so responses are not cleared automatically proof interrupt process Command Interrupt the proof assistant Warning This may confuse Proof General This sends an interrupt signal to the proof assistant if Proof General thinks it is busy This command is risky because when an interrupt is trapped in the proof assistant we don t know whether the last command succeeded or not The assumption is that it didn t which should be true most of the time and all of the time if the proof assistant has a careful handling of interrupt signals proof minibuffer cmd cmd Command Send cmd to proof assistant Interactively read from minibuffer The command isn t added to the locked region If a prefix arg is given and there is a selected region that is pasted into the command This is handy for co
83. ontified according to the setting of font lock keywords in the proof assistant specific portion of Proof General See Section 6 4 User options page 35 By the way the choice of colour font etc for each kind of markup is fully customizable in Proof General Each face Emacs terminology is controlled by its own customization setting You can display a list of all of them using the customize menu Proof General gt Advanced gt Customize gt Faces gt Proof Faces 5 2 X Symbol support The X Symbol package displays characters from a variety of fonts in Emacs buffers automatically converting between codes for special characters and tokens which are character sequences stored in files Proof General uses X Symbol to allow interaction between the user and the proof assistant to use tokens yet appear to be using special characters So proof scripts and proofs can be processed with real mathematical symbols Greek letters etc The X Symbol package is now bundled with Proof General You will be able to enable X Symbol support if support has been provided in Proof General for a token language for your proof assistant To enable X Symbol use the menu item Proof General gt Options gt X Symbol To enable it automatically every time you use Proof General just use Proof General gt Options gt Save Options once it has been selected Alternatively customize the setting PA x symbol enable You may also simply use M x x sym
84. oq Proof General is an instantiation of Proof General for the Coq proof assistant It supports most of the generic features of Proof General but does not have integrated file management or proof by pointing yet 9 1 Coq specific commands Coq Proof General supplies the following key bindings C c C a C i Inserts Intros C c C a C a Inserts Apply C c C a C s Inserts Section C c C a C e Inserts End lt section name gt this should work well with nested sections C c C a C o Prompts for a SearchIsos argument 9 2 Coq specific variables The variable coq version is Vx where x is 8 0 or 8 1 is used to force version of Coq if it is t then Coq is considered in version x ProofGeneral sets it automatically by doing the following shell command concat coq prog name v So you should not have to set this variable unless you have problems with different versions of Coq you can set to t the variable corresponding to the version you are using in your config file before ProofGeneral is loaded and ProofGeneral won t override it 9 3 Editing multiple proofs Coq allows the user to enter top level commands while editing a proof script For example if the user realizes that the current proof will fail without an additional axiom he or she can add that axiom to the system while in the middle of the proof Similarly the user can nest lemmas beginning a new lemma while in the middle of an earlier one and as the le
85. outline minor mode can be used on proof script files The headings taken for outlining are the goal statements at the start of goal save sequences see Section 2 3 2 Goal save sequences page 10 If you want to use outline to hide parts of the proof script in the locked region you need to disable proof strict read only Use M x outline minor mode to turn on outline minor mode Functions for navigating hiding and revealing the proof script are available in menus Please note that outline mode may not work well in processed proof script files because of read only restrictions of the protected region This is an inherent problem with outline because it works by modifying the buffer If you want to use outline with processed scripts you can turn off the Strict Read Only option See See Info file xemacs node Outline Mode for more information about outline mode 7 5 6 Support for completion You might find the completion facility of Emacs useful when you re using Proof General The key C RET is defined to invoke the complete command Pressing C RET cycles through completions displaying hints in the minibuffer Completions are filled in according to what has been recently typed from a database of symbols The database is automatically saved at the end of a session Proof General has the additional facility for setting a completion table for each supported proof assistant which gets loaded into the completion database automatica
86. pb RE EE 35 proof strict read Oonly epe IP ES 36 proof terninal char i 2 Li ep iasi iaaea 12 proof three window enable 34 proof tidy response re R Rer 37 proof toolbar enable dis prse ic beds 36 proof toolbar use button enablers 36 70 Proof General Keystroke Index Keystroke Index C Caa Sn hue lease es anos ee lia as bates o bbe ayes 28 c sag tr tice ala pales 2 ae 28 Cr b ttonl 2 065222 LER a REGE 1162 COS add rad ed 12 60 3 bra E anes gus 12 CI e P LULPPPTCUERE 50 C C CHa Canto re ho DR doxes Ro x wx E es 47 50 CTE CAD Se Bee eed bee 50 CHO Ca Ud berger Gea bec utente xp ore Sy 49 6078 E eye AEn E eed AT Qaod EB UE isis biu orem dioe BA does sus 49 GHG Cade L4 d IPIS 45 4T 50 CO Oti 45 G e Ca Coll iaa ci Ba fu sl ide 50 A II ee ie do dea 49 C 640 8 070 erlere han beh eats p eiie 47 A E 49 C c C a Gg nice fae s REP IR kaoks LP ERU Sebo 49 Cod Sa Eas dbi Bacardi ee bs alan naan debis teo 50 CAE a C R d Raider eR rcx dean 45 C c 0 8 Baud erre e Ad e POE PR 47 49 Cc Ua uad imas due Sadak i aped HE edet OE 50 CsciCra haria daa 49 Cc Ca iia a diia ia 49 COCA li Dic 49 COCA ira ads aid UEFA REOR 49 CRIA AG a a banded anes 49 C Ca AA 49 71 Cre Cra hri gies burs pra adde tum esp US adr e E 49 Casa a E E ET cided 49 e Dh Tene E E EE P OR Do dg 49 CARO Oi e a 49 G Ca Saee ba APR ih TURN naked 49 COC bs edid d eere etes qd Bae die 49 CECI B T ua sop nb RE
87. pg next matching input from input n Command Search forwards through input history for match for current input Following history elements are more recent commands With prefix argument n search for Nth following match If n is negative search backwards for the Nth previous match Chapter 4 Advanced Script Management and Editing 25 4 9 Experimental features During the development of Proof General we experiment with new features in the interface The particular features available the version of Proof General you have are described in the file README exper which is included in the distribution The experimental features are automatically enabled in development releases of Proof General but disabled in the stable releases To adjust the setting customize the variable below After changing the setting you should restart Proof General to see or remove the new features proof experimental features User Option Whether to enable certain features regarded as experimental Proof General includes a few features designated as experimental Enabling these will usually have no detrimental effects on using PG but the features themselves may be buggy We encourage users to set this flag and test the features but being aware that the features may be buggy problem reports and suggestions for improvements are welcomed The default value is nil 26 Proof General Chapter 5 Support for other Packages 27 5 Support for other Pac
88. ported Isabelle provides its own way to invoke Proof General via the Isabelle script Running Isabelle starts an Emacs session with Isabelle Proof General The defaults may be changed by editing the Isabelle settings see the Isabelle documentation for details Proof General for Isabelle manages Isar thy files The syntax of Isabelle input is technically simple enabling Proof General to provide reliable control over incremental execution of the text Thus it is very hard to let Proof General lose synchronization with the Isabelle process 10 1 Isabelle commands The Isabelle instance of Proof General supplies several specific help key bindings these functions are offered within the prover help menu as well C c C ar Invokes Isar command refute on the current subgoal Only available in HOL and derived logics C c C a C q Invokes Isar command quickcheck on the current subgoal C c C a C d Displays a draft document of the current theory C c C a C p Prints a draft document of the current theory C c C a h A Shows available antiquotation commands and options C c C a h C Shows the current Classical Reasoner context C c Ca h I Shows the current set of induct cases rules C c C ahS Shows the current Simplifier context C c C ahT Shows the current set of transitivity rules for calculational reasoning C c C aha Shows attributes available in current theory context C c C ahb Shows all local term bindings C c C ahc Shows all na
89. presses C x a g add global abbrev or C x a i g inverse add global abbrev To enable automatic expansion of abbreviations which can be annoying the Abbrev minor mode type M x abbrev mode RET When you are not in Abbrev mode you can expand an abbreviation by pressing C x expand abbrev See the Emacs manual for more details Chapter 7 Hints and Tips 43 Coq Proof General has a special experimental feature called Holes which makes use of the abbreviation mechanism and includes a large list of command abbreviations See Section 9 5 Holes feature page 48 for details With other provers you may use the standard Emacs commands above to set up your own abbreviation tables 44 Proof General Chapter 8 LEGO Proof General 45 8 LEGO Proof General LEGO proof script mode is a mode derived from proof script mode for editing LEGO scripts An important convention is that proof script buffers must start with a module declaration If the proof script buffer s file name is fermat 1 then it must commence with a declaration of the form Module fermat If in the development of the module fermat you require material from other module e g lib_nat and galois you need to specify this dependency as part of the module declaration Module fermat Import lib_nat galois No need to worry too much about efficiency When you retract back to a module declaration to add a new import item LEGO does not actually retract the pr
90. pt indent see Section 6 4 User op tions page 35 When indentation is enabled Proof General will indent lines of proof script with the usual Emacs functions particularly TAB indent for tab command Unfortunately inden tation in Proof General 3 7 is somewhat slow Therefore with large proof scripts we recommend proof script indent is turned off Here are the commands for moving around in a proof script with their default key bindings C c C a proof goto command start C c C e proof goto command end G C proof goto end of locked proof goto command start Command Move point to start of current or final command of the script proof goto command end Command Set point to end of command at point The variable proof terminal char is a prover specific character to terminate proof commands LEGO and Isabelle use a semicolon Coq employs a full stop proof goto end of locked amp optional switch Command Jump to the end of the locked region maybe switching to script buffer If called interactively or switch is non nil switch to script buffer If called interactively a mark is set at the current location with push mark During the course of a large proof it may be useful to copy previous commands As you move the mouse over previous portions of the script you ll notice that each proof command is highlighted individually Once a goal save sequence is closed the whole sequence is highlighted There
91. pying terms etc from the script If proof strict state preserving is set and proof state preserving p is config ured then the latter is used as a check that the command will be safe to execute in other words that it won t ruin synchronization If when applied to the command it returns false then an error message is given warning this command risks spoiling synchronization if the test proof state preserving p is not configured if it is only an approximate test or if proof strict state preserving is off nil 16 Proof General As if the last two commands weren t risky enough there s also a command which explicitly adjusts the end of the locked region to be used in extreme circumstances only See Section 4 7 Escaping script management page 23 There are a few commands for starting stopping and restarting the proof assistant process The first two have key bindings but restart does not As with any Emacs command you can invoke these with M x followed by the command name proof shell start Command Initialise a shell like buffer for a proof assistant Also generates goal and response buffers Does nothing if proof assistant is already running proof shell exit Command Query the user and exit the proof process This simply kills the proof shell buffer relying on the hook function proof shell kill function to do the hard work proof shell restart Command Clear script buffers and
92. ral and notes on its internals are in the Adapting Proof General manual You should find a copy of that second manual close to wherever you found this one consult the Proof General home page if in doubt The internal code of Proof General has been significantly overhauled for this version which should make it more robust and readable The generic code has an improved file structure and there is support for automatic generation of autoload functions There is also a new mechanism for defining prover specific customization and instantiation settings which fits better with the customize library These settings are named in the form PA setting name in the documenta tion you replace PA by the symbol for the proof assistant you are interested in See Chapter 6 Customizing Proof General page 33 for details Finally important bug fixes include the robustification against write file C x C w revert buffer and friends These are rather devious functions to use during script management but Proof General now tries to do the right thing if you re deviant enough to try them out Work on this release was undertaken by David Aspinall between May September 2000 and includes contributions from Markus Wenzel Pierre Courtieu and Christophe Raffalli Markus added some Isar documentation to this manual 66 Proof General Old News for 3 3 Proof General 3 3 includes a few feature additions but mainly the focus has been on compatibil ity improvem
93. res and some bug fixes One noticeable new feature is the addition of a prover specific menu for each of the supported provers This menu has a favourites feature that you can use to easily define new functions Please contribute other useful functions or suggestions for things you would like to appear on these menus Because of the new menus and to make room for more commands we have made a new key map for prover specific functions These now all begin with C c C a This has changed a few key bindings slightly Another new feature is the addition of prover specific completion tables to encourage the use of Emacs s completion facility using C RET See Section 5 6 Support for completion page 30 for full details A less obvious new feature is support for turning the proof assistant output on and off internally to improve efficiency when processing large scripts This means that more of your CPU cycles can be spent on proving theorems Adapting for new proof assistants continues to be made more flexible and easier in several places This has been motivated by adding experimental support for some new systems One new system which had good support added in a very short space of time is PhoX see the PhoX home page for more information PhoX joins the rank of officially supported Proof General instances thanks to its developer Christophe Raffalli Breaking the manual into two pieces was overdue now all details on adapting Proof Gene
94. ript Management and Editing 23 4 4 Retracting across files Make sure that the current script buffer has either been completely asserted or retracted Proof General enforces this Then you can retract proof scripts in a different file Simply visit a file that has been processed earlier and retract in it using the retraction commands from see Section 2 6 Script processing commands page 13 Apart from removing parts of the locked region in this buffer all files which depend on it will be retracted and thus unlocked automatically Proof General reminds you that now is a good time to save any unmodified buffers 4 5 Asserting across files Make sure that the current script buffer has either been completely asserted or retracted Then you can assert proof scripts in a different file Simply visit a file that contains no locked region and assert some command with the usual assertion commands see Section 2 6 Script processing commands page 13 Proof General reminds you that now is a good time to save any unmodified buffers This is particularly useful as assertion may cause the proof assistant to automatically process other files 4 6 Automatic multiple file handling To make it easier to adapt Proof General for a proof assistant there is another possibility for multiple file support that it is provided automatically by Proof General and not integrated with the file management system of the proof assistant In this case Proof General
95. rmer Sebastian Skalberg Mike Squire Norbert Voelker Tjark Weber Mitsuharu Yamamoto Thanks to all of you and apologies to anyone missed Chapter 1 Introducing Proof General 3 1 Introducing Proof General Proof General is a generic Emacs interface for interactive proof assistants developed at the LFCS in the University of Edinburgh It works best under XEmacs but can also be used with GNU Emacs You do not have to be an Emacs militant to use Proof General The interface is designed to be very easy to use You develop your proof script in place rather than line by line and later reassembling the pieces Proof General keeps track of which proof steps have been processed by the prover and prevents you editing them accidently You can undo steps as usual The aim of Proof General is to provide a powerful and configurable interface for numerous interactive proof assistants We target Proof General mainly at intermediate or expert users so that the interface should be useful for large proof developments Please help us Send us comments suggestsions or the best patches to improve support for your chosen proof assistant Contact us at http proofgeneral inf ed ac uk trac If your chosen proof assistant isn t supported read the accompanying Adapting Proof General manual to find out how to configure PG for a new prover 1 1 Installing Proof General If Proof General has not already been installed for you you should unpack
96. roof assistant may have a notion of which files have been processed but that it will only record files that have been completely processed For more explanation of the handling of multiple files See Section 4 2 Switching between proof scripts page 21 proof toggle active scripting amp optional arg Command Toggle active scripting mode in the current buffer With arg turn on scripting iff arg is positive 2 4 Summary of Proof General buffers Proof General manages several kinds of buffers in Emacs Here is a summary of the different kinds of buffers you will use when developing proofs e The proof shell buffer is an Emacs shell buffer used to run your proof assistant Usu ally it is hidden from view but see Section 4 7 Escaping script management page 23 Communication with the proof shell takes place via two or three intermediate buffers e A script buffer as we have explained is a buffer for editing a proof script The active scripting buffer is the script buffer which is currently being used to send commands to the proof shell Some proof assistants provide some level of support for switching between multiple concurrent proofs but Proof General does not use this Generally the exact context for such proofs is hard to define to easily split them into multiple files 12 Proof General e The goals buffer displays the list of subgoals to be solved for a proof in progress During a proof it is usually displayed together with th
97. s and keyboard Type C h m to get a list of the keyboard shortcuts for the current mode The commands available should be easy to understand but the rest of this manual describes them in some detail The proof assistant itself is started automatically inside Emacs as an inferior process when you ask for some of the proof script to be processed You can start the proof assistant manually with the menu command Start proof assistant To follow an example use of Proof General on a Isabelle proof see Section 2 1 Walkthrough example in Isabelle page 7 If you know the syntax for proof scripts in another theorem prover you can easily adapt the details given there 1 3 Features of Proof General Why would you want to use Proof General Proof General is designed to be useful for novices and expert users alike It will be useful to you if you use a proof assistant and you d like an interface with the following features simplified interaction script management multiple file scripting a script editing mode proof by pointing toolbar and menus syntax highlighting real symbols functions menu tags and finally adaptability Here is an outline of some of these features Look in the contents page or index of this manual to find out about the others e Simplified interaction Proof General is designed for proof assistants which have a command line shell interpreter When using Proof General the proof assistant s shell is hidden from
98. s of the proof script are analysed based on their syntax and the behaviour of the proof assistant after each proof command 10 Proof General 2 3 Script buffers A script buffer is a buffer displaying a proof script Its Emacs mode is particular to the proof assistant you are using but it inherits from proof mode A script buffer is divided into three regions locked queue and editing The proof commands in the script buffer can include a number of Goal save sequences 2 3 1 Locked queue and editing regions The three regions that a script buffer is divided into are e The locked region which appears in blue underlined on monochrome displays and contains commands which have been sent to the proof process and verified The commands in the locked region cannot be edited e The queue region which appears in pink inverse video and contains commands waiting to be sent to the proof process Like those in the locked region these commands can t be edited e The editing region which contains the commands the user is working on and can be edited as normal Emacs text These three regions appear in the buffer in the order above that is the locked region is always at the start of the buffer and the editing region always at the end The queue region only exists if there is input waiting to be processed by the proof process Proof General has two fundamental operations which transfer commands between these regions assertion or proc
99. send proof shell restart cmd All locked regions are cleared and the active scripting buffer deactivated If the proof shell is busy an interrupt is sent with proof interrupt process and we wait until the process is ready The restart command should re synchronize Proof General with the proof assistant without actually exiting and restarting the proof assistant process It is up to the proof assistant how much context is cleared for example theories already loaded may be cached in some way so that loading them the next time round only performs a re linking operation not full re processing One way of caching is via object files used by Lego and Coq 2 8 Toolbar commands The toolbar provides a selection of functions for asserting and retracting portions of the script issuing non scripting commands and inserting goal and save type commands The latter functions are not available on keys but are available from the from the menu or via M x as well as the toolbar proof issue goal arg Command Write a goal command in the script prompting for the goal Issues a command based on arg to the assistant using proof goal command The user is prompted for an argument proof issue save arg Command Write a save qed command in the script prompting for the theorem name Issues a command based on arg to the assistant using proof save command The user is prompted for an argument 2 9 Interrupting during trace output
100. sure that the token to symbol mapping is a bijection The Unicode Tokens mode also provides an input mechanism for assisting with entering tokens and providing short cuts for symbols one of the useful features of the X Symbol package Even if your proof assistant manages native Unicode symbols directly the input method and some of the provided commands may be useful C unicode tokens rotate glyph forward C unicode tokens rotate glyph backward gt unicode tokens electric suffix unicode tokens token insert arg amp optional argname Command Insert a Unicode string by a token name with completion If a prefix is given the string will be inserted regardless of whether or not it has displayable In fact the strings are mapped to Emacs internal encoding for display Unicode is just an appropriate mechanism for input Chapter 5 Support for other Packages 29 glyphs otherwise a numeric character reference for whichever codepoints are not in the unicode tokens glyph list If argname is given it is used for the prompt If argname uniquely identifies a character that character is inserted without the prompt unicode tokens rotate glyph forward amp optional n Command Rotate the character before point in the current code page by n steps If no character is found at the new codepoint no change is made This function may only work reliably for GNU Emacs gt 23 unicode tokens rotate glyph backward amp optional n Command
101. t new feature in Proof General 3 0 is support for X Symbol which means that real logical symbols Greek letters etc can be displayed during proof development instead of their ASCII approximations This makes Proof General a more serious competitor to native graphical user interfaces Finally Proof General has become much easier to adapt to new provers it fails gracefully or not at all when particular configuration variables are unset and provides more default settings which work out of the box An example configuration for Isabelle is provided which uses just 25 or so simple settings This manual has been updated and extended for Proof General 3 0 Amongst other improve ments it has a better description of how to add support for a new prover See the CHANGES file in the distribution for more information about the latest improvements in Proof General Developers should check the ChangeLog in the developer s release for detailed comments on internal changes Most of the work for Proof General 3 0 has been done by David Aspinall Markus Wenzel helped with Isabelle support and provided invaluable feedback and testing especially for the improve ments to multiple file handling Pierre Courtieu took responsibility from Patrick Loiseleur for Coq support although improvements in both Coq and LEGO instances for this release were made by David Aspinall Markus Wenzel provided support for his Isar language a new proof language for Isabelle
102. the user Communi cation takes place via three buffers Emacs text widgets Communication takes place via three buffers The script buffer holds input the commands to construct a proof The goals buffer displays the current list of subgoals to be solved The response buffer displays other output from the proof assistant By default only two of these three buffers are displayed This means that the user normally only sees the output from the most recent interaction rather than a screen full of output from the proof assistant Proof General does not commandeer the proof assistant shell the user still has complete access to it if necessary For more details see Section 2 4 Summary of Proof General buffers page 11 and see Section 6 3 Display customization page 34 e Script management Proof General colours proof script regions blue when they have been processed by the prover and colours regions red when the prover is currently processing them The appearance of Emacs buffers always matches the proof assistant s state Coloured parts of the buffer cannot be edited Proof General has functions for asserting or retracting parts of a proof script which alters the coloured regions For more details see Chapter 2 Basic Script Management page 7 Section 2 6 Script processing commands page 13 and Chapter 4 Advanced Script Management and Editing page 21 e Script editing mode Proof General provides useful facilities for editing pro
103. tion automatically when loading this file Please notice that all the strings above should never contain spaces see documentation of variables proof prog name and proof prog args Extending the previous example if the makefile for foo v is located in directory dir you can add the right compile command And if you want a non standard coq executable to be used here is what you should put in variables x Local Variables coq prog name coqsrc bin coqtop coq prog args emacs I theories compile command make C k bar foo vo End And then the right call to make will be done if you use the M x compile command Notice that the lines are commented in order to be ignored by the proof assistant It is possible to use this mechanism for any other buffer local variable See Info file xemacs node File Variables 7 3 Using abbreviations A very useful package of Emacs supports automatic expansions of abbreviations as you type See Info file xemacs node Abbrevs For example the proof assistant Coq has many command strings that are long such as reflex ivity Inductive Definition and Discriminate Here is a part of the Coq Proof General abbreviations abs absurd ap apply as assumption The above list was taken from the file that Emacs saves between sessions The easiest way to configure abbreviations is as you write by using the key
104. ts etc Note that you won t see this sub menu until Isabelle has been started because it is generated by Isabelle itself Proof General on the other hand is responsible for recording any settings that are configured when you select Isabelle gt Settings Save Settings They are stored along with the other Emacs customization settings 10 3 Isabelle customizations Here are some of the user options specific to Isabelle You can set these as usual with the customization mechanism isabelle web page Variable URL of web page for Isabelle 52 Proof General Chapter 11 HOL Proof General 53 11 HOL Proof General HOL Proof General is a technology demonstration of Proof General for HOL4 aka HOL98 This means that only a basic instantiation has been provided and that it is not yet supported as a maintained instantiation of Proof General HOL Proof General has basic script management support with a little bit of decoration of scripts and output It does not rely on a modified version of HOL so the pattern matching may be fragile in certain cases Support for multiple files deduces dependencies automatically so there is no interaction with the HOL make system yet See the example sm1 file for a demonstration proof script which works with Proof General Note that HOL proof scripts often use batch oriented single step tactic proofs but Proof General does not yet offer an easy way to edit these kind of proofs They wi
105. u x symbol INSERT notequal global set key super m x symbol INSERT arrowdblright global set key super i x symbol INSERT longarrowright This defines a bunch of short cuts for insert X Symbol logical symbols which are often used in Isabelle 7 2 Using file variables A very convenient way to customize file specific variables is to use the File Variables See Info file xemacs node File Variables This feature of Emacs allows to specify the values to use 42 Proof General for certain Emacs variables when a file is loaded Those values are written as a list at the end of the file For example in projects involving multiple directories it is often useful to set the variables proof prog name proof prog args and compile command for each file Here is an example for Coq users for the file dir bar foo v if you want Coq to be started with the path dir theories added in the libraries path I option you can put at the end of oo v Local Variables coq prog name coqtop coq prog args emacs I theories x End That way the good command is called when the scripting starts in foo v Notice that the command argument I theories is specific to the file foo v and thus if you set it via the configuration tool you will need to do it each time you load this file On the contrary with this method Emacs will do this opera
106. use the toolbar and menu functions instead The best way to learn Emacs key bindings is by using the menus You ll find the keys named below listed on the menus e First start Emacs with Proof General loaded According to how you have installed Proof General this may be by typing proofgeneral selecting it from a menu or simply by starting Emacs itself e Next find a new file by C x C f and typing as the filename Walkthrough thy This should load Isabelle Proof General and the toolbar and Proof General menus will appear You should have an empty buffer displayed The notation C x C f means control key with x followed by control key with f This is a standard notation for Emacs key bindings used throughout this manual This function also appears on the File menu of Emacs The remaining commands used will be on the Proof General menu If you re not using Isabelle you must choose a different file extension appropriately for your proof assistant If you don t know what to use see the previous chapter for the list of supported assistants and file extensions e Turn on electric terminator by typing C c and enter theory Walkthrough imports Main begin This first command begins the definition of a new theory inside Isabelle which extends the theory Main We re assuming that you have Isabelle HOL available which declares the Main theory You should be able to see the list of installed logics in Isabelle on the Logics m
107. ve selected a setting you are shown a buffer with its current value and facility to edit it Once you have edited it you can use the special buttons set save and done You must use one of set or save to get any effect The save button stores the setting in your emacs file The command M x customize save customized or XEmacs menubar item Options Save Options saves all settings you have edited A technical note In the customize menus the variable names mentioned later in this chapter may be abbreviated the proof or similar prefixes are omitted Also some of the option settings may have more descriptive names for example on and off than the low level lisp values non nil nil which are mentioned in this chapter These features make customize rather more friendly than raw lisp 34 Proof General You can also access the customize settings for Proof General from other non script buffers In XEmacs the menu path is Options gt Customize gt Emacs gt External gt Proof General in XEmacs In GNU Emacs use the menu Help gt Customize Emacs gt Top level Customization Group and select the External and then Proof General groups The complete set of customization settings will only be available after Proof General has been fully loaded Proof General is fully loaded when you visit a script file for the first time or if you type M x load library RET proof RET For more help with customize see See Info file
108. w be redis tributed by third parties and used in any context without applying for a special license Despite these legal changes we would still appreciate if you send us back any useful improvements you make to Proof General and register your use of Proof General on the web site Function and Command Index Function and Command Index A add completions from tags table 31 C Completa uoi ebIS see dz 30 I indent for tab command sess 12 is r strip terminato Sse uiii loweesissscees 50 P pe goals button actiOM iii tales 19 Pg goals yank s bterm i2 rr oe 19 pg hide all proofs 2 223 x RARE DES oo 21 DE next inputizdonnneisicamo n4 Be perdes des 24 pg next matching input sse ees es 24 pg next matching input from input 24 Pg previous input i 2 zo bb e RR ins 24 pg previous matching input 24 pg previous matching input from input 24 pg response clear displays 15 pesshowsall pro0 S 27552 scabies ute thi 21 pg toggle visibility 000 21 proof assert next command interactive 13 proof assert until point interactive 14 proof ctXtii een ER SG dese Prep 15 proof debug message face sess 39 proof declaration name face 39 proof display some buffers 15 35 proof eager annotation face 39 proof electric terminator toggle
109. ween the human and the proof assistant Primitive interfaces for proof assistants simply present a shell command interpreter view of this dialogue the human repeatedly types commands to the shell until the proof is completed The system responds at each step perhaps with a new list of subgoals to be solved or perhaps with a failure report Proof General manages the dialogue to show the human only the information which is relevant at each step Often we want to keep a record of the proof commands used to prove a theorem to build up a library of proved results An easy way to store a proof is to keep a text file which contains a proof script proof assistants usually provide facilities to read a proof script from a file instead of the terminal Using the file we can replay the proof script to prove the theorem again Using only a primitive shell interface it can be tedious to construct proof scripts with cut and paste Proof General helps out by issuing commands directly from a proof script file while it is being written and edited Proof General can also be used conveniently to replay a proof step by step to see the progress at each stage Scripting is the process of building up a proof script file or replaying a proof When script ing Proof General sends proof commands to the proof assistant one at a time and prevents you from editing commands which have been successfully completed by the proof assistant to keep synchronization Region
110. y are currently being processed This is a limitation of the present implementation Proof General locks a buffer as soon as it sees the appropriate message from the proof assistant Different proof assistants may use different messages either early locking when processing a file begins e g LEGO or late locking when processing a file ends e g Isabelle With early locking you may find that a script which has only been partly processed due to an error or interrupt for example is wrongly completely locked by Proof General Visit the file and retract back to the start to fix this With late locking there is the chance that you can break synchronization by editing a file as it is being read by the proof assistant and saving it before processing finishes In fact there is a general problem of editing files which may be processed by the proof assistant automatically Synchronization can be broken whenever you have unsaved changes in a proof script buffer and the proof assistant processes the corresponding file Of course this problem is familiar from program development using separate editors and compilers The good news is that Proof General can detect the problem and flashes up a warning in the response buffer You can then visit the modified buffer save it and retract to the beginning Then you are back on track For example LEGO generates additional compiled optimised proof script files for efficiency Chapter 4 Advanced Sc
111. you have completed the soundness proof and are ready to tackle new challenges Perhaps you want to prove a property that builds on soundness or you want to prove an orthogonal property such as completeness Proof General lets you do all of this while maintaining the consistency between proof script buffers and the state of the proof assistant However you cannot have more than one buffer where only a fraction of the proof script contains a locked region Before you can employ script management in another proof script buffer you must either fully assert or retract the current script buffer 4 3 View of processed files Proof General tries to be aware of all files that the proof assistant has processed or is currently processing In the best case it relies on the proof assistant explicitly telling it whenever it processes a new file which corresponds to a file containing a proof script If the current proof script buffer depends on background material from other files proof assistants typically process these files automatically If you visit such a file the whole file is locked as having been processed in a single step From the user s point of view you can only retract but not assert in this buffer Furthermore retraction is only possible to the beginning of the buffer Unlike a script buffer that has been processed step by step via Proof General automatically loaded script buffers do not pass through a red phase to indicate that the

Download Pdf Manuals

image

Related Search

Related Contents

ベンゼン  カタログ    User manual F850    Denver MPM-4024  Pioneer FH-P4200MP User's Manual    Samsung GT-M7603 คู่มือการใช้งาน  ZenBoa mode d`emploi.pptx  

Copyright © All rights reserved.
DMCA: DMCA_mwitty#outlook.com.