proof-general solving holes

[ElifUskuplu]

I attempted to handle "solve a hole" in proofgeneral mode.

• When a hole created after a load (C-c C-n), use C-c C-SPC to enter the process
• Narya then asks for hole number. If the hole d exists, and the user prompts d, then Narya asks for a term.
• Provide the term and press enter. Then Narya fill the hole and load again.
• Since hole numbers increase after a new load, if the user is not sure about the hole number, one can use C-c C-? to see all holes.

I think it works, but let me know if you have any suggestions.

[mikeshulman]

This is a good start, thanks! Here are some suggestions for improvement:

• I don't think the user should have to know about hole numbers. Instead, I suggest that C-c C-SPC only works if the cursor is already on a hole, in which case it applies to that hole. The user can easily move the cursor between holes with C-c C-j and C-c C-k.
• I don't think it should be necessary to reset the processed region to the location of the solved hole with proof-assert-next-command-interactive. Since solve works on a past hole without undoing later commands, I think it should be okay to just do that and leave the processed region as-is. Unless I'm missing something?
• If the user-supplied term fails to solve the hole, nothing should be done to the buffer and Narya's error message should be displayed in the response buffer.

Let me know if it would be helpful to modify the output of solve when -proofgeneral is in effect.

[ElifUskuplu]

Thanks for the suggestions.

• First, I did that C-c C-SPC only works if the cursor is already on a hole. I personally don't want to bother with positioning the cursor :) but you're right, it is better. Agda does the same, so I assume many users are familiar with this need. Changing it in narya-solve-hole is easy.
• I'm not sure about reload issue. In -interactive mode, yes, when you solve a hole, later commands are not undone. Actually you're not changing the previous commands, just providing a new one. In -proofgeneral mode, however, if we expect to replace '?' with a succeeded term, this success means that loading with new term compiles without error. So we are changing the scripting buffer. So later commands are affected. Am I miss something?
• If we reload the buffer after some change, the hole numbers change increasingly. E.g. if there are hole 0, hole 1, hole 2 and you want to solve hole 1 manually, when you delete ? it automatically undone the later commands, so when you solved it and load the buffer again, the holes become hole 0, hole 3. If you don't solve hole 1 and reload, it becomes hole 0, hole 3, hole 4. Is this something you did intentionally?
• Also, in -proofgeneral mode, when you undo some commands, it changes holes. If you undo all commands involving holes and check C-c C-?, it says 'no open holes'.

[mikeshulman]

It's true that when we successfully solve a hole in proofgeneral mode, we should replace the ? with the supplied term in the source file, so that later executions of the same file will use that term directly rather than creating a hole. However, there's no need to do that immediately, because the solve command directly binds the hole metavariable to the value of the supplied term, so that going forward it is as if that term had been written in place of the ? in the first place. If going back and reloading the scripting buffer from the hole location produces any different behavior from not doing so, then that's a bug in the solve command.

In particular, what I'm saying is that the replacement of the ? by the supplied term should not cause later commands to be undone and the processed region of the buffer to be rolled back; it should modify the processed region without changing the location of the endpoint of that region. It's true that when the user tries to edit the processed region (outside a comment), ProofGeneral automatically rolls it back to the edit location, and that's correct since in general such edits would change the meaning of later commands. But when doing it programmatically in narya-solve-hole, it should be possible to temporarily disable or go around this behavior so that the processed region stays the same, because in this particular case we know (assuming solve is working correctly) that it won't change the meaning of later commands.

Hole numbers are assigned sequentially in each session. It would be too much trouble to try to keep track of which holes have been un-done so that their numbers could be re-used, and since the user isn't supposed to ever have to think about the hole numbers, it shouldn't matter.

[mikeshulman]

Another thing that needs to be dealt with somehow here is notation precedence. For instance, if we have a hole appearing as a function argument like f ?, and we solve the hole with something like x + y, then simply replacing the question-mark by the term x + y produces f x + y which would be parsed incorrectly as (f x) + y. So sometimes, at least, parentheses need to be added around the solving term when inserting it into the buffer to replace the ?.

The simplest thing would be to always insert such parentheses, but that would look a bit ugly in cases where they aren't necessary. However, the only other option I can think of is for each hole to store the precedence at which it was parsed (which shouldn't be too hard) and for parsing of a new term to somehow compute the maximum precedence in which it could be parsed without parentheses (which would require some less trivial alterations to the parser), so that they could be compared and parentheses inserted only if necessary.

How does Agda deal with this issue?

[ElifUskuplu]

I'll check Agda-mode and try to figure out it later. I have other questions before proceed:

If going back and reloading the scripting buffer from the hole location produces any different behavior from not doing so, then that's a bug in the solve command.

