Unknown error in process filter

[ElifUskuplu]

We're working on PG configuration for a new proof assistant narya. You can check the current .el file here. I'd like to add a function to solve holes (terms in ? form). It does seem working, but we realized a problem and don't understand why. Here is the function

(defun narya-solve-hole ()
  "Solve the current hole with a user-provided term."
  (interactive)
  (let ((hole-overlay (car (seq-filter (lambda (ovl)
                                         (overlay-get ovl 'narya-hole))
                                       (overlays-at (point))))))
    (if (not hole-overlay)
        ;; If the cursor is not on a hole, display a warning message.
        (message "Place the cursor on a hole.")
      ;; If the cursor is on a hole, prompt the user to enter a term.
      (let ((term (read-string "Enter the term to solve the hole: ")))
        ;; Wait a bit since the following part causes freezing in some cases
        (with-timeout (2 (message "The solve command timed out."))
          ;; Execute the solve command with the entered term.
          (proof-shell-invisible-command
           (format "solve %d := %s" (overlay-get hole-overlay 'narya-hole) term)
           t))
        ;; Check the output after executing the solve command.
        (if (eq proof-shell-last-output-kind 'error)
            ;; Display error message if the entered term is incorrect.
            (message "You entered an incorrect term.")
          ;; Otherwise, replace the hole with the entered term.
          (let ((inhibit-read-only t))
            (goto-char (overlay-start hole-overlay))
            (delete-region (overlay-start hole-overlay) (overlay-end hole-overlay))
            (insert term)
            (delete-overlay hole-overlay)
            (setq narya-hole-overlays (delq hole-overlay narya-hole-overlays))
            (message "Hole solved.")))))))

(keymap-set narya-mode-map "C-c C-SPC" 'narya-solve-hole)

As a working example, suppose I have basic setup:

axiom X : Type

axiom a : A

def f : X -> X := ?

1. When I try to solve the hole with x |-> a, the function narya-solve-hole succeeds as I expected.
2. When I try to solve the hole with c, it says "You entered an incorrect term." as I expected.
3. However, the problem happens when I try to use ? or x|-> ? as solutions. It basically means "keep the hole" or create a term involving new holes. Narya allows it, so proof-shell-last-output-kind is not 'error and replacement should be done. The problem occurs at proof-shell-invisible-command . After the function timed out, it does replacement, but gives the following message

   error in process filter: proof-shell-filter-wrapper: Wrong type argument: integer-or-marker-p, nil
   error in process filter: Wrong type argument: integer-or-marker-p, nil
   The solve command timed out.
   Hole solved.

   Without timeout, emacs is freezing. It seems there is not a complete command available to parse in the buffer after the hole being solved, but I don't get it why.

Even more weird part is that this is only happening in a new narya .ny file. If you work in a file obtained by github repo of the program, it works. For example, we tried this file, and no problem occured.

Any idea or suggestion would be great.

[monnier]

However, the problem happens when I try to use ? or x|-> ? as solutions. It basically means "keep the hole" or create a term involving new holes. Narya allows it, so proof-shell-last-output-kind is not 'error and replacement should be done. The problem occurs at proof-shell-invisible-command . After the function timed out, it does replacement, but gives the following message:

error in process filter: proof-shell-filter-wrapper: Wrong type argument: integer-or-marker-p, nil
error in process filter: Wrong type argument: integer-or-marker-p, nil
The solve command timed out.
Hole solved.

Without timeout, Emacs is freezing. It seems there is not a complete command available to parse in the buffer after the hole being solved, but I don't get it why. [...] Any idea or suggestion would be great.

You should be able to get a backtrace with (setq debug-on-error t). Also, without the timeout, when Emacs freezes, you should be able to get a backtrace by (previously) setting both (setq debug-on-error t) and (setq debug-on-quit t) and then hitting C-g while Emacs appears frozen. If C-g doesn't work, try kill -USR2 <EMACSPID>.

[ElifUskuplu]

When adding these settings to .emacs, no freezing in errors occurs even without the timeout, thanks.

From Backtrace, I receive

Debugger entered--Lisp error: (wrong-type-argument integer-or-marker-p nil)
  signal(wrong-type-argument (integer-or-marker-p nil))
  proof-shell-filter-wrapper(" ￫ \33[33mwarning[W3000]\33[m\n ￮ \33[33mthere is 1 open ...")
  run-hook-with-args(proof-shell-filter-wrapper " ￫ \33[33mwarning[W3000]\33[m\n ￮ \33[33mthere is 1 open ...")
  scomint-output-filter(#<process narya> " ￫ \33[33mwarning[W3000]\33[m\n ￮ \33[33mthere is 1 open ...")
  accept-process-output(#<process narya> 0.01 nil 1)
  proof-shell-wait()
  proof-shell-invisible-command("solve 0 := ?" t)
  (let ((term (read-string "Enter the term to solve the hole: "))) (proof-shell-invisible-command (format "solve %d := %s" (overlay-get hole-overlay 'narya-hole) term) t) (if (eq proof-shell-last-output-kind 'error) (message "You entered an incorrect term.") (let ((inhibit-read-only t)) (goto-char (overlay-start hole-overlay)) (delete-region (overlay-start hole-overlay) (overlay-end hole-overlay)) (insert term) (delete-overlay hole-overlay) (setq narya-hole-overlays (delq hole-overlay narya-hole-overlays)) (message "Hole solved."))))
  (if (not hole-overlay) (message "Place the cursor on a hole.") (let ((term (read-string "Enter the term to solve the hole: "))) (proof-shell-invisible-command (format "solve %d := %s" (overlay-get hole-overlay 'narya-hole) term) t) (if (eq proof-shell-last-output-kind 'error) (message "You entered an incorrect term.") (let ((inhibit-read-only t)) (goto-char (overlay-start hole-overlay)) (delete-region (overlay-start hole-overlay) (overlay-end hole-overlay)) (insert term) (delete-overlay hole-overlay) (setq narya-hole-overlays (delq hole-overlay narya-hole-overlays)) (message "Hole solved.")))))
  (let ((hole-overlay (car (seq-filter #'(lambda (ovl) (overlay-get ovl ...)) (overlays-at (point)))))) (if (not hole-overlay) (message "Place the cursor on a hole.") (let ((term (read-string "Enter the term to solve the hole: "))) (proof-shell-invisible-command (format "solve %d := %s" (overlay-get hole-overlay 'narya-hole) term) t) (if (eq proof-shell-last-output-kind 'error) (message "You entered an incorrect term.") (let ((inhibit-read-only t)) (goto-char (overlay-start hole-overlay)) (delete-region (overlay-start hole-overlay) (overlay-end hole-overlay)) (insert term) (delete-overlay hole-overlay) (setq narya-hole-overlays (delq hole-overlay narya-hole-overlays)) (message "Hole solved."))))))
  narya-solve-hole()
  funcall-interactively(narya-solve-hole)
  command-execute(narya-solve-hole)

[monnier]

Debugger entered--Lisp error: (wrong-type-argument integer-or-marker-p nil)
  signal(wrong-type-argument (integer-or-marker-p nil))
  proof-shell-filter-wrapper("...")
  [...]

Hmm... this backtrace is probably not as useful as it could because proof-shell-filter-wrapper catches errors and re-signals them. Can you install the patch below (which avoids the catch+resignal, thus hopefully preserving the true origin of the error) and then try again, to see if you get a "better" backtrace?

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 14e1ede318..ccd7d0dee9 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.

 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2021  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2024  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
@@ -1506,14 +1506,14 @@ calls."
       (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))))
+   (let ((non-local-exit t))
+     (unwind-protect
+         (progn
+           (proof-shell-filter)
+           (setq non-local-exit nil))
+       (setq proof-shell-filter-active nil)
+       (when non-local-exit
+         (setq proof-shell-filter-was-blocked nil))))
    (setq call-proof-shell-filter proof-shell-filter-was-blocked)))
     ;; finally leaving proof-shell-filter - maybe somebody has added
     ;; priority items inside proof-shell-filter?

[ElifUskuplu]

Now, it becomes

Debugger entered--Lisp error: (wrong-type-argument integer-or-marker-p nil)
  make-overlay(nil nil nil nil nil)
  (let* ((hole (string-to-number (match-string 1 string))) (bpos (position-bytes (save-excursion (goto-char (proof-unprocessed-begin)) (skip-chars-forward " \11\n") (point)))) (hstart (byte-to-position (+ bpos (string-to-number (match-string 2 string))))) (hend (byte-to-position (+ bpos (string-to-number (match-string 3 string))))) (ovl (make-overlay hstart hend nil nil nil))) (setq narya-hole-overlays (cons ovl narya-hole-overlays)) (overlay-put ovl 'narya-hole hole) (overlay-put ovl 'face 'narya-hole-face))
  (save-current-buffer (set-buffer proof-script-buffer) (let* ((hole (string-to-number (match-string 1 string))) (bpos (position-bytes (save-excursion (goto-char (proof-unprocessed-begin)) (skip-chars-forward " \11\n") (point)))) (hstart (byte-to-position (+ bpos (string-to-number (match-string 2 string))))) (hend (byte-to-position (+ bpos (string-to-number (match-string 3 string))))) (ovl (make-overlay hstart hend nil nil nil))) (setq narya-hole-overlays (cons ovl narya-hole-overlays)) (overlay-put ovl 'narya-hole hole) (overlay-put ovl 'face 'narya-hole-face)))
  (cond ((eq proof-buffer-type 'script) (progn (let* ((hole (string-to-number (match-string 1 string))) (bpos (position-bytes (save-excursion ... ... ...))) (hstart (byte-to-position (+ bpos ...))) (hend (byte-to-position (+ bpos ...))) (ovl (make-overlay hstart hend nil nil nil))) (setq narya-hole-overlays (cons ovl narya-hole-overlays)) (overlay-put ovl 'narya-hole hole) (overlay-put ovl 'face 'narya-hole-face)))) ((buffer-live-p proof-script-buffer) (save-current-buffer (set-buffer proof-script-buffer) (let* ((hole (string-to-number (match-string 1 string))) (bpos (position-bytes (save-excursion ... ... ...))) (hstart (byte-to-position (+ bpos ...))) (hend (byte-to-position (+ bpos ...))) (ovl (make-overlay hstart hend nil nil nil))) (setq narya-hole-overlays (cons ovl narya-hole-overlays)) (overlay-put ovl 'narya-hole hole) (overlay-put ovl 'face 'narya-hole-face)))))
  (while (string-match "^\\([0-9]+\\) \\([0-9]+\\) \\([0-9]+\\).*\n" string dpos) (cond ((eq proof-buffer-type 'script) (progn (let* ((hole (string-to-number ...)) (bpos (position-bytes ...)) (hstart (byte-to-position ...)) (hend (byte-to-position ...)) (ovl (make-overlay hstart hend nil nil nil))) (setq narya-hole-overlays (cons ovl narya-hole-overlays)) (overlay-put ovl 'narya-hole hole) (overlay-put ovl 'face 'narya-hole-face)))) ((buffer-live-p proof-script-buffer) (save-current-buffer (set-buffer proof-script-buffer) (let* ((hole (string-to-number ...)) (bpos (position-bytes ...)) (hstart (byte-to-position ...)) (hend (byte-to-position ...)) (ovl (make-overlay hstart hend nil nil nil))) (setq narya-hole-overlays (cons ovl narya-hole-overlays)) (overlay-put ovl 'narya-hole hole) (overlay-put ovl 'face 'narya-hole-face))))) (setq dpos (match-end 0)))
  (progn (progn (setq rend (match-beginning 0)) (setq gstart (match-end 0))) (string-match "\f\\[data\\]\f\n" string gstart) (progn (setq gend (match-beginning 0)) (setq dpos (match-end 0))) (while (string-match "^\\([0-9]+\\) \\([0-9]+\\) \\([0-9]+\\).*\n" string dpos) (cond ((eq proof-buffer-type 'script) (progn (let* ((hole ...) (bpos ...) (hstart ...) (hend ...) (ovl ...)) (setq narya-hole-overlays (cons ovl narya-hole-overlays)) (overlay-put ovl 'narya-hole hole) (overlay-put ovl 'face 'narya-hole-face)))) ((buffer-live-p proof-script-buffer) (save-current-buffer (set-buffer proof-script-buffer) (let* ((hole ...) (bpos ...) (hstart ...) (hend ...) (ovl ...)) (setq narya-hole-overlays (cons ovl narya-hole-overlays)) (overlay-put ovl 'narya-hole hole) (overlay-put ovl 'face 'narya-hole-face))))) (setq dpos (match-end 0))) (if (proof-shell-exec-loop) (progn (setq proof-shell-last-goals-output (substring string gstart gend)) (proof-shell-display-output-as-response flags (substring string rstart rend)) (if (memq 'no-goals-display flags) nil (pg-goals-display proof-shell-last-goals-output t)))) (setq proof-shell-last-output-kind 'goals) (if proof-tree-external-display (progn (proof-tree-handle-delayed-output old-proof-marker cmd flags span))))
  (if (string-match "\f\\[goals\\]\f\n" string rstart) (progn (progn (setq rend (match-beginning 0)) (setq gstart (match-end 0))) (string-match "\f\\[data\\]\f\n" string gstart) (progn (setq gend (match-beginning 0)) (setq dpos (match-end 0))) (while (string-match "^\\([0-9]+\\) \\([0-9]+\\) \\([0-9]+\\).*\n" string dpos) (cond ((eq proof-buffer-type 'script) (progn (let* (... ... ... ... ...) (setq narya-hole-overlays ...) (overlay-put ovl ... hole) (overlay-put ovl ... ...)))) ((buffer-live-p proof-script-buffer) (save-current-buffer (set-buffer proof-script-buffer) (let* (... ... ... ... ...) (setq narya-hole-overlays ...) (overlay-put ovl ... hole) (overlay-put ovl ... ...))))) (setq dpos (match-end 0))) (if (proof-shell-exec-loop) (progn (setq proof-shell-last-goals-output (substring string gstart gend)) (proof-shell-display-output-as-response flags (substring string rstart rend)) (if (memq 'no-goals-display flags) nil (pg-goals-display proof-shell-last-goals-output t)))) (setq proof-shell-last-output-kind 'goals) (if proof-tree-external-display (progn (proof-tree-handle-delayed-output old-proof-marker cmd flags span)))))
  (let ((span (car (car proof-action-list))) (cmd (nth 1 (car proof-action-list))) (flags (nth 3 (car proof-action-list))) (rstart 0) (rend 0) (gstart 0) (gend 0) (dpos 0)) (if (string-match "\f\\[goals\\]\f\n" string rstart) (progn (progn (setq rend (match-beginning 0)) (setq gstart (match-end 0))) (string-match "\f\\[data\\]\f\n" string gstart) (progn (setq gend (match-beginning 0)) (setq dpos (match-end 0))) (while (string-match "^\\([0-9]+\\) \\([0-9]+\\) \\([0-9]+\\).*\n" string dpos) (cond ((eq proof-buffer-type 'script) (progn (let* ... ... ... ...))) ((buffer-live-p proof-script-buffer) (save-current-buffer (set-buffer proof-script-buffer) (let* ... ... ... ...)))) (setq dpos (match-end 0))) (if (proof-shell-exec-loop) (progn (setq proof-shell-last-goals-output (substring string gstart gend)) (proof-shell-display-output-as-response flags (substring string rstart rend)) (if (memq 'no-goals-display flags) nil (pg-goals-display proof-shell-last-goals-output t)))) (setq proof-shell-last-output-kind 'goals) (if proof-tree-external-display (progn (proof-tree-handle-delayed-output old-proof-marker cmd flags span))))))
  narya-handle-output(("solve 0 := ?\n\f\n") " ￫ \33[32minfo[I0005]\33[m\n ￮ \33[32mhole solved, contai...")
  proof-shell-handle-immediate-output(("solve 0 := ?\n\f\n") 491 731 (invisible))
  proof-shell-filter-manage-output(491 731)
  proof-shell-filter()
  proof-shell-filter-wrapper(" ￫ \33[33mwarning[W3000]\33[m\n ￮ \33[33mthere is 1 open ...")
  run-hook-with-args(proof-shell-filter-wrapper " ￫ \33[33mwarning[W3000]\33[m\n ￮ \33[33mthere is 1 open ...")
  scomint-output-filter(#<process narya> " ￫ \33[33mwarning[W3000]\33[m\n ￮ \33[33mthere is 1 open ...")
  accept-process-output(#<process narya> 0.01 nil 1)
  proof-shell-wait()
  proof-shell-invisible-command("solve 0 := ?" t)
  (let ((term (read-string "Enter the term to solve the hole: "))) (proof-shell-invisible-command (format "solve %d := %s" (overlay-get hole-overlay 'narya-hole) term) t) (if (eq proof-shell-last-output-kind 'error) (message "You entered an incorrect term.") (let ((inhibit-read-only t)) (goto-char (overlay-start hole-overlay)) (delete-region (overlay-start hole-overlay) (overlay-end hole-overlay)) (insert term) (delete-overlay hole-overlay) (setq narya-hole-overlays (delq hole-overlay narya-hole-overlays)) (message "Hole solved."))))
  (if (not hole-overlay) (message "Place the cursor on a hole.") (let ((term (read-string "Enter the term to solve the hole: "))) (proof-shell-invisible-command (format "solve %d := %s" (overlay-get hole-overlay 'narya-hole) term) t) (if (eq proof-shell-last-output-kind 'error) (message "You entered an incorrect term.") (let ((inhibit-read-only t)) (goto-char (overlay-start hole-overlay)) (delete-region (overlay-start hole-overlay) (overlay-end hole-overlay)) (insert term) (delete-overlay hole-overlay) (setq narya-hole-overlays (delq hole-overlay narya-hole-overlays)) (message "Hole solved.")))))
  (let ((hole-overlay (car (seq-filter #'(lambda (ovl) (overlay-get ovl ...)) (overlays-at (point)))))) (if (not hole-overlay) (message "Place the cursor on a hole.") (let ((term (read-string "Enter the term to solve the hole: "))) (proof-shell-invisible-command (format "solve %d := %s" (overlay-get hole-overlay 'narya-hole) term) t) (if (eq proof-shell-last-output-kind 'error) (message "You entered an incorrect term.") (let ((inhibit-read-only t)) (goto-char (overlay-start hole-overlay)) (delete-region (overlay-start hole-overlay) (overlay-end hole-overlay)) (insert term) (delete-overlay hole-overlay) (setq narya-hole-overlays (delq hole-overlay narya-hole-overlays)) (message "Hole solved."))))))
  narya-solve-hole()
  funcall-interactively(narya-solve-hole)
  command-execute(narya-solve-hole)

[monnier]

So the error seems to be in your code (in narya-handle-output). I assume you'll take it from there.

Side note: byte-to-position and position-to-byte are usually the wrong tool here, because they work with Emacs's internal encoding whereas you're presumably concerned with mapping from "byte position in the file" to "char position in the buffer" which depends on the file's encoding. For that we have bufferpos-to-filepos and filepos-to-bufferpos.

[ElifUskuplu]

Thanks, I'll look at it.

Also, I'm asking because I don't know it. Is your note also related to position-bytes? Is there any better option?

[monnier]

Also, I'm asking because I don't know it. Is your note also related to position-bytes?

Yes (I just misspelled it position-to-byte, sorry).

Is there any better option?

The two I mentioned.

[ElifUskuplu]

This change seems like the solution because it worked in a file previously problematic. However, in this case other cases were affected. The situation is related to the difference between X -> X and X → X, I mean Unicode characters. Narya has this setup. For holes defined like f : X -> X := ? narya-solve-hole worked after I made changes you suggested in narya-handle-output. For holes defined like f : X → X ≔ ? it does not even capture the hole overlay. How can I solve the issue?

[monnier]

I think you're going to have to track down the details yourself: look at the buffer positions in the Emacs buffer, the positions sent/received by the prover (check how those are specified and interpreted), etc... to figure out where is the error. These issues are often delicate because too many protocols don't consider them very carefully (e.g. the authors didn't think about them at all and assumed char=byte=column). And then there are the off-by-one, of course.

[ElifUskuplu]

I understand, thanks for your help.

[ElifUskuplu]

I'll try to handle the rest.

[mikeshulman]

I agree that this is a problem we have to solve ourselves, not an issue with PG. But if you don't mind explaining further, I'm confused by your comment about bufferpos-to-filepos and filepos-to-bufferpos. In this function I don't think we are interacting with the buffer file at all -- doesn't PG take text directly out of the buffer and send it to the prover subprocess? So why should the file encoding matter?

[monnier]

I agree that this is a problem we have to solve ourselves, not an issue with PG. But if you don't mind explaining further, I'm confused by your comment about bufferpos-to-filepos and filepos-to-bufferpos. In this function I don't think we are interacting with the buffer file at all -- doesn't PG take text directly out of the buffer and send it to the prover subprocess? So why should the file encoding matter?

Hmm... right, it's more a question of the encoding used to communicate with the subprocess. If the encoding is always utf-8-unix, then position-bytes and byte-to-position should work to convert byte positions to buffer positions (modulo the proverbial off-by-one), since Emacs's internal encoding is (since Emacs-23) a variant of utf-8 (more specifically, it's the same as utf-8 for valid utf-8 byte sequences).

The error you get shows that the two calls to byte-to-position were passed an argument that's "outside" of the current buffer (presumably too large rather than too small). Could it be that the skip-chars-forward used to get bpos ended up further than intended?

[mikeshulman]

Yes, we already figured out our problem and that was it: the hole position offsets reported by the prover were relative to the beginning of the command, while the function creating overlays assumed that the entire command was present in the buffer, which in the case of an invisible command it isn't. Thanks.

Does ProofGeneral always use utf-8-unix for its prover subprocesses? Or is that configurable?

[monnier]

Does ProofGeneral always use utf-8-unix for its prover subprocesses? Or is that configurable?

AFAICT if proof-shell-unicode is non-nil, then PG will use utf-8. I don't see anything that enforces Unix encoding of line separators OTOH, so it's possible the byte positions will be off under Windows when the text spans several lines.

[mikeshulman]

Hmm, interesting. Would there be any prospect of updating PG to allow the line endings to also be specified? I observe that the Emacs Lisp manual 38.9.3 Decoding Process Output says

Warning: Coding systems such as undecided, which determine the coding system from the data, do not work entirely reliably with asynchronous subprocess output. This is because Emacs has to process asynchronous subprocess output in batches, as it arrives. Emacs must try to detect the proper coding system from one batch at a time, and this does not always work. Therefore, if at all possible, specify a coding system that determines both the character code conversion and the end of line conversion—that is, one like latin-1-unix, rather than undecided or latin-1.