Refine command does not work on Emacs 30

[patrick-nicodemus]

Refine command does not work on Emacs 30

[nad]

The documentation of pp states the following:

This function outputs object to stream, just like prin1, but does it in a prettier way. That is, it’ll indent and fill the object to make it more readable for humans.

If the only difference between pp (or pp-to-string) and prin1 is that pp can add extra whitespace to the output, then perhaps we could use prin1 instead.

[andreasabel]

@UlfNorell Maybe we should investigate before releasing 2.6.4.1 whether mentioned commit introduced a regression...

• #6954

[patrick-nicodemus]

Please let me know if anyone can reproduce this. I am new to Agda and it may be user error.

[UlfNorell]

It would be good if someone with some Emacs knowledge (@nad?) could take a look.

[nad]

Can you provide us with the contents of the *agda2* buffer (with any private information redacted)? You could start Emacs, load an Agda file, attempt to refine, and then switch to the *agda2* buffer and copy its contents.

[patrick-nicodemus]

Here you go! If there is any other information I can provide, let me know.
agda2-buffer.log

IOTCM "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda" NonInteractive Indirect ( Cmd_load_highlighting_info "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda" )
(agda2-status-action "")
IOTCM "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda" NonInteractive Indirect ( Cmd_load "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda" [] )
(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-status-action "Checked")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
IOTCM "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda" NonInteractive Indirect ( Cmd_tokenHighlighting "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda" Keep )
IOTCM "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda" NonInteractive Indirect ( Cmd_load "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda" [] )
(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-info-action "*Type-checking*" "Checking hello-world-dep (/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda).\n" t)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : unit\n" nil)
((last . 1) . (agda2-goals-action '(0)))
IOTCM "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda" NonInteractive Indirect ( Cmd_refine_or_intro False 0 (intervalsToRange (Just (mkAbsolute "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda"
)) [Interval (Pn () 126 7 6) (Pn () 126 7 6)]) "" )
cannot read: IOTCM "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda" NonInteractive Indirect ( Cmd_refine_or_intro False 0 (intervalsToRange (Just (mkAbsolute "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda"
cannot read: )) [Interval (Pn () 126 7 6) (Pn () 126 7 6)]) "" )
IOTCM "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda" NonInteractive Indirect ( Cmd_refine_or_intro False 0 (intervalsToRange (Just (mkAbsolute "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda"
)) [Interval (Pn () 126 7 6) (Pn () 126 7 6)]) "" )
cannot read: IOTCM "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda" NonInteractive Indirect ( Cmd_refine_or_intro False 0 (intervalsToRange (Just (mkAbsolute "/home/patrick/programming/agda/hello-world-dep/hello-world-dep.agda"
cannot read: )) [Interval (Pn () 126 7 6) (Pn () 126 7 6)]) "" )

[nad]

It seems as if the Emacs mode sends malformed strings with newlines to the Agda backend:

IOTCM "[…]/hello-world-dep.agda" NonInteractive Indirect ( Cmd_refine_or_intro False 0 (intervalsToRange (Just (mkAbsolute "[…]/hello-world-dep.agda"
)) [Interval (Pn () 126 7 6) (Pn () 126 7 6)]) "" )
cannot read: IOTCM "[…]/hello-world-dep.agda" NonInteractive Indirect ( Cmd_refine_or_intro False 0 (intervalsToRange (Just (mkAbsolute "[…]/hello-world-dep.agda"
cannot read: )) [Interval (Pn () 126 7 6) (Pn () 126 7 6)]) "" )

[andreasabel]

This text is produced here:

agda/src/data/emacs-mode/agda2-mode.el

Lines 1668 to 1669 in fa70e79

	(format "(intervalsToRange (Just (mkAbsolute %s)) %s)"
	(agda2-string-quote (file-truename (buffer-file-name)))

A new line could end up before )) if agda2-string-quote produced a newline at the end.
@patrick-nicodemus coud you test if the expression (agda2-string-quote (file-truename (buffer-file-name))) produces something ending with a newline? In that case, wrapping it in string-trim could help.

[andreasabel]

Actually, this issue looks like another effect of the recent change in pp.el (adding extra newlines) as reported in #6953.

@patrick-nicodemus wrote:

I rolled back to the last release Agda 2.6.4 and I was able to get it working ok, so I think this is a problem with relatively recent code.
As I am on Emacs 30, perhaps it is related to this #6953
and this 4b23885

This is really the only patch added after 2.6.4, and it seems unlikely that it could cause such behavior.
In fact, this patch rather fixes problems with additional newlines introduced by a recent pp.el.

Could it be that your rollback to 2.6.4 also include a rollback to an older version of pp.el?

[andreasabel]

@patrick-nicodemus and @kutsurak could you please test the agda2-mode from the following PR:

• #6995

[patrick-nicodemus]

@patrick-nicodemus and @kutsurak could you please test the agda2-mode from the following PR:

* [[ emacs ] `string-trim` to combat recent change in `pp.el` adding newlines #6995](https://github.com/agda/agda/pull/6995)

This works for me!

[patrick-nicodemus]

Oh, I realize now that I said something misleading. Agda 2.6.4 was not "working fine". Another user had given me a patch to fix it and it worked fine downstream of that change.

This is really the only patch added after 2.6.4, and it seems unlikely that it could cause such behavior.
In fact, this patch rather fixes problems with additional newlines introduced by a recent pp.el.
Could it be that your rollback to 2.6.4 also include a rollback to an older version of pp.el?

Yes I left out something important. Agda mode in 2.6.4. was basically not working at all in Emacs 30 but another user suggested I patch it by running
(defun agda2-string-quote (s) (format "%S" s))
after opening Emacs.
What I meant to say was that Agda-mode in 2.6.4 works fine for me on Emacs 30 after running that command to patch things. I talked about this in the previous bug report I filed but forgot to reiterate it here.

I did not use that patch when testing Agda 2.6.4.1.

[kutsurak]

@patrick-nicodemus and @kutsurak could you please test the agda2-mode from the following PR:

* [[ emacs ] `string-trim` to combat recent change in `pp.el` adding newlines #6995](https://github.com/agda/agda/pull/6995)

This works for me as well.

In my original issue I mentioned that I am not convinced this change in the pp- functions was correct, but I haven't had time to take it up to the emacs mailing list. However thinking about it a bit more I realized that pp- functions are meant to be used for presenting a string to humans. Maybe agda-mode needs different functions with stable API, that prepare strings for communication with the agda process. I am not sure if functions like these exist already or need to be written, but I don't think it would be terribly difficult. What do you think?

[andreasabel]

@kutsurak wrote:

However thinking about it a bit more I realized that pp- functions are meant to be used for presenting a string to humans. Maybe agda-mode needs different functions with stable API, that prepare strings for communication with the agda process. I am not sure if functions like these exist already or need to be written, but I don't think it would be terribly difficult. What do you think?

I could well be that using pp- only works "by accident". So, yes, I approve the move to something more systematic.

https://www.gnu.org/software/emacs/manual/html_node/elisp/Formatting-Strings.html

@patrick-nicodemus wrote:

patch it by running
(defun agda2-string-quote (s) (format "%S" s))
after opening Emacs.

Thanks for the clarification. This explains the behavior.

Maybe format "%S" is what we want, but maybe it is not sufficient when it comes to Haskell-suitable unicode encoding. The manual just says

strings are enclosed in ‘"’ characters, and ‘\’ characters appear where necessary before special characters.

[andreasabel]

@nad: Administrative remark: Since this issue is on milestone 2.6.4.1 and listed as closed in the release notes for 2.6.4.1, please open a new issue for this.

[nad]

Agda 2.6.4.1 has not been released yet, right? However, if you don't plan to amend your fix, then this issue can be closed again.