You mean after binding the hole metavariable to the value of the supplied term, if we going back and reload, the hole shouldn't be captured? I understand that since there is still ? in the script, when we undo and reload a hole, it's still a hole. You can try it with the following basic solve function

(defun narya-solve-hole ()
  (interactive)
  (let ((hole (get-char-property (point) 'narya-hole)))
    (if hole
        (let ((term (read-string (format "Term to solve hole: "))))
          (proof-shell-invisible-command (concat "solve " (number-to-string hole) " := " term)))
        (message "No hole at point to solve."))))

Am I missing something?

Second, to do replacement, I should check whether solve n := term command has an error or not. So I would like to use output of it. I tried proof-shell-last-output, but it is not recognized. I can define separately, but there is also narya-handle-output function, so maybe I can use it. Do you have any suggestion?

[mikeshulman]

No, I mean that in two hypothetical different worlds, in which we do two different things, namely:

1. In world number 1, we solve hole n with term t.
2. In world number 2, we instead undo back to the command where hole n was defined, replace the ? that defined it with term t, and then re-execute that command and all the following commands up to the point where we were,

Then the future behavior of these two worlds, as far as interaction with Narya goes, should be indistinguishable.

This is like Agda's behavior with filling holes too, except that Agda doesn't have a notion of only partially processing the file. When you fill a hole in Agda, it replaces the hole in the Emacs buffer with the new term, but it doesn't reload the entire file: it internally binds that hole to the term you supplied, and other commands that use that hole now behave as if you'd written that term in place of the hole originally. Sometimes something goes wrong and you do have to reload the entire file, but (I would argue) whenever that happens it is a bug in Agda, even if it's one that's been declared unfixable.

[mikeshulman]

Regarding checking for errors, did you try proof-shell-last-output-kind?

[ElifUskuplu]

Yes, I tried (string-match-p proof-shell-error-regexp (proof-shell-last-output-kind)) to check the error, but when I run the function, I receive string-match-p: Symbol’s function definition is void: proof-shell-last-output-kind. If there is no mistake in the idea, maybe we need another require at the beginning of narya.el to call this function.

[mikeshulman]

proof-shell-last-output-kind is a variable, not a function. Do C-h v on it.

[ElifUskuplu]

I think it's better now. Also in the case we need to get the response after executing solve command, I added

;; Wait for the process to output its result
        (accept-process-output (get-buffer-process proof-shell-buffer) 1) ;; Adjust timeout if needed

Let me know if you suggest any improvement.

[mikeshulman]

Thanks! I haven't tested it yet, but according to the documentation of proof-shell-invisible-command there is an optional WAIT argument that makes it wait for processing to finish before returning, which would probably be better than accept-process-output with a timeout.

[ElifUskuplu]

Thanks, you're right. I edited it.

[mikeshulman]

Another option here would be to iterate only through the overlays at point with overlays-in, looking for one that has a narya-hole property. I don't know which would be better, just thought I would mention it.

[ElifUskuplu]

If you mean the following

(let ((hole-overlay (car (seq-filter (lambda (ovl)
                                       (overlay-get ovl 'narya-hole))
                                     (overlays-in (point) (point))))))

It didn't work because it does not capture a hole overlay. But I might have mistyped it.

However, the following worked

(let ((hole-overlay (car (seq-filter (lambda (ovl)
                                         (overlay-get ovl 'narya-hole))
                                       (overlays-at (point))))))

[mikeshulman]

Ah, yes, that makes sense -- overlays-in requires at least one character to be contained in both the overlay and the region supplied, whereas the region from point to point is always empty. So overlays-at is correct.

[mikeshulman]

This is good! Two more things to do that I can think of, before we merge this:

1. If the new term includes new holes, there should be overlays created for them. This means doing some or all of narya-handle-output. I'm not sure whether you can just call narya-handle-output directly, or whether the hole-creating code should be factored out of it into another function that is called on solving.
2. Deal somehow with precedence, so that the inserted term is at least guaranteed to parse correctly if we undo and re-execute it. The simple solution would be to just always add parentheses around it; we could do that for now and put a smarter approach on the to-do list. Did you check what Agda does?

[ElifUskuplu]

1. If the new term includes new holes, there should be overlays created for them. This means doing some or all of narya-handle-output. I'm not sure whether you can just call narya-handle-output directly, or whether the hole-creating code should be factored out of it into another function that is called on solving.
2. Deal somehow with precedence, so that the inserted term is at least guaranteed to parse correctly if we undo and re-execute it. The simple solution would be to just always add parentheses around it; we could do that for now and put a smarter approach on the to-do list. Did you check what Agda does?

I'll look at those soon.