diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/PG-adapting.texi | 6 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 147 | ||||
| -rw-r--r-- | doc/dir | 5 | ||||
| -rw-r--r-- | doc/docstring-magic.el | 36 |
4 files changed, 138 insertions, 56 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 44c40549..5740faa2 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -51,14 +51,14 @@ @c @ref{node} without "see". Careful for info. -@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 -* Adapting Proof General: (PG-adapting). Adapt Proof General to new provers +* Adapting PG: (PG-adapting). Adapt Proof General to new provers END-INFO-DIR-ENTRY @end direntry 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. @@ -1,4 +1,3 @@ -$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. @@ -16,5 +15,5 @@ File: dir Node: Top This is the top of the INFO tree * Menu: Theorem proving -* Proof General: (ProofGeneral). Organize your proofs with Emacs! -* Adapting Proof General: (PG-adapting). Adapt Proof General to new provers +* ProofGeneral: (ProofGeneral). Organize your proofs with Emacs! +* Adapting PG: (PG-adapting). Adapt Proof General to new provers diff --git a/doc/docstring-magic.el b/doc/docstring-magic.el index 1d074d8d..409fd22a 100644 --- a/doc/docstring-magic.el +++ b/doc/docstring-magic.el @@ -1,13 +1,24 @@ -;; doc/docstring-magic.el -- hack for using texi-docstring-magic. -;; -;; Copyright (C) 1998 LFCS Edinburgh. +;;; doc/docstring-magic.el --- hack for using texi-docstring-magic. + +;; This file is part of Proof General. + +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall ;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> + +;;; Commentary: ;; ;; Ensure that non-compiled versions of everything are loaded. ;; -;; $Id$ -;; + +;;; Code: + (setq load-path (append '("../generic/") load-path)) (load "proof-site.el") @@ -25,15 +36,15 @@ (let ((assistants (mapcar (function car) proof-assistant-table))) ; assume not customized (while assistants - (let* + (let* ((assistant (car assistants)) ; compiler bogus warning here - (nameregexp - (or - (cdr-safe + (nameregexp + (or + (cdr-safe (assoc assistant proof-assistant-table)) - (error "proof-site: symbol " (symbol-name assistant) - "is not in proof-assistant-table"))) + (error "Symbol %s is not in proof-assistant-table (in docstring-magic)" + (symbol-name assistant)))) (assistant-name (car nameregexp)) (sname (symbol-name assistant)) (elisp-file sname)) @@ -74,3 +85,6 @@ (setq func-menu 'markup-hack) (load "texi-docstring-magic.el") + +(provide 'docstring-magic) +;;; docstring-magic.el ends here |