proofgeneral/pg

This repo is the new home of Proof General

pg's Issues

constant msg: "Zero or more than one goals window, guessing window width."

I get this msg after every prover step in my minibuffer. Maybe because I'm running in 3-window mode?

It's a minor annoyance - but makes me wonder if I might see some other useful msgs in the minibuffer if this one wasn't there all the time.

-- Jonathan

3 frames mode - get frames to appear at specific positions with specific sizes

I work mostly in 3 windows mode with separate frames (Proof-General -> Quick Options -> Display -> Multiple Windows checked). Is there a way, when restarting Coq, to get the proof and response frames to appear at consistent places with specific sizes? I think there used to be a way to do this, as by setting the places/sizes by hand and then triggering some memoization option of those settings, but I can't find it anymore.

How does one require proof-shell?

I'm writing a plugin that depends on variables in proof-shell.el. Unfortunately, requireing causes an error:

mapcar: Symbol’s value as variable is void: nil-completion-table

I found this bit in the source:

;; NB: completion table is expected to be set when proof-script
;; is loaded!  Call `proof-script-add-completions' to update.

(unless noninteractive ; during compilation
  (eval-after-load "completion"
  '(proof-add-completions)))

What’s the proper procedure?

Failure while processing imports

Hi all,
Dutifully following Clément's post over the Coq list, I installed the latest version of PG. The installation went smoothly but I get, despite using Coq 8.4pl6, quite a weird failure when trying to process a Require Import:

Invalid version syntax: '8.5snapshot'

Would anyone know what might be going on?
Best,
Yannick

Some commands are not highlighted correctly

• erewrite should be blue like rewrite
  
• Local in Local Ltac (and others?) should be highlighted
  

Automatic compliation of dependencies does not work with Coq 8.5's "From ... Require Import..."

When a file starts, for example, with

From program_logic Require Import ownership.

ProofGeneral fails to notice that it has to re-compile the file, and then immediately fails because of inconsistent assumptions about other modules.

coq-insert-intros: missing whitespace after period for multiple autogenerated intros

This issue was originally detected in company-coq for its `intros!' feature:
cpitclaudel/company-coq#23
It turns out that it is already present in ProofGeneral (coq-insert-intros).

When coq-insert-intros generates several calls to intros, they are separated with a period without whitespace.

Consider the following Coq script (23 True hypotheses imply False):

Goal True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> True -> False.

Now, when doing coq-insert-intros, here is the generated sequence of tactic calls:

intros H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H15 H16 H17 H18 H19 H20.intros H21.

There should be a whitespace after "H20." so that intros can be considered as a tactic call rather than a name qualified by the "H20" namespace.

In other words, there should be a whitespace after each "intros ... ." tactic line generated by coq-insert-intros for each line output by Show Intros.

(This seemingly small bug can be annoying for autogenerated lemmas with many hypotheses.)

ProofGeneral (sometimes?) does not build with Emacs 24.3.1 on Windows

Jason@JasonGross-x230t ~/Documents/GitHub/PG
$ make
****************************************************************
 Byte compiling...
