- fix 1 second problem

- add limitations in the docs

2 files changed, 47 insertions, 8 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 22df5540..91e5768f 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1095,8 +1095,9 @@ Currently this doesn't take the loadpath into account."
 ;;
 
 ;; TODO list:
-;; - 1 second precision problem
-;; - bug: killing buffer omits coqtop restart
+;; - Bug: undo in locked ancestor
+;; - Bug: never stopping busy cursor
+;; - Bug: coq not running for the first comment after switching
 ;; - modify behavior of locked ancestors, see proof-span-read-only
 ;; - display coqdep errors in the recompile-response buffer
 ;; - use a variable for the recompile-response buffer
@@ -1448,7 +1449,12 @@ dependencies. It is either
 
 If this function decides to compile SRC to OBJ it returns
 'just-compiled. Otherwise it returns the modification time of
-OBJ."
+OBJ.
+
+Note that file modification times inside emacs have only a
+precisision of 1 second. To avoid spurious recompilations we do
+not recompile if the youngest object file of the dependencies and
+OBJ have identical modification times."
   (let (src-time obj-time)
     (if (eq max-dep-obj-time 'just-compiled)
         (progn
@@ -1462,7 +1468,7 @@ OBJ."
            (and
             max-dep-obj-time            ; there is a youngest dependency
                                         ; which is newer than obj
-            (time-less-or-equal obj-time max-dep-obj-time)))
+            (time-less-p obj-time max-dep-obj-time)))
           (progn
             (coq-compile-library src)
             'just-compiled)
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index f4cc618f..ecc5af37 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4023,6 +4023,11 @@ necessary files whenever a @code{Require} command is processed.
 The compilation feature does currently not support ML modules.
 @end table
 
+The current version works reliably, even when stress-tested with
+changing random files in large Coq projects. However, some
+features have spared for the next release, @ref{Current
+Limitations}.
+
 To enable the automatic compilation feature there are three
 points to adhere to:
 
@@ -4039,9 +4044,8 @@ For a nonstandard compilation procedure and limited ML module
 support, @code{coq-compile-command} can be set to an external
 compilation command. For standard dependency analysis with
 @code{coqdep} and compilation with @code{coqc} the option
-@code{coq-compile-command} can be left empty. If this option is
-empty Proof General calls @code{coqdep} and @code{coqc} as
-needed.
+@code{coq-compile-command} can be left empty. In this case Proof
+General calls @code{coqdep} and @code{coqc} as needed.
 @end itemize
 
 
@@ -4050,6 +4054,7 @@ needed.
 * Automatic Compilation in Detail::
 * Locking Ancestors::
 * Customizing Coq Multiple File Support::
+* Current Limitations::
 @end menu
 
 
@@ -4138,7 +4143,7 @@ current scripting buffer without interruption.
 @node Customizing Coq Multiple File Support
 @subsection Customizing Coq Multiple File Support
 
-The customization setting for multiple file support of Coq Proof
+The customization settings for multiple file support of Coq Proof
 General are in a separate customization group, the
 @code{coq-auto-compile} group. To view all options in this
 group do @code{M-x customize-group coq-auto-compile} or select
@@ -4325,6 +4330,34 @@ identifier and should therefore not be matched by this regexp.
 
 
 
+@node Current Limitations
+@subsection Current Limitations
+
+In the current release some aspects of multiple file support have
+not been implemented. The following points will hopefully
+addressed in the next release:
+
+@itemize
+@item
+Support @code{Declare ML Module} commands.
+@item
+Properly display errors from @code{coqdep} and @code{coqc},
+enable @code{C-x `} (@code{M-x next-error}) for these error
+messages.
+@item
+Improved undo behaviour for locked ancestors.
+@item
+Integrate with older options for multiple file support, such as,
+for instance, @code{coq-auto-compile-vos}.
+@item
+Increase precision when comparing modification times. Because of
+an Emacs limitation, modification time stamps of files have only a
+precision of 1 second. If several compiled Coq object files have
+been created in the same second, Proof General is optimistic and
+does not recompile. (Note that GNU make behaves the same on file
+systems that record time stamps only with a precision of 1
+second.)
+@end itemize
 
 
 @node Editing multiple proofs