Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Emacs 30 breaks agda mode #6953

Closed
kutsurak opened this issue Nov 5, 2023 · 1 comment · Fixed by #6954 or #6995
Closed

Emacs 30 breaks agda mode #6953

kutsurak opened this issue Nov 5, 2023 · 1 comment · Fixed by #6954 or #6995
Labels
ux: emacs Issues relating to the Emacs agda2-mode
Milestone

Comments

@kutsurak
Copy link
Contributor

kutsurak commented Nov 5, 2023

A relatively recent change in pp.el in the development branch of emacs breaks the function agda2-send-command by adding newlines at the end of filenames.

To reproduce open any agda file in a recent emacs 30 build running version 2.6.4 or master (the issue is reproducible in both), and call agda2-load. This results in the following errors in the *agda2* buffer:

IOTCM "/tmp/hello-world-dep.agda"
 NonInteractive Indirect ( Cmd_load "/tmp/hello-world-dep.agda"
 [] )
Agda2> cannot read: IOTCM "/tmp/hello-world-dep.agda"
Agda2> cannot read:  NonInteractive Indirect ( Cmd_load "/tmp/hello-world-dep.agda"
Agda2> cannot read:  [] )

I used the following as a minimal emacs configuration after installing agda using stack:

;;; -*- lexical-binding: t -*-

(load-file (let ((coding-system-for-read 'utf-8))
             (shell-command-to-string "agda-mode locate")))

;; auto-load agda-mode for .agda and .lagda.md
(setq auto-mode-alist
   (append
     '(("\\.agda\\'" . agda2-mode)
       ("\\.lagda.md\\'" . agda2-mode))
     auto-mode-alist))

I am not entirely convinced that the change in the behavior of pp-to-string is correct, but I have a simple workaround until the issue has been investigated/resolved on the emacs side. A PR with it follows.

kutsurak added a commit to kutsurak/agda that referenced this issue Nov 5, 2023
@andreasabel andreasabel added this to the 2.6.4.1 milestone Nov 11, 2023
@andreasabel andreasabel added the ux: emacs Issues relating to the Emacs agda2-mode label Nov 11, 2023
@andreasabel
Copy link
Member

A relatively recent change in pp.el in the development branch of emacs breaks the function agda2-send-command by adding newlines at the end of filenames.

Oh, but this is also an explanation for the malformed strings in #6983 (comment) which have additional line-breaks after filenames.

So this issue is not fully fixed with

More string-trimming is needed after we invoke pp- functions.

andreasabel added a commit that referenced this issue Nov 14, 2023
…lines

Fixes #6953 which reports the symptom and identifies `pp.el` as cause.
Closes #6983.
andreasabel added a commit that referenced this issue Nov 15, 2023
…lines

Fixes #6953 which reports the symptom and identifies `pp.el` as cause.
Closes #6983.
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 12, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 12, 2024
…lines

Fixes agda#6953 which reports the symptom and identifies `pp.el` as cause.
Closes agda#6983.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ux: emacs Issues relating to the Emacs agda2-mode
Projects
None yet
2 participants