****************************************************************
make elc
make[1]: Entering directory '/cygdrive/d/Documents/GitHub/PG'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (concat "/cygdrive/d/Documents/GitHub/PG/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile acl2/acl2.el

In toplevel form:
acl2/acl2.el:14:1:Error: Cannot open load file: proof-easy-config
Makefile:121: recipe for target 'acl2/acl2.elc' failed
make[1]: *** [acl2/acl2.elc] Error 1
make[1]: Leaving directory '/cygdrive/d/Documents/GitHub/PG'
Makefile:84: recipe for target 'compile' failed
make: *** [compile] Error 2

Jason@JasonGross-x230t ~/Documents/GitHub/PG
$ emacs --version
GNU Emacs 24.3.1
Copyright (C) 2013 Free Software Foundation, Inc.
GNU Emacs comes with ABSOLUTELY NO WARRANTY.
You may redistribute copies of Emacs
under the terms of the GNU General Public License.
For more information about these matters, see the file named COPYING.

Indentation is wrong after [exists]

This is the default indentation (on TABing the document). The proof script should be indented by 2 spaces.

Goal exists x, x = true.
                 evar (a : bool).
                 exists a.
                 refine (unit_rec (fun s => unit_rec _ _ s = _) _ tt).
                 exact true.

change coq-prog-name from _CoqProject

Hi,
Is it possible to change coq-prog-name from the _CoqProject?
I tried to add:
COQTOP = ~/.opam/coq/bin/coqtop
COQC = ~/.opam/coq/bin/coqc
to my _CoqProject but it dosn't work (PG still uses the coqtop of my system).
Thank you very much!

Time Print foo doesn't print foo

Definition foo (n : nat) : nat :=
match n with
| 0 => 1
| S _ => 0
end.

Time Extraction foo. (prints extraction and time)
Time Print foo. (prints only the time)

This is Coq 8.5beta3 (version 5122a39), PG version e0e2cea, emacs 24.4.1

ProofGeneral incorrectly parses unterminated strings in comments in Coq

$ cat src/foo.v
Check (* "a *) True.
$ coqc src/foo.v
Warning: Not interpreting "*)" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment.
File "D:\Documents\GitHub\fiat\src/foo.v", line 1, characters 9-21:
Syntax Error: Lexer: Unterminated string

But PG thinks this is fine.

compile-before-require does not use _CoqProject options or Makefile

I have been experimenting with modularizing a large Coq source file into multiple smaller source files. In conjunction with this, I would like to use the Coq->Settings->Compile Before Require option, but this always fails because my files require -impredicative-set, which is present at the head of my _CoqProject file, but which PG does not notice. How can I get PG to either pick up the proper settings from _CoqProject, or use the coq_makefile-generated Makefile to handle compile-before-require properly?

Relatedly - when editing a file that is Required by another, where that requirer is in proof mode in PG, PG asks to retract the requirer file and then starts up proof mode in the requiree file. Is there a way I can control this more precisely? One side-effect is that, since I am using 3 separate panes/frames/windows for proof mode, a retract and restart of Coq (because there is no way to save pane/frame/window size and position info) throws things out of wack such that I have to then spend some time reconfiguring things. Could PG just revert the other file to just prior to the problematic Require, leaving the panes/frames/windows as they are already configured, and allow me to edit the requiree file? In most cases, I don't really want to enter proof mode in the requiree file - I'm just making some trivial fix. If I want to enter proof mode in that requiree file, I can do something like PG toolbar Goto in that file.

Undo does not revert the processed region

If I C-/, and this deletes a word from the already processed region, the region is not reverted.

PG gets confused when there is another frame visible at start

I am trying out using the speedbar (Emacs->Options->Show/Hide->Speedbar) with PG, and noticed that when the speedbar is visible, PG can't start (as when doing a process-next-proof-command to start it up) properly - it gets an error about "Attempt to delete a surrogate minibuffer frame". I'm using PG in 3-windows/panes (but one one frame) mode.

At other times, when there are multiple Emacs frames, I have noticed that PG gets confused about which frame to use - sometimes preferring the frame not in focus when it is started (and deleting the other frame). I think this occurs when PG is started (as above) in the non-first frame.

This is using emacs 24.4.1, with PG e0e2cea and company-coq (although I am pretty sure it happens without company-coq as well).

Failed on-the-fly compilation dedicates goals window to compilation error message, confusing PG

Originally reported by @vzaliva on cpitclaudel/company-coq#66:

When one of the modules which is I am importing contains syntax error, after error 
message "Recompling binary failed with X status" company-coq (or proof general)
ends up in inconsistent state.
Attempting to step through any proofs leads to error message:

    "Window is dedicated to coq-compile response"

Even though I am focused in right buffer. The only solution is to restart Emacs.

Environment: 
  * Aquamacs 3.2
  * PG 4.3pre150313 (latest from git)
  *  Company-coq latest from MELPA

Does that ring a bell for anyone?

Cyclic dependencies

It would look better to get rid of this dependency :)

  … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el")

Connects with #32

prooftree is broken with 8.5 syntax

Regexp are outdated, I tried to fix it but I don't get the exact things to be matched. I guess we need Hendrik Tews for this. I will try to reach him.

Electric terminator and newlines

Hello,

I am using the electric terminator mode and I have "Proof Next Command Insert Space" enabled but when I enter a terminator ('.' in coq) PG moves the cursor ('|' in the example below) to the beginning of the next line, where I usually have 'Qed.' (or next lemma) so I have to do <RET>C-p<TAB> after writing a line in my proof. Is this an expected behaviour or a bug? I would like PG to insert a line and indent for me (unless the proof is finished or the editing was done somewhere in the middle of the proof). Thank you.

     exact a.
|  Qed.

I am using GNU Emacs 24.5.1, ProofGeneral (downloaded today from GitHub), company-coq and the following minor modes.

Auto-Composition Auto-Compression Auto-Encryption
Blink-Cursor Company Company-Coq Company-Coq--Keybindings
Diff-Auto-Refine Electric-Indent File-Name-Shadow Font-Lock
Global-Font-Lock Holes Hs Line-Number Menu-Bar Mouse-Wheel Outline
Prettify-Symbols Proof-Active-Buffer-Fake
Proof-Electric-Terminator-Enable Show-Paren Tooltip Transient-Mark Yas

Tip of master is broken on Coq 8.4pl*

It tries to pass -Q pwd``, which Coq 8.4 does not recognize.

Statement splitting incorrect in the presence of some notation

The following file compiles fine with Coq, but PG fails to step through it:

Definition ndot (n1 n2 : nat) := n1 + n2.
Infix ".:." := ndot (at level 19, left associativity).

Lemma name N x : (N .:. x) = (x .:. N).
Proof. Admitted.

lazymatch with bullets confuses C-M-f

Hey @Matafou,

This is in the indentation code, so I have no clue how to fix it :/

C-M-f on this bullet goes to end as expected:

- match goal with
  | [ H: forall x, ?f x -> _, H': ?f ?x |- _ ] => learn (H x)
  end.

But it goes after goal on this one:

- lazymatch goal with
  | [ H: forall x, ?f x -> _, H': ?f ?x |- _ ] => learn (H x)
  end.

Is there a way to make Double Hit Electric Terminator do an indent after the newline?

I am experimenting with ways of speeding up my Coqing (such as using company-coq) - and Double Hit Electric Terminator seems worth a try. But, now I have to hit Tab to indent after the newline. Is there a setting to get Double Hit to do the indent?

Also, speaking of indents - I know I mentioned this once before, but the extra indenting after the first line after a let/match clause is really bugging me - is there a way I can turn that off?

"Use project file" option does not work

I have a driectory structure like this:

dir1/
    __CoqProject
    dir2/
          _CoqProject
          File.v

I open File.v but before starting Coq process I uncheck menu item "Coq/Coq Program (ARGS)/Use project fie". However when I start Coq process and try to interpret buffer, options from project files are still used. Removing both project files helps.

Add *.elc to .gitignore

I've done this in my own clone, but you should probably do this globally. At least that way, users who do git status after building aren't flooded with warnings.

-- Jonathan

Do we support narrowing?

I'm seeing a lot of references to (point-min) and (point-max) in the code. @DavidAspinall, do you know if these really meant (point-min) and (point-max), or rather beginning and end of the buffer?

At the moment PG seems to break in a number of subtle ways when narrowing is in effect.

(Some) Imports from Coq standard library make the background compilation fail

I have a file containing just

Require Export Coq.Permutation.

If I step through this file with automatic compilation of dependencies enabled (either sequential or parallel), PG complains:

-*- mode: compilation; -*-

echo "Require Coq.Permutation." > /tmp/ProofGeneral-coq30265RNO.v /home/r/bin/coq-8.5/bin/coqdep -Q /home/r/Desktop/  /tmp/ProofGeneral-coq30265RNO.v
*** Warning: in file /tmp/ProofGeneral-coq30265RNO.v, library Coq.Permutation is required and has not been found in the loadpath!
*** Warning: in file /tmp/ProofGeneral-coq30265RNO.v, library Coq.Permutation is required and has not been found in the loadpath!
/tmp/ProofGeneral-coq30265RNO.vo /tmp/ProofGeneral-coq30265RNO.glob /tmp/ProofGeneral-coq30265RNO.v.beautified: /tmp/ProofGeneral-coq30265RNO.v
/tmp/ProofGeneral-coq30265RNO.vio: /tmp/ProofGeneral-coq30265RNO.v

easycrypt

Currently, adding PG support for easycrypt require a little bit of work.
See the README.
Perhaps, this can be one of the supported proof assistants?

PG files are here

Personally, I currently have some installation issues. Hence and issue and no pull-request.

warning building latest version d3d7622

jil@jess:~/git/PG$ make

---

Byte compiling...

---

make elc
make[1]: Entering directory '/home/jil/git/PG'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (concat "/home/jil/git/PG/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-par-compile.el
Source file `/home/jil/git/PG/coq/coq-system.el' newer than byte-compiled file

In coq-par-coqdep-arguments:
coq/coq-par-compile.el:463:11:Warning: coq-coqdep-prog-args called with 3
arguments, but accepts only 0-2

In coq-par-coqc-arguments:
coq/coq-par-compile.el:471:11:Warning: coq-coqc-prog-args called with 3
arguments, but accepts only 0-2

In end of data:
coq/coq-par-compile.el:1367:1:Warning: the function coq--pre-v85' is not known to be defined. Wrote /home/jil/git/PG/coq/coq-par-compile.elc emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (concat "/home/jil/git/PG/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-seq-compile.el Source file/home/jil/git/PG/coq/coq-system.el' newer than byte-compiled file

In coq-seq-get-library-dependencies:
coq/coq-seq-compile.el:77:18:Warning: coq-include-options called with 3
arguments, but accepts only 2

In coq-seq-compile-library:
coq/coq-seq-compile.el:116:12:Warning: coq-coqc-prog-args called with 3
arguments, but accepts only 0-2

In end of data:
coq/coq-seq-compile.el:407:1:Warning: the function `coq--pre-v85' is not known
to be defined.
Wrote /home/jil/git/PG/coq/coq-seq-compile.elc
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (concat "/home/jil/git/PG/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-system.el
Wrote /home/jil/git/PG/coq/coq-system.elc
make[1]: Leaving directory '/home/jil/git/PG'

---

Finished.

---

Errors encountered when a Compile Before Require fails

Hi all,

I have been encountering a couple of times the following error: "wrong-type-argument overlayp nil"

Here is the context in which one it occurs as far as I can tell:

• In file B, I try to compile file A by processing a Require Import A (using the option Compile Before Require)
• The compilation fails due to an error of mine, I therefore switch to file A
• Trying to process anything in A, I get the error "wrong-type-argument overlayp nil"
• If I try to get back to A, PG seems to try to process the command but it remains red and I get another error : Assertion failed: (eq proof-shell-busy queuemode)

The only solution I found is to restart Emacs.

Encountered on Mac Os X (El Capitan), with Emacs 24.5, PG 4.4pre, Coq 8.4pl6.

Here is an example of the stack trace when occuring:

Debugger entered--Lisp error: (wrong-type-argument overlayp nil)
span-set-endpoints(nil 1 25)
proof-extend-queue(25 ((#<overlay from 1 to 25 in logic.v> ("Require Import language.") proof-done-advancing nil)))
proof-assert-semis(((cmd "Require Import language." 25)) nil)
proof-assert-until-point()
proof-assert-next-command-interactive()
call-interactively(proof-assert-next-command-interactive nil nil)
command-execute(proof-assert-next-command-interactive)

Does it make sense to anyone?
Thanks,
Best,
Yannick.

Is `proof-shell-invisible-cmd-get-result' broken in Coq 8.5?

Hey @Matafou,

Running the following snippet with 8.5 shows the response in the Response buffer for me, and returns the goal as a string.

(proof-shell-invisible-cmd-get-result "Extraction nat.")

Is that expected? It didn't happen that way in 8.4.

Clément.

Incompatibility in the handling of _CoqProject files between coq_makefile and ProofGeneral

As far as I can tell, it's currently impossible to design a _CoqProject which passes -compat 8.4 -require Coq.Compat.Coq84 to both coq_makefile and ProofGeneral. I need something along the lines of

-arg "-compat 8.4"
-arg "-require Coq.Compat.Coq84"

to satisfy coq_makefile, which will blindly reorder -arg arguments. However, I need something along the lines of

-arg -compat
-arg 8.4
-arg -require
-arg Coq.Compat.Coq84

to satisfy ProofGeneral, which will otherwise invoke coqtop -emacs "-compat 8.4" "-require Coq.Compat.Coq84", which causes coqtop to barf. I think the correct thing to do is to fix PG to do string splitting on things that come after -arg in _CoqProjects.

error in process filter: Wrong number of arguments: window-frame, 0

Hello,
With the latest master commit 0f9b407 PG complains when I start processing a Coq file:
(progn (setq debug-on-entry t) (proof-assert-next-command-interactive))
leads to the backtrace below. Would you have a simple fix for this issue?
Best regards.

Debugger entered--Lisp error: (wrong-number-of-arguments window-frame 0)
  signal(wrong-number-of-arguments (window-frame 0))
  (condition-case err (progn (proof-shell-filter) (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))))
  (while call-proof-shell-filter (setq proof-shell-filter-active t proof-shell-filter-was-blocked nil) (condition-case err (progn (proof-shell-filter) (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))
  (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) (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)))
  (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) (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))))
  proof-shell-filter-wrapper("\n<prompt>Coq < 2 || 0 < </prompt>")
  run-hook-with-args(proof-shell-filter-wrapper "\n<prompt>Coq < 2 || 0 < </prompt>")
  (let ((saved-point (copy-marker (point) t))) (goto-char (process-mark process)) (set-marker scomint-last-output-start (point)) (insert string) (set-marker (process-mark process) (point)) (goto-char saved-point) (run-hook-with-args (quote scomint-output-filter-functions) string) (set-marker saved-point (point)))
  (save-current-buffer (set-buffer oprocbuf) (let ((saved-point (copy-marker (point) t))) (goto-char (process-mark process)) (set-marker scomint-last-output-start (point)) (insert string) (set-marker (process-mark process) (point)) (goto-char saved-point) (run-hook-with-args (quote scomint-output-filter-functions) string) (set-marker saved-point (point))))
  (progn (save-current-buffer (set-buffer oprocbuf) (let ((saved-point (copy-marker (point) t))) (goto-char (process-mark process)) (set-marker scomint-last-output-start (point)) (insert string) (set-marker (process-mark process) (point)) (goto-char saved-point) (run-hook-with-args (quote scomint-output-filter-functions) string) (set-marker saved-point (point)))))
  (if (and string (buffer-live-p oprocbuf)) (progn (save-current-buffer (set-buffer oprocbuf) (let ((saved-point (copy-marker (point) t))) (goto-char (process-mark process)) (set-marker scomint-last-output-start (point)) (insert string) (set-marker (process-mark process) (point)) (goto-char saved-point) (run-hook-with-args (quote scomint-output-filter-functions) string) (set-marker saved-point (point))))))
  (let ((oprocbuf (process-buffer process))) (if (and string (buffer-live-p oprocbuf)) (progn (save-current-buffer (set-buffer oprocbuf) (let ((saved-point (copy-marker ... t))) (goto-char (process-mark process)) (set-marker scomint-last-output-start (point)) (insert string) (set-marker (process-mark process) (point)) (goto-char saved-point) (run-hook-with-args (quote scomint-output-filter-functions) string) (set-marker saved-point (point)))))))
  scomint-output-filter(#<process coq> "\n<prompt>Coq < 2 || 0 < </prompt>")
  accept-process-output(#<process coq> 0.01 nil 1)
  (while (and proof-shell-busy (not quit-flag) (if timecount (> (setq timecount (1- timecount)) 0) t) (not (and interrupt-on-input (input-pending-p)))) (accept-process-output proverproc accepttime nil 1))
  (progn (while (and proof-shell-busy (not quit-flag) (if timecount (> (setq timecount (1- timecount)) 0) t) (not (and interrupt-on-input (input-pending-p)))) (accept-process-output proverproc accepttime nil 1)) (redisplay) (if quit-flag (error "Proof General: quit in proof-shell-wait")))
  (if proverproc (progn (while (and proof-shell-busy (not quit-flag) (if timecount (> (setq timecount (1- timecount)) 0) t) (not (and interrupt-on-input (input-pending-p)))) (accept-process-output proverproc accepttime nil 1)) (redisplay) (if quit-flag (error "Proof General: quit in proof-shell-wait"))))
  (let* ((proverproc (get-buffer-process proof-shell-buffer)) (accepttime 0.01) (timecount (if (numberp timeoutsecs) (/ timeoutsecs accepttime)))) (if proverproc (progn (while (and proof-shell-busy (not quit-flag) (if timecount (> (setq timecount ...) 0) t) (not (and interrupt-on-input (input-pending-p)))) (accept-process-output proverproc accepttime nil 1)) (redisplay) (if quit-flag (error "Proof General: quit in proof-shell-wait")))))
  proof-shell-wait()
  (if wait (proof-shell-wait))
  (progn (if (or (null proof-terminal-string) (not proof-shell-auto-terminate-commands) (string-match (concat (regexp-quote proof-terminal-string) "[   ]*$") cmd)) nil (setq cmd (concat cmd proof-terminal-string))) (if wait (proof-shell-wait)) (proof-shell-ready-prover) (let* ((callback (if invisiblecallback (let ((--cl-icb-- ...)) (let* (...) (set v invisiblecallback)) (progn (list ... ... ...))) (quote proof-done-invisible)))) (proof-start-queue nil nil (list (proof-shell-action-list-item cmd callback (cons (quote invisible) flags))))) (if wait (proof-shell-wait)))
  (if cmd (progn (if (or (null proof-terminal-string) (not proof-shell-auto-terminate-commands) (string-match (concat (regexp-quote proof-terminal-string) "[   ]*$") cmd)) nil (setq cmd (concat cmd proof-terminal-string))) (if wait (proof-shell-wait)) (proof-shell-ready-prover) (let* ((callback (if invisiblecallback (let (...) (let* ... ...) (progn ...)) (quote proof-done-invisible)))) (proof-start-queue nil nil (list (proof-shell-action-list-item cmd callback (cons (quote invisible) flags))))) (if wait (proof-shell-wait))))
  proof-shell-invisible-command("Set Undo 500 . " waitforit nil no-response-display)
  proof-shell-invisible-command-invisible-result("Set Undo 500 . ")
  mapc(proof-shell-invisible-command-invisible-result ("Set Undo 500 . " "Set Printing Width 75."))
  (if (listp proof-shell-init-cmd) (mapc (quote proof-shell-invisible-command-invisible-result) proof-shell-init-cmd) (proof-shell-invisible-command-invisible-result proof-shell-init-cmd))
  (progn (if (listp proof-shell-init-cmd) (mapc (quote proof-shell-invisible-command-invisible-result) proof-shell-init-cmd) (proof-shell-invisible-command-invisible-result proof-shell-init-cmd)))
  (if proof-shell-init-cmd (progn (if (listp proof-shell-init-cmd) (mapc (quote proof-shell-invisible-command-invisible-result) proof-shell-init-cmd) (proof-shell-invisible-command-invisible-result proof-shell-init-cmd))))
  (progn (run-hooks (quote proof-shell-init-hook)) (if proof-shell-init-cmd (progn (if (listp proof-shell-init-cmd) (mapc (quote proof-shell-invisible-command-invisible-result) proof-shell-init-cmd) (proof-shell-invisible-command-invisible-result proof-shell-init-cmd)))) (proof-shell-wait) (if proof-assistant-settings (mapcar (function (lambda (c) (proof-shell-invisible-command c t))) (proof-assistant-settings-cmds))))
  (unwind-protect (progn (run-hooks (quote proof-shell-init-hook)) (if proof-shell-init-cmd (progn (if (listp proof-shell-init-cmd) (mapc (quote proof-shell-invisible-command-invisible-result) proof-shell-init-cmd) (proof-shell-invisible-command-invisible-result proof-shell-init-cmd)))) (proof-shell-wait) (if proof-assistant-settings (mapcar (function (lambda (c) (proof-shell-invisible-command c t))) (proof-assistant-settings-cmds)))))
  (progn (setq proof-action-list nil) (proof-maybe-askprefs) (unwind-protect (progn (run-hooks (quote proof-shell-init-hook)) (if proof-shell-init-cmd (progn (if (listp proof-shell-init-cmd) (mapc (quote proof-shell-invisible-command-invisible-result) proof-shell-init-cmd) (proof-shell-invisible-command-invisible-result proof-shell-init-cmd)))) (proof-shell-wait) (if proof-assistant-settings (mapcar (function (lambda (c) (proof-shell-invisible-command c t))) (proof-assistant-settings-cmds))))))
  (if (memq (process-status proc) (quote (open run))) (progn (setq proof-action-list nil) (proof-maybe-askprefs) (unwind-protect (progn (run-hooks (quote proof-shell-init-hook)) (if proof-shell-init-cmd (progn (if (listp proof-shell-init-cmd) (mapc ... proof-shell-init-cmd) (proof-shell-invisible-command-invisible-result proof-shell-init-cmd)))) (proof-shell-wait) (if proof-assistant-settings (mapcar (function (lambda ... ...)) (proof-assistant-settings-cmds)))))))
  (let ((proc (get-buffer-process proof-shell-buffer))) (add-hook (quote kill-buffer-hook) (quote proof-shell-kill-function) t t) (set-process-sentinel proc (quote proof-shell-bail-out)) (if proof-shell-pre-sync-init-cmd (proof-shell-insert proof-shell-pre-sync-init-cmd (quote init-cmd))) (while (and (memq (process-status proc) (quote (open run))) (null (marker-position proof-marker))) (accept-process-output proc 1)) (if (memq (process-status proc) (quote (open run))) (progn (setq proof-action-list nil) (proof-maybe-askprefs) (unwind-protect (progn (run-hooks (quote proof-shell-init-hook)) (if proof-shell-init-cmd (progn (if ... ... ...))) (proof-shell-wait) (if proof-assistant-settings (mapcar (function ...) (proof-assistant-settings-cmds))))))))
  (save-current-buffer (set-buffer proof-shell-buffer) (progn (let ((--dolist-tail-- proof-shell-important-settings) sym) (while --dolist-tail-- (setq sym (car --dolist-tail--)) (proof-warn-if-unset "proof-shell-config-done" sym) (setq --dolist-tail-- (cdr --dolist-tail--))))) (setq font-lock-defaults (quote (proof-shell-font-lock-keywords))) (set (make-local-variable (quote font-lock-global-modes)) (list (quote not) proof-mode-for-shell)) (let ((proc (get-buffer-process proof-shell-buffer))) (add-hook (quote kill-buffer-hook) (quote proof-shell-kill-function) t t) (set-process-sentinel proc (quote proof-shell-bail-out)) (if proof-shell-pre-sync-init-cmd (proof-shell-insert proof-shell-pre-sync-init-cmd (quote init-cmd))) (while (and (memq (process-status proc) (quote (open run))) (null (marker-position proof-marker))) (accept-process-output proc 1)) (if (memq (process-status proc) (quote (open run))) (progn (setq proof-action-list nil) (proof-maybe-askprefs) (unwind-protect (progn (run-hooks (quote proof-shell-init-hook)) (if proof-shell-init-cmd (progn ...)) (proof-shell-wait) (if proof-assistant-settings (mapcar ... ...))))))))
  proof-shell-config-done()
  coq-shell-mode-config()
  (let ((delay-mode-hooks t)) (proof-shell-mode) (setq major-mode (quote coq-shell-mode)) (setq mode-name "Coq Shell") (progn (if (get (quote proof-shell-mode) (quote mode-class)) (put (quote coq-shell-mode) (quote mode-class) (get (quote proof-shell-mode) (quote mode-class)))) (if (keymap-parent coq-shell-mode-map) nil (set-keymap-parent coq-shell-mode-map (current-local-map))) (let ((parent (char-table-parent coq-shell-mode-syntax-table))) (if (and parent (not (eq parent (standard-syntax-table)))) nil (set-char-table-parent coq-shell-mode-syntax-table (syntax-table)))) (if (or (abbrev-table-get coq-shell-mode-abbrev-table :parents) (eq coq-shell-mode-abbrev-table local-abbrev-table)) nil (abbrev-table-put coq-shell-mode-abbrev-table :parents (list local-abbrev-table)))) (use-local-map coq-shell-mode-map) (set-syntax-table coq-shell-mode-syntax-table) (setq local-abbrev-table coq-shell-mode-abbrev-table) (coq-shell-mode-config))
  (progn (make-local-variable (quote delay-mode-hooks)) (let ((delay-mode-hooks t)) (proof-shell-mode) (setq major-mode (quote coq-shell-mode)) (setq mode-name "Coq Shell") (progn (if (get (quote proof-shell-mode) (quote mode-class)) (put (quote coq-shell-mode) (quote mode-class) (get (quote proof-shell-mode) (quote mode-class)))) (if (keymap-parent coq-shell-mode-map) nil (set-keymap-parent coq-shell-mode-map (current-local-map))) (let ((parent (char-table-parent coq-shell-mode-syntax-table))) (if (and parent (not (eq parent ...))) nil (set-char-table-parent coq-shell-mode-syntax-table (syntax-table)))) (if (or (abbrev-table-get coq-shell-mode-abbrev-table :parents) (eq coq-shell-mode-abbrev-table local-abbrev-table)) nil (abbrev-table-put coq-shell-mode-abbrev-table :parents (list local-abbrev-table)))) (use-local-map coq-shell-mode-map) (set-syntax-table coq-shell-mode-syntax-table) (setq local-abbrev-table coq-shell-mode-abbrev-table) (coq-shell-mode-config)))
  coq-shell-mode()
  funcall(coq-shell-mode)
  (save-current-buffer (set-buffer proof-shell-buffer) (erase-buffer) (proof-shell-set-text-representation) (save-current-buffer (set-buffer proof-response-buffer) (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-response)) (save-current-buffer (set-buffer proof-goals-buffer) (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-goals)) (if (buffer-live-p proof-trace-buffer) (save-current-buffer (set-buffer proof-trace-buffer) (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-response) (setq pg-response-eagerly-raise nil))) (funcall proof-mode-for-shell) (if (proof-shell-live-buffer) nil (switch-to-buffer proof-shell-buffer) (error "%s process exited!" proc)) (if proof-shell-fiddle-frames (let ((save-selected-window--state (internal--before-save-selected-window))) (save-current-buffer (unwind-protect (progn (let (...) (unwind-protect ... ...))) (internal--after-save-selected-window save-selected-window--state))))))
  (let ((proc (downcase proof-assistant))) (let* ((prog-name-list1 (if (functionp (intern (concat ... "-" ...))) (cons proof-prog-name (funcall (intern ...))) (if (symbol-value (intern ...)) (cons proof-prog-name (symbol-value ...)) (split-string proof-prog-name)))) (prog-name-list (if (and proof-rsh-command (> (length proof-rsh-command) 0)) (append (split-string proof-rsh-command) prog-name-list1) prog-name-list1)) (prog-command-line (mapconcat (quote identity) prog-name-list " ")) (process-connection-type proof-shell-process-connection-type) (process-adaptive-read-buffering nil) (process-environment (append (symbol-value (intern (concat ... "-" ...))) (if proof-shell-unicode process-environment (cons (if ... ... "LANG=C") (delete ... process-environment))))) (normal-coding-system-for-read coding-system-for-read) (coding-system-for-read (if proof-shell-unicode (or (condition-case nil (check-coding-system ...) (error nil)) normal-coding-system-for-read) (if (string-match "Linux" (shell-command-to-string "uname")) (quote raw-text) normal-coding-system-for-read))) (coding-system-for-write coding-system-for-read)) (message "Starting: %s" prog-command-line) (apply (quote scomint-make) (append (list proc (car prog-name-list) nil) (cdr prog-name-list))) (setq proof-shell-buffer (get-buffer (concat "*" proc "*"))) (if (proof-shell-live-buffer) nil (setq proof-shell-buffer nil) (error "Starting process: %s..failed" prog-command-line))) (proof-shell-make-associated-buffers) (save-current-buffer (set-buffer proof-shell-buffer) (erase-buffer) (proof-shell-set-text-representation) (save-current-buffer (set-buffer proof-response-buffer) (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-response)) (save-current-buffer (set-buffer proof-goals-buffer) (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-goals)) (if (buffer-live-p proof-trace-buffer) (save-current-buffer (set-buffer proof-trace-buffer) (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-response) (setq pg-response-eagerly-raise nil))) (funcall proof-mode-for-shell) (if (proof-shell-live-buffer) nil (switch-to-buffer proof-shell-buffer) (error "%s process exited!" proc)) (if proof-shell-fiddle-frames (let ((save-selected-window--state (internal--before-save-selected-window))) (save-current-buffer (unwind-protect (progn (let ... ...)) (internal--after-save-selected-window save-selected-window--state)))))) (message "Starting %s process... done." proc))
  (if (proof-shell-live-buffer) nil (setq proof-shell-filter-active nil) (setq proof-included-files-list nil) (let ((name (buffer-file-name (current-buffer)))) (if (and name proof-prog-name-guess proof-guess-command-line) (setq proof-prog-name (apply proof-guess-command-line (list name))))) (if proof-prog-name-ask (setq proof-prog-name (read-shell-command "Run process: " proof-prog-name))) (let ((proc (downcase proof-assistant))) (let* ((prog-name-list1 (if (functionp (intern ...)) (cons proof-prog-name (funcall ...)) (if (symbol-value ...) (cons proof-prog-name ...) (split-string proof-prog-name)))) (prog-name-list (if (and proof-rsh-command (> ... 0)) (append (split-string proof-rsh-command) prog-name-list1) prog-name-list1)) (prog-command-line (mapconcat (quote identity) prog-name-list " ")) (process-connection-type proof-shell-process-connection-type) (process-adaptive-read-buffering nil) (process-environment (append (symbol-value (intern ...)) (if proof-shell-unicode process-environment (cons ... ...)))) (normal-coding-system-for-read coding-system-for-read) (coding-system-for-read (if proof-shell-unicode (or (condition-case nil ... ...) normal-coding-system-for-read) (if (string-match "Linux" ...) (quote raw-text) normal-coding-system-for-read))) (coding-system-for-write coding-system-for-read)) (message "Starting: %s" prog-command-line) (apply (quote scomint-make) (append (list proc (car prog-name-list) nil) (cdr prog-name-list))) (setq proof-shell-buffer (get-buffer (concat "*" proc "*"))) (if (proof-shell-live-buffer) nil (setq proof-shell-buffer nil) (error "Starting process: %s..failed" prog-command-line))) (proof-shell-make-associated-buffers) (save-current-buffer (set-buffer proof-shell-buffer) (erase-buffer) (proof-shell-set-text-representation) (save-current-buffer (set-buffer proof-response-buffer) (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-response)) (save-current-buffer (set-buffer proof-goals-buffer) (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-goals)) (if (buffer-live-p proof-trace-buffer) (save-current-buffer (set-buffer proof-trace-buffer) (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-response) (setq pg-response-eagerly-raise nil))) (funcall proof-mode-for-shell) (if (proof-shell-live-buffer) nil (switch-to-buffer proof-shell-buffer) (error "%s process exited!" proc)) (if proof-shell-fiddle-frames (let ((save-selected-window--state (internal--before-save-selected-window))) (save-current-buffer (unwind-protect (progn ...) (internal--after-save-selected-window save-selected-window--state)))))) (message "Starting %s process... done." proc)))
  proof-shell-start()
  proof-shell-ready-prover(advancing)
  (save-excursion (if proof-script-buffer (progn (proof-deactivate-scripting) (if proof-script-buffer (error "You cannot have more than one active scripting buffer!")))) (proof-unregister-buffer-file-name (quote tell-the-prover)) (if proof-script-buffer (proof-deactivate-scripting)) (progn (or (null proof-script-buffer) (signal (quote cl-assertion-failed) (list (quote (null proof-script-buffer)) proof-script-buffer))) nil) (proof-shell-ready-prover queuemode) (setq proof-script-buffer (current-buffer)) (if (proof-locked-region-empty-p) (proof-init-segmentation)) (setq proof-active-buffer-fake-minor-mode t) (force-mode-line-update) (if (and proof-query-file-save-when-activating-scripting (not nosaves)) (save-some-buffers nil (function proof-query-save-this-buffer-p))) (if proof-activate-scripting-hook (let ((activated-interactively (called-interactively-p (quote any)))) (setq proof-shell-last-output-kind nil) (run-hooks (quote proof-activate-scripting-hook)) (if (or (eq (quote error) proof-shell-last-output-kind) (eq (quote interrupt) proof-shell-last-output-kind)) (progn (proof-deactivate-scripting) (error "Scripting not activated because of error or interrupt"))))))
  (if (equal (current-buffer) proof-script-buffer) nil (save-excursion (if proof-script-buffer (progn (proof-deactivate-scripting) (if proof-script-buffer (error "You cannot have more than one active scripting buffer!")))) (proof-unregister-buffer-file-name (quote tell-the-prover)) (if proof-script-buffer (proof-deactivate-scripting)) (progn (or (null proof-script-buffer) (signal (quote cl-assertion-failed) (list (quote (null proof-script-buffer)) proof-script-buffer))) nil) (proof-shell-ready-prover queuemode) (setq proof-script-buffer (current-buffer)) (if (proof-locked-region-empty-p) (proof-init-segmentation)) (setq proof-active-buffer-fake-minor-mode t) (force-mode-line-update) (if (and proof-query-file-save-when-activating-scripting (not nosaves)) (save-some-buffers nil (function proof-query-save-this-buffer-p))) (if proof-activate-scripting-hook (let ((activated-interactively (called-interactively-p (quote any)))) (setq proof-shell-last-output-kind nil) (run-hooks (quote proof-activate-scripting-hook)) (if (or (eq (quote error) proof-shell-last-output-kind) (eq (quote interrupt) proof-shell-last-output-kind)) (progn (proof-deactivate-scripting) (error "Scripting not activated because of error or interrupt")))))))
  proof-activate-scripting(nil advancing)
  proof-assert-until-point()
  (save-excursion (goto-char (proof-queue-or-locked-end)) (skip-chars-forward "     \n") (proof-assert-until-point))
  (progn (save-excursion (goto-char (proof-queue-or-locked-end)) (skip-chars-forward "  \n") (proof-assert-until-point)) (proof-maybe-follow-locked-end))
  (cond ((eq proof-buffer-type (quote script)) (progn (save-excursion (goto-char (proof-queue-or-locked-end)) (skip-chars-forward "     \n") (proof-assert-until-point)) (proof-maybe-follow-locked-end))) ((buffer-live-p proof-script-buffer) (save-current-buffer (set-buffer proof-script-buffer) (save-excursion (goto-char (proof-queue-or-locked-end)) (skip-chars-forward "     \n") (proof-assert-until-point)) (proof-maybe-follow-locked-end))))
  proof-assert-next-command-interactive()
  (progn (setq debug-on-entry t) (proof-assert-next-command-interactive))
  eval((progn (setq debug-on-entry t) (proof-assert-next-command-interactive)) nil)
  eval-expression((progn (setq debug-on-entry t) (proof-assert-next-command-interactive)) nil)
  call-interactively(eval-expression nil nil)

cursor is covering up my code when used in the terminal

When I'm using emacs in windowed mode, everything seems fine. However, when in the terminal, Proof General's cursor (indicating where it is in the code) covers up the first two characters of the line it's on.

This looks like a bug, but perhaps it's some sort of setting?

query-replace inside the processed region selects the first match, rather than the next one

If I use query-replace, and press RET to replace a match inside the processed region, the processed region (correctly) reverts, but then the next match selected is the first match of the document, rather than the subsequent match in the sequence.

proofdepth sometimes ends up being nil

From time to time I get this message:

Debugger entered--Lisp error: (wrong-type-argument number-or-marker-p nil)
  =(nil 0)
  (if (= proofdepth 0) (proof-clean-buffer proof-goals-buffer))
  (let* (ans (naborts 0) (nundos 0) (proofdepth (coq-get-span-proofnum span)) (proofstack (coq-get-span-proofstack span)) (span-staten (coq-get-span-statenum span)) (naborts (count-not-intersection coq-last-but-one-proofstack proofstack))) (if (= proofdepth 0) (proof-clean-buffer proof-goals-buffer)) (if (and (equal coq-last-but-one-proofstack proofstack) (= coq-last-but-one-proofnum proofdepth) (= coq-last-but-one-statenum span-staten)) nil (list (format "Backtrack %s %s %s . " (int-to-string span-staten) (int-to-string proofdepth) naborts))))
  (if (eq (span-property span (quote type)) (quote proverproc)) nil (let* (ans (naborts 0) (nundos 0) (proofdepth (coq-get-span-proofnum span)) (proofstack (coq-get-span-proofstack span)) (span-staten (coq-get-span-statenum span)) (naborts (count-not-intersection coq-last-but-one-proofstack proofstack))) (if (= proofdepth 0) (proof-clean-buffer proof-goals-buffer)) (if (and (equal coq-last-but-one-proofstack proofstack) (= coq-last-but-one-proofnum proofdepth) (= coq-last-but-one-statenum span-staten)) nil (list (format "Backtrack %s %s %s . " (int-to-string span-staten) (int-to-string proofdepth) naborts)))))
  coq-find-and-forget(#<overlay from 32260 to 32313 in ADTExamples.v>)
  funcall(coq-find-and-forget #<overlay from 32260 to 32313 in ADTExamples.v>)
  (proof-setup-retract-action start end (funcall proof-find-and-forget-fn target) undo-action displayflags)
  (nconc actions (proof-setup-retract-action start end (funcall proof-find-and-forget-fn target) undo-action displayflags))
  (setq actions (nconc actions (proof-setup-retract-action start end (funcall proof-find-and-forget-fn target) undo-action displayflags)))
  (if (> end start) (setq actions (nconc actions (proof-setup-retract-action start end (funcall proof-find-and-forget-fn target) undo-action displayflags))))
  (let ((end (proof-unprocessed-begin)) (start (span-start target)) (span (if proof-arbitrary-undo-positions target (proof-last-goal-or-goalsave))) actions) (if (and span proof-kill-goal-command (not (or (memq (span-property span (quote type)) (quote (goalsave proverproc)))))) (if (< (span-end span) (span-end target)) (progn (setq span target) (while (and span (memq (span-property span ...) (quote ...))) (setq span (next-span span (quote type)))) (setq actions (proof-setup-retract-action start end (if (null span) nil (funcall proof-count-undos-fn span)) undo-action) end start)) (setq proof-nesting-depth (1- proof-nesting-depth)) (setq actions (proof-setup-retract-action (span-start span) end (list proof-kill-goal-command) undo-action displayflags) end (span-start span)))) (if (> end start) (setq actions (nconc actions (proof-setup-retract-action start end (funcall proof-find-and-forget-fn target) undo-action displayflags)))) (proof-start-queue (min start end) (proof-unprocessed-begin) actions (quote retracting)))
  proof-retract-target(#<overlay from 32260 to 32313 in ADTExamples.v> nil nil)
  (if span (proof-retract-target span undo-action displayflags) (proof-debug "proof-retract-until-point: couldn't find a span!"))
  (let ((span (span-at (point) (quote type)))) (if span nil (proof-goto-end-of-locked) (backward-char) (setq span (span-at (point) (quote type)))) (if span (proof-retract-target span undo-action displayflags) (proof-debug "proof-retract-until-point: couldn't find a span!")))
  (if (proof-locked-region-empty-p) nil (let ((span (span-at (point) (quote type)))) (if span nil (proof-goto-end-of-locked) (backward-char) (setq span (span-at (point) (quote type)))) (if span (proof-retract-target span undo-action displayflags) (proof-debug "proof-retract-until-point: couldn't find a span!"))))
  (if (proof-locked-region-empty-p) (error "No locked region") (proof-activate-scripting) (proof-shell-ready-prover) (if (proof-locked-region-empty-p) nil (let ((span (span-at (point) (quote type)))) (if span nil (proof-goto-end-of-locked) (backward-char) (setq span (span-at (point) (quote type)))) (if span (proof-retract-target span undo-action displayflags) (proof-debug "proof-retract-until-point: couldn't find a span!")))))
  proof-retract-until-point(nil)
  (progn (goto-char (span-start lastspan)) (proof-retract-until-point undo-action))
  (if (setq lastspan (span-at-before (proof-unprocessed-begin) (quote type))) (progn (goto-char (span-start lastspan)) (proof-retract-until-point undo-action)) (error "Nothing to undo!"))
  (if (proof-locked-region-empty-p) nil (if (setq lastspan (span-at-before (proof-unprocessed-begin) (quote type))) (progn (goto-char (span-start lastspan)) (proof-retract-until-point undo-action)) (error "Nothing to undo!")))
  (save-excursion (if (proof-locked-region-empty-p) nil (if (setq lastspan (span-at-before (proof-unprocessed-begin) (quote type))) (progn (goto-char (span-start lastspan)) (proof-retract-until-point undo-action)) (error "Nothing to undo!"))))
  (let (lastspan) (save-excursion (if (proof-locked-region-empty-p) nil (if (setq lastspan (span-at-before (proof-unprocessed-begin) (quote type))) (progn (goto-char (span-start lastspan)) (proof-retract-until-point undo-action)) (error "Nothing to undo!")))) (if lastspan (proof-maybe-follow-locked-end (span-start lastspan))))
  (progn (let (lastspan) (save-excursion (if (proof-locked-region-empty-p) nil (if (setq lastspan (span-at-before (proof-unprocessed-begin) (quote type))) (progn (goto-char (span-start lastspan)) (proof-retract-until-point undo-action)) (error "Nothing to undo!")))) (if lastspan (proof-maybe-follow-locked-end (span-start lastspan)))))
  (cond ((eq proof-buffer-type (quote script)) (progn (let (lastspan) (save-excursion (if (proof-locked-region-empty-p) nil (if (setq lastspan ...) (progn ... ...) (error "Nothing to undo!")))) (if lastspan (proof-maybe-follow-locked-end (span-start lastspan)))))) ((buffer-live-p proof-script-buffer) (save-current-buffer (set-buffer proof-script-buffer) (let (lastspan) (save-excursion (if (proof-locked-region-empty-p) nil (if (setq lastspan ...) (progn ... ...) (error "Nothing to undo!")))) (if lastspan (proof-maybe-follow-locked-end (span-start lastspan)))))))
  proof-undo-last-successful-command-1()
  proof-undo-last-successful-command()
  funcall-interactively(proof-undo-last-successful-command)
  #<subr call-interactively>(proof-undo-last-successful-command nil nil)
  ad-Advice-call-interactively(#<subr call-interactively> proof-undo-last-successful-command nil nil)
  apply(ad-Advice-call-interactively #<subr call-interactively> (proof-undo-last-successful-command nil nil))
  call-interactively(proof-undo-last-successful-command nil nil)
  command-execute(proof-undo-last-successful-command)

I don't have a good way to reproduce this yet, unfortunately.

Highlighting of evars

Evars are currently using a pretty agressive highlighting scheme (heavy orange background). It's nice, but it's apply to slightly too many things. In particular, it also ctaches Ltac binders ( as in match _ with ?x = ?y). This is particulary unpleasant when reading a large match-goal form using Print Ltac.

It used to be easy to fix the problem, since evars always used numbers. In 8.5, however, evars now keep their names. If there was a way to tell evars from non-evars I'd be all for highlighting them differently, but I don't think there is such a way anymore; is there?

Company-coq currently highlights ltac binders as variables in Coq buffers. Maybe we should justhiglight all patterns like ?abc as variables, instead of the heavy orange highlighting? It might even make the new style evars more readable. The suggesting boild down to making proof-eager-annotation-face inherit from font-lock-variable-name-face

btw, do you know why the dependent evars line at the end of a proof doesn't show the new-style names? For example:

Goal exists x y z, x + y = z.
Proof.
  exists 1.
  exists 2.
  eexists; reflexivity.

prints

No more subgoals.
(dependent evars: ?X11 using ,)

"Setting" menu should we pre-fill string options for all provers

Currently when setting something via [Coq/Settings/foo] the current value of the foo is not pre-filled.

When an integer is asked to the user (like for the Printing Width) this is ok.

But if a (long) string is asked (I am thinking about the [Coq/Settings/Search Blacklist] option that I just pushed (commit ff9ec2e)) I prefer to have it prefilled with the current value and be able modify it in the minibuffer.

The commit I just made does this (for string options) only for coq by redefining a macro defined in generic/proof-utils.el (namely proof-defstringset-fn).

But if we think this is what all provers want I would rather modify the macro instead of redefining it. What do other prover users think about that?

P.

Edit Abbrevs broken?

I don't succeed in editing abbrevs.

Step to reproduce:

• Click Coq > ABBREVS > Abbrev Mode (here it works)
• Click Coq > ABBREVS > Edit Abbrevs
• edit an abbrev (let's say change "a" in "aa" for auto)
• save the buffer (it says "Wrote /home/rascar/.emacs.d/abbrev_defs" and it indeed creates this file, which is merely empty, see here)
• go back to Coq (it works with the edited abbrevs)
• try to close emacs, it asks "Save abbrevs to ~/.emacs.d/abbrev_defs?"
• answer Yes (the file abbrev_defs stay the same)
• now if you reopen emacs and enable abbrevs no one abbrev is available ...

Temporarily, is there a way to change abbrevs directly in the code of PG?

Cleaning up whitespace shouldn't require rewinding

In most cases (in all?), removing extra whitespace at the end of a line shouldn't require rewinding; even outside of comments. Yet at the moment calling whitespace-cleanup will cause PG to rewind to the earliest point where some space was removed.

This is a bit frustrating, so I'd like to push a patch to suppress the rewinding behaviour when removing space at the end of the line. Are there objections?

Also, what should be the proper behaviour? Do we allow insertion of spaces as well? Only at the end of lines? Or anywhere outside of strings and outside of symbols? (is space significant anywhere in Coq?)

indentation takes a long time, maybe forever

Apparently, some recent change has made indentation take a very long time to do a single tab or newline-and-indent. I'm not even sure how long -as I have to stop it. It might just be looping forever.

The problem doesn't always occur, only after certain constructs. I will attempt to isolate it.

I'm using version c480238 with emacs 24.4.1.

We should edit the README

I don't know how far we support old Emacsen, and I don't know if we have the resources to try to support very old versions. I'd vote for supporting anything that ships with debian stable (24.4), and nothing older.

I think the README should give installation instructions, too.

PG does not compile

$ make clean
...
$ git log -1
commit 2626ed51dc27abbdb44331542642c03e7f65ef3a
Author: Clément Pit--Claudel <[email protected]>
Date:   Sat Feb 20 22:56:14 2016 -0500

    Simplify code to add to .emacs

$ make
****************************************************************
 Byte compiling...
****************************************************************
make elc
make[1]: Entering directory '/cygdrive/d/Documents/GitHub/PG'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (concat "/cygdrive/d/Documents/GitHub/PG/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile acl2/acl2.el

In toplevel form:
acl2/acl2.el:14:1:Error: Cannot open load file: proof-easy-config
Makefile:121: recipe for target 'acl2/acl2.elc' failed
make[1]: *** [acl2/acl2.elc] Error 1
make[1]: Leaving directory '/cygdrive/d/Documents/GitHub/PG'
Makefile:84: recipe for target 'compile' failed
make: *** [compile] Error 2

Support ssreflect-style indentation

Dear PG devs,

it would be great if proofgeneral coq could support ssreflect's style indentation.

In order to maximize horizontal proof space, the ssreflect library uses a more conservative indentation, for instance, this is typical code:

Section A.

Lemma a : P.
Proof.
case/orP=> ...
  by rewrite U.
exact: Pm.
Qed.

End A.

AFAICT, the current recommendation is to disable indentation which is a pity. IMHO we could:

• have an explicit variable use-ssreflect-indent.
• automatically detect the import of ssreflect and switch the variable on.

I would be happy to try to provide a patch if the PG devs agree on how they would like this feature to be integrated.

Thanks,
Emilio

Should we bind C-c C-j in terminals?

C-c C-RET (proof-goto-point) doesn't work in shells. Should we bind C-c C-j instead on TTYs?

More commands are not highlighted

• Set Universe Polymorphism
  
• Set Printing Universes
  
• Local in Local Ltac (and others?) should be highlighted
  
• Set Keyed Unification
  

Request to add keystroke for Coq's "Print Assumptions" command

I received a request to add a keystroke, calling this code:

(defun coq-Print-Assumptions ()
   "Ask for an ident and print the assumptions it depends on."
   (interactive)
   (coq-ask-do "Print Assumptions" "Print Assumptions"))

PG hangs with a commands > 4096 characters

I have read in forums that process output may be cut every 4098 characters, but comint mode seems to send only the first 4096 chars of a command if there is no newline, and wait for the next linebreak to send the remaining part. This makes pg hang because the commands are "stripped" of CR before being sent to the comint buffer.

Don't know the right fix here. Stripping is done to ensure having only one prompt per command.

Buffer coq-compile-response sometimes takes over the whole window

Sometimes when there is an error while compiling files (parallel compilation in background enabled), the buffer *coq-compile-response* pops up to cover the entire window (as in, the X11 window) of emacs. In this case, switching back to the buffer that I am actually editing is impossible; emacs says I cannot switch buffers in a "dedicated window". I have to kill multiple buffers to go on working; usually I just restart emacs.

Unfortunately, I found no way to reproduce this.

Proof General automatically resizes goals/response windows between proof steps

In any coq proof script, whenever I step through a proof in three-window mode, the goal and response windows automatically resize. More specifically, the response window shrinks/expands to fit whatever text it is showing, and thus the goals window expands/shrinks accordingly. Based on my understanding of the proof-three-window-enable option (which I have enabled), this behavior should not occur:

"Setting this option triggers a three-buffer mode of interaction where the goals buffer and response buffer are both displayed, rather than the two-buffer mode where they are switched between. It also prevents Emacs automatically resizing windows between proof steps."

I can always get back to the original window positions by hitting ^C^L.

My software platform:
OSX 10.11.3
Aquamacs 3.2
PG 4.4pre (updated 2/19/2016, installed through homebrew)
Coq 8.5 (installed through homebrew)