From 78a60e73ff0398392d55be24f60446c58808509c Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 14 Nov 2012 09:09:32 +0000 Subject: update documentation --- doc/PG-adapting.texi | 33 +++++++++++++++++++++++++++++++-- 1 file changed, 31 insertions(+), 2 deletions(-) (limited to 'doc/PG-adapting.texi') diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index bd80d47e..4969b5db 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -364,7 +364,7 @@ file for the mode, which will be where @var{proof-home-directory} is the value of the variable @samp{@code{proof-home-directory}}. -The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (phox "PhoX" "phx") (hol-light "HOL Light" "ml") (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci"))}. +The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (phox "PhoX" "phx") (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci"))}. @end defopt @@ -3216,7 +3216,7 @@ 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{'isar} @code{'coq} @code{'phox} @code{'hol-light} @code{'pgshell} @code{'pgocaml} @code{'pghaskell}. +A list of symbols chosen from: @code{'isar} @code{'coq} @code{'phox} @code{'pgshell} @code{'pgocaml} @code{'pghaskell}. If nil, the default will be ALL available proof assistants. Each proof assistant defines its own instance of Proof General, @@ -3814,6 +3814,35 @@ printing hints). See the functions @samp{@code{proof-start-queue}} and @samp{@code{proof-shell-exec-loop}}. @end defvar +In Proof General 4.2 and earlier it was always the case that all +items from the queue region were present in +@code{proof-action-list}. Because of the new parallel background +compilation for Coq, this is no longer the case. Prover specific +code may now store items from the queue region somewhere else. To +notify generic Proof General about this, it must set +@code{proof-second-action-list-active} for the time where some +queue items are missing from @code{proof-action-list}. In this +case Proof General keeps the proof shell lock and the queue span +even in case @code{proof-action-list} gets empty. Coq uses this +feature to hold back Require commands and the following text +until the asynchronous background compilation finishes. + +@c TEXI DOCSTRING MAGIC: proof-second-action-list-active +@defvar proof-second-action-list-active +Signals that some items are waiting outside of @samp{@code{proof-action-list}}.@* +If this is t it means that some items from the queue region are +waiting for being processed in a place different from +@samp{@code{proof-action-list}}. In this case Proof General must behave as if +@samp{@code{proof-action-list}} would be non-empty, when it is, in fact, +empty. + +This is used, for instance, for parallel background compilation +for Coq: The Require command and the following items are not put +into @samp{@code{proof-action-list}} and are stored somewhere else until the +background compilation finishes. Then those items are put into +@samp{@code{proof-action-list}} for getting processed. +@end defvar + @c TEXI DOCSTRING MAGIC: pg-subterm-anns-use-stack @defvar pg-subterm-anns-use-stack Choice of syntax tree encoding for terms. -- cgit v1.2.3