gmane.emacs.proofgeneral.devel

Re: non-fatal warnings for make compile

David Aspinall — 2013-05-22T20:55:59

Hendrik,

Thanks a lot for tackling this, I looked at it a while ago and saw it 
was going to be a nuisance to fix...

  - David.

non-fatal warnings for make compile

Hendrik Tews — 2013-05-22T20:40:33

Hi,

I spend some time to find a fix for tickets #458. The problem is
that special-display-regexps is obsolete in 24.3, while its
replacement, display-buffer-alist was only introduced in 24.1 and
not fully functional before 24.3. Writing compatible code for
emacs 23 and 24 without obsolete warning therefore requires
explicit version checks.

I therefore suggest that we change to display-buffer-alist when
we drop support for Emacs 23.

To fix #458, warnings should be non-fatal when users compile
Proof General for their local emacs. I just committed the
necessary changes in the Makefile. For developers, there is now
the new target 'check' that retains the old behavior, i.e.,
stopping compilation on every byte-compilation warning.


Bye,

Hendrik

Re: Ticket #467: vernacular command no longer displaystimings

Jason Gross — 2013-04-19T17:11:07

I think I started learning Coq around March 2012, so it must have been
8.3pl3 or 8.3pl4.

Setting coq-end-goals-regexp-show-subgoals to nil does what I want (or, at
least, is plenty good).  Thanks for the workaround!

-Jason


On Fri, Apr 19, 2013 at 4:55 AM, Hendrik Tews <tews-IG//nw+yl+iQIjdd1DhZXWfrygkm6VTR< at >public.gmane.org>wrote:

Re: Ticket #467: vernacular command no longer displaystimings

Hendrik Tews — 2013-04-19T08:55:46

I believe all Proof General versions (including the latest trunk)
show the timing in the *goals* buffer when you use them with Coq
8.3pl4 or earlier. If you have more than one subgoal the timing
is shown only when coq-hide-additional-subgoals is off. Then the
*goals* buffer looks like

######################################################################
2 subgoals

  ============================
   True

subgoal 2 is:
 True
Finished transaction in 0. secs (0.u,0.s)
######################################################################


When coq-hide-additional-subgoals is on, only the text before
"subgoal 2" is copied to the *goals* buffer, and then the timing
is obviously only displayed when you have one subgoal.

Coq 8.4 displays the dependent evar line under Proof General.
Therefore, with Coq 8.4, Proof General only copies the material
before the dependent evar line to the *goals* buffer, and the
timing is lost. 

Jason, can you try setting coq-end-goals-regexp-show-subgoals to
nil? (M-x customize-variable coq-end-goals-regexp-show-subgoals,
Value Menu -> nil; State -> Save for furture sessions; then
restart Proof General) Then the goals buffer looks like

######################################################################
2 subgoals, subgoal 1 (ID 3)
  
  ============================
   True
subgoal 2 (ID 4) is:
 True
(dependent evars:)

Finished transaction in 0. secs (0.u,0.s)
######################################################################



Bye,

Hendrik

Re: Ticket #467: vernacular command no longer displaystimings

Hendrik Tews — 2013-04-19T07:30:09

   
   I remember how PG used to behave, but I do not recall which version it was.
    I started using Coq at version 8.3pl2, or there-abouts, so I can try to

8.3pl3 was released in December 2011, so it was probably Proof
General 4-2pre111207 or earlier.

Hendrik

Re: Ticket #467: vernacular command no longer displaystimings

Jason Gross — 2013-04-18T17:13:27

I remember how PG used to behave, but I do not recall which version it was.
 I started using Coq at version 8.3pl2, or there-abouts, so I can try to
figure out which version of PG behaved how I expect.  I will try to get
back to the email list within the next few days with a response about this.

-Jason


On Thu, Apr 18, 2013 at 2:54 AM, Hendrik Tews <tews-IG//nw+yl+iQIjdd1DhZXWfrygkm6VTR< at >public.gmane.org>wrote:

Ticket #467: vernacular command no longer displays timings

Hendrik Tews — 2013-04-18T06:54:31

Hi,

somebody wrote in the bug tracker:

    Btw, is it possible to get me added to the cc list for this bug?
    (jasongross9+PG AT gmail DOT com)

I don't know how. I therefore suggest to continue the discussion
here at ProofGeneral-devel. 

I have some suspicions, what caused the timings to disappear.
However, before I dig into the issue, I would like to see how
Proof General used to behave. I therefore ask for the third time:

Do you remember a PG version that had the behavior you expect?

Bye,

Hendrik

Reminder: CICM/MKM deadline nearly here!

David Aspinall — 2013-02-27T15:59:49

Dear PG users and developers,

Hopefully many of you will know the CICM conference and have seen the CFP:

   http://www.cicm-conference.org/2013/cicm.php?event=&menu=cfp

I'm the track chair for MKM (Mathematical Knowledge Management) this 
year, I'm keen to see plenty of submissions for our track to put 
together an interesting programme.  If you've been using Proof General 
(or even another tool) to manage large developments, maybe there is 
something to write about?

