diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/.cvsignore | 48 | ||||
| -rw-r--r-- | doc/Makefile | 24 | ||||
| -rw-r--r-- | doc/Makefile.doc | 164 | ||||
| -rw-r--r-- | doc/PG-adapting.texi | 3786 | ||||
| -rw-r--r-- | doc/ProofGeneral.jpg | bin | 0 -> 12002 bytes | |||
| -rw-r--r-- | doc/ProofGeneral.texi | 3957 | ||||
| -rw-r--r-- | doc/README.doc | 38 | ||||
| -rw-r--r-- | doc/dir | 19 | ||||
| -rw-r--r-- | doc/docstring-magic.el | 67 | ||||
| -rw-r--r-- | doc/localdir | 3 |
10 files changed, 8106 insertions, 0 deletions
diff --git a/doc/.cvsignore b/doc/.cvsignore new file mode 100644 index 00000000..6a126a00 --- /dev/null +++ b/doc/.cvsignore @@ -0,0 +1,48 @@ +ProofGeneral.log +ProofGeneral.dvi +ProofGeneral.ps +ProofGeneral.pdf +ProofGeneral.ps.gz +ProofGeneral.kys +ProofGeneral.aux +ProofGeneral.cp +ProofGeneral.fn +ProofGeneral.vr +ProofGeneral.tp +ProofGeneral.ky +ProofGeneral.pg +ProofGeneral.toc +ProofGeneral.info +ProofGeneral.cps +ProofGeneral.fns +ProofGeneral.vrs +ProofGeneral.info-* +ProofGeneral.txt +ProofGeneral_*.html +ProofGeneral_toc.html +ProofGeneral_foot.html +PG-adapting.log +PG-adapting.dvi +PG-adapting.ps +PG-adapting.pdf +PG-adapting.ps.gz +PG-adapting.kys +PG-adapting.aux +PG-adapting.cp +PG-adapting.fn +PG-adapting.vr +PG-adapting.tp +PG-adapting.ky +PG-adapting.pg +PG-adapting.toc +PG-adapting.info +PG-adapting.cps +PG-adapting.fns +PG-adapting.vrs +PG-adapting.info-* +PG-adapting.txt +PG-adapting_*.html +PG-adapting_toc.html +PG-adapting_foot.html +ProofGeneralPortrait.eps +ProofGeneralPortrait.pdf diff --git a/doc/Makefile b/doc/Makefile new file mode 100644 index 00000000..2d008717 --- /dev/null +++ b/doc/Makefile @@ -0,0 +1,24 @@ +## +## Makefile for Proof General doc directory. +## +## Author: David Aspinall <da@dcs.ed.ac.uk> +## +## Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> +## +## $Id$ +## +########################################################################### +## +## Use: +## make info,dvi,pdf,html - build respective docs from texi source. +## make doc - make default kinds of doc (dvi, info). +## +########################################################################### + +default: + $(MAKE) doc + +%: + make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" $@ + make -f Makefile.doc DOCNAME=ProofGeneral MAKE="make -f Makefile.doc" $@ + diff --git a/doc/Makefile.doc b/doc/Makefile.doc new file mode 100644 index 00000000..b1004218 --- /dev/null +++ b/doc/Makefile.doc @@ -0,0 +1,164 @@ +## +## Makefile for Proof General doc directory. +## +## Author: David Aspinall <da@dcs.ed.ac.uk> +## +## Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> +## +## $Id$ +## +########################################################################### +## +## Use: +## make info,dvi,pdf,html - build respective docs from texi source. +## make doc - make default kinds of doc (dvi, info). +## +########################################################################### + + +MAKE = make -f Makefile.doc +MAKEINFO = makeinfo +TEXI2DVI = texi2dvi + +# `dviutils' package contains these useful utilities. +# "make rearrange" will only be called if you have dviselect. +DVISELECT = dviselect +DVICONCAT = dviconcat + + +# Assumes actual first two pages belong to titlepage +TITLERANGE = =1,=2 + +# Assumes that main document starts on third actual page +MAINRANGE = =3,=4,3: + +TOC = :_1 + +DVI2PS = dvips +TEXI2PDF = texi2pdf +TEXI2HTML = texi2html -expandinfo -number -split_chapter +# FIXME: choose emacs automatically if xemacs not available +EMACS = xemacs -batch + +TMPFILE=pgt + +.SUFFIXES: .texi .info .dvi .html .pdf .ps .eps .tiff .gz + +default: doc + +.texi.info: + $(MAKEINFO) $< + +.texi.dvi: + $(TEXI2DVI) $< + if `which $(DVISELECT) > /dev/null`; then $(MAKE) rearrange DOCNAME=$*; fi + +rearrange: + $(DVISELECT) -i $(DOCNAME).dvi -o $(DOCNAME).tmp1 $(TITLERANGE) + $(DVISELECT) -i $(DOCNAME).dvi -o $(DOCNAME).tmp2 $(MAINRANGE) + $(DVISELECT) -i $(DOCNAME).dvi -o $(DOCNAME).tmp3 $(TOC) + $(DVICONCAT) -o $(DOCNAME).dvi $(DOCNAME).tmp1 $(DOCNAME).tmp3 $(DOCNAME).tmp2 + rm -f $(DOCNAME).tmp1 $(DOCNAME).tmp2 $(DOCNAME).tmp3 + +.tiff.eps: + tiff2ps -e -w 3.48 -h 5 $*.tiff > $*.eps + +## FIXME: need to do page rearrangement here, too! +.texi.pdf: + $(TEXI2PDF) $< + +.dvi.ps: + $(DVI2PS) $< -o $*.ps + +.texi.html: + $(TEXI2HTML) $< + +default: doc + +FORCE: + +ProofGeneral.txt: + echo > ProofGeneral.txt + +ProofGeneralPortrait.eps: FORCE + if [ -f ProofGeneralPortrait.eps.gz ]; then gunzip -c ProofGeneralPortrait.eps.gz > ProofGeneralPortrait.eps; fi + if [ -f ProofGeneralPortrait.eps ]; then \ + sed 's/@clear haveeps/@set haveeps/g' $(DOCNAME).texi > $(TMPFILE); \ + sed 's/@c image{ProofGeneralPortrait}/@image{ProofGeneralPortrait}/g' $(TMPFILE) > $(DOCNAME).texi; \ + else \ + sed 's/@set haveeps/@clear haveeps/g' $(DOCNAME).texi > $(TMPFILE); \ + sed 's/@image{ProofGeneralPortrait}/@c image{ProofGeneralPortrait}/g' $(TMPFILE) > $(DOCNAME).texi; \ + fi + rm -f $(TMPFILE) + +ProofGeneralPortrait.pdf: + if [ -f ProofGeneralPortrait.eps.gz ]; then gunzip -c ProofGeneralPortrait.eps.gz > ProofGeneralPortrait.eps; epstopdf ProofGeneralPortrait.eps; fi + if [ -f ProofGeneralPortrait.pdf ]; then \ + sed 's/@clear haveeps/@set haveeps/g' $(DOCNAME).texi > $(TMPFILE); \ + sed 's/@c image{ProofGeneralPortrait}/@image{ProofGeneralPortrait}/g' $(TMPFILE) > $(DOCNAME).texi; \ + else \ + sed 's/@set haveeps/@clear haveeps/g' $(DOCNAME).texi > $(TMPFILE); \ + sed 's/@image{ProofGeneralPortrait}/@c image{ProofGeneralPortrait}/g' $(TMPFILE) > $(DOCNAME).texi; \ + fi + rm -f $(TMPFILE) + +%.gz : % + gzip -f -9 $* + +## +## doc : build info and dvi files from $(DOCNAME).texi +## +doc: dvi info + + +## +## all : build all documentation targets +## +all: dvi ps html info pdf + +## +## dist: build distribution targets +## +dist: info html psz pdf + +dvi: ProofGeneralPortrait.eps $(DOCNAME).dvi +ps: dvi $(DOCNAME).ps +psz: ps $(DOCNAME).ps.gz +pdf: ProofGeneralPortrait.pdf $(DOCNAME).pdf +html: $(DOCNAME).html + ln -sf $(DOCNAME)_toc.html index.html +info: ProofGeneral.txt $(DOCNAME).info + +# NB: for info, could make localdir automatically from +# START-INFO-DIR-ENTRY / END-INFO-DIR-ENTRY. +# Does some utility do this? + +## +## clean: Remove subsidiary documentation files +## +clean: + rm -f ProofGeneral.txt ProofGeneralPortrait.eps ProofGeneralPortrait.pdf + rm -f $(DOCNAME).{cp,fn,vr,tp,ky,pg} + rm -f $(DOCNAME).{fns,vrs,cps,aux,log,toc,kys,cp0} + rm -f *~ + +## +## distclean: Remove documentation targets +## +distclean: clean + rm -f $(DOCNAME).info* $(DOCNAME).dvi $(DOCNAME)*.ps $(DOCNAME).pdf $(DOCNAME)*.html + +## +## texi: update magic comments in texi from docstrings in code. +## (developer use only!) +## +$(DOCNAME).texi: ../*/*.el + $(MAKE) magic +magic: + $(EMACS) -l docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer + + + + + + diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi new file mode 100644 index 00000000..5bbfb093 --- /dev/null +++ b/doc/PG-adapting.texi @@ -0,0 +1,3786 @@ + +\def\fontdefs{\psfamily{bsf}{r}{c}{b}{b}{ri}{ri}{ro}{bo}\def\mainmagstep{1200}} +\input texinfo +@c +@c $Id$ +@c +@c NB: the first line of this file uses a non-standard TeXinfo +@c hack to print in Serifa fonts. It has no effect if you don't have +@c my hacked version of TeXinfo - da. +@c +@c +@setfilename PG-adapting.info +@settitle Adapting Proof General +@setchapternewpage odd +@paragraphindent 0 +@c A flag for whether to include the front image in the +@c DVI file. You can download the front image from +@c http://www.proofgeneral.org/ProofGeneralPortrait.eps.gz +@c then put it into this directory and 'make dvi' (pdf,ps) +@c will set the flag below automatically. +@set haveeps +@iftex +@afourpaper +@end iftex + +@c +@c Some URLs. +@c FIXME: unfortunately, broken in buggy pdftexinfo. +@c so removed for now. +@set URLxsymbol http://www.fmi.uni-passau.de/~wedler/x-symbol/ +@set URLisamode http://zermelo.dcs.ed.ac.uk/~isamode +@set URLpghome http://www.proofgeneral.org +@set URLpglatestrpm http://www.proofgeneral.org/ProofGeneral-latest.noarch.rpm +@set URLpglatesttar http://www.proofgeneral.org/ProofGeneral-latest.tar.gz +@set URLpglatestdev http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz +@c +@c + +@c +@c IMPORTANT NOTE ABOUT THIS TEXINFO FILE: +@c I've tried keep full node lines *out* of this file because Emacs makes a +@c mess of updating them and they are a nuisance to do by hand. +@c Instead, rely on makeinfo and friends to do the equivalent job. +@c For this to work, we must follow each node +@c immediately with a section command, i.e.: +@c +@c @node node-name +@c <section-command> +@c +@c And each section with lower levels must have a menu command in +@c it. Menu updating with Emacs is a bit better than node updating, +@c but tends to delete the first section of the file in XEmacs! +@c (it's better in FSF Emacs at the time of writing). +@c +@c +@c reminder about references: +@c @xref{node} blah start of sentence: See [ref] +@c blah (@pxref{node}) blah bla (see [ref]), best at end of sentence +@c @ref{node} without "see". Careful for info. + + +@set version 3.3pre +@set xemacsversion 21.1 +@set fsfversion 20.7 +@set last-update October 2000 +@set rcsid $Id$ + +@ifinfo +@format +START-INFO-DIR-ENTRY +* Adapting PG: (PG-adapting). How to adapt Proof General for new provers +END-INFO-DIR-ENTRY +@end format +@end ifinfo + +@c +@c MACROS +@c +@c define one here for a command with a key-binding? +@c +@c I like the idea, but it's maybe against the TeXinfo +@c style to fix together a command and its key-binding. +@c +@c merge functions and variables into concept index. +@c @syncodeindex fn cp +@c @syncodeindex vr cp + +@c merge functions into variables index +@c @syncodeindex fn vr + +@finalout +@titlepage +@title Adapting Proof General +@subtitle Proof General --- Organize your proofs! +@sp 1 +@subtitle Adapting Proof General @value{version} to new provers +@subtitle @value{last-update} +@subtitle @b{www.proofgeneral.org} + +@c nested ifs fail here completely, WHY? +@iftex +@ifset haveeps +@c @vskip 1cm +@c The .eps file takes 8.4M! A pity texi can't seem +@c to deal with gzipped files? (goes down to 1.7M). +@c But this still seems too much to put into the +@c PG distribution just for an image on the manual page, +@c so we take it out for now. +@c Ideally would like some way of generating eps from +@c the .jpg file. +@image{ProofGeneralPortrait} +@end ifset +@end iftex +@author David Aspinall with T. Kleymann +@page +@vskip 0pt plus 1filll +This manual and the program Proof General are +Copyright @copyright{} 2000 Proof General team, LFCS Edinburgh. + + +@c +@c COPYING NOTICE +@c +@ignore +Permission is granted to process this file through TeX and print the +results, provided the printed document carries copying permission notice +identical to this one except for the removal of this paragraph (this +paragraph not being relevant to the printed manual). +@end ignore + +@sp 2 +Permission is granted to make and distribute verbatim copies of this +manual provided the copyright notice and this permission notice are +preserved on all copies. +@sp 2 + +This manual documents Proof General, Version @value{version}, for use +with XEmacs @value{xemacsversion} and FSF GNU Emacs @value{fsfversion} +or later versions. + +Visit Proof General on the web at @code{http://www.proofgeneral.org} + +Version control: @code{@value{rcsid}} +@end titlepage + +@page + + +@ifinfo +@node Top +@top Proof General + +This file documents configuration mechanisms for version @value{version} +of @b{Proof General}, a generic Emacs interface for proof assistants. + +Proof General @value{version} has been tested with XEmacs +@value{xemacsversion} and FSF GNU Emacs @value{fsfversion}. It is +supplied ready customized for the proof assistants Coq, Lego, +Isabelle, and HOL. + +This manual contains information for customizing to new proof +assistants; see the user manual for details about how to use +Proof General. + +@menu +* Introduction:: +* Beginning with a new prover:: +* Menus and toolbar and user-level commands:: +* Proof script settings:: +* Proof shell settings:: +* Goals buffer settings:: +* Splash screen settings:: +* Global constants:: +* Handling multiple files:: +* Configuring Font Lock:: +* Configuring X-Symbol:: +* Writing more lisp code:: +* Internals of Proof General:: +* Plans and ideas:: +* Demonstration Instantiations:: +* Function Index:: +* Variable Index:: +* Concept Index:: +@end menu +@end ifinfo + +@node Introduction +@unnumbered Introduction + +Welcome to Proof General! + +Proof General a generic Emacs-based interface for proof assistants. + +This manual contains information for adapting Proof General to new proof +assistants, and some sketches of the internal implementation. It is not +intended for most ordinary users of the system. + +For full details about how to use Proof General, and information on its +availability and installation, please see the main Proof General manual +which should accompany this one. + +We positively encourage the support of new systems. Proof General has +grown more flexible and useful as it has been adapted to more proof +assistants. + +Typically, adding support for a new prover improves support for others, +both because the code becomes more robust, and because new ideas are +brought into the generic setting. Notice that the Proof General +framework has been built as a "product line architecture": generality +has been introduced step-by-step in a demand-driven way, rather than at +the outset as a grand design. Despite this strategy, the interface has +a surprisingly clean structure. The approach means that we fully expect +hiccups when adding support for new assistants, so the generic core may +need extension or modification. To support this we have an open +development method: if you require changes in the generic support, +please contact us (or make adjustments yourself and send them to us). + +Proof General has a home page at +@uref{http://www.proofgeneral.org}. Visit this page +for the latest version of the manuals, other documentation, system +downloads, etc. + + +@menu +* Future:: +* Credits:: +@end menu + +@node Future +@unnumberedsec Future +@cindex Proof General Kit +@cindex Future + +The aim of the Proof General project is to provide a powerful and +configurable interfaces which help user-interaction with interactive +proof assistants. + +The strategy Proof General uses is to targets power users rather than +novices; other interfaces have often neglected this class of users. But +we do include general user interface niceties, such as toolbar and +menus, which make use easier for all. + +Proof General has been Emacs based so far, but plans are afoot to +liberate it from the points and parentheses of Emacs Lisp. The +successor project Proof General Kit proposes that proof assistants use a +@i{standard} XML-based protocol for interactive proof, dubbed @b{PGIP}. + +PGIP is a 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. This means that effort on +customizing Emacs Proof General to a new proof assistant is worthwhile +even in the light of PGIP: it will help you to understand Proof +General's model of interaction, and moreover, we hope to use the Emacs +customizations to provide experimental filters which allow supported +provers to communicate using PGIP. + +At the time of writing, these ideas are in early stages. For latest +details, or to become involved, see +@uref{http://www.proofgeneral.org/kit.html, the Proof General Kit +webpage}. + + +@node Credits +@unnumberedsec Credits + +This manual was put together and mostly written by David Aspinall. Thomas +Kleymann wrote some of the text in Chapter 8. +Much of the content is generated automatically from Emacs docstrings, +some of which have been written by other Proof General developers. + + + +@node Beginning with a new prover +@chapter Beginning with a new prover + +Proof General has about 100 configuration variables which are set on a +per-prover basis to configure the various features. It may sound like a +lot but don't worry! Many of the variables occur in pairs (typically +regular expressions matching the start and end of some text), and you +can begin by setting just a fraction of the variables to get the basic +features of script management working. The bare minimum for a working +prototype is about 25 simple settings. + +For more advanced features you may need (or want) to write some Emacs +Lisp. If you're adding new functionality please consider making it +generic for different proof assistants, if appropriate. When writing +your modes, please follow the Emacs Lisp conventions @inforef{Style +Tips, ,lispref}. + +The configuration variables are declared in the file +@file{generic/proof-config.el}. The details in the central part of this +manual are based on the contents of that file, beginning in @ref{Menus and toolbar +and user-level commands}, and continuing until @ref{Global constants}. +Other chapters cover the details of configuring for multiple files and +for supporting the other Emacs packages mentioned in the user manual +(@i{Support for other Packages}). If you write additional Elisp code +interfacing to Proof General, you can find out about some useful functions +by reading @ref{Writing more lisp code}. The last chapter of this +manual describes some of the internals of Proof General, in case you are +interested, maybe because you need to extend the generic core to do +something new. + +In the rest of this chapter we describe the general mechanisms for +instantiating Proof General. + +@menu +* Overview of adding a new prover:: +* Demonstration instance and easy configuration:: +* Major modes used by Proof General:: +@end menu + + +@node Overview of adding a new prover +@section Overview of adding a new prover + +Each proof assistant supported has its own subdirectory under +@code{proof-home-directory}, used to store a root elisp file and any +other files needed to adapt the proof assistant for Proof General. + +@c Here we show how a minimal configuration of Proof General works for +@c Isabelle, without any special changes to Isabelle. + +Here is how to go about adding support for a new prover. + +@enumerate +@item Make a directory called @file{myassistant/} under the Proof General home +directory @code{proof-home-directory}, to put the specific customization +and associated files in. +@item Add a file @file{myassistant.el} to the new directory. +@item Edit @file{proof-site.el} to add a new entry to the + @code{proof-assistants-table} variable. The new entry should look +like this: +@lisp + (myassistant "My Proof Assistant" "\\.myasst$") +@end lisp +The first item is used to form the name of the internal variables for +the new mode as well as the directory and file where it loads from. The +second is a string, naming the proof assistant. The third item is a +regular expression to match names of proof script files for this +assistant. See the documentation of @code{proof-assistant-table} for +more details. +@item Define the new Proof General modes in @file{myassistant.el}, + by setting configuration variables to customize the + behaviour of the generic modes. +@end enumerate + +@c You could begin by setting a minimum number of the variables, then +@c adjust the settings via the customize menus, under Proof-General -> +@c Internals. + +@c TEXI DOCSTRING MAGIC: proof-assistant-table +@defopt proof-assistant-table +Proof General's table of supported proof assistants.@* +Extend this table to add a new proof assistant. +Each entry is a list of the form +@lisp + (@var{symbol} @var{name} @var{automode-regexp}) +@end lisp +The @var{name} is a string, naming the proof assistant. +The @var{symbol} is used to form the name of the mode for the +assistant, @samp{SYMBOL-mode}, run when files with @var{automode-regexp} +are visited. @var{symbol} is also used to form the name of the +directory and elisp file for the mode, which will be +@lisp + @var{proof-home-directory}/@var{symbol}/@var{symbol}.el +@end lisp +where @samp{PROOF-HOME-DIRECTORY} is the value of the +variable @code{proof-home-directory}. + +The default value is @code{((demoisa "Isabelle Demo" "\\.ML$") (isar "Isabelle/Isar" "\\.thy$") (isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$") (phox "PhoX" "\\.phx$") (hol98 "HOL" "\\.sml$") (acl2 "ACL2" "\\.acl2$") (plastic "Plastic" "\\.lf$") (twelf "Twelf" "\\.elf$"))}. +@end defopt + + +The final step of the description above is where the work lies. There +are two basic methods. You can write some Emacs lisp functions and +define the modes using the macro @code{define-derived-mode}. Or you can +use the new easy configuration mechanism of Proof General 3.0 described +in the next section, which calls @code{define-derived-mode} for you. +You still need to know which configuration variables should be set, and +how to set them. + +The documentation below (and inside Emacs) should help with that, but +the best way to begin might be to use an existing Proof General instance +as an example. Even better is to use the new easy configuration +mechanism, which avoids the need to call @code{define-derived-mode} +directly. + + +@node Demonstration instance and easy configuration +@section Demonstration instance and easy configuration + +Proof General is supplied with a demonstration instance for Isabelle +which configures the basic features. This is a whittled down version of +Isabelle Proof General, which you can use as a template to get support +for a new assistant going. Check the directory @file{demoisa} for the +two files @file{demoisa.el} and @file{demoisa-easy.el}. + +The file @file{demoisa.el} follows the scheme described in @ref{Major +modes used by Proof General}. It uses the Emacs Lisp macro +@code{define-derived-mode} to define the four modes for a Proof General +instance, by inheriting from the generic code. Settings which configure +Proof General are made by functions called from within each mode, as +appropriate. + +The file @file{demoisa-easy.el} uses a new simplified mechanism to +achieve (virtually) the same result. It uses the macro +@code{proof-easy-config} defined in @file{proof-easy-configl.el} to make +all of the settings for the Proof General instance in one go, defining +the derived modes automatically using a regular naming scheme. No lisp +code is used in this file except the call to this macro. The minor +difference in the end result is that all the variables are set at once, +rather than inside each mode. But since the configuration variables are +all global variables anyway, this makes no real difference. + +The macro @code{proof-easy-config} is called like this: +@lisp + (proof-easy-config @var{myprover} "@var{MyProver}" + @var{config_1} @var{val_1} + ... + @var{config_n} @var{val_n}) +@end lisp +The main body of the macro call is like the body of a @code{setq}. It +contains pairs of variables and value settings. The first argument to +the macro is a symbol defining the mode root, the second argument is a +string defining the mode name. These should be the same as the first +part of the entry in @code{proof-assistant-table} for your prover. +@xref{Overview of adding a new prover}. After the call to +@code{proof-easy-config}, the new modes @code{@var{myprover}-mode}, +@code{@var{myprover}-shell-mode}, @code{@var{myprover}-response-mode}, +and @code{@var{myprover}-goals-mode} will be defined. The configuration +variables in the body will be set immediately. + + +This mechanism is in fact recommended for new instantiations of +Proof General since it follows a regular pattern, and we can more +easily adapt it in the future to new versions of Proof General. + +Even Emacs Lisp experts should prefer the simplified mechanism. If you +want to set some buffer-local variables in your Proof General modes, or +invoke supporting lisp code, this can easily be done by adding functions +to the appropriate mode hooks after the @code{proof-easy-config} call. +For example, to add extra settings for the shell mode for +@code{demoisa}, we could do this: +@lisp + (defun demoisa-shell-extra-config () + @var{extra configuration ...} + ) + (add-hook 'demoisa-shell-mode-hook 'demoisa-shell-extra-config) +@end lisp +The function to do extra configuration @code{demoisa-shell-extra-config} +is then called as the final step when @code{demoisa-shell-mode} is +entered (be wary, this will be after the generic +@code{proof-shell-config-done} is called, so it will be too late to set +normal configuration variables which may be examined by +@code{proof-shell-config-done}). + + +@node Major modes used by Proof General +@section Major modes used by Proof General + +There are four major modes used by Proof General, one for each type of +buffer it handles. The buffer types are: script, shell, response and +goals. Each of these has a generic mode, respectively: +@code{proof-mode}, @code{proof-shell-mode}, @code{proof-response-mode}, +and @code{proof-goals-mode}. + +The pattern for defining the major mode for an instance of Proof General +is to use @code{define-derived-mode} to define a specific mode to inherit from +each generic one, like this: +@lisp +(define-derived-mode myass-shell-mode proof-shell-mode + "MyAss shell" nil + (myass-shell-config) + (proof-shell-config-done)) +@end lisp +Where @code{myass-shell-config} is a function which sets the +configuration variables for the shell (@pxref{Proof shell settings}). + +It's important that each of your modes invokes one of the functions + @code{proof-config-done}, + @code{proof-shell-config-done}, + @code{proof-response-config-done}, or + @code{proof-goals-config-done} +once it has set its configuration variables. These functions +finalize the configuration of the mode. + +For each mode, there is a configuration variable which names it so that +Proof General can set buffers to the proper mode, or find buffers in +that mode. These are documented below, and set like this: +@lisp + (setq proof-mode-for-script 'myass-mode) +@end lisp +where @code{myass-mode} is your major mode for scripts, derived from +@code{proof-mode}. You must set these variables before the proof shell +is started; one way to do this is inside a function which is called from +the hook @code{pre-shell-start-hook}. See the file @file{demoisa.el} +for details of how to do this. + +@c TEXI DOCSTRING MAGIC: proof-mode-for-script +@defvar proof-mode-for-script +Mode for proof script buffers.@* +This is used by Proof General to find out which buffers +contain proof scripts. +The regular name for this is <PA>-mode. If you use any of the +convenience macros Proof General provides for defining commands +etc, then you should stick to this name. +Suggestion: this can be set in the script mode configuration. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-mode-for-shell +@defvar proof-mode-for-shell +Mode for proof shell buffers.@* +Usually customised for specific prover. +Suggestion: this can be set a function called by @samp{pre-shell-start-hook}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-mode-for-response +@defvar proof-mode-for-response +Mode for proof response buffer.@* +Usually customised for specific prover. +Suggestion: this can be set a function called by @samp{pre-shell-start-hook}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-mode-for-goals +@defvar proof-mode-for-goals +Mode for proof state display buffers.@* +Usually customised for specific prover. +Suggestion: this can be set a function called by @samp{pre-shell-start-hook}. +@end defvar + +@node Menus and toolbar and user-level commands +@chapter Menus, toolbar, and user-level commands + +The variables described in this chapter should be set in the script mode +before @code{proof-config-done} is called. (Toolbar configuration must +be made before @file{proof-toolbar.el} is loaded, which usually is +triggered automatically by an attempt to display the toolbar). + +@menu +* Settings for generic user-level commands:: +* Menu configuration:: +* Toolbar configuration:: +@end menu + +@node Settings for generic user-level commands +@section Settings for generic user-level commands + +@c TEXI DOCSTRING MAGIC: proof-assistant-home-page +@defvar proof-assistant-home-page +Web address for information on proof assistant.@* +Used for Proof General's help menu. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-context-command +@defvar proof-context-command +Command to display the context in proof assistant. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-info-command +@defvar proof-info-command +Command to ask for help or information in the proof assistant.@* +String or fn. If a string, the command to use. +If a function, it should return the command string to insert. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-showproof-command +@defvar proof-showproof-command +Command to display proof state in proof assistant. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-goal-command +@defvar proof-goal-command +Command to set a goal in the proof assistant. String or fn.@* +If a string, the format character @samp{%s} will be replaced by the +goal string. +If a function, it should return the command string to insert. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-save-command +@defvar proof-save-command +Command to save a proved theorem in the proof assistant. String or fn.@* +If a string, the format character @samp{%s} will be replaced by the +theorem name. +If a function, it should return the command string to insert. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-find-theorems-command +@defvar proof-find-theorems-command +Command to search for a theorem containing a given term. String or fn.@* +If a string, the format character @samp{%s} will be replaced by the term. +If a function, it should return the command string to insert. +@end defvar + + + +@node Menu configuration +@section Menu configuration + +As well as the generic Proof General menu, each proof assistant is +provided with a specific menu which can have prover-specific commands. +Proof General puts some default things on this menu, including the +commands to start/stop the prover, and the user-extensible "Favourites" +menu. + +@c TEXI DOCSTRING MAGIC: PA-menu-entries +@defvar PA-menu-entries +Extra entries for proof assistant specific menu. @* +A list of menu items [@var{name} @var{callback} @var{enabler} ...]. See the documentation +of @samp{@code{easy-menu-define}} for more details. +@end defvar + +@c TEXI DOCSTRING MAGIC: PA-help-menu-entries +@defvar PA-help-menu-entries +Extra entries for help submenu for proof assistant specific help menu.@* +A list of menu items [@var{name} @var{callback} @var{enabler} ...]. See the documentation +of @samp{@code{easy-menu-define}} for more details. +@end defvar + + +@node Toolbar configuration +@section Toolbar configuration + +Unlike the menus, Proof General has only one toolbar. For the "generic" +aspect of Proof General to work well, we shouldn't change (the meaning +of) the existing toolbar buttons too far. This would discourage people +from experimenting with different proof assistants when they don't +really know them, which is one of the advantages that Proof General +brings. + +But in case it is hard to map some of the generic buttons +onto functions in particular provers, and to allow extra +buttons, there is a mechanism for adjustment. + +I used The Gimp to create the buttons for Proof General. The +development distribution includes a button blank and some notes in +@file{etc/notes.txt} about making new buttons. + + +@c TEXI DOCSTRING MAGIC: proof-toolbar-entries-default +@defvar proof-toolbar-entries-default +Example value for proof-toolbar-entries. Also used to define Scripting menu.@* +This gives a bare toolbar that works for any prover, providing the +appropriate configuration variables are set. +To add/remove prover specific buttons, adjust the @samp{<PA>-toolbar-entries} +variable, and follow the pattern in @samp{@code{proof-toolbar}.el} for +defining functions, images. +@end defvar + +@c TEXI DOCSTRING MAGIC: PA-toolbar-entries +@defvar PA-toolbar-entries +List of entries for Proof General toolbar and Scripting menu.@* +Format of each entry is (@var{token} @var{menuname} @var{tooltip} @var{enabler-p}). + +For each @var{token}, we expect an icon with base filename @var{token}, +a function proof-toolbar-<TOKEN>, and (optionally) an enabler +proof-toolbar-<TOKEN>-enable-p. + +If @var{menuname} is nil, item will not appear on the scripting menu. + +If @var{tooltip} is nil, item will not appear on the toolbar. + +The default value is @samp{@code{proof-toolbar-entries-default}} which contains +the standard Proof General buttons. +@end defvar + +Here's an example of how to remove a button, from @file{af2.el}: +@lisp +(setq af2-toolbar-entries + (remassoc 'state af2-toolbar-entries)) +@end lisp + + + +@c defgroup proof-script +@node Proof script settings +@chapter Proof script settings + +The variables described in this chapter should be set in the script mode +before @code{proof-config-done} is called. These configure the mode for +the script buffer. The settings here configure the recognition of +commands in the proof script, and also control some of the behaviour of +script management. + + +@menu +* Recognizing commands and comments:: +* Recognizing proofs:: +* Recognizing other elements:: +* Configuring undo behaviour:: +* Nested proofs:: +* Safe (state-preserving) commands:: +* Activate scripting hook:: +* Automatic multiple files:: +* Completions:: +@end menu + + +@node Recognizing commands and comments +@section Recognizing commands and comments + +The first four settings configure the generic parsing strategy for +commands in the proof script. Usually only one of these three needs to +be set. If the generic parsing functions are not flexible for your +needs, you can supply a value for @code{proof-script-parse-function}. + +Note that for the generic functions to work properly, it is +@strong{essential} that you set the syntax table for your mode properly, +so that comments and strings are recognized. See the Emacs +documentation to discover how to do this (particularly for the function +@code{modify-syntax-entry}). + +@xref{Proof script mode}, for more details of the parsing +functions. + +@c TEXI DOCSTRING MAGIC: proof-terminal-char +@defvar proof-terminal-char +Character which terminates every command sent to proof assistant. nil if none. + +To configure command recognition properly, you must set at least one +of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}}, +@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-char}}, +or @samp{@code{proof-script-parse-function}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-sexp-commands +@defvar proof-script-sexp-commands +Non-nil if proof script has a LISP-like syntax, and commands are @code{top-level} sexps.@* +You should set this variable in script mode configuration. + +To configure command recognition properly, you must set at least one +of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}}, +@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-char}}, +or @samp{@code{proof-script-parse-function}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-command-start-regexp +@defvar proof-script-command-start-regexp +Regular expression which matches start of commands in proof script.@* +You should set this variable in script mode configuration. + +To configure command recognition properly, you must set at least one +of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}}, +@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-char}}, +or @samp{@code{proof-script-parse-function}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-command-end-regexp +@defvar proof-script-command-end-regexp +Regular expression which matches end of commands in proof script.@* +You should set this variable in script mode configuration. + +To configure command recognition properly, you must set at least one +of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}}, +@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-char}}, +or @samp{@code{proof-script-parse-function}}. +@end defvar + + +The next four settings configure the comment syntax. Notice that to get +reliable behaviour of the parsing functions, you may need to modify the +syntax table for your prover's mode. Read the Elisp manual for details +about that. + +@c TEXI DOCSTRING MAGIC: proof-comment-start +@defvar proof-comment-start +String which starts a comment in the proof assistant command language.@* +The script buffer's @code{comment-start} is set to this string plus a space. +Moreover, comments are usually ignored during script management, and not +sent to the proof process. + +You should set this variable for reliable working of Proof General, +as well as @samp{@code{proof-comment-end}}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-comment-start-regexp + +@defvar proof-comment-start-regexp +Regexp which matches a comment start in the proof command language. + +The default value for this is set as (@code{regexp-quote} @code{proof-comment-start}) +but you can set this variable to something else more precise if necessary. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-comment-end +@defvar proof-comment-end +String which ends a comment in the proof assistant command language.@* +The script buffer's @code{comment-end} is set to a space plus this string. +See also @samp{@code{proof-comment-start}}. + +You should set this variable for reliable working of Proof General, +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-comment-end-regexp +@defvar proof-comment-end-regexp +Regexp which matches a comment end in the proof command language. + +The default value for this is set as (@code{regexp-quote} @code{proof-comment-end}) +but you can set this variable to something else more precise if necessary. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-case-fold-search +@defvar proof-case-fold-search +Value for @code{case-fold-search} when recognizing portions of proof scripts.@* +Also used for completion, via @samp{@code{proof-script-complete}}. +The default value is @samp{nil}. If your prover has a case @strong{insensitive} +input syntax, @code{proof-case-fold-search} should be set to @samp{t} instead. +NB: This setting is not used for matching output from the prover. +@end defvar + + +@node Recognizing proofs +@section Recognizing proofs + +Up to three settings each may be supplied for recognizing goal-like and +save-like commands. The @code{-with-hole-} settings are used to make a +record of the name of the theorem proved, and also to build a default +value for the rather complicated setting +@code{proof-script-next-entity-regexps}, which activates the @i{function +menu} feature. + +The @code{-p} subsidiary predicates were added to allow more +discriminating behaviour for particular proof assistants. (This is a +typical example of where the core framework needs some additional +generalization, to simplify matters, and allow for a smooth handling of +nested proofs). + + +@c TEXI DOCSTRING MAGIC: proof-goal-command-regexp +@defvar proof-goal-command-regexp +Matches a goal command in the proof script. @* +This is used (1) to make the default value for @samp{@code{proof-goal-command-p}}, +used as an important part of script management to find the start +of an atomic undo block, and (2) to construct the default +for @samp{@code{proof-script-next-entity-regexps}} used for function menus. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-goal-with-hole-regexp +@defvar proof-goal-with-hole-regexp +Regexp which matches a command used to issue and name a goal.@* +The name of the theorem is build from the variable +@code{proof-goal-with-hole-result} using the same convention as +@code{query-replace-regexp}. +Used for setting names of goal..save regions and for default +@code{function-menu} configuration in @code{proof-script-find-next-entity}. + +It's safe to leave this setting as nil. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-goal-command-p +@defvar proof-goal-command-p +A function to test: is this really a goal command? + +This is added as a more refined addition to @code{proof-goal-command-regexp}, +to solve the problem that Coq and some other provers can have goals which +look like definitions, etc. (In the future we may generalize +@code{proof-goal-command-regexp} instead). +@end defvar + + +@c TEXI DOCSTRING MAGIC: proof-save-command-regexp +@defvar proof-save-command-regexp +Matches a save command. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-save-with-hole-regexp +@defvar proof-save-with-hole-regexp +Regexp which matches a command to save a named theorem.@* +The name of the theorem is build from the variable +@code{proof-save-with-hole-result} using the same convention as +@code{query-replace-regexp}. +Used for setting names of goal..save regions and for default +@code{function-menu} configuration in @code{proof-script-find-next-entity}. + +It's safe to leave this setting as nil. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-completed-proof-behaviour +@defvar proof-completed-proof-behaviour +Indicates how Proof General treats commands beyond the end of a proof.@* +Normally goal...save regions are "closed", i.e. made atomic for undo. +But once a proof has been completed, there may be a delay before +the "save" command appears --- or it may not appear at all. Unless +nested proofs are supported, this can spoil the undo-behaviour in +script management since once a new goal arrives the old undo history +may be lost in the prover. So we allow Proof General to close +off the goal..[save] region in more flexible ways. +The possibilities are: +@lisp + nil - nothing special; close only when a save arrives + @code{'closeany} - close as soon as the next command arrives, save or not + @code{'closegoal} - close when the next "goal" command arrives + @code{'extend} - keep extending the closed region until a save or goal. +@end lisp +If your proof assistant allows nested goals, it will be wrong to close +off the portion of proof so far, so this variable should be set to nil. +There is no built-in understanding of the undo behaviour of nested +proofs; instead there is some support for un-nesting nested proofs in +the @code{proof-lift-global} mechanism. (Of course, this is risky in case of +nested contexts!) +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-really-save-command-p +@defvar proof-really-save-command-p +Is this really a save command? + +This is a more refined addition to @code{proof-save-command-regexp}. +It should be a function taking a span and command as argument, +and can be used to track nested proofs. (See what is done in +isar/ for example). In the future, this setting should be +removed when the generic core is extended to handle nested +proofs smoothly. +@end defvar + + +@node Recognizing other elements +@section Recognizing other elements + +To configure the @i{function menu} feature, there are a couple of +settings. These can be used to recognize named proofs, and other +elements in the proof script as well. + +@c TEXI DOCSTRING MAGIC: proof-script-next-entity-regexps +@defvar proof-script-next-entity-regexps +Regular expressions to help find definitions and proofs in a script.@* +This is the list of the form +@lisp + (@var{anyentity-regexp} + @var{discriminator-regexp} ... @var{discriminator-regexp}) +@end lisp +The idea is that @var{anyentity-regexp} matches any named entity in the +proof script, on a line where the name appears. This is assumed to be +the start or the end of the entity. The discriminators then test +which kind of entity has been found, to get its name. A +@var{discriminator-regexp} has one of the forms +@lisp + (@var{regexp} @var{matchnos}) + (@var{regexp} @var{matchnos} @code{'backward} @var{backregexp}) + (@var{regexp} @var{matchnos} @code{'forward} @var{forwardregexp}) +@end lisp +If @var{regexp} matches the string captured by @var{anyentity-regexp}, then +@var{matchnos} are the match numbers for the substrings which name the entity +(these may be either a single number or a list of numbers). + +If @code{'backward} @var{backregexp} is present, then the start of the entity +is found by searching backwards for @var{backregexp}. + +Conversely, if @code{'forward} @var{forwardregexp} is found, then the end of +the entity is found by searching forwards for @var{forwardregexp}. + +Otherwise, the start and end of the entity will be the region matched +by @var{anyentity-regexp}. + +This mechanism allows fairly complex parsing of the buffer, in +particular, it allows for goal..save regions which are named +only at the end. However, it does not parse strings, +comments, or parentheses. + +This variable may not need to be set: a default value which should +work for goal..saves is calculated from @code{proof-goal-with-hole-regexp}, +@code{proof-goal-command-regexp}, and @code{proof-save-with-hole-regexp}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-find-next-entity-fn +@defvar proof-script-find-next-entity-fn +Name of function to find next interesting entity in a script buffer.@* +This is used to configure @code{func-menu}. The default value is +@code{proof-script-find-next-entity}, which searches for the next entity +based on fume-function-name-regexp which by default is set from +@code{proof-script-next-entity-regexps}. + +The function should move point forward in a buffer, and return a cons +cell of the name and the beginning of the entity's region. + +Note that @code{proof-script-next-entity-regexps} is set to a default value +from @code{proof-goal-with-hole-regexp} and @code{proof-save-with-hole-regexp} in +the function @code{proof-config-done}, so you may not need to worry about any +of this. See whether function menu does something sensible by +default. +@end defvar + +@node Configuring undo behaviour +@section Configuring undo behaviour + +The settings here are used to configure the way "undo" commands are +calculated. + +@c TEXI DOCSTRING MAGIC: proof-non-undoables-regexp +@defvar proof-non-undoables-regexp +Regular expression matching commands which are @strong{not} undoable.@* +Used in default functions @samp{@code{proof-generic-state-preserving-p}} +and @samp{@code{proof-generic-count-undos}}. If you don't use those, +may be left as nil. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-ignore-for-undo-count +@defvar proof-ignore-for-undo-count +Matcher for script commands to be ignored in undo count.@* +May be left as nil, in which case it will be set to +@samp{@code{proof-non-undoables-regexp}}. +Used in default function @samp{@code{proof-generic-count-undos}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-count-undos-fn +@defvar proof-count-undos-fn +Function to calculate a command to issue undos to reach a target span.@* +The function takes a span as an argument, and should return a string +which is the command to undo to the target span. The target is +guaranteed to be within the current (open) proof. +This is an important function for script management. +The default setting @samp{@code{proof-generic-count-undos}} is based on the +settings @samp{@code{proof-non-undoables-regexp}} and +@samp{@code{proof-non-undoables-regexp}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-generic-count-undos +@defun proof-generic-count-undos span +Count number of undos in a span, return command needed to undo that far.@* +Command is set using @samp{@code{proof-undo-n-times-cmd}}. + +A default value for @samp{@code{proof-count-undos-fn}}. + +For this function to work properly, you must configure +@samp{@code{proof-undo-n-times-cmd}} and @samp{@code{proof-ignore-for-undo-count}}. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-find-and-forget-fn +@defvar proof-find-and-forget-fn +Function that returns a command to forget back to before its argument span.@* +This setting is used to for retraction (undoing) in proof scripts. + +It should undo the effect of all settings between its target span +up to (@code{proof-locked-end}). This may involve forgetting a number +of definitions, declarations, or whatever. + +The special string @code{proof-no-command} means there is nothing to do. + +Important: the generic implementation @samp{@code{proof-generic-find-and-forget}} +does nothing, it always returns @samp{@code{proof-no-command}}. + +This is an important function for script management. +Study one of the existing instantiations for examples of how to write it, +or leave it set to the default function @samp{@code{proof-generic-find-and-forget}} +(which see). +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-generic-find-and-forget +@defun proof-generic-find-and-forget span +Calculate a forget/undo command to forget back to @var{span}.@* +This is a long-range forget: we know that there is no +open goal at the moment, so forgetting involves unbinding +declarations, etc, rather than undoing proof steps. + +Currently this has a trivial implementation: it +just returns @code{proof-no-command}, meaning @samp{do nothing}. + +Check the @code{lego-find-and-forget} or @code{coq-find-and-forget} +functions for examples of how to write this function. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-goal-hyp-fn +@defvar proof-goal-hyp-fn +Function which returns cons cell if point is at a goal/hypothesis.@* +This is used to parse the proofstate output to mark it up for +proof-by-pointing. It should return a cons or nil. First element of +the cons is a symbol, @code{'goal'} or @code{'hyp'}. The second element is a +string: the goal or hypothesis itself. + +If you leave this variable unset, no proof-by-pointing markup +will be attempted. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-kill-goal-command +@defvar proof-kill-goal-command +Command to kill the currently open goal.@* +You must set this (perhaps to a no-op) for script management to work. +@end defvar + + +@node Nested proofs +@section Nested proofs + +Proof General doesn't yet have a flexible understanding of +nested proofs, but can do something with them. + +@c TEXI DOCSTRING MAGIC: proof-global-p +@defvar proof-global-p +Whether a command is a global declaration. Predicate on strings or nil.@* +This is used to handle nested goals allowed by some provers, by +recognizing global declarations as candidates for rearranging the +proof script. + +May be left as nil to disable this function. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-lift-global +@defvar proof-lift-global +Function which lifts local lemmas from inside goals out to top level.@* +This function takes the local goalsave span as an argument. Leave this +set this at @samp{nil} if the proof assistant does not support nested goals, +or if you don't want to write a function to do move them around. +@end defvar + + +@node Safe (state-preserving) commands +@section Safe (state-preserving) commands + +A proof command is "safe" if it can be issued away from the proof +script. For this to work it should be state-preserving in the proof +assistant. + +@c TEXI DOCSTRING MAGIC: proof-state-preserving-p +@defvar proof-state-preserving-p +A predicate, non-nil if its argument (a command) preserves the proof state.@* +If set, used by @code{proof-minibuffer-cmd} to filter out scripting +commands which should be entered directly into the script itself. + +The default setting for this function, @samp{@code{proof-generic-state-preserving-p}} +tests by negating the match on @samp{@code{proof-non-undoables-regexp}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-generic-state-preserving-p +@defun proof-generic-state-preserving-p cmd +Is @var{cmd} state preserving? Match on @code{proof-non-undoables-regexp}. +@end defun + + +@node Activate scripting hook +@section Activate scripting hook + + +@c TEXI DOCSTRING MAGIC: proof-activate-scripting-hook +@defvar proof-activate-scripting-hook +Hook run when a buffer is switched into scripting mode.@* +The current buffer will be the newly active scripting buffer. + +This hook may be useful for synchronizing with the proof +assistant, for example, to switch to a new theory +(in case that isn't already done by commands in the proof +script). + +When functions in this hook are called, the variable +@samp{activated-interactively} will be non-nil if +@code{proof-activate-scripting} was called interactively +(rather than as a side-effect of some other action). +If a hook function sends commands to the proof process, +it should wait for them to complete (so the queue is cleared +for scripting commands), unless activated-interactively is set. +@end defvar + + +@node Automatic multiple files +@section Automatic multiple files + +@xref{Handling multiple files}, for more details about this +setting. + +@c TEXI DOCSTRING MAGIC: proof-auto-multiple-files +@defvar proof-auto-multiple-files +Whether to use automatic multiple file management.@* +If non-nil, Proof General will automatically retract a script file +whenever another one is retracted which it depends on. It assumes +a simple linear dependency between files in the order which +they were processed. + +If your proof assistant has no management of file dependencies, or one +which depends on a simple linear context, you may be able to use this +setting to good effect. If the proof assistant has more complex +file dependencies then you should configure it to communicate with +Proof General about the dependencies rather than using this setting. +@end defvar + + +@node Completions +@section Completions + +Proof General allows provers to create a @i{completion table} to help +writing identifiers in proof scripts. This is documented in the main +@i{Proof General} user manual but summarized here for +(a different kind of) completion. + +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. Completion is usually a hand-wavy thing, so we don't +make any attempt to maintain a precise completion table or anything. + +The completion table maintained by @file{complete.el} is initialized +from @code{PA-completion-table} when @file{proof-script.el} is loaded. +This is done with the function @code{proof-add-completions} which +you may want to call at other times. + + +@c TEXI DOCSTRING MAGIC: PA-completion-table +@defvar PA-completion-table +List of identifiers to use for completion for this proof assistant.@* +Completion is activated with C-return. + +If this table is empty or needs adjusting, please make changes using +@samp{@code{customize-variable}} and send suggestions to proofgen@@dcs.ed.ac.uk. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-add-completions +@deffn Command proof-add-completions +Add completions from <PA>-completion-table to completion database.@* +Uses @samp{@code{add-completion}} with a negative number of uses and ancient +last use time, to discourage saving these into the users database. +@end deffn + + + + + + +@node Proof shell settings +@chapter Proof shell settings + +The variables in this chapter concern the proof shell mode, and are the +largest group. They are split into several subgroups. The first +subgroup are commands invoked at various points. The second subgroup of +variables are concerned with matching the output from the proof +assistant. The final subgroup contains various hooks which you can set +to add lisp customization to Proof General in various points (some of +them are also used internally for behaviour you may wish to adjust). + +Variables for configuring the proof shell are put into the customize +group @code{proof-shell}. + +These should be set in the shell mode configuration, before +@code{proof-shell-config-done} is called. + +To understand the way the proof assistant runs inside Emacs, you may +want to refer to the @code{comint.el} (Command interpreter) package +distributed with Emacs. This package controls several shell-like modes +available in Emacs, including the @code{proof-shell-mode} and +all specific shell modes derived from it. + +@menu +* Proof shell commands:: +* Script input to the shell:: +* Settings for matching various output from proof process:: +* Settings for matching urgent messages from proof process:: +* Hooks and other settings:: +@end menu + +@node Proof shell commands +@section Commands + +Settings in this section configure Proof General with commands +to send to the prover to activate certain actions. + +@c TEXI DOCSTRING MAGIC: proof-prog-name +@defvar proof-prog-name +System command to run the proof assistant in the proof shell.@* +Suggestion: this can be set in @code{proof-pre-shell-start-hook} from +a variable which is in the proof assistant's customization +group. This allows different proof assistants to coexist +(albeit in separate Emacs sessions). +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-auto-terminate-commands + +@defvar proof-shell-auto-terminate-commands +Non-nil if Proof General should try to add terminator to every command.@* +If non-nil, whenever a command is sent to the prover using +@samp{@code{proof-shell-invisible-command}}, Proof General will check to see if it +ends with @code{proof-terminal-char}, and add it if not. +If @code{proof-terminal-char} is nil, this has no effect. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-pre-sync-init-cmd +@defvar proof-shell-pre-sync-init-cmd +The command for configuring the proof process to gain synchronization.@* +This command is sent before Proof General's synchronization +mechanism is engaged, to allow customization inside the process +to help gain syncrhonization (e.g. engaging special markup). + +It is better to configure the proof assistant for this purpose +via command line options if possible, in which case this variable +does not need to be set. + +See also @samp{@code{proof-shell-init-cmd}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-init-cmd +@defvar proof-shell-init-cmd +The command for initially configuring the proof process.@* +This command is sent to the process as soon as syncrhonization is gained +(when an annotated prompt is first recognized). It can be used to configure +the proof assistant in some way, or print a welcome message +(since output before the first prompt is discarded). + +See also @samp{@code{proof-shell-pre-sync-init-cmd}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-restart-cmd +@defvar proof-shell-restart-cmd +A command for re-initialising the proof process. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-quit-cmd +@defvar proof-shell-quit-cmd +A command to quit the proof process. If nil, send EOF instead. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-quit-timeout +@defvar proof-shell-quit-timeout +The number of seconds to wait after sending @code{proof-shell-quit-cmd}.@* +After this timeout, the proof shell will be killed off more rudely. +If your proof assistant takes a long time to clean up (for +example writing persistent databases out or the like), you may +need to bump up this value. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-cd-cmd +@defvar proof-shell-cd-cmd +Command to the proof assistant to change the working directory.@* +The format character @samp{%s} is replaced with the directory, and +the escape sequences in @samp{@code{proof-shell-filename-escapes}} are +applied to the filename. + +This setting is used to define the function @code{proof-cd} which +changes to the value of (@code{default-directory}) for script buffers. +For files, the value of (@code{default-directory}) is simply the +directory the file resides in. + +NB: By default, @code{proof-cd} is called from @code{proof-activate-scripting-hook}, +so that the prover switches to the directory of a proof +script every time scripting begins. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-start-silent-cmd +@defvar proof-shell-start-silent-cmd +Command to turn prover goals output off when sending many script commands.@* +If non-nil, Proof General will automatically issue this command +to help speed up processing of long proof scripts. +See also @code{proof-shell-stop-silent-cmd}. +NB: terminator not added to command. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-stop-silent-cmd +@defvar proof-shell-stop-silent-cmd +Command to turn prover output off. @* +If non-nil, Proof General will automatically issue this command +to help speed up processing of long proof scripts. +See also @code{proof-shell-start-silent-cmd}. +NB: Terminator not added to command. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-silent-threshold +@defvar proof-shell-silent-threshold +Number of waiting commands in the proof queue needed to trigger silent mode.@* +Default is 2, but you can raise this in case switching silent mode +on or off is particularly expensive (or make it ridiculously large +to disable silent mode altogether). +@end defvar +@xref{Handling multiple files}, +for more details about the final two settings in this group, + + +@c TEXI DOCSTRING MAGIC: proof-shell-inform-file-processed-cmd +@defvar proof-shell-inform-file-processed-cmd +Command to the proof assistant to tell it that a file has been processed.@* +The format character @samp{%s} is replaced by a complete filename for a +script file which has been fully processed interactively with +Proof General. See @samp{@code{proof-format-filename}} for other possibilities +to process the filename. + +This setting used to interface with the proof assistant's internal +management of multiple files, so the proof assistant is kept aware of +which files have been processed. Specifically, when scripting +is deactivated in a completed buffer, it is added to Proof General's +list of processed files, and the prover is told about it by +issuing this command. + +If this is set to nil, no command is issued. + +See also: @code{proof-shell-inform-file-retracted-cmd}, +@code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-inform-file-retracted-cmd +@defvar proof-shell-inform-file-retracted-cmd +Command to the proof assistant to tell it that a file has been retracted.@* +The format character @samp{%s} is replaced by a complete filename for a +script file which Proof General wants the prover to consider as not +completely processed. See @samp{@code{proof-format-filename}} for other +possibilities to process the filename. + +This is used to interface with the proof assistant's internal +management of multiple files, so the proof assistant is kept aware of +which files have been processed. Specifically, when scripting +is activated, the file is removed from Proof General's list of +processed files, and the prover is told about it by issuing this +command. The action may cause the prover in turn to suggest to +Proof General that files depending on this one are +also unlocked. + +If this is set to nil, no command is issued. + +See also: @code{proof-shell-inform-file-processed-cmd}, +@code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}. +@end defvar + + +@node Script input to the shell +@section Script input to the shell + +Generally, commands from the proof script are sent verbatim to the proof +process running in the proof shell. For historical reasons, carriage +returns are stripped by default. You can set +@code{proof-shell-strip-crs-from-input} to adjust that. For more +sophisticated pre-processing of the sent string, you may like to set +@code{proof-shell-insert-hook}. + +@c TEXI DOCSTRING MAGIC: proof-shell-strip-crs-from-input +@defvar proof-shell-strip-crs-from-input +If non-nil, replace carriage returns in every input with spaces.@* +This is enabled by default: it is appropriate for some systems +because several CR's can result in several prompts, which may mess +up the display (or even worse, the synchronization). +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-insert-hook +@defvar proof-shell-insert-hook +Hooks run by @code{proof-shell-insert} before inserting a command.@* +Can be used to configure the proof assistant to the interface in +various ways -- for example, to observe or alter the commands sent to +the prover, or to sneak in extra commands to configure the prover. + +This hook is called inside a @code{save-excursion} with the @code{proof-shell-buffer} +current, just before inserting and sending the text in the +variable @samp{string}. The hook can massage @samp{string} or insert additional +text directly into the @code{proof-shell-buffer}. +Before sending @samp{string}, it will be stripped of carriage returns. + +Additionally, the hook can examine the variable @samp{action}. It will be +a symbol, set to the callback command which is executed in the proof +shell filter once @samp{string} has been processed. The @samp{action} variable +suggests what class of command is about to be inserted: +@lisp + @code{'proof-done-invisible} A non-scripting command + @code{'proof-done-advancing} A "forward" scripting command + @code{'proof-done-retracting} A "backward" scripting command +@end lisp +Caveats: You should be very careful about setting this hook. Proof +General relies on a careful synchronization with the process between +inputs and outputs. It expects to see a prompt for each input it +sends from the queue. If you add extra input here and it causes more +prompts than expected, things will break! Extending the variable +@samp{string} may be safer than inserting text directly, since it is +stripped of carriage returns before being sent. + +Example uses: +@var{lego} uses this hook for setting the pretty printer width if +the window width has changed; +Plastic uses it to remove literate-style markup from @samp{string}. +The x-symbol support uses this hook to convert special characters +into tokens for the proof assistant. +@end defvar + + + + + + +@node Settings for matching various output from proof process +@section Settings for matching various output from proof process + + +@c TEXI DOCSTRING MAGIC: proof-shell-wakeup-char +@defvar proof-shell-wakeup-char +A special character which terminates an annotated prompt.@* +Set to nil if proof assistant does not support annotated prompts. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-first-special-char +@defvar proof-shell-first-special-char +First special character.@* +Codes above this character can have special meaning to Proof General, +and are stripped from the prover's output strings. +Leave unset if no special characters are being used. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-prompt-pattern +@defvar proof-shell-prompt-pattern +Proof shell's value for comint-prompt-pattern, which see.@* +This pattern is just for interaction in comint (shell buffer). +You don't really need to set it. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-annotated-prompt-regexp +@defvar proof-shell-annotated-prompt-regexp +Regexp matching a (possibly annotated) prompt pattern.@* +Output is grabbed between pairs of lines matching this regexp. +To help matching you may be able to annotate the proof assistant +prompt with a special character not appearing in ordinary output. +The special character should appear in this regexp, and should +be the value of @code{proof-shell-wakeup-char}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-abort-goal-regexp +@defvar proof-shell-abort-goal-regexp +Regexp matching output from an aborted proof. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-error-regexp +@defvar proof-shell-error-regexp +Regexp matching an error report from the proof assistant. + +We assume that an error message corresponds to a failure in the last +proof command executed. So don't match mere warning messages with +this regexp. Moreover, an error message should not be matched as an +eager annotation (see @code{proof-shell-eager-annotation-start}) otherwise it +will be lost. + +Error messages are considered to begin from @code{proof-shell-error-regexp} +and continue until the next prompt. + +The engine matches interrupts before errors, see @code{proof-shell-interrupt-regexp}. + +It is safe to leave this variable unset (as nil). +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-interrupt-regexp +@defvar proof-shell-interrupt-regexp +Regexp matching output indicating the assistant was interrupted.@* +We assume that an interrupt message corresponds to a failure in the last +proof command executed. So don't match mere warning messages with +this regexp. Moreover, an interrupt message should not be matched as an +eager annotation (see @code{proof-shell-eager-annotation-start}) otherwise it +will be lost. + +The engine matches interrupts before errors, see @code{proof-shell-error-regexp}. + +It is safe to leave this variable unset (as nil). +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-proof-completed-regexp +@defvar proof-shell-proof-completed-regexp +Regexp matching output indicating a finished proof. + +When output which matches this regexp is seen, we clear the goals +buffer in case this is not also marked up as a @samp{goals} type of +message. + +We also enable the QED function (save a proof) and will automatically +close off the proof region if another goal appears before a save +command. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-start-goals-regexp +@defvar proof-shell-start-goals-regexp +Regexp matching the start of the proof state output.@* +This is an important setting. Output between @samp{@code{proof-shell-start-goals-regexp}} +and @samp{@code{proof-shell-end-goals-regexp}} will be pasted into the goals buffer +and possibly analysed further for proof-by-pointing markup. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-end-goals-regexp +@defvar proof-shell-end-goals-regexp +Regexp matching the end of the proof state output, or nil.@* +If nil, just use the rest of the output following @code{proof-shell-start-goals-regexp}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-assumption-regexp +@defvar proof-shell-assumption-regexp +A regular expression matching the name of assumptions. + +At the moment, this setting is not used in the generic Proof General. + +In the future it will be used for a generic implementation for @samp{@code{proof-goal-hyp-fn}}, +used to help parse the goals buffer to annotate it for proof by pointing. +@end defvar + + + +@node Settings for matching urgent messages from proof process +@section Settings for matching urgent messages from proof process + +Among the various dialogue messages that the proof assistant outputs +during proof, Proof General can consider certain messages to be +"urgent". When processing many lines of a proof, Proof General will +normally supress the output, waiting until the final message appears +before displaying anything to the user. Urgent messages escape this: +typically they include messages that the prover wants the user to +notice, for example, perhaps, file loading messages, or timing +statistics. + +So that Proof General notices, these urgent messages should be marked-up +with "eager" annotations. + +@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-start +@defvar proof-shell-eager-annotation-start +Eager annotation field start. A regular expression or nil.@* +An eager annotation indicates to Proof General that some following output +should be displayed (or processed) immediately and not accumulated for +parsing later. + +It is nice to recognize (starts of) warnings or file-reading messages +with this regexp. You must also recognize any special messages +from the prover to PG with this regexp (e.g. @samp{@code{proof-shell-clear-goals-regexp}}, +@samp{@code{proof-shell-retract-files-regexp}}, etc.) + +See also @samp{@code{proof-shell-eager-annotation-start-length}}, +@samp{@code{proof-shell-eager-annotation-end}}. + +Set to nil to disable this feature. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-start-length + +@defvar proof-shell-eager-annotation-start-length +Maximum length of an eager annotation start. @* +Must be set to the maximum length of the text that may match +@samp{@code{proof-shell-eager-annotation-start}} (at least 1). +If this value is too low, eager annotations may be lost! + +This value is used internally by Proof General to optimize the process +filter to avoid unnecessary searching. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-end +@defvar proof-shell-eager-annotation-end +Eager annotation field end. A regular expression or nil.@* +An eager annotation indicates to Emacs that some following output +should be displayed or processed immediately. + +See also @samp{@code{proof-shell-eager-annotation-start}}. + +It is nice to recognize (ends of) warnings or file-reading messages +with this regexp. You must also recognize (ends of) any special messages +from the prover to PG with this regexp (e.g. @samp{@code{proof-shell-clear-goals-regexp}}, +@samp{@code{proof-shell-retract-files-regexp}}, etc.) + +The default value is "\n" to match up to the end of the line. +@end defvar + + +The default action for urgent messages is to display them in the +response buffer, highlighted. But we also allow for some control +messages, issued from the proof assistant to Proof General and not +intended for the user to see. These are recognized in the same way as +urgent messages (marked with eager annotations), so they will +be acted on as soon as they are issued by the prover. + + +@c TEXI DOCSTRING MAGIC: proof-shell-clear-response-regexp +@defvar proof-shell-clear-response-regexp +Regexp matching output telling Proof General to clear the response buffer.@* +This feature is useful to give the prover more control over what output +is shown to the user. Set to nil to disable. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-clear-goals-regexp +@defvar proof-shell-clear-goals-regexp +Regexp matching output telling Proof General to clear the goals buffer.@* +This feature is useful to give the prover more control over what output +is shown to the user. Set to nil to disable. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-set-elisp-variable-regexp +@defvar proof-shell-set-elisp-variable-regexp +Regexp matching output telling Proof General to set some variable.@* +This allows the proof assistant to configure Proof General directly +and dynamically. + +If the regexp matches output from the proof assistant, there should be +two match strings: (@code{match-string} 1) should be the name of the elisp +variable to be set, and (@code{match-string} 2) should be the value of the +variable (which will be evaluated as a lisp expression). + +A good markup for the second string is to delimit with #'s, since +these are not valid syntax for elisp evaluation. + +Elisp errors will be trapped when evaluating; set +@code{proof-show-debug-messages} to be informed when this happens. + +Example uses are to adjust PG's internal copies of proof assistant's +settings, or to make automatic dynamic syntax adjustments in Emacs to +match changes in theory, etc. + +If you pick a dummy variable name (e.g. @samp{proof-dummy-setting}) you +can just evaluation arbitrary elisp expressions for their side +effects, to adjust menu entries, or even launch auxiliary programs. +But use with care -- there is no protection against catastrophic elisp! + +This setting could also be used to move some configuration settings +from PG to the prover, but this is not really supported (most settings +must be made before this mechanism will work). In future, the PG +standard protocol, @var{pgip}, will use this mechanism for making all +settings. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-theorem-dependency-list-regexp +@defvar proof-shell-theorem-dependency-list-regexp +Regexp matching output telling Proof General what the dependencies are. @* +This is so that the dependent theorems can be highlighted somehow. +Set to nil to disable. +This is an experimental feature, currently work-in-progress. +@end defvar + +Two important control messages are recognized by +@code{proof-shell-process-file} and +@code{proof-shell-retract-files-regexp}, used for synchronizing Proof +General with a file loading mechanism built into the proof assistant. +@xref{Handling multiple files}, for more details about how to use the +final three settings described here. + +@vindex proof-included-files-list +@c TEXI DOCSTRING MAGIC: proof-shell-process-file +@defvar proof-shell-process-file +A pair (@var{regexp} . @var{function}) to match a processed file name. + +If @var{regexp} matches output, then the function @var{function} is invoked on the +output string chunk. It must return the name of a script file (with +complete path) that the system has successfully processed. In +practice, @var{function} is likely to inspect the match data. If it returns +the empty string, the file name of the scripting buffer is used +instead. If it returns nil, no action is taken. + +Care has to be taken in case the prover only reports on compiled +versions of files it is processing. In this case, @var{function} needs to +reconstruct the corresponding script file name. The new (true) file +name is added to the front of @samp{@code{proof-included-files-list}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-retract-files-regexp +@defvar proof-shell-retract-files-regexp +Matches a message that the prover has retracted a file. + +At this stage, Proof General's view of the processed files is out of +date and needs to be updated with the help of the function +@samp{@code{proof-shell-compute-new-files-list}}. +@end defvar +@vindex proof-included-files-list + +@c TEXI DOCSTRING MAGIC: proof-shell-compute-new-files-list +@defvar proof-shell-compute-new-files-list +Function to update @samp{proof-included-files list}. + +It needs to return an up to date list of all processed files. Its +output is stored in @samp{@code{proof-included-files-list}}. Its input is the +string of which @samp{@code{proof-shell-retract-files-regexp}} matched a +substring. In practice, this function is likely to inspect the +previous (global) variable @samp{@code{proof-included-files-list}} and the match +data triggered by @samp{@code{proof-shell-retract-files-regexp}}. +@end defvar + + + +@node Hooks and other settings +@section Hooks and other settings + +@c TEXI DOCSTRING MAGIC: proof-shell-filename-escapes +@defvar proof-shell-filename-escapes +A list of escapes that are applied to %s for filenames.@* +A list of cons cells, car of which is string to be replaced +by the cdr. +For example, when directories are sent to Isabelle, HOL, and Coq, +they appear inside ML strings and the backslash character and +quote characters must be escaped. The setting +@lisp + '(("@var{\\\\}" . "@var{\\\\}") + ("\"" . "\\\"")) +@end lisp +achieves this. This does not apply to @var{lego}, which does not +need backslash escapes and does not allow filenames with +quote characters. + +This setting is used inside the function @samp{@code{proof-format-filename}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-process-connection-type +@defvar proof-shell-process-connection-type +The value of @code{process-connection-type} for the proof shell.@* +Set non-nil for ptys, nil for pipes. +The default (and preferred) option is to use pty communication. +However there is a long-standing backslash/long line problem with +Solaris which gives a mess of ^G characters when some input is sent +which has a in the 256th position. +So we select pipes by default if it seems like we're on Solaris. +We do not force pipes everywhere because this risks loss of data. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-pre-shell-start-hook +@defvar proof-pre-shell-start-hook +Hooks run before proof shell is started.@* +Suggestion: set this to a function which configures just these proof +shell variables: +@lisp + @code{proof-prog-name} + @code{proof-mode-for-shell} + @code{proof-mode-for-response} + @code{proof-mode-for-goals} +@end lisp +This is the bare minimum needed to get a shell buffer and +its friends configured in the function @code{proof-shell-start}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-handle-error-or-interrupt-hook +@defvar proof-shell-handle-error-or-interrupt-hook +Run after an error or interrupt has been reported in the response buffer.@* +Hook functions may inspect @samp{@code{proof-shell-error-or-interrupt-seen}} to +determine whether the cause was an error or interrupt. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-pre-interrupt-hook +@defvar proof-shell-pre-interrupt-hook +Run immediately after @samp{@code{comint-interrupt-subjob}} is called.@* +This hook is added to allow customization for Poly/ML and other +systems where the system queries the user before returning to +the top level. For Poly/ML it can be used to send the string "f", +for example. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-process-output-system-specific +@defvar proof-shell-process-output-system-specific +Set this variable to handle system specific output.@* +Errors, start of proofs, abortions of proofs and completions of +proofs are recognised in the function @samp{@code{proof-shell-process-output}}. +All other output from the proof engine is simply reported to the +user in the @var{response} buffer. + +To catch further special cases, set this variable to a pair of +functions '(condf . actf). Both are given (cmd string) as arguments. +@samp{cmd} is a string containing the currently processed command. +@samp{string} is the response from the proof system. To change the +behaviour of @samp{@code{proof-shell-process-output}}, (condf cmd string) must +return a non-nil value. Then (actf cmd string) is invoked. + +See the documentation of @samp{@code{proof-shell-process-output}} for the required +output format. +@end defvar + + + + + +@node Goals buffer settings +@chapter Goals buffer settings + +The goals buffer settings allow configuration of Proof General for proof +by pointing or similar features. +@c At the moment these settings are disabled. + +@c TEXI DOCSTRING MAGIC: pbp-change-goal +@defvar pbp-change-goal +Command to change to the goal @samp{%s} +@end defvar +@c TEXI DOCSTRING MAGIC: pbp-goal-command +@defvar pbp-goal-command +Command informing the prover that @samp{@code{pbp-button-action}} has been@* +requested on a goal. +@end defvar +@c TEXI DOCSTRING MAGIC: pbp-hyp-command +@defvar pbp-hyp-command +Command informing the prover that @samp{@code{pbp-button-action}} has been@* +requested on an assumption. +@end defvar +@c TEXI DOCSTRING MAGIC: pbp-error-regexp +@defvar pbp-error-regexp +Regexp indicating that the proof process has identified an error. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-result-start +@defvar proof-shell-result-start +Regexp matching start of an output from the prover after pbp commands.@* +In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-result-end +@defvar proof-shell-result-end +Regexp matching end of output from the prover after pbp commands.@* +In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-start-char +@defvar proof-shell-start-char +Starting special for a subterm markup.@* +Subsequent characters with values @strong{below} @code{proof-shell-first-special-char} +are assumed to be subterm position indicators. Subterm markups should +be finished with @code{proof-shell-end-char}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-end-char +@defvar proof-shell-end-char +Finishing special for a subterm markup.@* +See documentation of @code{proof-shell-start-char}. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-goal-char +@defvar proof-shell-goal-char +Mark for goal. + +This setting is also used to see if proof-by-pointing features +are configured. If it is unset, some of the code +for parsing the is disabled. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-field-char +@defvar proof-shell-field-char +Annotated field end +@end defvar + + +@node Splash screen settings +@chapter Splash screen settings + +The splash screen can be configured, in a rather limited way. + +@c TEXI DOCSTRING MAGIC: proof-splash-time +@defvar proof-splash-time +Minimum number of seconds to display splash screen for.@* +The splash screen may be displayed for a couple of seconds longer than +this, depending on how long it takes the machine to initialise +Proof General. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-splash-contents +@defvar proof-splash-contents +Evaluated to configure splash screen displayed when entering Proof General.@* +A list of the screen contents. If an element is a string or an image +specifier, it is displayed centred on the window on its own line. +If it is nil, a new line is inserted. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-splash-extensions +@defvar proof-splash-extensions +Prover specific extensions of splash screen.@* +These are evaluated and appended to @samp{@code{proof-splash-contents}}. +@end defvar + + + + + + +@node Global constants +@chapter Global constants + +The settings here are internal constants used by Proof General. +You don't need to configure these for your proof assistant +unless you want to modify or extend the defaults. + +@c TEXI DOCSTRING MAGIC: proof-general-name +@defvar proof-general-name +Proof General name used internally and in menu titles. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-general-home-page +@defopt proof-general-home-page +Web address for Proof General + +The default value is @code{"http://www.proofgeneral.org"}. +@end defopt +@c TEXI DOCSTRING MAGIC: proof-universal-keys +@defvar proof-universal-keys +List of key-bindings made for the script, goals and response buffer. @* +Elements of the list are tuples @samp{(k . f)} +where @samp{k} is a @code{key-binding} (vector) and @samp{f} the designated function. +@end defvar + + + +@node Handling multiple files +@chapter Handling multiple files +@cindex Multiple files + +Large proof developments are typically spread across multiple files. +Many provers support such developments by keeping track of dependencies +and automatically processing scripts. Proof General supports this +mechanism. The user's point of view is considered in the user manual. +Here, we describe the more technical nitty gritty. This is what you +need to know when you customise another proof assistant to work with +Proof General. + +Documentation for the configuration settings mentioned here appears in +the previous sections, this section is intended to help explain the use +of those settings. + +Proof General maintains a list @code{proof-included-files-list} of files +which it thinks have been processed by the proof assistant. When a file +which is on this list is visited in Emacs, it will be coloured entirely +blue to indicate that it has been processed. No editing of the file +will be allowed (unless @code{proof-strict-read-only} allows it). + + +@c TEXI DOCSTRING MAGIC: proof-included-files-list +@defvar proof-included-files-list +List of files currently included in proof process.@* +This list contains files in canonical truename format +(see @samp{@code{file-truename}}). + +Whenever a new file is being processed, it gets added to this list +via the @code{proof-shell-process-file} configuration settings. +When the prover retracts a file, this list is resynchronised via the +@code{proof-shell-retract-files-regexp} and @code{proof-shell-compute-new-files-list} +configuration settings. + +Only files which have been @strong{fully} processed should be included here. +Proof General itself will automatically add the filenames of a script +buffer which has been completely read when scripting is deactivated. +It will automatically remove the filename of a script buffer which +is completely unread when scripting is deactivated. + +NB: Currently there is no generic provision for removing files which +are only partly read-in due to an error, so ideally the proof assistant +should only output a processed message when a file has been successfully +read. +@end defvar + +The way that @code{proof-included-files-list} is maintained is the key +to multiple file management. (But you should not set this variable +directly, it is managed via the configuration settings). + +@vindex proof-shell-process-file +@vindex proof-shell-retract-files-regexp +@vindex proof-shell-compute-new-files-list + +There is a range of strategies for managing multiple files. Ideally, +file dependencies should be managed by the proof assistant. Proof +General will use the prover's low-level commands to process a whole file +and its requirements non-interactively, without going through script +management. So that the user knows which files have been processed, the +proof assistant should issue messages which Proof General can recognize +(``file @code{foo} has been processed'') --- see +@code{proof-shell-process-file}. When the user wants to edit a file +which has been processed, the file must be retracted (unlocked). The +proof assistant should provide a command corresponding to this action, +which undoes a given file and all its dependencies. As each file is +undone, a message should be issued which Proof General can recognize +(``file @code{foo} has been undone'') -- see +@code{proof-shell-retract-files-regexp}. (The function +@code{proof-shell-compute-new-files-list} should be set to calculate the +new value for @code{proof-included-files-list} after a retract message +has been seen). + + +@c The key idea is that we leave it to the specific proof assistant to +@c worry about managing multiple files, as far as possible. Whenever the +@c proof assistant processes or retracts a file it must clearly say so, so +@c that Proof General can register this. + +As well as this communication from the assistant to Proof General about +processed or retracted files, Proof General can communicate the other +way: it will tell the proof assistant when it has processed or retracted +a file via script management. This is because during script management, +the proof assistant may not be aware that it is actually dealing with a +file of proof commands (rather than just terminal input). + +Proof General will provide this information in two special instances. +First, when scripting is turned off in a file that has been completely +processed, Proof General will tell the proof assistant using +@code{proof-shell-inform-file-processed-cmd}. Second, when scripting is +turned on in a file which is completely processed, Proof General will +tell the proof assistant to reconsider: the file should not be +considered completely processed yet. This uses the setting +@code{proof-shell-inform-file-retracted-cmd}. This second case might +lead to a series of messages from the prover telling Proof General to +unlock files which depend on the present one, again via +@code{proof-shell-retract-files-regexp}. + +What we have described so far is the ideal case, but it may require some +support from the proof assistant to set up (for example, if file-level +undo is not normally supported, or the messages during file processing +are not suitable). Moreover, some proof assistants may not have file +handling with dependencies, or may have a particularly simple case of a +linear context: each file depends on all the ones processed before it. +Proof General allows you a shortcut to get automatic management of +multiple files in these cases by setting the flag +@code{proof-auto-multiple-files}. This setting is probably an +approximation to the right thing for any proof assistant. More files +than necessary will be retracted if the prover has a tree-like file +dependency rather than a linear one. + +@vindex proof-shell-eager-annotation-start +@vindex proof-shell-eager-annotation-end +Finally, we should mention how Proof General recognizes file processing +messages from the proof assistant. Proof General considers @var{output} +delimited by the the two regular expressions +@code{proof-shell-eager-annotation-start} and +@code{proof-shell-eager-annotation-end} as being important. It displays +the @var{output} in the Response buffer and analyses the contents +further. Among other important messages characterised by these regular +expressions (warnings, errors, or information), the prover can tell the +interface whenever it processes or retracts a file. + + +To summarize, the settings for multiple file management that may be +customized are as follows. To recognize file-processing, +@code{proof-shell-process-file}. To recognize messages about file +undoing, @code{proof-shell-retract-files-regexp} and +@code{proof-shell-compute-new-files-list}. @xref{Settings for matching +urgent messages from proof process}. To tell the prover about files +handled with script management, use + @code{proof-shell-inform-file-processed-cmd} and + @code{proof-shell-inform-file-retracted-cmd}. @xref{Proof shell + commands}. Finally, set the flag @code{proof-auto-multiple-files} +for a automatic approximation to multiple file handling. +@xref{Proof script settings}. + + +@node Configuring Font Lock +@chapter Configuring Font Lock +@cindex font lock + +Support for Font Lock in Proof General is described in the user manual +(see the @i{Syntax highlighting} section). To configure Font Lock for a +new proof assistant, you need to set the variable +@code{font-lock-keywords} in each of the mode functions you want +highlighting for. Proof General will automatically install these +settings, and enable Font Lock minor mode (for syntax highlighting as +you type) in script buffers. + +@c nope: too big. TEXI DOCSTRING MAGIC: font-lock-keywords +To understand its format, check the documentation of +@code{font-lock-keywords} inside Emacs. + +Proof General has a special hack for simplifying font lock settings +@code{proof-font-lock-zap-commas}, but it is recommended to restrict to +using the @code{font-lock-keywords} setting if possible. + + +@c TEXI DOCSTRING MAGIC: proof-font-lock-zap-commas +@defvar proof-font-lock-zap-commas +If non-nil, enable a font-lock hack which unfontifies commas.@* +If you fontify variables inside lists like [a,b,c] by matching +on the brackets @samp{[} and @samp{]}, you may take objection to the commas +being coloured as well. In that case, enable this hack which +will magically restore the commas to the default font for you. + +The hack is rather painful and forces immediate fontification of +files on loading (no lazy, caching locking). It is unreliable +under FSF Emacs, to boot. + +@var{lego} and Coq enable it by tradition. +@end defvar + + + + +@node Configuring X-Symbol +@chapter Configuring X-Symbol +@cindex X-Symbol + +The X-Symbol package is described in the Proof General user manual. To +configure X-Symbol for Proof General, you must understand a little bit +of how X-Symbol works: read the documentation that is supplied with it. + +The basic task is to set up a @i{token language} for your proof +assistant. If your assistant is stored in the subdirectory +@var{myprover}, the token language will be called @var{myprover} and be +defined in a file @file{x-symbol-@var{myprover}.el} which is +automatically loaded by X-Symbol. The name of the token language mode +will be @code{@var{myprover}sym}. + +Proof General will check that the file @file{x-symbol-@var{myprover}.el} +exists and set up X-Symbol to load it. The token language file must +define a number of standard settings, and X-Symbol will give warnings if +any of them are missing. + +Apart from the token language file, there are several settings for +X-Symbol which you can set in the usual configuration file +@file{@var{myprover}.el}. These settings are optional. + +@c There's also proof-xsym-font-lock-keywords, but I don't +@c really know what this setting is good for. + +@c TEXI DOCSTRING MAGIC: proof-xsym-activate-command +@defvar proof-xsym-activate-command +Command to activate token input/output for X-Symbol.@* +If non-nil, this command is sent to the proof assistant when +X-Symbol support is activated. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-xsym-deactivate-command +@defvar proof-xsym-deactivate-command +Command to deactivate token input/output for X-Symbol.@* +If non-nil, this command is sent to the proof assistant when +X-Symbol support is deactivated. +@end defvar + +We expect tokens to be used uniformly, so that along with each script +mode buffer, the response buffer and goals buffer also invoke X-Symbol +to display special characters in the same token language. This happens +automatically. If you want additional modes to use X-Symbol with the +token language for your proof assistant, you can set +@code{proof-xsym-extra-modes}. + +@c TEXI DOCSTRING MAGIC: proof-xsym-extra-modes +@defvar proof-xsym-extra-modes +List of additional mode names to use X-Symbol with Proof General tokens.@* +These modes will have X-Symbol enabled for the proof assistant token language, +in addition to the four modes for Proof General (script, shell, response, pbp). + +Set this variable if you want additional modes to also display +tokens (for example, editing documentation or source code files). +@end defvar + + + +@node Writing more lisp code +@chapter Writing more lisp code + +You may want to add some extra features to your instance of Proof +General which are not supported in the generic core. To do this, you +can use the settings described above, plus a small number of fundamental +functions in Proof General which you can consider as exported in the +generic interface. Be careful using more functions than are mentioned +here because the internals of Proof General may change between versions. + +@menu +* Default values for generic settings:: +* Adding prover-specific configurations:: +* Useful variables:: +* Useful functions and macros:: +@end menu + +@node Default values for generic settings +@section Default values for generic settings + +Several generic settings are defined using @code{defpgcustom} in +@file{proof-config.el}. This introduces settings of the form +@code{<PA>-name} for each proof assistant @var{PA}. + +To set the default value for these settings in prover-specific cases, +you should use the special @code{defpgdefault} macro: + +@c TEXI DOCSTRING MAGIC: defpgdefault +@deffn Macro defpgdefault +Set default for the proof assistant specific variable <PA>@var{-sym} to @var{value}.@* +This should be used in prover-specific code to alter the default values +for prover specific settings. + +Usage: (defpgdefault SYM @var{value}) +@end deffn + +In your prover-specific code you can simply use the setting +@code{<PA>-sym} directly, i.e., write @code{myprover-home-page}. + +In the generic code, you can use a macro, writing @code{(proof-ass +home-page)} to refer to the @code{<PA>-home-page} setting for the +currently running instance of Proof General. + +@xref{Configuration variable mechanisms}, for more details on this +mechanism. + + +@node Adding prover-specific configurations +@section Adding prover-specific configurations + +Apart from the generic settings, your prover instance will probably need +some specific customizable settings. + +Defining new prover-specific settings using customize is pretty easy. +You should do it at least for your prover-specific user options. + +The code in @file{proof-site.el} provides each prover with two +customization groups automatically (based on the name of the assistant): +@code{<PA>} for user options for prover @var{PA} +and +@code{<PA>-config} for configuration of prover @var{PA}. +Typically @code{<PA>-config} holds settings which are +constants but which may be nice to tweak. + +The first group appears in the menu +@lisp + ProofGeneral -> Customize -> <PA> +@end lisp +The second group appears in the menu: +@lisp + ProofGeneral -> Internals -> <PA> config +@end lisp + +A typical use of @code{defcustom} looks like this: +@lisp +(defcustom myprover-search-page + "http://findtheorem.myprover.org" + "URL of search web page for myprover." + :type 'string + :group 'myprover-config) +@end lisp +This introduces a new customizable setting, which you might use to make +a menu entry, for example. The default value is the string +@code{"http://findtheorem.myprover.org"}. + + + + + + +@node Useful variables +@section Useful variables + +In @file{proof-compat}, two architecture flags are defined. These can +be used to write conditional pieces of code for different Emacs and +operating systems. + + +@c TEXI DOCSTRING MAGIC: proof-running-on-XEmacs + +@defvar proof-running-on-XEmacs +Non-nil if Proof General is running on XEmacs. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-running-on-win32 + + + + +@defvar proof-running-on-win32 +Non-nil if Proof General is running on a win32 system. +@end defvar +@node Useful functions and macros +@section Useful functions and macros + +The recommended functions you may invoke are these: + +@itemize @bullet +@item Any of the interactive commands (i.e. anything you + can invoke with @kbd{M-x}, including all key-bindings) +@item Any of the internal functions and macros mentioned below +@end itemize + +To insert text into the current (usually script) buffer, the function +@code{proof-insert} is useful. There's also a handy macro +@code{proof-defshortcut} for defining shortcut functions using it. + + +@c TEXI DOCSTRING MAGIC: proof-insert +@defun proof-insert text +Insert @var{text} into the current buffer.@* +@var{text} may include these special characters: +@lisp + %p - place the point here after input +@end lisp +Any other %-prefixed character inserts itself. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-defshortcut +@deffn Macro proof-defshortcut +Define shortcut function FN to insert @var{string}, optional keydef KEY.@* +This is intended for defining proof assistant specific functions. +@var{string} is inserted using @samp{@code{proof-insert}}, which see. +KEY is added onto @code{proof-assistant} map. +@end deffn +The function @code{proof-shell-invisible-command} is a useful utility +for sending a single command to the process. You should use this to +implement user-level or internal functions rather than attempting to +directly manipulate the proof action list, or insert into the shell +buffer. + +@c TEXI DOCSTRING MAGIC: proof-shell-invisible-command +@defun proof-shell-invisible-command cmd &optional wait +Send @var{cmd} to the proof process. @* +Automatically add @code{proof-terminal-char} if necessary, examining +proof-shell-no-auto-terminate-commands. +By default, let the command be processed asynchronously. +But if optional @var{wait} command is non-nil, wait for processing to finish +before and after sending the command. +If @var{wait} is an integer, wait for that many seconds afterwards. +@end defun + +There are several handy macros to help you define functions +which invoke @code{proof-shell-invisible-command}. + +@c TEXI DOCSTRING MAGIC: proof-definvisible +@deffn Macro proof-definvisible +Define function FN to send @var{string} to proof assistant, optional keydef KEY.@* +This is intended for defining proof assistant specific functions. +@var{string} is sent using @code{proof-shell-invisible-command}, which see. +KEY is added onto @code{proof-assistant} map. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-define-assistant-command +@deffn Macro proof-define-assistant-command +Define command FN to send string @var{body} to proof assistant, based on @var{cmdvar}.@* +@var{body} defaults to @var{cmdvar}, a variable. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-define-assistant-command-witharg +@deffn Macro proof-define-assistant-command-witharg +Define command FN to prompt for string @var{cmdvar} to proof assistant.@* +@var{cmdvar} is a function or string. Automatically has history. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-format-filename + + + + + + +@defun proof-format-filename string filename +Format @var{string} by replacing quoted chars by escaped version of @var{filename}. + +%e uses the canonicalized expanded version of filename (including +directory, using @code{default-directory} -- see @samp{@code{expand-file-name}}). + +%r uses the unadjusted (possibly relative) version of @var{filename}. + +%m ('module') uses the basename of the file, without directory +or extension. + +%s means the same as %e. + +Using %e can avoid problems with dumb proof assistants who don't +understand ~, for example. + +For all these cases, the escapes in @samp{@code{proof-shell-filename-escapes}} +are processed. + +If @var{string} is in fact a function, instead invoke it on @var{filename} and +return the resulting (string) value. +@end defun +@node Internals of Proof General +@chapter Internals of Proof General + +This chapter sketches some of the internal functions and variables of +Proof General, to help developers who wish to understand or modify the +code. + +Most of the documentation below is generated automatically from the +comments in the code. Because Emacs lisp is interpreted and +self-documenting, the best way to find your way around the source is +inside Emacs once Proof General is loaded. Read the source files, and +use functions such as @kbd{C-h v} and @kbd{C-h f}. + +The code is split into files. The following sections document the +important files, kept in the @file{generic/} subdirectory. + +@menu +* Spans:: +* Configuration variable mechanisms:: +* Proof General site configuration:: +* Global variables:: +* Proof script mode:: +* Proof shell mode:: +* Debugging:: +@end menu + + + +@node Spans +@section Spans +@cindex spans +@cindex extents +@cindex overlays + +@dfn{Spans} are an abstraction of XEmacs @dfn{extents} used to help +bridge the gulf between FSF GNU Emacs and XEmacs. In FSF GNU Emacs, spans are +implemented using @dfn{overlays}. + +See the files @file{span-extent.el} and @file{span-overlay.el} for the +implementation of the common interface in each case. + +@node Proof General site configuration +@section Proof General site configuration +@cindex installation directories +@cindex site configuration + +The file @file{proof-site.el} contains the initial configuration for +Proof General for the site (or user) and the choice of provers. + +The first part of the configuration is to set +@code{proof-home-directory} to the directory that @file{proof-site.el} +is located in, or to the variable of the environment variable +@code{PROOFGENERAL_HOME} if that is set. + +@c TEXI DOCSTRING MAGIC: proof-home-directory +@defvar proof-home-directory +Directory where Proof General is installed. Ends with slash.@* +Default value taken from environment variable @samp{PROOFGENERAL_HOME} if set, +otherwise based on where the file @samp{proof-site.el} was loaded from. +You can use customize to set this variable. +@end defvar + +@c They're no longer options. +@c The default value for @code{proof-home-directory} mentioned above is the +@c one for the author's system, it won't be the same for you! + +Further directory variables allow the files of Proof General to be split +up and installed across a system if need be, rather than under the +@code{proof-home-directory} root. + +@c TEXI DOCSTRING MAGIC: proof-images-directory +@defvar proof-images-directory +Where Proof General image files are installed. Ends with slash. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-info-directory +@defvar proof-info-directory +Where Proof General Info files are installed. Ends with slash. +@end defvar + + + +@cindex mode stub +After defining these settings, we define a @dfn{mode stub} for each +proof assistant enabled. The mode stub will autoload Proof General for +the right proof assistant when a file is visited with the corresponding +extension. The proof assistants enabled are the ones listed +in the @code{proof-assistants} setting. + +@c TEXI DOCSTRING MAGIC: proof-assistants +@defopt proof-assistants +Choice of proof assistants to use with Proof General.@* +A list of symbols chosen from: @code{'demoisa} @code{'isar} @code{'isa} @code{'lego} @code{'coq} @code{'phox} @code{'hol98} @code{'acl2} @code{'plastic} @code{'twelf}. +Each proof assistant defines its own instance of Proof General, +providing session control, script management, etc. Proof General +will be started automatically for the assistants chosen here. +To avoid accidently invoking a proof assistant you don't have, +only select the proof assistants you (or your site) may need. + +You can select which proof assistants you want by setting this +variable before @samp{proof-site.el} is loaded, or by setting +the environment variable @samp{PROOFGENERAL_ASSISTANTS} to the +symbols you want, for example "lego isa". Or you can +edit the file @samp{proof-site.el} itself. + +Note: to change proof assistant, you must start a new Emacs session. + +The default value is @code{nil}. +@end defopt + +The file @file{proof-site.el} also defines a version variable. + +@c TEXI DOCSTRING MAGIC: proof-general-version +@defvar proof-general-version +Version string identifying Proof General release. +@end defvar + + + +@node Configuration variable mechanisms +@section Configuration variable mechanisms +@cindex conventions +@cindex user options +@cindex configuration +@cindex settings + +The file @file{proof-config.el} defines the configuration variables for +Proof General, including instantiation parameters and user options. See +previous chapters for details of its contents. Here we mention some +conventions for declaring user options. + +Global user options and instantiation parameters are declared using +@code{defcustom} as usual. User options should have `@code{*}' as the +first character of their docstrings (standard Emacs convention) and live +in the customize group @code{proof-user-options}. See +@file{proof-config.el} for the groups for instantiation parameters. + +User options which are generic (having separate instances for each +prover) and instantiation parameters (by definition generic) can be +declared using the special macro @code{defpgcustom}. It is used in the +same way as @code{defcustom}, except that the symbol declared will +automatically be prefixed by the current proof assistant symbol. + +@c TEXI DOCSTRING MAGIC: defpgcustom +@deffn Macro defpgcustom +Define a new customization variable <PA>@var{-sym} for the current proof assistant.@* +The function proof-assistant-<SYM> is also defined, which can be used in the +generic portion of Proof General to set and retrieve the value for the current p.a. +Arguments as for @samp{defcustom}, which see. + +Usage: (defpgcustom SYM &rest @var{args}). +@end deffn + +In specific instances of Proof General, the macro @code{defpgdefault} +can be used to give a default value for a generic setting. + +@c TEXI DOCSTRING MAGIC: defpgdefault +@deffn Macro defpgdefault +Set default for the proof assistant specific variable <PA>@var{-sym} to @var{value}.@* +This should be used in prover-specific code to alter the default values +for prover specific settings. + +Usage: (defpgdefault SYM @var{value}) +@end deffn + +All new instantiation variables are best declared using the +@code{defpgcustom} mechanism (old code may be converted gradually). +Customizations which are liable to be different for different instances +of Proof General are also best declared in this way. An example is the +use of X Symbol, controlled by @code{@emph{PA}-x-symbol-enable}, since +it works poorly or not at all with some provers. + +To access the generic settings, the following four functions and +macros are useful. + +@c TEXI DOCSTRING MAGIC: proof-ass +@deffn Macro proof-ass +Return the value for SYM for the current prover. +@end deffn +@c TEXI DOCSTRING MAGIC: proof-ass-sym +@deffn Macro proof-ass-sym +Return the symbol for SYM for the current prover. SYM not evaluated. +@end deffn +@c TEXI DOCSTRING MAGIC: proof-ass-symv +@defun proof-ass-symv sym +Return the symbol for @var{sym} for the current prover. @var{sym} is evaluated. +@end defun + +If changing a user option setting amounts to more than just setting a +variable (it may have some dynamic effect), we can set the +@code{custom-set} property for the variable to the function +@code{proof-set-value} which does an ordinary @code{set-default} to set +the variable, and then calls a function with the same name as the +variable, to do whatever is necessary according to the new value for the +variable. + +There are several settings which can be switched on or off by the user, +which use this @code{proof-set-value} mechanism. They are controlled by +boolean variables with names like @code{proof-@var{foo}-enable}, and +appear at the start of the customize group @code{proof-user-options}. +They should be edited by the user through the customization mechanism, +and set in the code using @code{customize-set-variable}. + +In @code{proof-utils.el} there is a handy macro, +@code{proof-deftoggle}, which constructs an interactive function +for toggling boolean customize settings. We can use this to make an +interactive function @code{proof-@var{foo}-toggle} to put on a menu or +bind to a key, for example. + +This general scheme is followed as far as possible, to give uniform +behaviour and appearance for boolean user options, as well as +interfacing properly with the @code{customize} mechanism. + +@c TEXI DOCSTRING MAGIC: proof-set-value +@defun proof-set-value sym value +Set a customize variable using @code{set-default} and a function.@* +We first call @samp{@code{set-default}} to set @var{sym} to @var{value}. +Then if there is a function @var{sym} (i.e. with the same name as the +variable @var{sym}), it is called to take some dynamic action for the new +setting. + +If there is no function @var{sym}, we try stripping +@code{proof-assistant-symbol} and adding "proof-" instead to get +a function name. This extends @code{proof-set-value} to work with +generic individual settings. + +The dynamic action call only happens when values @strong{change}: as an +approximation we test whether proof-config is fully-loaded yet. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-deftoggle +@deffn Macro proof-deftoggle +Define a function VAR-toggle for toggling a boolean customize setting VAR.@* +The toggle function uses @code{customize-set-variable} to change the variable. +@var{othername} gives an alternative name than the default <VAR>-toggle. +The name of the defined function is returned. +@end deffn +@node Global variables +@section Global variables + +Global variables are defined in @file{proof.el}. The same file defines +a few utility functions and some triggers to load in the other files. + +@c TEXI DOCSTRING MAGIC: proof-script-buffer +@defvar proof-script-buffer +The currently active scripting buffer or nil if none. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-buffer +@defvar proof-shell-buffer +Process buffer where the proof assistant is run. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-response-buffer +@defvar proof-response-buffer +The response buffer. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-goals-buffer +@defvar proof-goals-buffer +The goals buffer. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-buffer-type +@defvar proof-buffer-type +Symbol indicating the type of this buffer: @code{'script}, @code{'shell}, @code{'pbp}, or @code{'response}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-included-files-list +@defvar proof-included-files-list +List of files currently included in proof process.@* +This list contains files in canonical truename format +(see @samp{@code{file-truename}}). + +Whenever a new file is being processed, it gets added to this list +via the @code{proof-shell-process-file} configuration settings. +When the prover retracts a file, this list is resynchronised via the +@code{proof-shell-retract-files-regexp} and @code{proof-shell-compute-new-files-list} +configuration settings. + +Only files which have been @strong{fully} processed should be included here. +Proof General itself will automatically add the filenames of a script +buffer which has been completely read when scripting is deactivated. +It will automatically remove the filename of a script buffer which +is completely unread when scripting is deactivated. + +NB: Currently there is no generic provision for removing files which +are only partly read-in due to an error, so ideally the proof assistant +should only output a processed message when a file has been successfully +read. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-proof-completed +@defvar proof-shell-proof-completed +Flag indicating that a completed proof has just been observed.@* +If non-nil, the value counts the commands from the last command +of the proof (starting from 1). +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-error-or-interrupt-seen +@defvar proof-shell-error-or-interrupt-seen +Flag indicating that an error or interrupt has just occurred.@* +Set to @code{'error} or @code{'interrupt} if one was observed from the proof +assistant during the last group of commands. +@end defvar + + +@node Proof script mode +@section Proof script mode + +The file @file{proof-script.el} contains the main code for proof script +mode, as well as definitions of menus, key-bindings, and user-level +functions. + +Proof scripts have two important variables for the locked and queue +regions. These variables are local to each script buffer (although we +only really need one queue span in total rather than one per buffer). + +@c TEXI DOCSTRING MAGIC: proof-locked-span +@defvar proof-locked-span +The locked span of the buffer.@* +Each script buffer has its own locked span, which may be detached +from the buffer. +Proof General allows buffers in other modes also to be locked; +these also have a non-nil value for this variable. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-queue-span +@defvar proof-queue-span +The queue span of the buffer. May be detached if inactive or empty. +@end defvar + +Various utility functions manipulate and examine the spans. An +important one is @code{proof-init-segmentation}. + +@c TEXI DOCSTRING MAGIC: proof-init-segmentation +@defun proof-init-segmentation +Initialise the queue and locked spans in a proof script buffer.@* +Allocate spans if need be. The spans are detached from the +buffer, so the regions are made empty by this function. +@end defun + +For locking files loaded by a proof assistant, we use the next function. + +@c TEXI DOCSTRING MAGIC: proof-complete-buffer-atomic +@defun proof-complete-buffer-atomic buffer +Make sure @var{buffer} is marked as completely processed, completing with a single step. + +If buffer already contains a locked region, only the remainder of the +buffer is closed off atomically. + +This works for buffers which are not in proof scripting mode too, +to allow other files loaded by proof assistants to be marked read-only. +@end defun + +Atomic locking is instigated by the next function, which uses the +variables @code{proof-included-files-list} documented earlier +(@pxref{Handling multiple files} and @pxref{Global variables}). + +@c TEXI DOCSTRING MAGIC: proof-register-possibly-new-processed-file +@defun proof-register-possibly-new-processed-file file &optional informprover noquestions +Register a possibly new @var{file} as having been processed by the prover. + +If @var{informprover} is non-nil, the proof assistant will be told about this, +to co-ordinate with its internal file-management. (Otherwise we assume +that it is a message from the proof assistant which triggers this call). +In this case, the user will be queried to save some buffers, unless +@var{noquestions} is non-nil. + +No action is taken if the file is already registered. + +A warning message is issued if the register request came from the +proof assistant and Emacs has a modified buffer visiting the file. +@end defun + +An important pair of functions activate and deactivate scripting for the +current buffer. A change in the state of active scripting can trigger +various actions, such as starting up the proof assistant, or altering +@code{proof-included-files-list}. + +@c TEXI DOCSTRING MAGIC: proof-activate-scripting +@deffn Command proof-activate-scripting &optional nosaves queuemode +Ready prover and activate scripting for the current script buffer. + +The current buffer is prepared for scripting. No changes are +necessary if it is already in Scripting minor mode. Otherwise, it +will become the new active scripting buffer, provided scripting +can be switched off in the previous active scripting buffer +with @samp{@code{proof-deactivate-scripting}}. + +Activating a new script buffer may be a good time to ask if the +user wants to save some buffers; this is done if the user +option @samp{@code{proof-query-file-save-when-activating-scripting}} is set +and provided the optional argument @var{nosaves} is non-nil. + +The optional argument @var{queuemode} relaxes the test for a +busy proof shell to allow one which has mode @var{queuemode}. +In all other cases, a proof shell busy error is given. + +Finally, the hooks @samp{@code{proof-activate-scripting-hook}} are run. +This can be a useful place to configure the proof assistant for +scripting in a particular file, for example, loading the +correct theory, or whatever. If the hooks issue commands +to the proof assistant (via @samp{@code{proof-shell-invisible-command}}) +which result in an error, the activation is considered to +have failed and an error is given. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-deactivate-scripting +@deffn Command proof-deactivate-scripting &optional forcedaction +Deactivate scripting for the active scripting buffer. + +Set @code{proof-script-buffer} to nil and turn off the modeline indicator. +No action if there is no active scripting buffer. + +We make sure that the active scripting buffer either has no locked +region or a full locked region (everything in it has been processed). +If this is not already the case, we question the user whether to +retract or assert, or automatically take the action indicated in the +user option @samp{@code{proof-auto-action-when-deactivating-scripting}.} + +If the scripting buffer is (or has become) fully processed, and it is +associated with a file, it is registered on +@samp{@code{proof-included-files-list}}. Conversely, if it is (or has become) +empty, we make sure that it is @strong{not} registered. This is to be +certain that the included files list behaves as we might expect with +respect to the active scripting buffer, in an attempt to harmonize +mixed scripting and file reading in the prover. + +This function either succeeds, fails because the user refused to +process or retract a partly finished buffer, or gives an error message +because retraction or processing failed. If this function succeeds, +then @code{proof-script-buffer} is nil afterwards. + +The optional argument @var{forcedaction} overrides the user option +@samp{@code{proof-auto-action-when-deactivating-scripting}} and prevents +questioning the user. It is used to make a value for +the @code{kill-buffer-hook} for scripting buffers, so that when +a scripting buffer is killed it is always retracted. +@end deffn + +The function @code{proof-segment-up-to} is the main one used for parsing +the proof script buffer. There are several variants of this function +available corresponding to different parsing strategies; the appropriate +one is aliased to @code{proof-segment-up-to} according to which +configuration variables have been set. If only +@code{proof-script-command-end-regexp} or @code{proof-terminal-char} are set, +then the default is @code{proof-segment-up-to-cmdend}. If +@code{proof-script-command-start-regexp} is set, the choice is +@code{proof-segment-up-to-cmdstart}. + +@c TEXI DOCSTRING MAGIC: proof-segment-up-to-cmdend +@defun proof-segment-up-to-cmdend pos &optional next-command-end +Parse the script buffer from end of locked to @var{pos}.@* +Return a list of (type, string, int) tuples. + +Each tuple denotes the command and the position of its terminator, +type is one of @code{'comment}, or @code{'cmd}. @code{'unclosed-comment} may be consed onto +the start if the segment finishes with an unclosed comment. + +If optional @var{next-command-end} is non-nil, we include the command +which continues past @var{pos}, if any. + +This version is used when @samp{@code{proof-script-command-end-regexp}} is set. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-segment-up-to-cmdstart +@defun proof-segment-up-to-cmdstart pos &optional next-command-end +Parse the script buffer from end of locked to @var{pos}.@* +Return a list of (type, string, int) tuples. + +Each tuple denotes the command and the position of its terminator, +type is one of @code{'comment}, or @code{'cmd}. + +If optional @var{next-command-end} is non-nil, we include the command +which continues past @var{pos}, if any. (NOT @var{implemented} IN @var{this} @var{version}). + +This version is used when @samp{@code{proof-script-command-start-regexp}} is set. +@end defun + + +The function @code{proof-semis-to-vanillas} is used to convert +a parsed region of the script into a series of commands to +be sent to the proof assistant. + +@c TEXI DOCSTRING MAGIC: proof-semis-to-vanillas +@defun proof-semis-to-vanillas semis &optional callback-fn +Convert a sequence of terminator positions to a set of vanilla extents.@* +Proof terminator positions @var{semis} has the form returned by +the function proof-segment-up-to. +Set the callback to @var{callback-fn} or @code{'proof-done-advancing} by default. +@end defun + +The function @code{proof-assert-until-point} is the main one used to +process commands in the script buffer. It's actually used to implement +the assert-until-point, electric terminator keypress, and +find-next-terminator behaviours. In different cases we want different +things, but usually the information (i.e. are we inside a comment) isn't +available until we've actually run @code{proof-segment-up-to (point)}, +hence all the different options when we've done so. + +@c TEXI DOCSTRING MAGIC: proof-assert-until-point +@defun proof-assert-until-point &optional unclosed-comment-fun ignore-proof-process-p +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. + +If you want something different, put it inside +@var{unclosed-comment-fun}. If @var{ignore-proof-process-p} is set, no commands +will be added to the queue and the buffer will not be activated for +scripting. +@end defun + +@code{proof-assert-next-command} is a variant of this function. + +@c TEXI DOCSTRING MAGIC: proof-assert-next-command +@deffn Command proof-assert-next-command &optional unclosed-comment-fun ignore-proof-process-p dont-move-forward for-new-command +Process until the end of the next unprocessed command after point.@* +If inside a comment, just process until the start of the comment. + +If you want something different, put it inside @var{unclosed-comment-fun}. +If @var{ignore-proof-process-p} is set, no commands will be added to the queue. +Afterwards, move forward to near the next command afterwards, unless +@var{dont-move-forward} is non-nil. If @var{for-new-command} is non-nil, +a space or newline will be inserted automatically. +@end deffn + +The main command for retracting parts of a script is +@code{proof-retract-until-point}. + +@c TEXI DOCSTRING MAGIC: proof-retract-until-point +@defun proof-retract-until-point &optional delete-region +Set up the proof process for retracting until point.@* +In particular, set a flag for the filter process to call +@samp{@code{proof-done-retracting}} after the proof process has successfully +reset its state. +If @var{delete-region} is non-nil, delete the region in the proof script +corresponding to the proof command sequence. +If invoked outside a locked region, undo the last successfully processed +command. +@end defun + +To clean up when scripting is stopped, a script buffer is killed, or the +proof assistant exits, we use the functions +@code{proof-restart-buffers} and +@code{proof-script-remove-all-spans-and-deactivate}. + +@c TEXI DOCSTRING MAGIC: proof-restart-buffers +@defun proof-restart-buffers buffers +Remove all extents in @var{buffers} and maybe reset @samp{@code{proof-script-buffer}}.@* +No effect on a buffer which is nil or killed. If one of the buffers +is the current scripting buffer, then @code{proof-script-buffer} +will deactivated. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-script-remove-all-spans-and-deactivate +@defun proof-script-remove-all-spans-and-deactivate +Remove all spans from scripting buffers via @code{proof-restart-buffers}. +@end defun + + +@c +@c SECTION: Proof Shell Mode +@c +@node Proof shell mode +@section Proof shell mode +@cindex proof shell mode +@cindex comint-mode + +The proof shell mode code is in the file @file{proof-shell.el}. Proof +shell mode is defined to inherit from @code{comint-mode} using +@code{define-derived-mode} near the end of the file. The bulk of the +code in the file is concerned with sending code to and from the shell, +and processing output for the associated buffers (goals and response). + +Good process handling is a tricky issue. Proof General attempts to +manage the process strictly, by maintaining a queue of commands to send +to the process. Once a command has been processed, another one is +popped off the queue and sent. + +There are several important internal variables which control +interaction with the process. + +@c TEXI DOCSTRING MAGIC: proof-shell-busy +@defvar proof-shell-busy +A lock indicating that the proof shell is processing.@* +When this is non-nil, @code{proof-shell-ready-prover} will give +an error. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-marker +@defvar proof-marker +Marker in proof shell buffer pointing to previous command input. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-action-list +@defvar proof-action-list +A list of@* +@lisp + (@var{span} @var{command} @var{action}) +@end lisp +triples, which is a queue of things to do. +See the functions @samp{@code{proof-start-queue}} and @samp{proof-exec-loop}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-analyse-using-stack +@defvar proof-analyse-using-stack +Choice of syntax tree encoding for terms. + +If nil, prover is expected to make no optimisations. +If non-nil, the pretty printer of the prover only reports local changes. +For @var{lego} 1.3.1 use @samp{nil}, for Coq 6.2, use @samp{t}. +@end defvar + + +The function @code{proof-shell-start} is used to initialise a shell +buffer and the associated buffers. + +@c TEXI DOCSTRING MAGIC: proof-shell-start +@deffn Command proof-shell-start +Initialise a shell-like buffer for a proof assistant. + +Also generates goal and response buffers. +Does nothing if proof assistant is already running. +@end deffn + +The function @code{proof-shell-kill-function} performs the converse +function of shutting things down; it is used as a hook function for +@code{kill-buffer-hook}. Then no harm occurs if the user kills the +shell directly, or if it is done more cautiously via +@code{proof-shell-exit}. The function @code{proof-shell-restart} allows +a less drastic way of restarting scripting, other than killing and +restarting the process. + +@c TEXI DOCSTRING MAGIC: proof-shell-kill-function +@defun proof-shell-kill-function +Function run when a proof-shell buffer is killed.@* +Attempt to shut down the proof process nicely and +clear up all the locked regions and state variables. +Value for @code{kill-buffer-hook} in shell buffer. +Also called by @code{proof-shell-bail-out} if the process is +exited by hand (or exits by itself). +@end defun + +@c TEXI DOCSTRING MAGIC: proof-shell-exit +@deffn Command proof-shell-exit +Query the user and exit the proof process. + +This simply kills the @code{proof-shell-buffer} relying on the hook function +@code{proof-shell-kill-function} to do the hard work. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-shell-bail-out +@defun proof-shell-bail-out process event +Value for the process sentinel for the proof assistant process.@* +If the proof assistant dies, run @code{proof-shell-kill-function} to +cleanup and remove the associated buffers. The shell buffer is +left around so the user may discover what killed the process. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-shell-restart +@deffn Command proof-shell-restart +Clear script buffers and send @code{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 +@code{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). +@end deffn + +@c +@c INPUT +@c +@subsection Input to the shell + +Input to the proof shell via the queue region is managed by the +functions @code{proof-start-queue} and @code{proof-shell-exec-loop}. + +@c TEXI DOCSTRING MAGIC: proof-start-queue +@defun proof-start-queue start end alist +Begin processing a queue of commands in @var{alist}.@* +If @var{start} is non-nil, @var{start} and @var{end} are buffer positions in the +active scripting buffer for the queue region. + +This function calls @samp{@code{proof-append-alist}}. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-append-alist + +@defun proof-append-alist alist &optional queuemode +Chop off the vacuous prefix of the command queue @var{alist} and queue it.@* +For each @samp{@code{proof-no-command}} item at the head of the list, invoke its +callback and remove it from the list. + +Append the result onto @samp{@code{proof-action-list}}, and if the proof +shell isn't already busy, grab the lock with @var{queuemode} and +start processing the queue. + +If the proof shell is busy when this function is called, +then @var{queuemode} must match the mode of the queue currently +being processed. +@end defun +@vindex proof-action-list +@c TEXI DOCSTRING MAGIC: proof-shell-exec-loop +@defun proof-shell-exec-loop +Process the @code{proof-action-list}. + +@samp{@code{proof-action-list}} contains a list of (@var{span} @var{command} @var{action}) triples. + +If this function is called with a non-empty @code{proof-action-list}, the +head of the list is the previously executed command which succeeded. +We execute (@var{action} @var{span}) on the first item, then (@var{action} @var{span}) on any +following items which have @code{proof-no-command} as their cmd components. +If a there is a next command after that, send it to the process. If +the action list becomes empty, unlock the process and remove the queue +region. + +The return value is non-nil if the action list is now empty. +@end defun + +Input is actually inserted into the shell buffer and sent to the process +by the low-level function @code{proof-shell-insert}. + +@c TEXI DOCSTRING MAGIC: proof-shell-insert +@defun proof-shell-insert string action +Insert @var{string} at the end of the proof shell, call @code{comint-send-input}. + +First call @code{proof-shell-insert-hook}. The argument @var{action} may be +examined by the hook to determine how to process the @var{string} variable. + +Then strip @var{string} of carriage returns before inserting it and updating +@code{proof-marker} to point to the end of the newly inserted text. + +Do not use this function directly, or output will be lost. It is only +used in @code{proof-append-alist} when we start processing a queue, and in +@code{proof-shell-exec-loop}, to process the next item. +@end defun + + +When Proof General is processing a queue of commands, the lock +is managed using a couple of utility functions. You should +not need to use these directly. + + +@c TEXI DOCSTRING MAGIC: proof-grab-lock + +@defun proof-grab-lock &optional queuemode +Grab the proof shell lock, starting the proof assistant if need be.@* +Runs @code{proof-state-change-hook} to notify state change. +Clears the @code{proof-shell-error-or-interrupt-seen} flag. +If @var{queuemode} is supplied, set the lock to that value. +@end defun +@c TEXI DOCSTRING MAGIC: proof-release-lock + + + + + + + +@defun proof-release-lock &optional err-or-int +Release the proof shell lock, with error or interrupt flag @var{err-or-int}.@* +Clear @code{proof-shell-busy}, and set @code{proof-shell-error-or-interrupt-seen} +to err-or-int. +@end defun + + +@c +@c OUTPUT +@c +@subsection Output from the shell + +Two main functions deal with output, @code{proof-shell-process-output} +and @code{proof-shell-process-urgent-message}. In effect we consider +the output to be two streams intermingled: the "urgent" messages which +have "eager" annotations, as well as the ordinary ruminations from the +prover. + +The idea is to conceal as much irrelevant information from the user as +possible; only the remaining output between prompts and after the last +urgent message will be a candidate for the goal or response buffer. The +internal variable @code{proof-shell-urgent-message-marker} tracks the +last urgent message seen. + +When output is grabbed from the prover process, it is stored into +@code{proof-shell-last-output}, and its type is stored in +@code{proof-shell-last-output-kind}. Output which is deferred +or possibly discarded until the queue is empty is copied into +@code{proof-shell-delayed-output}, with type +@code{proof-shell-delayed-output-kind}. + + +@c TEXI DOCSTRING MAGIC: proof-shell-last-output +@defvar proof-shell-last-output +A record of the last string seen from the proof system. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-last-output-kind +@defvar proof-shell-last-output-kind +A symbol denoting the type of the last output string from the proof system.@* +Specifically: +@lisp + @code{'interrupt} An interrupt message + @code{'error} An error message + @code{'abort} A proof abort message + @code{'loopback} A command sent from the PA to be inserted into the script + @code{'response} A response message + @code{'goals} A goals (proof state) display + @code{'systemspecific} Something specific to a particular system, + -- see @samp{@code{proof-shell-process-output-system-specific}} +@end lisp +The output corresponding to this will be in @code{proof-shell-last-output}. + +See also @samp{@code{proof-shell-proof-completed}} for further information about +the proof process output, when ends of proofs are spotted. + +This variable can be used for instance specific functions which want +to examine @code{proof-shell-last-output}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-delayed-output +@defvar proof-shell-delayed-output +A copy of @code{proof-shell-last-output} held back for processing at end of queue. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-delayed-output-kind +@defvar proof-shell-delayed-output-kind +A copy of proof-shell-last-output-lind held back for processing at end of queue. +@end defvar +@vindex proof-action-list + +@c TEXI DOCSTRING MAGIC: proof-shell-process-output +@defun proof-shell-process-output cmd string +Process shell output (resulting from @var{cmd}) by matching on @var{string}.@* +@var{cmd} is the first part of the @code{proof-action-list} that lead to this +output. The result of this function is a pair (@var{symbol} @var{newstring}). + +Here is where we recognizes interrupts, abortions of proofs, errors, +completions of proofs, and proof step hints (proof by pointing results). +They are checked for in this order, using +@lisp + @code{proof-shell-interrupt-regexp} + @code{proof-shell-error-regexp} + @code{proof-shell-abort-goal-regexp} + @code{proof-shell-proof-completed-regexp} + @code{proof-shell-result-start} +@end lisp +All other output from the proof engine will be reported to the user in +the response buffer by setting @code{proof-shell-delayed-output} to a cons +cell of ('insert . @var{text}) where @var{text} is the text string to be inserted. + +Order of testing is: interrupt, abort, error, completion. + +To extend this function, set @code{proof-shell-process-output-system-specific}. + +The "aborted" case is intended for killing off an open proof during +retraction. Typically it matches the message caused by a +@code{proof-kill-goal-command}. It simply inserts the word "Aborted" into +the response buffer. So it is expected to be the result of a +retraction, rather than the indication that one should be made. + +This function sets @samp{@code{proof-shell-last-output}} and @samp{@code{proof-shell-last-output-kind}}, +which see. +@end defun + +@c TEXI DOCSTRING MAGIC: proof-shell-urgent-message-marker +@defvar proof-shell-urgent-message-marker +Marker in proof shell buffer pointing to end of last urgent message. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-shell-process-urgent-message +@defun proof-shell-process-urgent-message message +Analyse urgent @var{message} for various cases.@* +Cases are: included file, retracted file, cleared response buffer, +variable setting or dependency list. +If none of these apply, display @var{message}. + +@var{message} should be a string annotated with +@code{proof-shell-eager-annotation-start}, @code{proof-shell-eager-annotation-end}. +@end defun + +The main processing point which triggers other actions is +@code{proof-shell-filter}. + +@c TEXI DOCSTRING MAGIC: proof-shell-filter +@defun proof-shell-filter str +Filter for the proof assistant shell-process.@* +A function for @code{comint-output-filter-functions}. + +Deal with output and issue new input from the queue. + +Handle urgent messages first. As many as possible are processed, +using the function @samp{@code{proof-shell-process-urgent-messages}}. + +Otherwise wait until an annotated prompt appears in the input. +If @code{proof-shell-wakeup-char} is set, wait until we see that in the +output chunk @var{str}. This optimizes the filter a little bit. + +If a prompt is seen, run @code{proof-shell-process-output} on the output +between the new prompt and the last input (position of @code{proof-marker}) +or the last urgent message (position of +@code{proof-shell-urgent-message-marker}), whichever is later. +For example, in this case: +@lisp + PROMPT> @var{input} + @var{output-1} + @var{urgent-message} + @var{output-2} + PROMPT> +@end lisp +@code{proof-marker} is set after @var{input} by @code{proof-shell-insert} and +@code{proof-shell-urgent-message-marker} is set after @var{urgent-message}. +Only @var{output-2} will be processed. For this reason, error +messages and interrupt messages should @strong{not} be considered +urgent messages. + +Output is processed using @code{proof-shell-filter-process-output}. + +The first time that a prompt is seen, @code{proof-marker} is +initialised to the end of the prompt. This should +correspond with initializing the process. The +ordinary output before the first prompt is ignored (urgent messages, +however, are always processed; hence their name). +@end defun + +@c TEXI DOCSTRING MAGIC: proof-shell-filter-process-output +@defun proof-shell-filter-process-output string +Subroutine of @code{proof-shell-filter} to process output @var{string}. + +Appropriate action is taken depending on the what +@code{proof-shell-process-output} returns: maybe handle an interrupt, an +error, or deal with ordinary output which is a candidate for the goal +or response buffer. Ordinary output is only displayed when the proof +action list becomes empty, to avoid a confusing rapidly changing +output. + +After processing the current output, the last step undertaken +by the filter is to send the next command from the queue. +@end defun + + + + + + +@c +@c SECTION: Debugging +@c +@node Debugging +@section Debugging +@cindex debugging + +@c FIXME: better to have general hints on Elisp earlier, plus some +@c links to helpful docs. + +To debug Proof General, it may be helpful to set the +configuration variable @code{proof-show-debug-messages}. + +@c TEXI DOCSTRING MAGIC: proof-show-debug-messages +@defopt proof-show-debug-messages +Whether to display debugging messages in the response buffer.@* +If non-nil, debugging messages are displayed in the response giving +information about what Proof General is doing. +To avoid erasing the messages shortly after they're printed, +you should set @samp{@code{proof-tidy-response}} to nil. + +The default value is @code{nil}. +@end defopt + +For more information about debugging Emacs lisp, consult the Emacs Lisp +Reference Manual. I recommend using the source-level debugger +@code{edebug}. + + + + + + + + + + + + + + +@c +@c +@c APPENDIX: Plans and ideas +@c +@c +@node Plans and ideas +@appendix Plans and ideas + +This appendix contains some tentative plans and ideas for improving +Proof General. + +This appendix is no longer extended: instead we keep a list of Proof +General projects on the web, and forthcoming plans and ideas in the +@file{TODO} and @file{todo} files included in the ordinary and +developers PG distributions, respectively. Once the items mentioned +below are implemented, they will be removed from here. + +Please send us contributions to our wish lists, or better still, an +offer to implement something from them! + +@menu +* Proof by pointing and similar features:: +* Granularity of atomic command sequences:: +* Browser mode for script files and theories:: +@end menu + +@node Proof by pointing and similar features +@section Proof by pointing and similar features +@cindex proof by pointing + +This is a note by David Aspinall about proof by pointing and similar +features. + +Proof General already supports proof by pointing, and experimental +support is provided in LEGO. We would like to extend this support to +other proof assistants. Unfortunately, proof by pointing requires +rather heavy support from the proof assistant. There are two aspects to +the support: +@itemize @bullet +@item term structure mark-up +@item proof by pointing command generation +@end itemize +Term structure mark-up is useful in itself: it allows the user 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. + +Command generation for proof by pointing is usually specific to a +particular logic in use, if we hope to generate a good proof command +unambiguously for any particular click. However, Proof General could +easily be generalised to offer the user a context-sensitive choice of +next commands to apply, which may be more useful in practice, and a +worthy addition to Proof General. + +Implementors of new proof assistants should be encouraged to consider +supporting term-structure mark up from the start. Command generation +should be something that the logic-implementor can specify in some way. + +Of the supported provers, we can certainly hope for proof-by-pointing +support from Coq, since the CtCoq proof-by-pointing code has been moved +into the Coq kernel lately. I hope the Coq community can encourage +somebody to do this. + + +@node Granularity of atomic command sequences +@section Granularity of atomic command sequences +@c @cindex Granularity of Atomic Sequences +@c @cindex Retraction +@c @cindex Goal +@cindex ACS (Atomic Command Sequence) + +This is a proposal by Thomas Kleymann for generalising the way Proof +General handles sequences of proof commands (see @i{Goal-save +sequences} in the user manual), particularly to make retraction more flexible. + +The blue region of a script buffer contains the initial segment of +the proof script which has been processed successfully. It consists of +atomic sequences of commands (ACS). Retraction is supported to the +beginning of every ACS. By default, every command is an ACS. But the +granularity of atomicity should be able to be adjusted. + +This is essential when arbitrary retraction is not supported. Usually, +after a theorem has been proved, one may only retract to the start of +the goal. One needs to mark the proof of the theorem as an ACS. At +present, support for goal-save sequences (see @i{Goal-save sequences} in +the user manual), has been hard wired. No other ACS are currently +supported. We propose the following to overcome this deficiency: + +@vtable @code +@item proof-atomic-sequents-list +is a list of instructions for setting up ACSs. Each instruction is a +list of the form @code{(@var{end} @var{start} &optional +@var{forget-command})}. @var{end} is a regular expression to recognise +the last command in an ACS. @var{start} is a function. Its input is the +last command of an ACS. Its output is a regular expression to recognise +the first command of the ACS. It is evaluated once and, starting with the +command matched by @var{end}, the output is +successively matched against previously processed commands until a match +occurs (or the beginning of the current buffer is reached). The region +determined by (@var{start},@var{end}) is locked as an ACS. Optionally, +the ACS is annotated with the actual command to retract the ACS. This is +computed by applying @var{forget-command} to the first and last command +of the ACS. + +For convenience one might also want to allow @var{start} to be the +symbol @samp{t} as a convenient short-hand for @code{'(lambda (str) +".")} which always matches. +@end vtable + +@node Browser mode for script files and theories +@section Browser mode for script files and theories + +This is a proposal by David Aspinall for a browser window. + +A browser window should provide support for browsing script files and +theories. We should be able to inspect data in varying levels of +detail, perhaps using outlining mechanisms. For theories, it would be +nice to query the running proof assistant. This may require support +from the assistant in the form of output which has been specially +marked-up with an SGML like syntax, for example. + +A browser would be useful to: +@itemize @bullet +@item Provide impoverished proof assistants with a browser +@item Extend the uniform interface of Proof General to theory browsing +@item Interact closely with proof script writing +@end itemize +The last point is the most important. We should be able to integrate a +search mechanism for proofs of similar theorems, theorems containing +particular constants, etc. + + + + +@c +@c +@c APPENDIX: Demonstration instantiation for Isabelle +@c +@c +@node Demonstration Instantiations +@appendix Demonstration Instantiations + +This appendix contains the code for the two demonstration +instantiations of Proof General, for Isabelle. + +These instantiations make an almost-bare minimum of settings to get +things working. To add embellishments, you should refer to +the instantiations for other systems distributed with +Proof General. + +@menu +* demoisa-easy.el:: +* demoisa.el:: +@end menu + +@node demoisa-easy.el +@section demoisa-easy.el + +@lisp +@c FIXME: MAGIC NEEDED TO INCLUDE FILE VERBATIM +@c @includeverbatim ../demoisa/demoisa-easy.el +;; demoisa-easy.el Example Proof General instance for Isabelle +;; +;; Copyright (C) 1999 LFCS Edinburgh. +;; +;; Author: David Aspinall <da@@dcs.ed.ac.uk> +;; +;; $Id$ +;; +;; This is an alternative version of demoisa.el which uses the +;; proof-easy-config macro to do the work of declaring derived modes, +;; etc. +;; +;; See demoisa.el and the Proof General manual for more documentation. +;; +;; To test this file you must rename it demoisa.el. +;; + +(require 'proof-easy-config) ; easy configure mechanism + +(proof-easy-config + 'demoisa "Isabelle Demo" + proof-prog-name "isabelle" + proof-terminal-char ?\; + proof-comment-start "(*" + proof-comment-end "*)" + proof-goal-command-regexp "^Goal" + proof-save-command-regexp "^qed" + proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\"" + proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\"" + proof-non-undoables-regexp "undo\\|back" + proof-goal-command "Goal \"%s\";" + proof-save-command "qed \"%s\";" + proof-kill-goal-command "Goal \"PROP no_goal_set\";" + proof-showproof-command "pr()" + proof-undo-n-times-cmd "pg_repeat undo %s;" + proof-auto-multiple-files t + proof-shell-cd-cmd "cd \"%s\"" + proof-shell-prompt-pattern "[ML-=#>]+>? " + proof-shell-interrupt-regexp "Interrupt" + proof-shell-start-goals-regexp "Level [0-9]" + proof-shell-end-goals-regexp "val it" + proof-shell-quit-cmd "quit();" + proof-assistant-home-page + "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" + proof-shell-annotated-prompt-regexp + "^\\(val it = () : unit\n\\)?ML>? " + proof-shell-error-regexp + "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " + proof-shell-init-cmd + "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));" + proof-shell-proof-completed-regexp "^No subgoals!" + proof-shell-eager-annotation-start + "^\\[opening \\|^###\\|^Reading") + +(provide 'demoisa) +@end lisp + +@node demoisa.el +@section demoisa.el + +@lisp +@c FIXME: MAGIC NEEDED TO INCLUDE FILE VERBATIM +@c @includeverbatim ../demoisa/demoisa-easy.el +;; demoisa.el Example Proof General instance for Isabelle +;; +;; Copyright (C) 1999 LFCS Edinburgh. +;; +;; Author: David Aspinall <da@@dcs.ed.ac.uk> +;; +;; $Id$ +;; +;; ================================================================= +;; +;; See README in this directory for an introduction. +;; +;; Basic configuration is controlled by one line in `proof-site.el'. +;; It has this line in proof-assistant-table: +;; +;; (demoisa "Isabelle Demo" "\\.ML$") +;; +;; From this it loads this file "demoisa/demoisa.el" whenever +;; a .ML file is visited, and sets the mode to `demoisa-mode' +;; (defined below). +;; +;; I've called this instance "Isabelle Demo Proof General" just to +;; avoid confusion with the real "Isabelle Proof General" in case the +;; demo gets loaded by accident. +;; +;; To make the line above take precedence over the real Isabelle mode +;; later in the table, set PROOFGENERAL_ASSISTANTS=demoisa in the +;; shell before starting Emacs (or customize proof-assistants). +;; + + +(require 'proof) ; load generic parts + + +;; ======== User settings for Isabelle ======== +;; +;; Defining variables using customize is pretty easy. +;; You should do it at least for your prover-specific user options. +;; +;; proof-site provides us with two customization groups +;; automatically: (based on the name of the assistant) +;; +;; 'isabelledemo - User options for Isabelle Demo Proof General +;; 'isabelledemo-config - Configuration of Isabelle Proof General +;; (constants, but may be nice to tweak) +;; +;; The first group appears in the menu +;; ProofGeneral -> Customize -> Isabelledemo +;; The second group appears in the menu: +;; ProofGeneral -> Internals -> Isabelledemo config +;; + +(defcustom isabelledemo-prog-name "isabelle" + "*Name of program to run Isabelle." + :type 'file + :group 'isabelledemo) + +(defcustom isabelledemo-web-page + "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html" + "URL of web page for Isabelle." + :type 'string + :group 'isabelledemo-config) + + +;; +;; ======== Configuration of generic modes ======== +;; + +(defun demoisa-config () + "Configure Proof General scripting for Isabelle." + (setq + proof-terminal-char ?\; ; ends every command + proof-comment-start "(*" + proof-comment-end "*)" + proof-goal-command-regexp "^Goal" + proof-save-command-regexp "^qed" + proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\"" + proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\"" + proof-non-undoables-regexp "undo\\|back" + proof-undo-n-times-cmd "pg_repeat undo %s;" + proof-showproof-command "pr()" + proof-goal-command "Goal \"%s\";" + proof-save-command "qed \"%s\";" + proof-kill-goal-command "Goal \"PROP no_goal_set\";" + proof-assistant-home-page isabelledemo-web-page + proof-auto-multiple-files t)) + + +(defun demoisa-shell-config () + "Configure Proof General shell for Isabelle." + (setq + proof-shell-annotated-prompt-regexp "^\\(val it = () : unit\n\\)?ML>? " + proof-shell-cd-cmd "cd \"%s\"" + proof-shell-prompt-pattern "[ML-=#>]+>? " + proof-shell-interrupt-regexp "Interrupt" + proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " + proof-shell-start-goals-regexp "Level [0-9]" + proof-shell-end-goals-regexp "val it" + proof-shell-proof-completed-regexp "^No subgoals!" + proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading" + proof-shell-init-cmd ; define a utility function, in a lib somewhere? + "fun pg_repeat f 0 = () + | pg_repeat f n = (f(); pg_repeat f (n-1));" + proof-shell-quit-cmd "quit();")) + + + +;; +;; ======== Defining the derived modes ======== +;; + +;; The name of the script mode is always <proofsym>-script, +;; but the others can be whatever you like. +;; +;; The derived modes set the variables, then call the +;; <mode>-config-done function to complete configuration. + +(define-derived-mode demoisa-mode proof-mode + "Isabelle Demo script" nil + (demoisa-config) + (proof-config-done)) + +(define-derived-mode demoisa-shell-mode proof-shell-mode + "Isabelle Demo shell" nil + (demoisa-shell-config) + (proof-shell-config-done)) + +(define-derived-mode demoisa-response-mode proof-response-mode + "Isabelle Demo response" nil + (proof-response-config-done)) + +(define-derived-mode demoisa-goals-mode proof-goals-mode + "Isabelle Demo goals" nil + (proof-goals-config-done)) + +;; The response buffer and goals buffer modes defined above are +;; trivial. In fact, we don't need to define them at all -- they +;; would simply default to "proof-response-mode" and "pbp-mode". + +;; A more sophisticated instantiation might set font-lock-keywords to +;; add highlighting, or some of the proof by pointing markup +;; configuration for the goals buffer. + +;; The final piece of magic here is a hook which configures settings +;; to get the proof shell running. Proof General needs to know the +;; name of the program to run, and the modes for the shell, response, +;; and goals buffers. + +(add-hook 'proof-pre-shell-start-hook 'demoisa-pre-shell-start) + +(defun demoisa-pre-shell-start () + (setq proof-prog-name isabelledemo-prog-name) + (setq proof-mode-for-shell 'demoisa-shell-mode) + (setq proof-mode-for-response 'demoisa-response-mode) + (setq proof-mode-for-goals 'demoisa-goals-mode)) + +(provide 'demoisa) +@end lisp + + + + +@node Function Index +@unnumbered Function and Command Index +@printindex fn + +@node Variable Index +@unnumbered Variable and User Option Index +@printindex vr + +@c Nothing in this one! +@c @node Keystroke Index +@c @unnumbered Keystroke Index +@c @printindex ky + +@node Concept Index +@unnumbered Concept Index +@printindex cp + +@page +@contents +@bye + + diff --git a/doc/ProofGeneral.jpg b/doc/ProofGeneral.jpg Binary files differnew file mode 100644 index 00000000..6d5bfbfe --- /dev/null +++ b/doc/ProofGeneral.jpg diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi new file mode 100644 index 00000000..9ef74c53 --- /dev/null +++ b/doc/ProofGeneral.texi @@ -0,0 +1,3957 @@ + +\def\fontdefs{\psfamily{bsf}{r}{c}{b}{b}{ri}{ri}{ro}{bo}\def\mainmagstep{1200}} +\input texinfo +@c +@c $Id$ +@c +@c NB: the first line of this file uses a non-standard TeXinfo +@c hack to print in Serifa fonts. It has no effect if you don't have +@c my hacked version of TeXinfo - da. +@c +@c +@setfilename ProofGeneral.info +@settitle Proof General +@setchapternewpage odd +@paragraphindent 0 +@c A flag for whether to include the front image in the +@c DVI file. You can download the front image from +@c http://www.proofgeneral.org/ProofGeneralPortrait.eps.gz +@c then put it into this directory and 'make dvi' (pdf,ps) +@c will set the flag below automatically. +@set haveeps +@iftex +@afourpaper +@end iftex + +@c +@c Some URLs. +@c FIXME: unfortunately, broken in buggy pdftexinfo. +@c so removed for now. +@set URLxsymbol http://www.fmi.uni-passau.de/~wedler/x-symbol/ +@set URLisamode http://www.proofgeneral.org/~isamode +@set URLpghome http://www.proofgeneral.org +@set URLpglatestrpm http://www.proofgeneral.org/ProofGeneral-latest.noarch.rpm +@set URLpglatesttar http://www.proofgeneral.org/ProofGeneral-latest.tar.gz +@set URLpglatestdev http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz +@c +@c + +@c +@c IMPORTANT NOTES ABOUT THIS TEXINFO FILE: +@c I've tried keep full node lines *out* of this file because Emacs makes a +@c mess of updating them and they are a nuisance to do by hand. +@c Instead, rely on makeinfo and friends to do the equivalent job. +@c For this to work, we must follow each node +@c immediately with a section command, i.e.: +@c +@c @node node-name +@c <section-command> +@c +@c And each section with lower levels must have a menu command in +@c it. Menu updating with Emacs is a bit better than node updating, +@c but tends to delete the first section of the file in XEmacs! +@c (it's better in FSF Emacs at the time of writing). +@c +@c LINE BREAKS: For html generated from this to look good, it is +@c important that there are lots of line breaks/blank lines, esp +@c after @enddefn's and similar. Otherwise text flows on the same +@c paragraph but gets coloured wrongly with Netscape's handling of +@c style sheets. +@c +@c reminder about references: +@c @xref{node} blah start of sentence: See [ref] +@c blah (@pxref{node}) blah bla (see [ref]), best at end of sentence +@c @ref{node} without "see". Careful for info. +@c + +@set version 3.3pre +@set xemacsversion 21.1 +@set fsfversion 20.7 +@set last-update October 2000 +@set rcsid $Id$ + +@ifinfo +@format +START-INFO-DIR-ENTRY +* Proof General: (ProofGeneral). Organize your proofs with Emacs! +END-INFO-DIR-ENTRY +@end format +@end ifinfo + +@c +@c MACROS +@c +@c define one here for a command with a key-binding? +@c +@c I like the idea, but it's maybe against the TeXinfo +@c style to fix together a command and its key-binding. +@c +@c merge functions and variables into concept index. +@c @syncodeindex fn cp +@c @syncodeindex vr cp + +@c merge functions into variables index +@c @syncodeindex fn vr + +@finalout +@titlepage +@title Proof General +@subtitle Organize your proofs! +@sp 1 +@subtitle User Manual for Proof General @value{version} +@subtitle @value{last-update} +@subtitle @b{www.proofgeneral.org} + +@c nested ifs fail here completely, WHY? +@iftex +@ifset haveeps +@c @vskip 1cm +@c The .eps file takes 8.4M! A pity texi can't seem +@c to deal with gzipped files? (goes down to 1.7M). +@c But this still seems too much to put into the +@c PG distribution just for an image on the manual page, +@c so we take it out for now. +@c Ideally would like some way of generating eps from +@c the .jpg file. +@image{ProofGeneralPortrait} +@end ifset +@end iftex +@author David Aspinall with H. Goguen, T. Kleymann and D. Sequeira + +@page +@vskip 0pt plus 1filll +This manual and the program Proof General are +Copyright @copyright{} 1998-2000 Proof General team, LFCS Edinburgh. + +@c +@c COPYING NOTICE +@c +@ignore +Permission is granted to process this file through TeX and print the +results, provided the printed document carries copying permission notice +identical to this one except for the removal of this paragraph (this +paragraph not being relevant to the printed manual). +@end ignore + +@sp 2 +Permission is granted to make and distribute verbatim copies of this +manual provided the copyright notice and this permission notice are +preserved on all copies. +@sp 2 + +This manual documents Proof General, Version @value{version}, for use +with XEmacs @value{xemacsversion} and FSF GNU Emacs @value{fsfversion} +or later versions. + +@sp 1 + +Visit Proof General on the web at @code{http://www.proofgeneral.org} + +@sp 1 + +@code{@value{rcsid}} +@end titlepage + +@page + + +@ifinfo +@node Top +@top Proof General + +This file documents version @value{version} of @b{Proof General}, a +generic Emacs interface for proof assistants. + +Proof General @value{version} has been tested with XEmacs +@value{xemacsversion} and FSF GNU Emacs @value{fsfversion}. It is +supplied ready customized for the proof assistants AF2, Coq, Lego, +Isabelle, and HOL. + +@menu +* Preface:: +* Introducing Proof General:: +* Basic Script Management:: +* Proof by Pointing:: +* Advanced Script Management:: +* Support for other Packages:: +* Hints and Tips:: +* Customizing Proof General:: +* LEGO Proof General:: +* Coq Proof General:: +* Isabelle Proof General:: +* HOL Proof General:: +@c * AF2 Proof General:: +* Obtaining and Installing:: +* Known bugs and workarounds:: +* References:: +* Function Index:: +* Variable Index:: +* Keystroke Index:: +* Concept Index:: +@end menu +@end ifinfo + +@node Preface +@unnumbered Preface + +Welcome to Proof General! + +This preface has some news about the current release series, as well as +some history about previous releases, and acknowledgements to those who +have helped along the way. + +Proof General has a home page at +@uref{http://www.proofgeneral.org}. +Visit this page for the latest version of this manual, +other documentation, system downloads, etc. + + +@menu +* Latest news for 3.2:: +* Future:: +* Old News for 3.1:: +* Old News for 3.0:: +* History before 3.0:: +* Credits:: +@end menu + +@node Latest news for 3.2 +@unnumberedsec Latest news for 3.2 +@cindex news + +Proof General 3.2 has several new features 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 @kbd{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 +@kbd{C-RET}. @xref{Support for completion}, 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 @b{AF2} +(see @uref{http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html, the AF2 home page} +for more information). AF2 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 General, and notes on its internals, are in the +@i{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 @code{@i{PA}-setting-name} in the documentation; +you replace @i{PA} by the symbol for the proof assistant you are +interested in. @xref{Customizing Proof General}, for details. + +Finally, important bug fixes include the robustification against +@code{write-file} (@kbd{C-x C-w}), @code{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. + + +@node Future +@unnumberedsec Future +@cindex Proof General Kit +@cindex Future + +The aim of the Proof General project is to provide a powerful and +configurable interfaces which help user-interaction with interactive +proof assistants. + +The strategy Proof General uses is to targets power users rather than +novices; other interfaces have often neglected this class of users. But +we do include general user interface niceties, such as toolbar and +menus, which make use easier for all. + +Proof General has been Emacs based so far, but plans are afoot to +liberate it from the points and parentheses of Emacs Lisp. The +successor project Proof General Kit proposes that proof assistants use a +@i{standard} XML-based protocol for interactive proof, dubbed @b{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. + +For more details, see +@uref{http://www.proofgeneral.org/kit.html, the Proof General Kit webpage}. + + +@node Old News for 3.1 +@unnumberedsec Old News for 3.1 +@cindex news + +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 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 FSF 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. + + +@node Old News for 3.0 +@unnumberedsec 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-bindings 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 maintaining +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 important new feature in Proof General 3.0 is support for +@uref{http://www.fmi.uni-passau.de/~wedler/x-symbol/,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 improvements, it has a better description of how to add +support for a new prover. + +See the @code{CHANGES} file in the distribution for more information +about the latest improvements in Proof General. Developers should check +the @code{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 improvements to multiple file +handling. Pierre Courtieu took responsibility from Patrick Loiseleur +for Coq support, although the improvements in both the Coq and LEGO code +for this release were made by David Aspinall. Markus Wenzel also +provided support for his Isar language, a new proof language for +Isabelle. David von Oheimb helped to develop and debug the generic +version of his X-Symbol patch which he originally provided for Isabelle. + +A new instantiation of Proof General is being worked on for +@emph{Plastic}, a proof assistant being developed at the University of +Durham. + + + +@node History before 3.0 +@unnumberedsec History before 3.0 +@cindex @code{lego-mode} +@cindex history + +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 @uref{http://www.proofgeneral.org/~isamode,Isamode}. Soon +after, the package @code{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 @code{lego-mode} (1.9) was released in May 1995. + + +@cindex proof by pointing +@cindex CtCoq +@cindex Centaur +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 Thomas Kleymann managed to implement a first prototype of +proof-by-pointing in the Emacs interface for LEGO [BKS97]. + +@cindex structure editor +@cindex script management + +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. + +@cindex generic +In 1997, Dilip Sequeira implemented script management in our Emacs +interface for LEGO following the recipe in +[BT98]. 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 @code{lego-mode} to Coq. Part +of the generic code in the @code{lego} package was outsourced (and made +more generic) in a new package called @code{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 work across multiple files. + +It was time to come up with a better name than just @code{proof} +mode. David Aspinall suggested @emph{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. + +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 was used at the Types +Summer School held in Giens, France in September 1999 (see +@uref{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 now in Proof General 3.0. + +@c Why not adapt Proof General to your favourite proof assitant? + + + +@node Credits +@unnumberedsec Credits +@cindex @code{lego-mode} +@cindex maintenance + +The main developers of Proof General have been: + +@itemize @bullet +@item @b{David Aspinall}, +@item @b{Healfdene Goguen}, +@item @b{Thomas Kleymann} and +@item @b{Dilip Sequeira}. +@end itemize + +LEGO Proof General (the successor of @code{lego-mode}) was crafted by +Thomas Kleymann and Dilip Sequeira. +@c +It is presently maintained by David Aspinall and +Paul Callaghan @i{<P.C.Callaghan@@durham.ac.uk>}. +@c +Coq Proof General was crafted by Healfdene Goguen, with +later contributions from Patrick Loiseleur. +It is now maintained by Pierre Courtieu @i{<courtieu@@lri.fr>}. +@c +Isabelle Proof General was crafted and is being maintained by David +Aspinall @i{<da@@dcs.ed.ac.uk>}. It has benefited greatly from tweaks +and suggestions by Markus Wenzel @i{<wenzelm@@informatik.tu-muenchen.de>}, +who crafted and maintains Isabelle/Isar Proof General. Markus also +added Proof General support inside Isabelle. David von Oheimb supplied +the original patches for X-Symbol support. + +The generic base for Proof General was developed by Kleymann, Sequeira, +Goguen and Aspinall. It follows some of the ideas used in Project +@uref{http://www.inria.fr/croap/,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 wrote the section on +file variables. + +The Proof General project has benefited from funding by EPSRC +(Applications of a Type Theory Based Proof Assistant), the EC (Types for +Proofs and Programs) and the support of the LFCS. Version 3.1 was +prepared whilst David Aspinall was visiting ETL, Japan, supported by the +British Council. + +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. + +@c FIXME HERE! +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, and other folk who +tested pre-releases or sent bug reports, including +Pascal Brisset, +Martin Buechi, +Matt Fairtlough, +Kim Hyung Ho, +Pierre Lescanne, +John Longley, +Tobias Nipkow, +Leonor Prensa Nieto, +David von Oheimb, +Randy Pollack, +Sebastian Skalberg, +and +Mike Squire. Thanks to all of you! + + + + +@c +@c CHAPTER: Introduction +@c +@node Introducing Proof General +@chapter Introducing Proof General +@cindex proof assistant +@cindex Proof General + +@c would like the logo on the title page really but +@c it doesn't seem to work there for html. +@ifhtml +<IMG SRC="ProofGeneral.jpg" ALT="[ Proof General logo ]" > +@end ifhtml + +@dfn{Proof General} is a generic Emacs interface for interactive proof +assistants,@footnote{A @dfn{proof assistant} is a computerized helper for +developing mathematical proofs. For short, we sometimes call it a +@dfn{prover}, although we always have in mind an interactive system +rather than a fully automated theorem prover.} developed at the LFCS in +the University of Edinburgh. It works best under XEmacs, but can also +be used with FSF 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@footnote{A @dfn{proof script} is a sequence of commands + which constructs a proof, usually stored in a file.} + 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 +@code{proofgen@@dcs.ed.ac.uk}. + +If your chosen proof assistant isn't supported, read the accompanying +@i{Adapting Proof General} manual to find out how to configure PG for a +new prover. + +@menu +* Quick start guide:: +* Features of Proof General:: +* Supported proof assistants:: +* Prerequisites for this manual:: +* Organization of this manual:: +@end menu + + + + +@node Quick start guide +@section Quick start guide + +Proof General may have been installed for you already. If so, when you +visit a proof script file for your proof assistant, the corresponding +Proof General mode will be invoked automatically: +@multitable @columnfractions .3 .3 .4 +@item @b{Prover} @tab @b{Extensions} @tab @b{Mode} +@item LEGO @tab @file{.l} @tab @code{lego-mode} +@item Coq @tab @file{.v} @tab @code{coq-mode} +@item Isabelle @tab @file{.thy},@file{.ML} @tab @code{isa-mode} +@item Isabelle/Isar @tab @file{.thy} @tab @code{isar-mode} +@item HOL98 @tab @file{.sml} @tab @code{hol98-mode} +@end multitable +You can also invoke the mode command directly, e.g., type +@kbd{M-x lego-mode}, to turn a buffer into a lego script buffer. + +You'll find commands to process the proof script are available from the +toolbar, menus, and keyboard. Type @kbd{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 also start the proof assistant directly with the +menu command "Start proof assistant". + +To follow an example use of Proof General on a LEGO proof, +@pxref{Walkthrough example in LEGO}. If you know the syntax for proof +scripts in another theorem prover, you can easily adapt the details +given there. + +If Proof General has not already been installed, you should insert the +line: +@lisp + (load "@var{proof-general-home}/generic/proof-site.el") +@end lisp +into your @file{~/.emacs} file, where @var{proof-general-home} is the +top-level directory that was created when Proof General was unpacked. + +@xref{Obtaining and Installing}, if you need more +information. + + +@node Features of Proof General +@section Features of Proof General +@cindex Features +@cindex Why use Proof General? + +Why would you want to use Proof General? + +@c FIXME: would like to keep this synched with web page, really. +@c but web page needs extra markup. + +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! + +@itemize @bullet +@item @i{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 the user. Communication takes + place via three buffers (Emacs text widgets). +Communication takes place via three buffers. The @dfn{script +buffer} holds input, the commands to construct a proof. The @dfn{goals +buffer} displays the current list of subgoals to be solved. The +@dfn{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, @pxref{Summary of Proof General buffers} +and @pxref{Display customization}. + + +@item @i{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 @emph{asserting} or +@emph{retracting} parts of a proof script, which alters the coloured +regions. + +For more details, @pxref{Basic Script Management}, +@ref{Script processing commands}, +and @ref{Advanced Script Management}. +@item @i{Script editing mode}@* +Proof General provides useful facilities for editing proof scripts, +including syntax hilighting 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, @pxref{Script editing commands}, +and @ref{Script processing commands}. +@item @i{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, @pxref{Toolbar commands}, @ref{Proof assistant +commands}, and @ref{Customizing Proof General}. + +@item @i{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 appropriate 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. +@c Proof General expects to parse +@c term-structure annotations on the output syntax of the prover. +@c It uses these to construct a message to the prover indicating +@c where the user has clicked, and the proof assistant can +@c response with a suggested tactic. +@end itemize + + +@node Supported proof assistants +@section Supported proof assistants + +Proof General comes ready-customized for these proof assistants: + +@c FLAG VERSIONS HERE +@itemize @bullet +@item +@b{LEGO Proof General} for LEGO Version 1.3.1@* +@xref{LEGO Proof General}, for more details. +@item +@b{Coq Proof General} for Coq Version 6.3@* +@xref{Coq Proof General}, for more details. +@item +@b{Isabelle Proof General} for Isabelle99-1@* +@xref{Isabelle Proof General}, for more details. +@item +@b{Isabelle/Isar Proof General} for Isabelle99-1@* +@xref{Isabelle Proof General}, and documentation supplied with +Isabelle for more details. +@item +@b{HOL Proof General} for HOL98@* +@xref{HOL Proof General}, for more details. +@end itemize +Proof General is designed to be generic, so if you know how +to write regular expressions, you can make: +@itemize @bullet +@item +@b{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 @i{Adapting Proof General}. +@end itemize +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. + +@node Prerequisites for this manual +@section Prerequisites for this manual +@cindex Meta +@cindex Alt +@cindex key sequences + +This manual assumes that you understand a little about using Emacs, for +example, switching between buffers using @kbd{C-x b} and understanding +that a key sequence like @kbd{C-x b} means "control with x, followed by b". +A key sequence like @kbd{M-z} means "meta with z". (@key{Meta} may be +labelled @key{Alt} 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 use the +interface to @emph{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, +@pxref{How to customize}. @inforef{Easy customization, ,(xemacs)}, +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 @kbd{C-h} and find out +everything! Here are some useful commands: + +@table @asis +@item @kbd{C-h i} +@code{info} +@item @kbd{C-h m} +@code{describe-mode} +@item @kbd{C-h b} +@code{describe-bindings} +@item @kbd{C-h f} +@code{describe-function} +@item @kbd{C-h v} +@code{describe-variable} +@end table + + +@node Organization of this manual +@section Organization of this manual + +This manual covers the user-level view and customization of Proof +General. The accompanying @i{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 @file{INSTALL} and +@file{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. + + + + + + + +@c +@c CHAPTER: Basic Script Management +@c +@node Basic Script Management +@chapter 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. + +@menu +* Walkthrough example in LEGO:: +* Proof scripts:: +* Script buffers:: +* Summary of Proof General buffers:: +* Script editing commands:: +* Script processing commands:: +* Toolbar commands:: +* Proof assistant commands:: +@end menu + +@node Walkthrough example in LEGO +@section Walkthrough example in LEGO + +Here's a short example in LEGO to see how script management is used. +The file you are asked to type below is included in the distribution as +@file{lego/example.l}. If you're not using LEGO, substitute some lines +from a simple proof for your proof assistant, or consult the file +called something like @file{foo/example.foo} for proof assistant Foo. + +This walkthrough is keyboard based, but you could easily 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. + +@itemize @bullet +@item +First, find a new file by @kbd{C-x C-f} and typing as the filename +@file{example.l}. This should load LEGO Proof General and the toolbar +and Proof General menus will appear. You should have an empty buffer +displayed. +@end itemize + +The notation @kbd{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 @code{File} menu of Emacs. The remaining commands +used will be on the @code{Proof-General} menu. + +If you're not using LEGO, 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. + +@itemize @bullet +@item +Turn on @dfn{electric terminator} by typing @kbd{C-c ;} and +enter: +@lisp +Module example Import lib_logic; +@end lisp +This first command defines a file header and tells LEGO to use logic; +these steps are usually not necessary in other proof assistants. +@end itemize + +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. You can customize Proof General to +enable it everytime if you want, @xref{Customizing Proof General}. In +XEmacs, this is particularly easy: just use the menu item @code{Options +-> Save Options} to save some common options while using Proof General. + +The @code{Module} command should now be lit in pink (or inverse video if +you don't have a colour display). As LEGO imports each module, a line +will appear in the minibuffer showing the creation of context +marks. Eventually the command should turn blue, indicating that LEGO has +successfully processed it. + +@itemize @bullet +@item +Next type (on a new line if you like): +@lisp +Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A); +@end lisp +@end itemize + +The goal should be displayed in the goals buffer. + +@itemize @bullet +@item +Now type: +@lisp +Intros; +@end lisp +@end itemize +This will update the goals buffer. + +But whoops! That was the wrong command. + +@itemize @bullet +@item +Press @kbd{C-c C-BS} to pretend that didn't happen. +@end itemize +Note: @kbd{BS} means the backspace key. This key press sends an undo +command to LEGO, and deletes the @code{Intros;} command from the proof +script. If you just want to undo without deleting, you can type +@kbd{C-c C-u} instead, or use the toolbar navigation button. + +@itemize @bullet +@item +Instead, let's try: +@lisp +intros; andI; +@end lisp +We've used the conjunction-introduction rule. + +To finish off, use these commands: +@lisp +Refine H; intros; Immed; Refine H; intros; Immed; +@end lisp +@end itemize +Now you should see LEGO display the QED message. + +@itemize @bullet +@item +Finally, type: +@lisp +Save bland_commutes; +@end lisp +@end itemize + +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. This reflects +the fact that LEGO has thrown away the history of the proof, so if we +want to undo now, the whole proof must be retracted. + +@itemize @bullet +@item +Suppose we decide to call the goal something more sensible. Move the +cursor up into the locked region, somewhere between @samp{Goal} and +@samp{Save}, enter @kbd{C-c C-RET}. +@end itemize + +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 @kbd{C-c C-RET} moves the end of the locked region to the +cursor position, sending undoing commands or proof commands as +necessary. + +@itemize @bullet +@item +Now correct the goal name, for example: +@lisp +Goal and_commutes: @{A,B:Prop@} (and A B) -> (and B A); +@end lisp +Move the cursor to the end of the buffer, and +type @kbd{C-c C-RET} again. +@end itemize + +Proof General queues the commands for processing and executes them one +by one. You should see the proof turn pink, then quickly command by +command it is turned blue. The progress of pink to blue can be +much slower with long and complicated proofs! + + + +@node Proof scripts +@section Proof scripts +@cindex proof script +@cindex scripting + +A @dfn{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 +@i{interactive} proof assistants, where the mode of working is usually a +dialogue between the human and the proof assistant. + +Primitive interfaces for proof assistants simply present a @dfn{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 @dfn{replay} the proof +script to prove the theorem again. +@c Re-playing a proof script is a non-interactive procedure, +@c since it is supposed to succeed. + +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. +@c developing them in proof script files. + +@dfn{Scripting} is the process of building up a proof script file or +replaying a proof. When scripting, 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. Regions of the proof script are analysed +based on their syntax and the behaviour of the proof assistant after each +proof command. + + +@node Script buffers +@section Script buffers +@cindex script buffer +@cindex proof script mode + +A @dfn{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 @dfn{proof-mode}). + + +A script buffer is divided into three regions: @emph{locked}, +@emph{queue} and @emph{editing}. The proof commands +in the script buffer can include a number of +@emph{Goal-save sequences}. + +@menu +* Locked queue and editing regions:: +* Goal-save sequences:: +* Active scripting buffer:: +@end menu + + +@node Locked queue and editing regions +@subsection Locked, queue, and editing regions +@cindex Locked region +@cindex Queue region +@cindex Editing region +@cindex blue text +@cindex pink text + + +The three regions that a script buffer is divided into are: @c + +@itemize @bullet +@item The @emph{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. + +@item The @emph{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. + +@item The @emph{editing} region, which contains the commands the user is working +on, and can be edited as normal Emacs text. +@end itemize + +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: @emph{assertion} (or processing) and +@emph{retraction} (or undoing). + +@cindex Assertion +@strong{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. + +@cindex Retraction +@strong{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, +@xref{Script processing commands}. + + +@node Goal-save sequences +@subsection Goal-save sequences +@cindex goal +@cindex save +@cindex 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 @dfn{goal} command to the +corresponding @dfn{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 assumes that the proof script has a series of +proofs which look something like this: +@lisp + goal @var{mythm} is @var{G} + @dots{} + save theorem @var{mythm} +@end lisp +interspersed with comments, definitions, and the like. Of course, the +exact syntax and terminology will depend on the proof assistant you use. + +The name @var{mythm} can appear in a menu for the proof script to help +quickly find a proof (@pxref{Support for function menus}). + +@c Proof General recognizes the goal-save sequences in proof scripts. +@c once a goal-save region has been fully processed by the proof assistant, +@c it is treated as atomic when undoing proof steps. This reflects the +@c fact that most proof assistants discard the history of a proof once a it +@c is completed or once a new proof is begun. + + +@node Active scripting buffer +@subsection Active scripting buffer +@cindex 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 @dfn{active scripting buffer}. + +The active scripting buffer has a special indicator: the word +@code{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 @kbd{C-c C-s}. + +@table @asis +@item @kbd{C-c C-s} +@code{proof-toggle-active-scripting} +@end table + +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 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 @code{.ML} script +file and a @code{.thy} theory file which defines its theory. + +If you have a partly processed scripting buffer and use @kbd{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, +@code{Scripting incomplete in buffer myproof.l, retract?} +or if you want to process the remainder of the active buffer, +@code{Completely process buffer myproof.l instead?} +before you can start scripting in a new buffer. If you refuse to do +either, Proof General will give an error message: +@code{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.@footnote{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.} Second, we want to interface +with file management in the proof assistant. Proof General assumes that +a proof assistant may have a notion of which files have been processed, +but that it will only record files that have been @i{completely} +processed. For more explanation of the handling of multiple files, +@xref{Switching between proof scripts}. + +@c TEXI DOCSTRING MAGIC: proof-toggle-active-scripting +@deffn Command proof-toggle-active-scripting &optional arg +Toggle active scripting mode in the current buffer.@* +With @var{arg}, turn on scripting iff @var{arg} is positive. +@end deffn + + + + +@node Summary of Proof General buffers +@section Summary of Proof General buffers +@cindex shell buffer +@cindex goals buffer +@cindex response buffer +@cindex proof by pointing + +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. + +@itemize @bullet +@item The @dfn{proof shell buffer} is an Emacs shell buffer + used to run your proof assistant. Usually it is hidden from view + (but @pxref{Escaping script management}). + Communication with the proof shell takes place via two or three + intermediate buffers. +@item A @dfn{script buffer}, as we have explained, is a buffer for editing a + proof script. The @dfn{active scripting buffer} is the script buffer + which is currently being used to send commands to the proof shell. +@item The @dfn{goals buffer} displays the list of subgoals to be + solved for a proof in progress. During a proof it is usually + displayed together with the script buffer. + The goals buffer has facility for @dfn{proof-by-pointing}. +@item The @dfn{response buffer} displays other output from the proof + assistant, for example error messages or informative messages. + The response buffer is displayed whenever Proof General puts + a new message in it. +@end itemize + +Normally Proof General will automatically reveal and hide the goals and +response buffers as necessary during scripting. However there are ways +to customize the way the buffers are displayed (@pxref{Display +customization}). + +The menu @code{Proof General -> Buffers} provides a convenient way to +display or switch to one of the four buffers: active scripting, goals, +response, or shell. + +@c When +@c Proof General sees an error in the shell buffer, it will highlight the +@c error and display the buffer automatically. + + +@c This facility was not added: +@c +@c Optionally, the goals buffer and script buffer can be identified +@c @pxref{Identify goals and response}. The disadvantage of this is that +@c the goals display can be replaced by other messages, so you must ask for +@c it to be refreshed. The advantage is that it is simpler to deal with +@c fewer Emacs buffers. + + + +@node Script editing commands +@section 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. + +@findex indent-for-tab-command +@vindex proof-script-indent +Indentation is controlled by the user option @code{proof-script-indent} +(@pxref{User options}). When indentation is enabled, Proof General +will indent lines of proof script with the usual Emacs functions, +particularly @kbd{TAB}, @code{indent-for-tab-command}. +@c FIXME: remove when indentation is fixed. +Unfortunately, indentation in Proof General @value{version} is somewhat +slow. Therefore with large proof scripts, we recommend +@code{proof-script-indent} is turned off. + +Here are the commands for moving around in a proof script, +with their default key-bindings: +@kindex C-c C-a +@kindex C-c C-e +@kindex C-c C-. +@table @kbd +@item C-c C-a +@code{proof-goto-command-start} +@item C-c C-e +@code{proof-goto-command-end} +@item C-c C-. +@code{proof-goto-end-of-locked} +@end table + +@c TEXI DOCSTRING MAGIC: proof-goto-command-start +@deffn Command proof-goto-command-start +Move point to start of current (or final) command of the script. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-goto-command-end +@deffn Command proof-goto-command-end +Set point to end of command at point. +@end deffn + +@vindex proof-terminal-char +The variable @code{proof-terminal-char} is a prover-specific character +to terminate proof commands. LEGO and Isabelle use a semicolon, +@samp{;}. Coq employs a full-stop @samp{.}. + +@c TEXI DOCSTRING MAGIC: proof-goto-end-of-locked +@deffn Command proof-goto-end-of-locked &optional switch +Jump to the end of the locked region, maybe switching to script buffer.@* +If interactive or @var{switch} is non-nil, switch to script buffer first. +@end deffn + +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 is a useful mouse binding for copying the +highlighted command under the mouse: + +@kindex C-button1 +@table @kbd +@item C-button1 +@code{proof-mouse-track-insert} +@end table + +@c TEXI DOCSTRING MAGIC: proof-mouse-track-insert + + +@deffn Command proof-mouse-track-insert event +Copy highlighted command under the mouse to point. Ignore comments.@* +If there is no command under the mouse, behaves like @code{mouse-track-insert}. +@end deffn +Read the documentation in Emacs to find out about the normal behaviour +of @code{proof-mouse-track-insert}, if you don't already know what it +does. + + +@node Script processing commands +@section Script processing commands +@kindex C-c C-n +@kindex C-c C-u +@kindex C-c C-BS +@kindex C-c C-b +@kindex C-c C-r +@kindex C-c C-RET +@cindex prefix argument + +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 @code{Proof Process Busy!} if you try to +assert or retract when the queue is being processed.@footnote{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.} + +@table @kbd +@item C-c C-n +@code{proof-assert-next-command-interactive} +@item C-c C-u +@code{proof-undo-last-successful-command} +@item C-c C-BS +@code{proof-undo-and-delete-successful-command} +@item C-c C-RET +@code{proof-goto-point} +@item C-c C-b +@code{proof-process-buffer} +@item C-c C-r +@code{proof-retract-buffer} +@item C-c @var{terminator-character} +@code{proof-electric-terminator-toggle} +@end table + +The last command, @code{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 @kbd{C-c ;}, +for Coq, use @kbd{C-c .}. This not really a script processing +command. Instead, if enabled, it causes subsequent key presses of +@kbd{;} or @kbd{.} to automatically activate +@code{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 @kbd{C-c C-b} +(@code{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. + +@c TEXI DOCSTRING MAGIC: proof-assert-next-command-interactive +@deffn Command proof-assert-next-command-interactive +Process until the end of the next unprocessed command after point.@* +If inside a comment, just process until the start of the comment. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-undo-last-successful-command +@deffn Command proof-undo-last-successful-command +Undo last successful command at end of locked region. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-undo-and-delete-last-successful-command +@deffn Command proof-undo-and-delete-last-successful-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-pointing +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 @samp{yank} and similar commands to retrieve the +deleted text. +@end deffn + + +@c TEXI DOCSTRING MAGIC: proof-goto-point +@deffn Command proof-goto-point +Assert or retract to the command at current position.@* +Calls @code{proof-assert-until-point} or @code{proof-retract-until-point} as +appropriate. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-process-buffer +@deffn Command proof-process-buffer +Process the current (or script) buffer, and maybe move point to the end. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-retract-buffer +@deffn Command proof-retract-buffer +Retract the current buffer, and maybe move point to the start. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-electric-terminator-toggle +@deffn Command proof-electric-terminator-toggle arg +Toggle @samp{@code{proof-electric-terminator-enable}}. With @var{arg}, turn on iff ARG>0.@* +This function simply uses @code{customize-set-variable} to set the variable. +It was constructed with @samp{@code{proof-deftoggle-fn}}. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-assert-until-point-interactive +@deffn Command proof-assert-until-point-interactive +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. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-retract-until-point-interactive +@deffn Command proof-retract-until-point-interactive &optional delete-region +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 (@var{delete-region} non-nil), also +delete the retracted region from the proof-script. +@end deffn + +As experienced Emacs users will know, a @i{prefix argument} is a numeric +argument supplied by some key sequence typed before a command key +sequence. You can supply a specific number by typing @key{Meta} with +the digits, or a ``universal'' prefix of @kbd{C-u}. See +@inforef{Arguments, ,(xemacs)} for more details. Several Proof General +commands, like @code{proof-retract-until-point-interactive}, may accept +a @i{prefix argument} to adjust their behaviour somehow. + + +@node Proof assistant commands +@section Proof assistant commands +@kindex C-c C-p +@kindex C-c C-h +@kindex C-c C-c +@kindex C-c C-v +@kindex C-c C-f +@kindex C-c C-t + +There are several commands for interacting with the proof assistant away +from a proof script. Here are the key-bindings and functions. + +@table @kbd +@item C-c C-l +@code{proof-display-some-buffers} +@item C-c C-p +@code{proof-prf} +@item C-c C-t +@code{proof-ctxt} +@item C-c C-h +@code{proof-help} +@item C-c C-f +@code{proof-find-theorems} +@item C-c C-c +@code{proof-interrupt-process} +@item C-c C-v +@code{proof-minibuffer-cmd} +@end table + + +@c TEXI DOCSTRING MAGIC: proof-display-some-buffers +@deffn Command proof-display-some-buffers +Display the reponse or goals buffer, toggling between them.@* +Also move point to the end of the response buffer. +If in three window or multiple frame mode, display both buffers. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-prf +@deffn Command proof-prf +Show the current proof state.@* +Issues a command to the assistant based on @code{proof-showproof-command}. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-ctxt +@deffn Command proof-ctxt +Show the current context.@* +Issues a command to the assistant based on @code{proof-context-command}. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-help +@deffn Command proof-help +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 @code{proof-info-command}. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-find-theorems +@deffn Command proof-find-theorems arg +Search for items containing given constants.@* +Issues a command based on @var{arg} to the assistant, using @code{proof-find-theorems-command}. +The user is prompted for an argument. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-interrupt-process +@deffn Command proof-interrupt-process +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. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-minibuffer-cmd +@deffn Command proof-minibuffer-cmd cmd +Prompt for a command in the minibuffer and send it to proof assistant.@* +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 copying terms, etc from +the script. + +If @samp{@code{proof-strict-state-preserving}} is set, and @samp{@code{proof-state-preserving-p}} +is configured, 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. + +@var{warning}: this command risks spoiling synchronization if the test +@samp{@code{proof-state-preserving-p}} is not configured, if it is +only an approximate test, or if @samp{@code{proof-strict-state-preserving}} +is off (nil). +@end deffn + +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. @xref{Escaping script management}. + +There are a few commands for stopping, starting, and restarting the +proof assistant process which have menu entries but no key-bindings. +As with any Emacs command, you can invoke these with @kbd{M-x}. + +Here's a tip: if you accidently kill one of the Proof General special +buffers (goals or response), exiting the proof assistant and restarting +it will solve the problem. + +@c TEXI DOCSTRING MAGIC: proof-shell-start +@deffn Command proof-shell-start +Initialise a shell-like buffer for a proof assistant. + +Also generates goal and response buffers. +Does nothing if proof assistant is already running. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-shell-restart +@deffn Command proof-shell-restart +Clear script buffers and send @code{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 +@code{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). +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-shell-exit +@deffn Command proof-shell-exit +Query the user and exit the proof process. + +This simply kills the @code{proof-shell-buffer} relying on the hook function +@code{proof-shell-kill-function} to do the hard work. +@end deffn + + + +@node Toolbar commands +@section 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 +@kbd{M-x}, as well as the toolbar. + +@c TEXI DOCSTRING MAGIC: proof-issue-goal +@deffn Command proof-issue-goal arg +Write a goal command in the script, prompting for the goal.@* +Issues a command based on @var{arg} to the assistant, using @code{proof-goal-command}. +The user is prompted for an argument. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-issue-save +@deffn Command proof-issue-save arg +Write a save/qed command in the script, prompting for the theorem name.@* +Issues a command based on @var{arg} to the assistant, using @code{proof-save-command}. +The user is prompted for an argument. +@end deffn + + + + +@c +@c CHAPTER: Proof by Pointing +@c +@node Proof by Pointing +@chapter 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 proof by pointing support for Proof General in another proof +assistant, please petition the developers of that proof assistant to +provide it! + +@menu +* Goals buffer commands:: +@end menu + +@node Goals buffer commands +@section 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: + +@table @kbd +@item button2 +@code{pbp-button-action} +@item C-button2 +@code{proof-undo-and-delete-last-successful-command} +@item button3 +@code{pbp-yank-subterm} +@end table + +Where @kbd{button2} indicates the middle mouse button, and @kbd{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 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. + +@c TEXI DOCSTRING MAGIC: pbp-button-action + +@deffn Command pbp-button-action event +Construct a proof-by-pointing command based on the mouse-click @var{event}.@* +This function should be bound to a mouse button in the Proof General +goals buffer. + +The @var{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. +@end deffn + +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. + +The right-hand mouse button provides this convenient way to copy +subterms from the goals buffer, using the function +@code{pbp-yank-subterm}. + +@c TEXI DOCSTRING MAGIC: pbp-yank-subterm + +@deffn Command pbp-yank-subterm event +Copy the subterm indicated by the mouse-click @var{event}.@* +This function should be bound to a mouse button in the Proof General +goals buffer. + +The @var{event} is used to find the smallest subterm around a point. The +subterm is copied to the @code{kill-ring}, and immediately yanked (copied) +into the current buffer at the current cursor position. + +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. +@end deffn +@c Proof General expects to parse +@c term-structure annotations on the output syntax of the prover. +@c It uses these to construct a message to the prover indicating +@c where the user has clicked, and the proof assistant can +@c response with a suggested tactic. + + + + + +@c +@c CHAPTER: Advanced Script Management +@c +@node Advanced Script Management +@chapter Advanced Script Management +@cindex Multiple Files + +If you are working with large proof developments, you may want to know +about the advanced script management features of Proof General covered +in this chapter. + +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 proof assistant. Proof General provides +you with several escape mechanisms if you want to do this. + +@menu +* Switching between proof scripts:: +* View of processed files :: +* Retracting across files:: +* Asserting across files:: +* Automatic multiple file handling:: +* Escaping script management:: +@end menu + +@node Switching between proof scripts +@section Switching between proof scripts +@cindex 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@footnote{The suffix may depend of +the specific proof assistant you are using e.g, LEGO's proof script +files have to end with @file{.l}.} @file{HSound.l}. It +depends on a number of other 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 +@file{sos.l} and retract to where changes are required. Then, using +script management, you want to develop some more basic theory in +@file{sos.l}. 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 @file{HSound.l} and replay to the +point you got stuck previously. + +Some hours (or days) later 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. + +@node View of processed files +@section 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@footnote{For example, LEGO generates additional +compiled (optimised) proof script files for efficiency.} 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 @emph{beginning} of the buffer. +@c This isn't strictly true, is it? We lock off buffers atomically, +@c but spans in them to start with stay there. (Only meaningful +@c for reading currently active scripting file) + +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 they 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 @emph{early locking} when processing a file begins (e.g. LEGO) or +@emph{late locking} when processing a file ends (e.g. Isabelle). + +With @emph{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 @emph{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. + + + +@c only true for LEGO! +@c If the proof assistant is not happy with the script and +@c complains with an error message, the buffer will still be marked as +@c having been completely processed. Sorry. You need to visit the +@c troublesome file, retract (which will always retract to the beginning of +@c the file) and debug the problem e.g., by asserting all of the buffer +@c under the supervision of Proof General, see @ref{Script processing +@c commands}. + + +@node Retracting across files +@section Retracting across files +@cindex Retraction + +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 @pxref{Script processing commands}. 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. + +@node Asserting across files +@section Asserting across files +@cindex Assertion + +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, @pxref{Script processing +commands}. 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. + + +@node Automatic multiple file handling +@section 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 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 @emph{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 @i{Handling multiple files} in +the @i{Adapting Proof General} manual. + + + +@node Escaping script management +@section Escaping script management +@cindex Shell + +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, @pxref{Proof assistant commands}. + +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 @file{comint.el} distributed with your +version of Emacs). You can switch to it using the menu: + +@lisp + Proof-General -> Buffers -> Shell +@end lisp + +@b{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 from 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: + +@table @kbd +@item C-c C-z +@code{proof-frob-locked-end} +@end table + +This command is disabled by default, to protect novices using it +accidently. + +If @code{proof-frob-locked-end} does not work, you will need to restart +script management altogether (@pxref{Proof assistant commands}). + +@c TEXI DOCSTRING MAGIC: proof-frob-locked-end +@deffn Command proof-frob-locked-end +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. +@end deffn + + +@node Support for other Packages +@chapter Support for other Packages + +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 supported, as a convention. + +The packages currently supported are +@code{font-lock}, +@code{x-symbol}, +@code{func-menu}, +@code{outline-mode}, +@code{completion}, +and @code{etags}. + + +@menu +* Syntax highlighting:: +* X-Symbol support:: +* Support for function menus:: +* Support for outline mode:: +* Support for completion:: +* Support for tags:: +@end menu + +@node Syntax highlighting +@section Syntax highlighting +@vindex lego-mode-hooks +@vindex coq-mode-hooks +@vindex isa-mode-hooks +@cindex font lock +@cindex colour +@c Proof General specifics + +Proof script buffers are decorated (or @i{fontified}) with colours, bold +and italic fonts, etc, according to the syntax of the proof language and +the settings for @code{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 +@code{font-lock}. + +In XEmacs, fontification is automatically turned on. To automatically +switch on fontification in FSF GNU Emacs 20.4, you may need to engage +@code{M-x global-font-lock-mode}. The old mechanism of adding hooks to +the mode hooks (@code{lego-mode-hooks}, @code{coq-mode-hooks}, etc) is +no longer recommended; it should not be needed in latest Emacs versions +which have more flexible customization. + +Fontification for output is controlled by a separate switch in Proof +General. Set @code{proof-output-fontify-enable} to @code{nil} if you +don't want the output from your proof assistant to be fontified +according to the setting of @code{font-lock-keywords} in the proof +assistant specific portion of Proof General. @xref{User options}. + +By the way, the choice of colour, font, etc, for each kind of markup is +fully customizable in Proof General. Each @emph{face} (Emacs +terminology) controlled by its own customization setting. +You can display a list of all of them using the customize +menu: +@lisp +Proof General -> Customize -> Faces -> Proof Faces. +@end lisp + + +@node X-Symbol support +@section X-Symbol support +@cindex real symbols +@cindex X-Symbols +@cindex Greek letters +@cindex logical symbols +@cindex mathematical symbols + +The X-Symbol package displays characters from a variety of fonts in +Emacs buffers, automatically converting between codes for special +characters and @i{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. + +You will be able to enable X-Symbol support if you have installed the +X-Symbol package and support has been provided in Proof General for a +token language for your proof assistant. +The X-Symbol package is available from +@uref{http://www.fmi.uni-passau.de/~wedler/x-symbol/}. + +Notice that for proper symbol support, the proof assistant needs to have +a special @i{token language}, or a special character set, to use +symbols. In this case, the proof assistant will output, and accept as +input, tokens like @code{\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 character sequences such as @code{-->} with symbols. +The only problem with this hack is that it can cause surprising results, +when you really want character sequences instead of, for example, Greek +letters! + +@c @xref{Configuring X-Symbol}, for notes about how to configure +@c a proof assistant to use X-Symbol in Proof General. + + +@node Support for function menus +@section Support for function menus +@vindex proof-goal-with-hole-regexp +@cindex func-menu +@cindex fume-func + +The Emacs package @code{func-menu} (formerly called @code{fume-func}) is +a handy facility to make a menu from the names of entities declared in a +buffer. Proof General configures @code{func-menu} so that you can +quickly jump to particular proofs in a script buffer. (This is done +with the configuration variables @code{proof-goal-with-hole-regexp} and +@code{proof-save-with-hole-regexp}.) +@c , @pxref{Proof script mode} for further details. + +If you want to use function menu, you can simply select "Function menu" +from the Proof General menu, or type @kbd{M-x function-menu}. + +Although the package is distributed with XEmacs, it is not enabled by +default every time you visit a buffer. To enable it by default +(i.e. avoid typing @code{M-x function-menu}), you should find the file +@file{func-menu.el} and follow the instructions there. + +FSF Emacs 20.4 does not have the function menu library built in, but you +may be able to download it from the elisp archives. A similar mode +which is supported is @code{imenu}, also in XEmacs. Proof General would +be grateful if anyone can send patches for using @code{imenu} +as an alternative to function menu. + + +@node Support for outline mode +@section Support for outline mode +@cindex outline mode + +Proof General configures Emacs variables (@code{outline-regexp} and +@code{outline-heading-end-regexp}) so that 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, +@pxref{Goal-save sequences}. If you want to use @code{outline} to hide +parts of the proof script in the @emph{locked} region, you need to disable +@code{proof-strict-read-only}. + +Use @kbd{M-x outline-minor-mode} to turn on outline minor mode. +Functions for navigating, hiding, and revealing the proof script are +available in menus. + +See @inforef{Outline Mode, ,(xemacs)} for more information about +outline mode. + +@node Support for completion +@section Support for completion +@cindex completion + +You might find the @emph{completion} facility of Emacs useful when +you're using Proof General. The key @kbd{C-RET} is defined to invoke +the @code{complete} command. Pressing @kbd{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 automatically. 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 @code{@emph{PA}-completion-table} holds the list of +identifiers for a proof assistant. The function +@code{proof-add-completions} adds these into the completion +database. + +@c TEXI DOCSTRING MAGIC: PA-completion-table +@defvar PA-completion-table +List of identifiers to use for completion for this proof assistant.@* +Completion is activated with C-return. + +If this table is empty or needs adjusting, please make changes using +@samp{@code{customize-variable}} and send suggestions to proofgen@@dcs.ed.ac.uk. +@end defvar + +The completion facility uses a library @file{completion.el} which +usually ships with XEmacs and FSF Emacs, and supplies the +@code{complete} function. + +@c FIXME: edited from default. +@c NOT DOCSTRING MAGIC: complete +@deffn Command complete +Fill out a completion of the word before point. @* +Point is left at end. Consecutive calls rotate through all possibilities. +Prefix args: +@table @kbd +@item C-u +leave point at the beginning of the completion, not the end. +@item a number +rotate through the possible completions by that amount +@item 0 +same as -1 (insert previous completion) +@end table +See the comments at the top of @samp{completion.el} for more info. +@end deffn + + +@node Support for tags +@section Support for tags +@cindex 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 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 @kbd{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 (@file{legotags} and @file{coqtags}) for +making tags tables. For example, invoking @samp{coqtags *.v} produces a +file @file{TAGS} for all files @samp{*.v} in the current +directory. Invoking @samp{coqtags `find . -name \*.v`} produces a file +@file{TAGS} for all files ending in @samp{.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 @kbd{M-tab} to run @code{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 @file{.emacs} file: +@lisp +(add-hook 'proof-mode-hook + (lambda () (local-set-key '(meta tab) 'tag-complete-symbol))) +@end lisp +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 completion, there are several other operations on tags. One +common one is replacing identifiers across all files using +@code{tags-query-replace}. For more information on how to use tags, +@inforef{Tags, ,(xemacs)}. + +To use tags for completion at the same time as the completion mechanism +mentioned already, you can use the command @kbd{M-x add-completions-from-tags-table}. + +@c TEXI DOCSTRING MAGIC: add-completions-from-tags-table + + +@deffn Command add-completions-from-tags-table +Add completions from the current tags table. +@end deffn +@node Hints and Tips +@chapter Hints and Tips + +Apart from the packages officially supported in Proof General, many. +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! + +@menu +* Using file variables:: +* Using abbreviations:: +@end menu + + +@node Using file variables +@section Using file variables +@cindex file variables + +A very convenient way to customize file-specific variables is to use the +File Variables (@inforef{File Variables, ,xemacs}). This feature of +Emacs allows to specify the values to use 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 @code{proof-prog-name} and +@code{compile-command} for each file. Here is an example for Coq users: +for the file @file{.../dir/bar/foo.v}, if you want Coq to be started +with the path @code{.../dir/theories/} added in the libraries path +(@code{"-I"} option), you can put at the end of @file{foo.v}: +@lisp + +(* + Local Variables: + coq-prog-name: "coqtop -emacs -full -I ../theories" + End: +*) +@end lisp + +That way the good command is called when the scripting starts in +@file{foo.v}. Notice that the command argument @code{"-I ../theories"} +is specific to the file @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 operation +automatically. + +Extending the previous example, if the makefile for @file{foo.v} is +located in directory @file{.../dir/}, you can add the right compile +command: + +@lisp +(* + Local Variables: + coq-prog-name: "coqtop -emacs -full -I ../theories" + compile-command: "make -C .. -k bar/foo.vo" + End: +*) +@end lisp + +And then the right call to make will be done if you use the @kbd{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. @inforef{File Variables, +,xemacs}. + + + +@node Using abbreviations +@section Using abbreviations + +A very useful package of Emacs supports automatic expansions of +abbreviations as you type, @inforef{Abbrevs, ,(xemacs)}. + +Proof General has no special support for abbreviations, we just mention +it here to encourage its use. For example, the proof assistant Coq has +many command strings that are long, such as ``Reflexivity,'' +``Inductive,'' ``Definition'' and ``Discriminate.'' Here is the +Coq Proof General author's suggested abbreviations for Coq: +@lisp +"assn" 0 "Assumption" +"ax" 0 "Axiom" +"coern" 0 "Coercion" +"cofixpt" 0 "CoFixpt" +"coindv" 0 "CoInductive" +"constr" 0 "Constructor" +"contradn" 0 "Contradiction" +"defn" 0 "Definition" +"discr" 0 "Discriminate" +"extrn" 0 "Extraction" +"fixpt" 0 "Fixpoint" +"genz" 0 "Generalize" +"hypo" 0 "Hypothesis" +"immed" 0 "Immediate" +"indn" 0 "Induction" +"indv" 0 "Inductive" +"injn" 0 "Injection" +"intn" 0 "Intuition" +"invn" 0 "Inversion" +"pmtr" 0 "Parameter" +"refly" 0 "Reflexivity" +"rmk" 0 "Remark" +"specz" 0 "Specialize" +"symy" 0 "Symmetry" +"thm" 0 "Theorem" +"transpt" 0 "Transparent" +"transy" 0 "Transitivity" +"trivial" 0 "Trivial" +"varl" 0 "Variable" +@end lisp + +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 presses @kbd{C-x a g} (@code{add-global-abbrev}) or +@kbd{C-x a i g} (@code{inverse-add-global-abbrev}). To enable expansion +of abbreviations, the @code{Abbrev} minor mode, type @kbd{M-x +abbrev-mode RET}. See the Emacs manual for more details. + + + + + + +@node Customizing Proof General +@chapter Customizing Proof General +@cindex Customization + + +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 +@emph{adapting}. See the @i{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: +@itemize @bullet +@item Settings that apply @emph{globally} to all proof assistants. +@item those that can be adjusted for each proof assistant @emph{individually}. +@end itemize +The first sort have names beginning with @code{proof-}. The second sort +have names which begin with a symbol corresponding to the proof +assistant: for example, @code{isa-}, @code{coq-}, etc. The symbol is +the root of the mode name. @xref{Quick start guide}, for a table of the +supported modes. To stand for an arbitrary proof assistant, we write +@code{@emph{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 individual customization +settings not available in other proof assistants. See the chapters +covering each assistant for details of those settings. + + +@menu +* Basic options:: +* How to customize:: +* Display customization:: +* User options:: +* Changing faces:: +* Tweaking configuration settings:: +@end menu + +@node Basic options +@section Basic options + +Proof General has some common options which you can toggle directly from +the menu: +@lisp + Proof-General -> Options +@end lisp +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. @xref{Display customization}. + +To save the current settings, use the usual Emacs save options command, +for XEmacs on the menu: +@lisp + Options -> Save Options +@end lisp +or @code{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. + + +@node How to customize +@section How to customize +@cindex Using Customize +@cindex Emacs customization library + +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: +@lisp + Proof-General -> Customize +@end lisp + +Using the customize facility is straightforward. You can select the +setting to customize via the menus, or with @code{M-x +customize-variable}. When you have 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 @var{set}, @var{save} and +@var{done}. You must use one of @var{set} or @var{save} to get any +effect. The @var{save} button stores the setting in your @file{.emacs} +file. In XEmacs, the menu item @code{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 "@code{proof}-" or +similar prefixes are omitted. Also, some of the option settings may +have more descriptive names (for example, @var{on} and @var{off}) than +the low-level lisp values (non-@code{nil}, @code{nil}) which are +mentioned in this chapter. These features make customize rather more +friendly than raw lisp. + +You can also access the customize settings for Proof General from +other (non-script) buffers. In XEmacs, the menu path is: +@lisp + Options -> Customize -> Emacs -> External -> Proof General +@end lisp +in XEmacs. In FSF GNU Emacs, use the menu: +@lisp + Help -> Customize -> Top-level Customization Group +@end lisp +and select the @code{External} and then @code{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 @kbd{M-x +load-library RET proof RET}. + +For more help with customize, see @inforef{Easy Customization, ,xemacs}. + + + +@node Display customization +@section Display customization +@cindex display customization +@cindex multiple windows +@cindex buffer display customization +@cindex frames +@cindex multiple frames +@cindex three-buffer interaction + +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. @code{*isabelle-goals*}) +or the response buffer (@code{*isabelle-response*}). Proof General +switches between these last two automatically. + +Proof General allows several ways to customize this default display +model. + +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 @code{proof-find-theorems} command at the same time as +the subgoal list. Set the user option @code{proof-dont-switch-windows} to +make Proof General keep both the goals and response buffer displayed. + +@c TEXI DOCSTRING MAGIC: proof-dont-switch-windows +@defopt proof-dont-switch-windows +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, 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. + +For single frame use this option may be inconvenient for +experienced Emacs users. + +The default value is @code{nil}. +@end defopt + +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 @code{proof-delete-empty-windows} helps you do this. + +@c TEXI DOCSTRING MAGIC: proof-delete-empty-windows +@defopt proof-delete-empty-windows +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 @code{'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 @code{nil}. +@end defopt +This option only has an effect when you have set +@code{proof-dont-switch-windows}. + +If you are working on a machine with a window system, you can use Emacs +to manage several @i{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 option +@c TEXI DOCSTRING MAGIC: proof-multiple-frames-enable + +@defopt proof-multiple-frames-enable +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 +@samp{@code{special-display-regexps}}. + +The default value is @code{nil}. +@end defopt +Multiple frames work best when @code{proof-delete-empty-windows} is off +and @code{proof-dont-switch-windows} is on. + + +@node User options +@section User options +@c Index entries for each option 'concept' +@cindex User options +@cindex Strict read-only +@cindex Query program name +@cindex Dedicated windows +@cindex Remote host +@cindex Toolbar follow mode +@cindex Toolbar disabling +@cindex Toolbar button enablers +@cindex Proof script indentation +@cindex Indentation +@cindex Remote shell +@cindex Running proof assistant remotely +@c @cindex formatting proof script + +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 @code{M-x edit-options} mechanism, or simply by +adding @code{setq}'s to your @file{.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. + +@c TEXI DOCSTRING MAGIC: proof-splash-enable +@defopt proof-splash-enable +If non-nil, display a splash screen when Proof General is loaded. + +The default value is @code{t}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-electric-terminator-enable +@defopt proof-electric-terminator-enable +If non-nil, use electric terminator mode.@* +If electric terminator mode is enabled, pressing a terminator will +automatically issue @samp{@code{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 @code{nil}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-toolbar-enable +@defopt proof-toolbar-enable +If non-nil, display Proof General toolbar for script buffers.@* +NB: the toolbar is only available with XEmacs. + +The default value is @code{t}. +@end defopt + +@c TEXI DOCSTRING MAGIC: PA-x-symbol-enable +@defopt PA-x-symbol-enable +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 @code{nil}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-output-fontify-enable +@defopt proof-output-fontify-enable +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 @code{font-lock-keywords} have been set for the +buffer modes). + +The default value is @code{t}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-strict-read-only +@defopt proof-strict-read-only +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!). + +If you change @code{proof-strict-read-only} during a session, you must +use the "Restart" button (or M-x @code{proof-shell-restart}) before +you can see the effect in buffers. + +The default value for @code{proof-strict-read-only} depends on which +version of Emacs you are using. In FSF Emacs, strict read only is buggy +when it used in conjunction with font-lock, so it is disabled by default. + +The default value is @code{strict}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-toolbar-use-button-enablers +@defopt proof-toolbar-use-button-enablers +If non-nil, toolbars buttons may be enabled/disabled automatically.@* +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. + +Notes: +* Toolbar enablers are only available with XEmacs 21 and later. +* With this variable nil, buttons do nothing when they would +otherwise be disabled. +* If you change this variable it will only be noticed when you +next start Proof General. +* The default value for XEmacs built for solaris is nil, because +of unreliabilities with enablers there. + +The default value is @code{t}. +@end defopt + +@c This one removed: proof-auto-retract + +@c TEXI DOCSTRING MAGIC: proof-query-file-save-when-activating-scripting +@defopt proof-query-file-save-when-activating-scripting +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 @code{t}. +@end defopt + +@c TEXI DOCSTRING MAGIC: PA-script-indent +@defopt PA-script-indent +If non-nil, enable indentation code for proof scripts. + +The default value is @code{t}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-one-command-per-line +@defopt proof-one-command-per-line +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 @code{nil}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-prog-name-ask +@defopt proof-prog-name-ask +If non-nil, query user which program to run for the inferior process. + +The default value is @code{nil}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-prog-name-guess +@defopt proof-prog-name-guess +If non-nil, use @samp{@code{proof-guess-command-line}} to guess @code{proof-prog-name}.@* +This option is compatible with @code{proof-prog-name-ask}. +No effect if @code{proof-guess-command-line} is nil. + +The default value is @code{nil}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-tidy-response +@defopt proof-tidy-response +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 @code{t}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-show-debug-messages +@defopt proof-show-debug-messages +Whether to display debugging messages in the response buffer.@* +If non-nil, debugging messages are displayed in the response giving +information about what Proof General is doing. +To avoid erasing the messages shortly after they're printed, +you should set @samp{@code{proof-tidy-response}} to nil. + +The default value is @code{nil}. +@end defopt + + +@c ******* NON-BOOLEANS ******* + +@c TEXI DOCSTRING MAGIC: proof-follow-mode +@defopt proof-follow-mode +Choice of how point moves with script processing commands.@* +One of the symbols: @code{'locked}, @code{'follow}, @code{'ignore}. + +If @code{'locked}, point sticks to the end of the locked region. +If @code{'follow}, point moves just when needed to display the locked region end. +If @code{'ignore}, point is never moved after movement commands or on errors. + +If you choose @code{'ignore}, you can find the end of the locked using +@samp{M-x @code{proof-goto-end-of-locked}}. + +The default value is @code{locked}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-auto-action-when-deactivating-scripting +@defopt proof-auto-action-when-deactivating-scripting +If @code{'retract} or @code{'process}, do that when deactivating scripting. + +With this option set to @code{'retract} or @code{'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 @code{nil}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-script-command-separator +@defopt proof-script-command-separator +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 +set to a space. + +The default value is @code{" "}. +@end defopt + +@c TEXI DOCSTRING MAGIC: proof-rsh-command +@defopt proof-rsh-command +Shell command prefix to run a command on a remote host. @* +For example, +@lisp + ssh bigjobs +@end lisp +Would cause Proof General to issue the command @samp{ssh bigjobs isabelle} +to start Isabelle remotely on our large compute server called @samp{bigjobs}. + +The protocol used should be configured so that no user interaction +(passwords, or whatever) is required to get going. + +The default value is @code{""}. +@end defopt + + + + +@node Changing faces +@section Changing faces + +The fonts and colours that Proof General uses are configurable. If you +alter faces through the customize menus (or the command @kbd{M-x +customize-face}), only the particular kind of display in use (colour +window system, monochrome window system, console, @dots{}) 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 +@code{font-lock-} faces (eg @code{font-lock-keyword-face}, +@code{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! + + +@c TEXI DOCSTRING MAGIC: proof-queue-face +@deffn Face proof-queue-face +Face for commands in proof script waiting to be processed. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-locked-face +@deffn Face proof-locked-face +Face for locked region of proof script (processed commands). +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-error-face +@deffn Face proof-error-face +Face for error messages from proof assistant. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-warning-face +@deffn Face proof-warning-face +Face for warning messages.@* +Warning messages can come from proof assistant or from Proof General itself. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-debug-message-face +@deffn Face proof-debug-message-face +Face for debugging messages from Proof General. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-declaration-name-face +@deffn Face proof-declaration-name-face +Face for declaration names in proof scripts.@* +Exactly what uses this face depends on the proof assistant. +@end deffn + + +@c TEXI DOCSTRING MAGIC: proof-tacticals-name-face +@deffn Face proof-tacticals-name-face +Face for names of tacticals in proof scripts.@* +Exactly what uses this face depends on the proof assistant. +@end deffn + +@c TEXI DOCSTRING MAGIC: proof-eager-annotation-face +@deffn Face proof-eager-annotation-face +Face for important messages from proof assistant. +@end deffn + +@c Maybe this detail of explanation belongs in the internals, +@c with just a hint here. +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. + + + + +@node Tweaking configuration settings +@section Tweaking configuration settings + +This section is a note for advanced users. + +Configuration settings are the per-prover customizations of Proof +General. These are not intended 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 when 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 +@code{prover-config}, or via the menu +@lisp + Proof-General -> Internals -> Prover Config +@end lisp + +One basic example of a setting you may like to tweak is: + +@c TEXI DOCSTRING MAGIC: proof-assistant-home-page +@defvar proof-assistant-home-page +Web address for information on proof assistant.@* +Used for Proof General's help menu. +@end defvar + +Most of the others are more complicated. For more details of the +settings, see @i{Adapting Proof General} for full details. To browse +the settings, you can look through the customization groups +@code{prover-config}, @code{proof-script} and @code{proof-shell}. The +group @code{proof-script} contains the configuration variables for +scripting, and the group @code{proof-shell} contains those for +interacting with the proof assistant. + +Unfortunately, although you can use the customization mechanism to set +and save these variables, 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 +assistant specific configurations. For example, +@code{proof-assistant-home-page} is set in the LEGO code from the value +of the customization setting @code{lego-www-home-page}. At present +there is no easy way to save changes to other configuration variables +across sessions, other than by editing 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 @code{@emph{PA}-} mechanism). +@c Please contact us if this proves to be a problem for any variable. + + + + +@c +@c CHAPTER: LEGO Proof General +@c +@node LEGO Proof General +@chapter LEGO Proof General +@cindex 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 @emph{must} start with a module declaration. If the proof script +buffer's file name is @file{fermat.l}, then it must commence with a +declaration of the form + +@lisp +Module fermat; +@end lisp + +If, in the development of the module @samp{fermat}, you require material +from other module e.g., @samp{lib_nat} and @samp{galois}, you need to +specify this dependency as part of the module declaration: + +@lisp +Module fermat Import lib_nat galois; +@end lisp + +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 previously 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 @samp{Forget}, @samp{ForgetMark}, @samp{KillRef}, +@samp{Load}, @samp{Make}, @samp{Reload} and @samp{Undo} again +@footnote{And please, don't even think of including those in your LEGO +proof script!}. You can concentrate on your actual proof developments. +Script management in Proof General will invoke the appropriate commands +for you. Proving with LEGO has never been easier. + +@menu +* LEGO specific commands:: +* LEGO tags:: +* LEGO customizations:: +@end menu + + +@node LEGO specific commands +@section 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: + +@kindex C-c C-a C-i +@kindex C-c C-a C-I +@kindex C-c C-a C-R +@table @kbd +@item C-c C-a C-i +intros +@item C-c C-a C-I +Intros +@item C-c C-a C-R +Refine +@end table + +@node LEGO tags +@section LEGO tags + +You +might want to ask your local system administrator to tag the directories +@file{lib_Prop}, @file{lib_Type} and @file{lib_TYPE} of the LEGO +library. See @ref{Support for tags}, for further details on tags. + + + +@node LEGO customizations +@section LEGO customizations + +We refer to chapter @ref{Customizing Proof General}, for an introduction +to the customisation mechanism. In addition to customizations at the +generic level, for LEGO you can also customize: + +@c TEXI DOCSTRING MAGIC: lego-tags +@defopt lego-tags +The directory of the @var{tags} table for the @var{lego} library + +The default value is @code{"/usr/lib/lego/lib_Type/"}. +@end defopt + +@c TEXI DOCSTRING MAGIC: lego-www-home-page +@defvar lego-www-home-page +Lego home page URL. +@end defvar + +@c We don't worry about the following for now. These are too obscure. +@c lego-indent +@c lego-test-all-name + +@c We also don't document any of the internal variables which have been +@c set to configure the generic Proof General and which the user should +@c not tamper with + + +@node Coq Proof General +@chapter Coq Proof General + +Coq 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. + +@menu +* Coq-specific commands:: +* Editing multiple proofs:: +* User-loaded tactics:: +@end menu + + +@node Coq-specific commands +@section Coq-specific commands +@kindex C-c C-a C-i +@kindex C-c C-a C-a +@kindex C-c C-a C-s +@kindex C-c C-a C-e +@kindex C-c C-a C-o + +Coq Proof General supplies the following key-bindings: +@table @kbd +@item C-c C-a C-i +Inserts ``Intros '' +@item C-c C-a C-a +Inserts ``Apply '' +@item C-c C-a C-s +Inserts ``Section '' +@item C-c C-a C-e +Inserts ``End <section-name>.'' (this should work well with nested sections). +@item C-c C-a C-o +Prompts for a SearchIsos argument. +@end table + +@node Editing multiple proofs +@section 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 lemmas 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 promoted immediately above the outermost +active proof. 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 the +full proof of that lemma is promoted. This is supported to any nesting +depth that Coq allows. + +@b{Special note:} this feature is disabled since version 3.0 because the +implementation was unreliable. (Patches to improve the code in +@file{coq.el} are welcome). + +@node User-loaded tactics +@section 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. + +Unfortunately, Coq Proof General does not currently support tactic +extension in Coq. When the user tries to retract across an extended +tactic in a script, the algorithm for calculating how far to undo does +not recognize the extension, and so the proof buffer and Coq are not +synchronized. + +Until this feature is incorporated into Coq Proof General, the user can +use C-c C-v to resynchronize. For example, if the user does C-c C-u to +move the point back past one extended tactic, he or she can type C-c C-v +``Undo 1.'' This then undoes the tactic that Proof General failed to +recognize. + + + + + + + +@c Sorry, there is currently very little specific documentation written for +@c Coq Proof General. If any Coq user would like to contribute, please send +@c a message to @code{proofgen@@dcs.ed.ac.uk}. + +@c Type @kbd{C-h C-m} to get a list of all Coq specific commands and +@c browse the customize menus to find out what customization +@c options there are for Coq. + + + +@c +@c CHAPTER: Isabelle Proof General +@c + +@node Isabelle Proof General +@chapter Isabelle Proof General +@cindex Isabelle Proof General + +Isabelle Proof General supports all major generic features of Proof +General, including integration with Isabelle's theory loader for proper +automatic multiple file handling. Only support for tags and +proof-by-pointing is missing. + +It is very important to note that there are actually two different +versions of Isabelle Proof General: for ``classic'' Isabelle and for +Isabelle/Isar. An old-style Isabelle theory typically consists of +@file{.thy} and correspondent @file{.ML} files, while Isabelle/Isar +theories usually have a new-style @file{.thy} only, which has a slightly +different syntax and may contain both definitions and proofs. + +While Isabelle is able to manage both classic and Isar theories at the +same time (the theory loader determines the source format +automatically), Proof General does @b{not} admit to work on both kinds +of Isabelle source files at the same time! Proof General treats +@code{isa} and @code{isar} as different instances; there is no way to +switch modes once Proof General has been started. + +The classic version of Isabelle Proof General includes a mode for +editing theory files taken from David Aspinall's Isamode interface, see +@uref{http://www.proofgeneral.org/~isamode}. Detailed documentation for +the theory file mode is included with @code{Isamode}, there are some +notes on the special functions available and customization settings +below. + +Note that in ``classic'' Isabelle, @file{.thy} files contain definitions +and declarations for a theory, while @file{.ML} contain proof scripts. +So most of Proof General's functions only make sense in @file{.ML} +files, and there is no toolbar and only a short menu for @file{.thy} files. + +In Isabelle/Isar, on the other hand, @file{.thy} files contain proofs as +well as definitions for theories, so scripting takes place there and you +see the usual toolbar and scripting functions of Proof General. + +The default Emacs mode setup of Proof General prefers the @code{isa} +version over @code{isar}. To load the Isabelle/Isar, you can set the +environment variable @code{PROOFGENERAL_ASSISTANTS=isar} before starting +Emacs in order to prevent loading of the classic Isabelle theory file. +Another way of selecting Isar is to put a special modeline like this: +@lisp + (* -*- isar -*- *) +@end lisp +near the top of your Isabelle/Isar @file{.thy} files (or at least, the +first file you visit). This Emacs feature overrides the default choice +of mode based on the file extension. + +Isabelle provides yet another way to invoke Proof General, including +additional means to select either version. The standard installation of +Isabelle makes the @code{isar} version of Proof General its default user +interface: running plain @code{Isabelle} starts an Emacs session with +Isabelle/Isar Proof General; giving an option @code{-I false} refers to +the classic version instead. The defaults may be changed by editing the +Isabelle settings, see the Isabelle documentation for details. + +@menu +* Classic Isabelle:: +* Isabelle/Isar:: +@end menu + +@node Classic Isabelle +@section Classic Isabelle +@cindex Classic Isabelle + +Proof General for classic Isabelle primarily manages @file{.ML} files +containing proof scripts. There is a separate mode for editing +old-style @file{.thy} files, which supports batch mode only. + +@menu +* ML files:: +* Theory files:: +* General commands for Isabelle:: +* Specific commands for Isabelle:: +* Isabelle customizations:: +@end menu + +@node ML files +@subsection ML files +@cindex ML files (in Isabelle) +@cindex Isabelle proof scripts + +In Isabelle, ML files are used to hold proof scripts, as well as +definitions of tactics, proof procedures, etc. So ML files are the +normal domain of Proof General. But there are some things to be wary +of. + +Proof General does not understand full ML syntax(!), so ideally you +should only use Proof General's scripting commands on @file{.ML} files +which contain proof commands (no ML functions, structures, etc). + +If you do use files with Proof General which declare functions, +structures, etc, you should be okay provided your code doesn't include +non top-level semi-colons (which will confuse Proof General's simplistic +parser), and provided all value declarations (and other non proof-steps) +occur outside proofs. This is because within proofs, Proof General +considers every ML command to be a proof step which is undoable. + +For example, do this: +@lisp + structure S = struct + val x = 3 + val y = 4 + end; +@end lisp +instead of this: +@lisp + structure S = struct + val x = 3; + val y = 4; + end +@end lisp +In the second case, just the first binding in the structure body will be +sent to Isabelle and Proof General will wait indefinitely. + +And do this: +@lisp + val intros1 = REPEAT (resolve_tac [impI,allI] 1); + Goal "Q(x) --> (ALL x. P(x) --> P(x))"; + br impI 1; + by intros1; + ba 1; + qed "mythm"; +@end lisp +instead of this: +@lisp + Goal "Q(x) --> (ALL x. P(x) --> P(x))"; + br impI 1; + val intros1 = REPEAT (resolve_tac [impI,allI] 1); + by intros1; + ba 1; + qed "mythm"; +@end lisp +In the last case, when you undo, Proof General wrongly considers the +@code{val} declaration to be a proof step, and it will issue an +@code{undo} to Isabelle to undo it. This leads to a loss of +synchronization. To fix things when this happens, simply retract to +some point before the @code{Goal} command and fix your script. + +Having ML as a top-level, Isabelle even lets you redefine the entire +proof command language, which will certainly confuse Proof General! +Stick to using the standard functions, tactics, and tacticals and there +should be no problems. (In fact, there should be no problems provided +you don't use your own "goal" or "qed" forms, which Proof General +recognizes. As the example above shows, Proof General makes no +attempt to recognize arbitrary tactic applications). + + +@node Theory files +@subsection Theory files +@cindex Theory files (in Isabelle) +@cindex ML files (in Isabelle) + +As well as locking ML files, Isabelle Proof General locks theory files +when they are loaded. Theory files are always completely locked or +completely unlocked, because they are processed atomically. + +Proof General tries to load the theory file for a @file{.ML} file +automatically before you start scripting. This relies on new support +especially for Proof General built into Isabelle99's theory loader. + +However, because scripting cannot begin until the theory is loaded, and +it should not begin if an error occurs during loading the theory, Proof +General @strong{blocks} waiting for the theory loader to finish. If you +have a theory file which takes a long time to load, you might want to +load it directly, from the @file{.thy} buffer. Extra commands are +provided in theory mode for this: + +@c FIXME: should say something about this: +@c This can cause confusion in the theory loader later, +@c especially with @code{update()}. To be safe, try to use just the Proof +@c General interface, and report any repeatable problems to +@c @code{isabelle@dcs.ed.ac.uk}. + +@c Compared to Isamode's theory editing mode, some of the functions and key +@c bindings for interacting with Isabelle have been removed, and two new +@c functions are available. + +The key @kbd{C-c C-b} (@code{isa-process-thy-file}) will cause Isabelle +to read the theory file being edited. This causes the file and all its +children (both theory and ML files) to be read. Any top-level ML file +associated with this theory file is @emph{not} read, in contrast +with the @code{use_thy} command of Isabelle. + +The key @kbd{C-c C-u} (@code{isa-retract-thy-file}) will retract +(unlock) the theory file being edited. This unlocks the file and all +its children (theory and ML files); no changes occur in Isabelle itself. + +@c TEXI DOCSTRING MAGIC: isa-process-thy-file +@deffn Command isa-process-thy-file file +Process the theory file @var{file}. If interactive, use @code{buffer-file-name}. +@end deffn + +@c TEXI DOCSTRING MAGIC: isa-retract-thy-file +@deffn Command isa-retract-thy-file file +Retract the theory file @var{file}. If interactive, use @code{buffer-file-name}.@* +To prevent inconsistencies, scripting is deactivated before doing this. +So if scripting is active in an ML file which is not completely processed, +you will be asked to retract the file or process the remainder of it. +@end deffn + + +@node General commands for Isabelle +@subsection General commands for Isabelle + +This section has some notes on the instantiation of the generic part of +Proof General for Isabelle. (The generic part of Proof General applies +to all proof assistants supported, and is described in detail in the +rest of this manual). + +@strong{Find theorems}. This toolbar/menu command invokes a special +version of @code{thms_containing}. To give several constants, separate +their names with commas. + +@node Specific commands for Isabelle +@subsection Specific commands for Isabelle + +This section mentions some commands which are added specifically +to the Isabelle Proof General instance. + +@cindex Switching to theory files +@kindex C-c C-o + +In Isabelle proof script mode, @kbd{C-c C-o} (@code{thy-find-other-file}) +finds and switches to the associated theory file, that is, the file with +the same base name but extension @file{.thy} swapped for @file{.ML}. + +The same function (and key-binding) switches back to an ML file from the +theory file. + + +@c TEXI DOCSTRING MAGIC: thy-find-other-file +@deffn Command thy-find-other-file &optional samewindow +Find associated .ML or .thy file.@* +Finds and switch to the associated ML file (when editing a theory file) +or theory file (when editing an ML file). +If @var{samewindow} is non-nil (interactively, with an optional argument) +the other file replaces the one in the current window. +@end deffn + + + + +@node Isabelle customizations +@subsection Isabelle customizations + +Here are some of the user options specific to Isabelle. You can set +these as usual with the customization mechanism. + +@c TEXI DOCSTRING MAGIC: isabelle-web-page +@defvar isabelle-web-page +URL of web page for Isabelle. +@end defvar + + +@c @unnumberedsubsec Theory file editing customization + +@c TEXI DOCSTRING MAGIC: thy-use-sml-mode +@defopt thy-use-sml-mode +If non-nil, invoke @code{sml-mode} inside "ML" section of theory files.@* +This option is left-over from Isamode. Really, it would be more +useful if the script editing mode of Proof General itself could be based +on @code{sml-mode}, but at the moment there is no way to do this. + +The default value is @code{nil}. +@end defopt + +@c TEXI DOCSTRING MAGIC: thy-indent-level +@defopt thy-indent-level +Indentation level for Isabelle theory files. An integer. + +The default value is @code{2}. +@end defopt + +@c TEXI DOCSTRING MAGIC: thy-sections +@defvar thy-sections +Names of theory file sections and their templates.@* +Each item in the list is a pair of a section name and a template. +A template is either a string to insert or a function. Useful functions are: +@lisp + @code{thy-insert-header}, @code{thy-insert-class}, @code{thy-insert-default-sort}, + @code{thy-insert-const}, @code{thy-insert-rule}. +@end lisp +The nil template does nothing. +You can add extra sections to theory files by extending this variable. +@end defvar + +@c TEXI DOCSTRING MAGIC: thy-template +@defvar thy-template +Template for theory files.@* +Contains a default selection of sections in a traditional order. +You can use the following format characters: + +@samp{%t} --- replaced by theory name. + +@samp{%p} --- replaced by names of parents, separated by @samp{+} characters. +@end defvar + +@c ideal for above: +@c @defopt thy-template +@c Template for theory files. +@c Contains a default selection of sections in a traditional order. +@c You can use the following format characters: +@c @code{%t} -- replaced by theory name +@c @code{%p} -- replaced by names of parents, separated by @code{+}'s +@c @end defopt + + +@node Isabelle/Isar +@section Isabelle/Isar +@cindex Isabelle/Isar + +Proof General for Isabelle/Isar manages new-style @file{.thy} files, +which may contain both definitions and proofs (human readable proof +texts as well as traditional scripts following the Isar syntax). + +The syntax of Isabelle/Isar 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/Isar process. The caveats of @file{.ML} files +discussed for the classic Isabelle version (@pxref{Classic Isabelle}) do +@b{not} apply here. + +@menu +* General commands for Isabelle/Isar:: +* Specific commands for Isabelle/Isar:: +@end menu + +@node General commands for Isabelle/Isar +@subsection General commands for Isabelle/Isar + +@strong{Find theorems}. This toolbar/menu command invokes +@code{thms_containing}. Several constants may be given, separated by +white space as usual in Isar. + +@node Specific commands for Isabelle/Isar +@subsection Specific commands for Isabelle/Isar +@kindex C-c C-a h A +@kindex C-c C-a h C +@kindex C-c C-a h S +@kindex C-c C-a h T +@kindex C-c C-a h a +@kindex C-c C-a h b +@kindex C-c C-a h c +@kindex C-c C-a h f +@kindex C-c C-a h i +@kindex C-c C-a h m +@kindex C-c C-a h o +@kindex C-c C-a h t + +The Isabelle/Isar instance of Proof General supplies several specific +help key bindings; these functions are offered within the prover help +menu as well. + +@table @kbd +@item C-c C-a h A +Shows available antiquotation commands and options. +@item C-c C-a h C +Shows the current Classical Reasoner context. +@item C-c C-a h S +Shows the current Simplifier context. +@item C-c C-a h T +Shows the current set of transitivity rules (for calculational reasoning). +@item C-c C-a h a +Shows attributes available in current theory context. +@item C-c C-a h b +Shows all local term bindings. +@item C-c C-a h c +Shows all named local contexts (cases). +@item C-c C-a h f +Shows all local facts. +@item C-c C-a h i +Shows inner syntax of the current theory context (for types and terms). +@item C-c C-a h m +Shows proof methods available in current theory context. +@item C-c C-a h o +Shows all available commands of Isabelle/Isar's outer syntax. +@item C-c C-a h t +Shows theorems stored in the current theory node. +@end table + +Command termination via `@code{;}' is an optional feature of Isar +syntax. Neither Isabelle/Isar nor Proof General require semicolons to +do their job. The following command allows to get rid of command +terminators in existing texts. + +@c TEXI DOCSTRING MAGIC: isar-strip-terminators +@deffn Command isar-strip-terminators +Remove explicit Isabelle/Isar command terminators @samp{;} from the buffer. +@end deffn + +@c +@c CHAPTER: HOL Proof General +@c + +@node HOL Proof General +@chapter HOL Proof General +@cindex HOL Proof General + +HOL Proof General is a "technology demonstration" of Proof General for +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 @file{example.sml} 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 will 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. @xref{ML files}, for the same issue with Isabelle. + +HOL Proof General may work with variants of HOL other than HOL98, but is +untested. Probably 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). + +Hopefully somebody from the HOL community is willing to adopt HOL Proof +General and support and improve it. Please volunteer! It needn't be a +large or heavy committment. + + + +@c +@c +@c APPENDIX: Obtaining and Installing +@c +@c +@node Obtaining and Installing +@appendix Obtaining and Installing + +Proof General has its own +@uref{http://www.proofgeneral.org,home page} hosted at +Edinburgh. Visit this page for the latest news! + +@menu +* Obtaining Proof General:: +* Installing Proof General from tarball:: +* Installing Proof General from RPM package:: +* Setting the names of binaries:: +* Notes for syssies:: +@end menu + + +@node Obtaining Proof General +@section Obtaining Proof General + +You can obtain Proof General from the URL +@example +@uref{http://www.proofgeneral.org}. +@end example + +The distribution is available in three forms +@itemize @bullet +@item A source tarball, @* +@uref{http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz} +@item A Linux RPM package (for any architecture), @* +@uref{http://www.proofgeneral.org/ProofGeneral-latest.noarch.rpm} +@item A developer's tarball, @* +@uref{http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz} +@end itemize + +Both the source tarball and the RPM package include the generic elisp +code, code for LEGO, Coq, and Isabelle, installation instructions +(reproduced below) and this documentation. + +The developer's tarball contains our full source 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 +@code{proofgen@@dcs.ed.ac.uk}. + +@c was Installing Proof General from @file{.tar.gz} +@node Installing Proof General from tarball +@section Installing Proof General from tarball + +Copy the distribution to some directory @var{mydir}. +Unpack it there. For example: +@example +# cd @var{mydir} +# gunzip ProofGeneral-@var{version}.tar.gz +# tar -xpf ProofGeneral-@var{version}.tar +@end example +If you downloaded the version called @var{latest}, you'll find it +unpacks to a numeric version number. + +Proof General will now be in some subdirectory of @var{mydir}. The name +of the subdirectory will depend on the version number of Proof General. +For example, it might be @file{ProofGeneral-2.0}. It's convenient to +link it to a fixed name: +@example +# ln -sf ProofGeneral-2.0 ProofGeneral +@end example +Now put this line in your @file{.emacs} file: +@lisp + (load-file "@var{mydir}/ProofGeneral/generic/proof-site.el") +@end lisp + +@node Installing Proof General from RPM package +@section Installing Proof General from RPM package + +To install an RPM package you need to be root. Then type +@example +# rpm -Uvh ProofGeneral-latest.noarch.rpm +@end example + +Now add the line: +@lisp + (load-file "/usr/share/emacs/ProofGeneral/generic/proof-site.el") +@end lisp +to your @file{.emacs} or the site-wide initialisation file +@file{site-start.el}. + +@node Setting the names of binaries +@section Setting the names of binaries + +The @code{load-file} command you have added will load @file{proof-site} +which sets the Emacs load 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: +@example + Proof-General -> Customize -> @var{Name of Assistant} -> Prog Name +@end example +The Proof-General menu is available from script buffers after Proof +General is loaded. To load it manually, type +@lisp + M-x load-library RET proof RET +@end lisp + +If you do not want to use customize, simply add a line like this: +@lisp + (setq coq-prog-name "/usr/bin/coqtop -emacs") +@end lisp +to your @file{.emacs} file. + + + +@node Notes for syssies +@section 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. + +@unnumberedsubsec Byte compilation + +Compilation of the Emacs lisp files improves efficiency but can +sometimes cause compatibility problems, especially if you use more than +one version of Emacs with the same @code{.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 @code{.elc} files which aren't present using the source +@code{.el} files, please report them to us. + +You can compile Proof General by typing @code{make} in the directory +where you installed it. + + +@unnumberedsubsec Site-wide installation + +If you are installing Proof General site-wide, you can put the +components in the standard directories of the filesystem if you prefer, +providing the variables in @file{proof-site.el} are adjusted +accordingly (see @i{Proof General site configuration} in +@i{Adapting Proof General} for more details). Make sure that +the @file{generic/} and assistant-specific elisp files are kept in +subdirectories (@file{coq/}, @file{isa.}, @file{lego.}) of +@code{proof-home-directory} so that the autoload directory calculations +are correct. + +To prevent every user needing to edit their own @file{.emacs} files, you +can put the @code{load-file} command to load @file{proof-site.el} into +@file{site-start.el} or similar. Consult the Emacs documentation for more +details if you don't know where to find this file. + +@unnumberedsubsec 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 @file{.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 @code{proof-assistants} in @file{proof-site.el} to remove the +extra autoloads. This is advisable in case the extensions clash with +other Emacs modes, for example @code{sml-mode} for @file{.ML} files, or +Verilog mode for @file{.v} files. + +See @i{Proof General site configuration} in @i{Adapting Proof General}, +to find out how to disable support for provers you don't use. + +@c Via the Customize mechanism, see the menu: +@c @example +@c Options -> Customize -> Emacs -> External -> Proof General +@c @end example +@c or, after loading Proof General, in a proof script buffer +@c @example +@c Proof-General -> Customize +@c @end example + + + +@c +@c +@c APPENDIX: Known bugs and workarounds +@c +@c +@node Known bugs and workarounds +@appendix Known bugs and workarounds + +We mention a few of the known problems with the generic portion of Proof +General here. This is not a description of all bugs/problems known. +Please consult the file +@uref{http://www.proofgeneral.org/ProofGeneral/BUGS,@file{BUGS}} in the +distribution for more detailed and up-to-date information. @* + +If you discover a problem which isn't mentioned in @file{BUGS}, please +let us know by sending a note to @code{proofgen@@dcs.ed.ac.uk}. + +@menu +* Bugs at the generic level:: +@end menu + +@node Bugs at the generic level +@section Bugs at the generic level + +@subsection Undo in XEmacs + +When @code{proof-strict-read-only} is non-nil, ordinary undo in the +script buffer can edit the "uneditable region" in XEmacs. This doesn't +happen in FSF GNU Emacs. Test case: Insert some nonsense text after the +locked region. Kill the line. Process to the next command. Press +@kbd{C-x u}, nonsense text appears in locked region. + +@strong{Workaround:} be careful with undo. + +@subsection Font locking and read-only in FSF GNU Emacs + +When @code{proof-strict-read-only} is set and font lock is switched on, +spurious "Region read only" errors are given which break font lock. + +@strong{Workaround:} turn off @code{proof-strict-read-only}, font lock, +or for the best of all possible worlds, switch to XEmacs. + + +@subsection Pressing keyboard quit @kbd{C-g} + +Using @kbd{C-g} can leave script management in a mess. The code is not +properly protected from Emacs interrupts. + +@strong{Workaround:} Don't type @kbd{C-g} while script management is +processing. If you do, use @code{proof-shell-restart} to restart +the system. + +@c da: Removed 11.12.98: since PG handles this gracefully now, +@c I no longer consider it a bug really. +@c @subsection One prover at a time +@c You can't use more than one proof assistant at a time in the same Emacs +@c session. Attempting to load Proof General for a second prover will +@c fail, leaving a buffer in fundamental mode instead of the Proof General +@c mode for proof scripts. + +@c @strong{Workaround:} stick to one prover per Emacs session, make sure +@c that the @code{proof-assistants} variable only enables Proof General +@c for the provers you need. + + +@node References +@unnumbered References + +A short overview of the Proof General system is described in the +note: +@itemize @bullet +@item @b{[Asp00]} +David Aspinall. +@i{Proof General: A Generic Tool for Proof Development}. +Tools and Algorithms for the Construction and +Analysis of Systems, Proc TACAS 2000. LNCS 1785. +@end itemize + +Script management as used in Proof General is described in the paper: + +@itemize @bullet +@item @b{[BT98]} +Yves Bertot and Laurent Th@'ery. @i{A generic approach to building +user interfaces for theorem provers}. Journal of +Symbolic Computation, 25(7), pp. 161-194, February 1998. +@end itemize + +Proof General has support for proof by pointing, as described in the +document: + +@itemize @bullet +@item @b{[BKS97]} +Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. @i{Implementing +Proof by Pointing without a +Structure Editor}. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de +l'INRIA Sophia Antipolis RR-3286 +@end itemize + + + + +@node Function Index +@unnumbered Function and Command Index +@printindex fn + +@node Variable Index +@unnumbered Variable and User Option Index +@printindex vr + +@node Keystroke Index +@unnumbered Keystroke Index +@printindex ky + +@node Concept Index +@unnumbered Concept Index +@printindex cp + +@page +@contents +@bye + + diff --git a/doc/README.doc b/doc/README.doc new file mode 100644 index 00000000..e350baea --- /dev/null +++ b/doc/README.doc @@ -0,0 +1,38 @@ +Proof General Documentation +=========================== + +The distribution may include pre-built documentation for +your convenience. Otherwise you will need to run + + make info + make dvi + make pdf + make html + +according to what format you'd like. Everything is generated +from the master Texinfo files ProofGeneral.texi and PG-adapting.texi, +so you'll need the proper tools for conversion. Check Makefile.doc +for details. + +Front Image for Manual +---------------------- +If you want a front image on the printed dvi/gs manuals, you need to +have the ProofGeneral.eps file in this directory. You can download a +compressed version from + +http://www.proofgeneral.org/ProofGeneral/doc/ProofGeneral.eps.gz + +This file is not included with the distribution because it is rather +large (1.6M). + +Instead of downloading, you may be able to generate an alternative eps +from the included ProofGeneral.jpg file using an image manipulation +program such as gimp or Imagemagick. This will give you a slightly +different (and degraded) image compared to the distributed one +mentioned above. + +Running "made dvi" will adjust the Texinfo file to make the front +page blank if there is no ProofGeneral.eps file available. + +David Aspinall. +August 2000. diff --git a/doc/dir b/doc/dir new file mode 100644 index 00000000..134485ff --- /dev/null +++ b/doc/dir @@ -0,0 +1,19 @@ +$Id$ +This is the file .../info/dir, which contains the topmost node of the +Info hierarchy. The first time you invoke Info you start off +looking at that node, which is (dir)Top. + +File: dir Node: Top This is the top of the INFO tree + + This (the Directory node) gives a menu of major topics. + Typing "q" exits, "?" lists all Info commands, "d" returns here, + "h" gives a primer for first-timers, + "mEmacs<Return>" visits the Emacs topic, etc. + + In Emacs, you can click mouse button 2 on a menu item or cross reference + to select it. + +* Menu: + +Theorem proving +* Proof General: (ProofGeneral). Organize your proofs with Emacs! diff --git a/doc/docstring-magic.el b/doc/docstring-magic.el new file mode 100644 index 00000000..5550f324 --- /dev/null +++ b/doc/docstring-magic.el @@ -0,0 +1,67 @@ +;; doc/docstring-magic.el -- hack for using texi-docstring-magic. +;; +;; Copyright (C) 1998 LFCS Edinburgh. +;; Author: David Aspinall +;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> +;; +;; Ensure that non-compiled versions of everything are loaded. +;; +;; $Id$ +;; +(setq load-path + (append '("../generic/") load-path)) +(load "proof-site.el") +(require 'proof-autoloads) +(require 'proof-compat) +(require 'proof-utils) + +;; FIXME: Loading several prover files at once is a bit of a problem +;; with new config mechanism. +;; Could abstract more code in proof-site.el to avoid duplication here. +(let ((assistants (mapcar (function car) proof-assistant-table))) + ; assume not customized + (while assistants + (let* + ((assistant (car assistants)) ; compiler bogus warning here + (nameregexp + (or + (cdr-safe + (assoc assistant + proof-assistant-table)) + (error "proof-site: symbol " (symbol-name assistant) + "is not in proof-assistant-table"))) + (assistant-name (car nameregexp)) + (sname (symbol-name assistant)) + (elisp-file sname)) + (proof-ready-for-assistant assistant-name assistant) + ;; Must load proof-config each time to define proof assistant + ;; specific variables + (setq features (delete 'proof-config features)) + (load "proof-config.el") + (load-library elisp-file) + (setq assistants (cdr assistants))))) + +;; Now a fake proof assistant to document the automatically +;; specific variables +(proof-ready-for-assistant "PROOF ASSISTANT" 'PA) +(setq features (delete 'proof-config features)) +(load "proof-config.el") + + +;; These next few are autoloaded usually +(load "thy-mode.el") +(load "proof-menu.el") +(load "proof-toolbar.el") +(load "proof-script.el") +(load "proof-shell.el") + +;; A couple of comint symbols are mentioned in the docs +(require 'comint) +;; Also completion +(require 'completion) + +;; Set some symbols to make markup happen +(setq sml-mode 'markup-hack) +(setq func-menu 'markup-hack) + +(load "texi-docstring-magic.el")
\ No newline at end of file diff --git a/doc/localdir b/doc/localdir new file mode 100644 index 00000000..2b366965 --- /dev/null +++ b/doc/localdir @@ -0,0 +1,3 @@ +Theorem proving +* Proof General: (ProofGeneral). Organize your proofs with Emacs! +* Adapting Proof General: (PG-adapting). How to adapt Proof General for new provers |
