diff options
Diffstat (limited to 'doc/ProofGeneral.texi')
| -rw-r--r-- | doc/ProofGeneral.texi | 147 |
1 files changed, 108 insertions, 39 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 8dab17f0..56b9bbc6 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4,7 +4,7 @@ @c @c @c TODO: -@c MMM support, Theorem dependencies, history in script and response, +@c Theorem dependencies, history in script and response, @c identifier info commands @@ -57,14 +57,14 @@ @c @ref{node} without "see". Careful for info. @c -@set version 4.4.1~pre -@set emacsversion 24.4 +@set version 4.5-git +@set emacsversion 24.3 @set last-update September 2016 @set rcsid $Id$ @dircategory Theorem proving @direntry -* Proof General: (ProofGeneral). Organize your proofs with Emacs! +* ProofGeneral: (ProofGeneral). Organize your proofs with Emacs! @end direntry @c @@ -145,8 +145,7 @@ generic Emacs interface for proof assistants. Proof General @value{version} has been tested with GNU Emacs @value{emacsversion} on Linux. It is supplied ready to use for the proof -assistants LEGO, Coq, Isabelle, and PhoX. Experimental support is -provided for several other provers. +assistants Coq, EasyCrypt, and PhoX. @menu * Preface:: @@ -163,6 +162,7 @@ provided for several other provers. * Coq Proof General:: * Isabelle Proof General:: * HOL Light Proof General:: +* EasyCrypt Proof General:: * Shell Proof General:: @c * PhoX Proof General:: * Obtaining and Installing:: @@ -520,6 +520,7 @@ script file for your proof assistant, for example: @item Lambda-CLAM @tab @file{.lcm} @tab @code{lclam-mode} @item CCC @tab @file{.ccc} @tab @code{ccc-mode} @item PG-Shell @tab @file{.pgsh} @tab @code{pgshell-mode} +@item EasyCrypt @tab @file{.ec} @tab @code{easycrypt-mode} @end multitable (the exact list of Proof Assistants supported may vary according to the version of Proof General and its local configuration). You can also @@ -678,6 +679,9 @@ Isabelle for more details. @b{HOL Light Proof General} for HOL Light@* @xref{HOL Light Proof General}, for more details. @item +@b{EasyCrypt Proof General} for EasyCrypt@* +@xref{EasyCrypt Proof General}, for mode details. +@item @b{Shell Proof General} for shell scripts (not really a proof assistant!)@* @xref{Shell Proof General}, for more details. @end itemize @@ -3466,40 +3470,49 @@ For multiple frame mode, this function obeys the setting of For single frame mode: -- In two panes mode, this uses a canonical layout made by splitting +@itemize @bullet +@item +In two panes mode, this uses a canonical layout made by splitting Emacs windows in equal proportions. The splitting is vertical if emacs width is smaller than @samp{@code{split-width-threshold}} and horizontal otherwise. You can then adjust the proportions by dragging the separating bars. -- In three pane mode, there are three display modes, depending -@lisp - where the three useful buffers are displayed: scripting - buffer, goals buffer and response buffer. - - Here are the three modes: - - - vertical: the 3 buffers are displayed in one column. - - hybrid: 2 columns mode, left column displays scripting buffer - and right column displays the 2 others. - - horizontal: 3 columns mode, one for each buffer (script, goals, - response). - - By default, the display mode is automatically chosen by - considering the current emacs frame width: if it is smaller - than @samp{@code{split-width-threshold}} then vertical mode is chosen, - otherwise if it is smaller than 1.5 * @samp{@code{split-width-threshold}} - then hybrid mode is chosen, finally if the frame is larger than - 1.5 * @samp{@code{split-width-threshold}} then the horizontal mode is chosen. - - You can change the value of @samp{@code{split-width-threshold}} at your - will. - - If you want to force one of the layouts, you can set variable - @samp{@code{proof-three-window-mode-policy}} to @code{'vertical}, @code{'horizontal} or - @code{'hybrid}. The default value is @code{'smart} which sets the automatic - behaviour described above. -@end lisp +@item +In three pane mode, there are three display modes, depending +where the three useful buffers are displayed: scripting +buffer, goals buffer and response buffer. + +Here are the three modes: + +@itemize @bullet +@item +@code{vertical}: the 3 buffers are displayed in one column. + +@item +@code{hybrid}: 2 columns mode, left column displays scripting buffer +and right column displays the 2 others. + +@item +@code{horizontal}: 3 columns mode, one for each buffer (script, goals, response). +@end itemize + +By default, the display mode is automatically chosen by +considering the current emacs frame width: if it is smaller +than @samp{@code{split-width-threshold}} then vertical mode is chosen, +otherwise if it is smaller than 1.5 * @samp{@code{split-width-threshold}} +then hybrid mode is chosen, finally if the frame is larger than +1.5 * @samp{@code{split-width-threshold}} then the horizontal mode is chosen. + +You can change the value of @samp{@code{split-width-threshold}} at your +will. + +If you want to force one of the layouts, you can set variable +@samp{@code{proof-three-window-mode-policy}} to @code{'vertical}, @code{'horizontal} or +@code{'hybrid}. The default value is @code{'smart} which sets the automatic +behaviour described above. +@end itemize + @end deffn @c TEXI DOCSTRING MAGIC: proof-shrink-windows-tofit @@ -5450,7 +5463,7 @@ URL of web page for Isabelle. -@c FIXME todo: theorem dependencies, MMM +@c FIXME todo: theorem dependencies @c ================================================================= @@ -5495,9 +5508,66 @@ us know if you try this out and want help. We welcome any interested collaborators from the HOL communities to help improve Proof General as an interface for HOL provers. +@c ================================================================= +@c +@c CHAPTER: EasyCrypt Proof General +@c +@node EasyCrypt Proof General +@chapter EasyCrypt Proof General +@cindex EasyCrypt Proof General +@menu +* EasyCrypt specific commands:: +* EasyCrypt weak-check mode:: +* EasyCrypt customizations:: +@end menu + +EasyCrypt Proof General is an instantiation of Proof General for the +EasyCrypt proof assistant. + +@node EasyCrypt specific commands +@section EasyCrypt specific commands + +@kindex C-c C-a C-p +@kindex C-c C-a C-c + +EasyCrypt Proof General supplies the following key-bindings: +@table @kbd +@item C-c C-a C-p +Prompts for ``print'' query arguments. + +@item C-c C-a C-c +The same for a ``check'' query. +@end table + +@node EasyCrypt weak-check mode +@section EasyCrypt weak-check mode +The EasyCrypt menu contains a @code{Weak-check mode} toggle menu, which +allows you to enable or disable the EasyCrypt Weak-Check mode. When +enabled, all @code{smt} calls are ignored and assumed to succeed. + +@node EasyCrypt customizations +@section EasyCrypt customizations + +Here are some of the other user options specific to EasyCrypt. You can +set these as usual with the customization mechanism. +@c TEXI DOCSTRING MAGIC: easycrypt-prog-name +@defvar easycrypt-prog-name +Name of program to run EasyCrypt. +@end defvar + +@c TEXI DOCSTRING MAGIC: easycrypt-load-path +@defvar easycrypt-load-path +Non-standard EasyCrypt library load path. This list specifies the +include path for EasyCrypt. +@end defvar + +@c TEXI DOCSTRING MAGIC: easycrypt-web-page +@defvar easycrypt-web-page +URL of web page for EasyCrypt. +@end defvar @c ================================================================= @@ -6082,9 +6152,8 @@ Summer Schools. Many new features have been added to enhance Coq mode Support has been added for the useful Emacs packages Speedbar @c @uref{http://cedet.sourceforge.net/speedbar.shtml,Speedbar} -and Index Menu, both usually distributed with Emacs. Compatible -versions of the Emacs packages Math-Menu (for Unicode symbols) and MMM -Mode (for multiple modes in one buffer) are bundled with Proof General. +and Index Menu, both usually distributed with Emacs. A compatible +version of the Emacs package Math-Menu (for Unicode symbols) is bundled with Proof General. An experimental Unicode Tokens package has been added which will replace X-Symbol. |