The deadline for final submissions is Fri 8th March (abstracts ideally 
by this Friday).

Best Wishes,

  - David

Re: urgent message hide errors?

David Aspinall — 2013-02-26T14:58:23

 From Proof General's point of view, the first of these is the problem, 
since the behaviour has been well specified for a long time and I guess 
that Coq's behaviour has changed over time.  See fragment of 
documentation from proof-shell-filter below.

  - David


Error or interrupt messages are expected to terminate an
interactive output and appear last before a prompt and will
always be processed.  Error messages and interrupt messages are
therefore *not* considered as urgent messages.


see:

http://proofgeneral.inf.ed.ac.uk/htmlshow.php?title=Proof+General+adapting+manual&file=releases%2FProofGeneral%2Fdoc%2FPG-adapting%2FPG-adapting_15.html#index-proof_002dshell_002dfilter

Re: status of support for Proof General

David Aspinall — 2013-02-26T14:47:17

Hello Hendrik,

It is a good idea to add a note to the trac.  I would say that the 
support is currently by best efforts of people who have other jobs and 
little spare time -- such as you and I.

I think there are other people on this list but probably no very active 
developers at the moment.  (If anyone is keen to devote support effort 
to PG, they should get in touch with me, there might be ways to help 
provide a bit of project work.)

In general, the support problem is of course a typical problem with 
research software in our discipline, where it seems hard to get funding 
to provide baseline support for a system, and it is often done "on the 
side" with some research topic.  Proof General has only ever been 
supported indirectly by minor contributions from other research projects 
--- impressive that it has lasted and been maintained so well despite 
that, and I'm grateful for all the time people have dedicated.

  - David


On 26/02/13 14:21, Hendrik Tews wrote:

urgent message hide errors?

Hendrik Tews — 2013-02-26T14:30:17

Hi,

currently, proof-shell-filter looks for urgent messages before
looking for errors. Moreover, if an urgent message is found, it
searches for errors only in the output that follows the urgent
message. 

This behavior is responsible for issue #463, where Coq outputs an
error before a warning and the error is lost because the warning
is recognized as urgent message.

What is the problem here? Coq outputting the warning _after_ the
error? Or matching the warning as urgent message? Or searching
for errors only behind urgent messages?

Bye,

Hendrik

status of support for Proof General

Hendrik Tews — 2013-02-26T14:21:38

Hi,

do we have a support problem for Proof General?

I am asking because we have issues in the tracker that are quite
old and nobody seems to care... for instance #460 or #463 to
which I gave partial answers today.

Do we have a lack of developers or do the developers not like to
comment on issues in the tracker?

Whatever the reason is, if we cannot improve the situation, I
would suggest to put an appropriate note on the tracker, saying
issue handling may take some time. Letting users find this out
themselves is the worst we can do.

Bye,

Hendrik

prooftree users?

Hendrik Tews — 2013-01-15T08:55:31

Hi,

is anybody actually using prooftree with the cvs head of Proof
General? 

For supporting bullets, braces and "Grab Existential Variables" I
would like to make several commits that break compatibility with
the current release of prooftree. A suitable prooftree release
will follow within a month.

Please drop me a line, if you would be disturbed if compatibility
breaks between cvs head of Proof General and prooftree 
version 0.10.

Bye,

Hendrik

make clean deletes backup files

Hendrik Tews — 2013-01-15T08:40:25

Hi,

currently editor backup files are deleted by make clean. I find
this unfortunate, because I have to use make clean quite often to
remove elc files. If nobody disagrees, I move the removal of *~
to the distclean target.

Bye,

Hendrik

Re: overlapping calls to proof-shell-filter

Stefan Monnier — 2013-01-10T13:22:44

Thanks,


        Stefan

Re: overlapping calls to proof-shell-filter

Hendrik Tews — 2013-01-10T12:58:50

   here is a patch that solves the problem for me. Any comments?

I committed now. I deleted the argument of proof-shell-filter, to
make sure, nobody will use it. Reasons are described in the doc
comments.

Hendrik

Re: overlapping calls to proof-shell-filter

Hendrik Tews — 2013-01-10T11:09:34

   At a quick glance this looks like a reasonable way to fix without
   messing with the current filter code.  Luckily, I don't think the str
   argument is used.  

   I'm not completely clear on the error case, is the
   idea just to give up if we hit an error in some call?

If proof-shell-filter signals an error, the error is just
propagated, only the active flag is reset to enable later calls
again.

Or do you mean the case where a parallel, overlapping call is
detected? In this case the -was-blocked flag is set and the
already running instance of the wrapper stays for one more
iteration in the while loop, thus calling proof-shell-filter
after the previous call finished.

This effectively delays Coq until prooftree catches up. This is
just what you want, I believe. 

Under normal circumstances prooftree is much faster than Coq.
Because of the experience with PVS, where the proof tree
visualizer was often the bottleneck, I made some special
optimizations:

- tree layout is linear in the tree depth; for PVS it is
  apparently worse than linear in the number of nodes

- tree display is delayed until no display commands are available
  on input; nevertheless, when asserting large regions, you see
  the tree growing node by node, indicating that prooftree is
  faster than Coq

Bye,

Hendrik

Re: overlapping calls to proof-shell-filter

David Aspinall — 2013-01-10T10:44:25

At a quick glance this looks like a reasonable way to fix without 
messing with the current filter code.  Luckily, I don't think the str 
argument is used.  I'm not completely clear on the error case, is the 
idea just to give up if we hit an error in some call?

  - D.


On 09/01/13 20:53, Hendrik Tews wrote:

Re: overlapping calls to proof-shell-filter

Hendrik Tews — 2013-01-10T10:35:21

   I think this deserves an Emacs bug report.

see http://debbugs.gnu.org/cgi/bugreport.cgi?bug=13400

There are definitely some documentation problems.
process-send-string is not mentioned as function that might
trigger a filter call.

   I think many packages are vulnerable to this
   problem, although they usually don't suffer from it.  The most common
   case where they do suffer from it is when you try to Edebug the
   process filter.

I believe it would be good to have a process-specific flag that
inhibits overlapping parallel calls to the same process filter.
Emacs could accept output but buffer it until the previous filter
terminates.

Bye,

Hendrik

Re: overlapping calls to proof-shell-filter

Stefan Monnier — 2013-01-10T02:31:06

I think this deserves an Emacs bug report.  I'm not completely sure it's
a bug rather than a "feature", but it would be good to record this as
a problematic area.  I think many packages are vulnerable to this
problem, although they usually don't suffer from it.  The most common
case where they do suffer from it is when you try to Edebug the
process filter.


        Stefan

Re: overlapping calls to proof-shell-filter

Hendrik Tews — 2013-01-09T20:53:39

Hi,

here is a patch that solves the problem for me. Any comments?

Bye,

Hendrik

Index: generic/proof-shell.el
===================================================================
RCS file: /disk/cvs/proofgen/ProofGeneral/generic/proof-shell.el,v
retrieving revision 12.15
diff -u -r12.15 proof-shell.el
--- generic/proof-shell.el3 Jan 2013 09:33:38 -000012.15
+++ generic/proof-shell.el9 Jan 2013 20:49:38 -0000
< at >< at > -243,6 +243,13 < at >< at >
   :type 'boolean
   :group 'proof-shell)
 
+(defvar proof-shell-filter-active nil
+  "t when `proof-shell-filter' is running.")
+
+(defvar proof-shell-filter-was-blocked nil
+  "t when a recursive call of `proof-shell-filter' was blocked.
+In this case `proof-shell-filter' must be called again after it finished.")
+
 (defun proof-shell-set-text-representation ()
   "Adjust representation for current buffer, to match `proof-shell-unicode'."
   (unless proof-shell-unicode
< at >< at > -277,6 +284,7 < at >< at >
   (interactive)
   (unless (proof-shell-live-buffer)
 
+    (setq proof-shell-filter-active nil)
     (setq proof-included-files-list nil) ; clear some state
 
     (let ((name (buffer-file-name (current-buffer))))
< at >< at > -1288,12 +1296,37 < at >< at >
 ;; The proof shell process filter
 ;;
 
+(defun proof-shell-filter-wrapper (str)
+  "Wrapper for `proof-shell-filter', protecting against recursive calls.
+In Emacs a process filter function can be called while the same
+filter is currently running for the same process, for instance,
+when the filter bocks on I/O. This wrapper protects the main
+entry point, `proof-shell-filter' against such recursive calls."
+  (if proof-shell-filter-active
+      (progn
+(setq proof-shell-filter-was-blocked t))
+    (let ((call-proof-shell-filter t))
+      (while call-proof-shell-filter
+(setq proof-shell-filter-active t
+      proof-shell-filter-was-blocked nil)
+(condition-case err
+    (progn
+      (proof-shell-filter str)
+      (setq proof-shell-filter-active nil))
+  ((error quit)
+   (setq proof-shell-filter-active nil
+ proof-shell-filter-was-blocked nil)
+   (signal (car err) (cdr err))))
+(setq call-proof-shell-filter proof-shell-filter-was-blocked)))))  
+
+
 (defun proof-shell-filter (str)
   "Master filter for the proof assistant shell-process.
 A function for `scomint-output-filter-functions'.
 
-Deal with output STR and issue new input from the queue.  This is
-an important internal function.
+Deal with output STR and issue new input from the queue. This is
+an important internal function. Actually, STR is not used, the
+output is taken from `proof-shell-buffer'.
 
 Handle urgent messages first.  As many as possible are processed,
 using the function `proof-shell-process-urgent-messages'.
< at >< at > -1806,7 +1839,7 < at >< at >
   (setq scomint-output-filter-functions
 (append
  (if proof-shell-strip-crs-from-output 'scomint-strip-ctrl-m)
- (list 'proof-shell-filter)))
+ (list 'proof-shell-filter-wrapper)))
 
   (setq proof-marker ; follows prompt
 (make-marker)