Janitorial Changes to agda-mode #6536
Conversation
phikal
changed the title
|
See #6537. |
|
I might be getting confused by the GitHub interface, but it looks like each of these PRs have all the changes? |
|
If you check out my repository with all the branches, you should see a linear history. The PRs are all just check-points. I am more used to a mailing-like oriented workflow that are more flexible that what GitHub provides, so I apologize for the confusion |
|
@andreasabel @nad Are there any objections or suggestions to these changes? |
phikal
force-pushed
the
janitorial-changes
branch
from
da16bfa
to
a9e1691
Compare
|
In the CI it seems this job failed due to external reason: https://github.com/agda/agda/actions/runs/4473173434/jobs/7860232876?pr=6536. Does anyone know how I can restart the check? |
|
I've restarted the failed check |
|
Thanks, that seems to have resolved the "issue". |
phikal
force-pushed
the
janitorial-changes
branch
from
a9e1691
to
66173f7
Compare
* agda2-mode.el (agda2-infer-type-maybe-toplevel): Sharp-quote 'agda2-infer-type'. (agda2-solveAll-action): Sharp-quite 'agda2-solve-action'. (agda2-compute-normalised-maybe-toplevel): Sharp quote 'agda2-compute-normalised' and 'agda2-compute-normalised-toplevel'. Sharp-quoting functions indicates that a symbol should have a bound function slot, and that the byte compiler should check if this is the case, otherwise emit a warning.
|
There's a minor conflict with the new commands for mimer, but otherwise this could be merged? @phikal @andreasabel |
|
Ulf Norell ***@***.***> writes:
There's a minor conflict with the new commands for mimer, but
otherwise this could be merged? @phikal @andreasabel
What is mimer?
|
|
Mimer is the new proof search implementation that's replaced Agsy. The only change to the emacs mode was that a few functions changed name: So resolving the conflict should be very easy. |
|
Ulf Norell ***@***.***> writes:
Mimer is the new proof search implementation that's replaced Agsy. The only change to the emacs mode was that a few functions changed name:
```
agda2-auto-maybe-all -> agda2-mimer-maybe-all
agda2-autoOne -> agda2-mimer
agda2-autoAll -> agda2-mimerAll
```
So resolving the conflict should be very easy.
I have already pushed a commit that should do that, hope it works.
|
|
What is |
|
It's the test suite for interaction (including emacs mode) and latex/html backends. The failure is Looks like there's an |
phikal
force-pushed
the
janitorial-changes
branch
from
596d35b
to
4d04442
Compare
|
Ulf Norell ***@***.***> writes:
It's the test suite for interaction (including emacs mode) and
latex/html backends. The failure is
```
In toplevel form:
.stack-work/install/x86_64-linux-tinfo6/c[23](https://github.com/agda/agda/actions/runs/7899951138/job/21560919935?pr=6536#step:10:24)f5779f04ca365f7af9f8d9932e847eec90e64c6a7ddb9ecf116023008e198/9.8.1/share/x86_64-linux-ghc-9.8.1/Agda-2.6.5/emacs-mode/agda2-mode.el:1990:1:
Error: the function ‘agda2-auto-maybe-all’ is not known to be defined.
Unable to compile the following Emacs Lisp files:
/home/runner/work/agda/agda/.stack-work/install/x86_64-linux-tinfo6/c23f5779f04ca365f7af9f8d9932e847eec90e64c6a7ddb9ecf116023008e198/9.8.1/share/x86_64-linux-ghc-9.8.1/Agda-2.6.5/emacs-mode/agda2-mode.el
```
Looks like there's an `agda2-auto-maybe-all` that should be
`agda2-mimer-maybe-all`.
Right, I have adjusted that, the byte-compiler doesn't appear to
complain on my system anymore.
|
|
OK, looks like that was the mistake. |
|
Nice. Anyone with more elisp experience want to weigh in on this? @nad @andreasabel? |
|
FWIW there already was some discussion in #6123. @nad had some critical comments, where I am not sure if he was satifisied by my response. I hope I am not mistaken by the impression that @andreasabel is supportive of these changes, considering his helpful assistance along the way. |
|
I see that my changes have been merged in a single commit. Is there any particular reason for this, because it losses information on what change was made why, e.g. when using |
|
Ah, sorry, that's our default merge strategy. You can tag with the label |
|
Where can I add that tag? Asking for the other PRs. |
|
@UlfNorell : The Agda mode now badly malfunctions on my machine since today, when I pulled and rebuilt from master. |
|
Andreas Abel ***@***.***> writes:
@UlfNorell : The Agda mode now badly malfunctions on my machine since today, when I pulled and rebuilt from master.
So I guess this merge should be reverted.
Could you describe the issues you've been having?
Also, I wouldn't object to reverting the commit if we could apply it
again without squashing the commits.
|
|
It prints tons of errors and beeps inbetween. Here is an excerpt of my I'm on Emacs 29.1 (9.0) on macOS. |
|
I can locate where the error is coming from, but I'll have to study what has changed since I last worked on agda2-mode (I don't use Agda regularly anymore, so I might have missed some interal changes), and I'll have to see when I'll find the time to dive into that again. So in the meanwhile, please feel free to revert the commit, and my appologies for any problems this might have caused anyone. |
|
Reverting fixed the problem for me, so I am pushing a revert now. |
This reverts commit 90d82ae.
The labels are on the right side, but maybe you have to be a member of the organisation to add labels. I sent you an invite. |
phikal
added
the
pr: preserve commits
|
Seems to work now, thanks. |
|
OK, it turns out the issue wasn't that complicated, so I have pushed a commit on my branch: phikal@4b8c6e6. It appears that this PR is borked, so I'll have to open up a new one, right? |
|
Yes, I don't think it's possible to reopen this one after it's been merged. |
* agda-mode: Add a basic .dir-locals.el file for agda2-mode * agda-mode: Remove hanging parentheses * agda-mode: Set the input method just for the current agda2-mode buffer * agda-mode: Use dolist in agda2-goal-overlay * agda-mode: Have agda2-char-quote return strings * agda-mode: Use sharp-quotes where applicable * agda2-mode.el (agda2-infer-type-maybe-toplevel): Sharp-quote 'agda2-infer-type'. (agda2-solveAll-action): Sharp-quite 'agda2-solve-action'. (agda2-compute-normalised-maybe-toplevel): Sharp quote 'agda2-compute-normalised' and 'agda2-compute-normalised-toplevel'. Sharp-quoting functions indicates that a symbol should have a bound function slot, and that the byte compiler should check if this is the case, otherwise emit a warning. * agda-mode: Fix checkdoc and byte-compiler issues * agda-mode: Drop the 'agda2-let' macro * agda-mode: Add .agdai files to 'completion-ignored-extensions' * agda-mode: Remove compatibility code for versions older than GNU Emacs 25.1 * agda-mode: Replace 'agda2--case' with 'pcase' * agda-mode: Fix minor stylistic issues * agda-mode: Prefer 'defvar-local' over 'make-variable-buffer-local' * agda-mode: Prefer 'setq-local' over 'make-local-variable' * agda-mode: Flatten 'agda2-get-agda-program-versions' * agda-mode: Use 'cl-remove-if-not' instead of 'cl-mapcan' * agda-mode: Prefer member functions over (or (eq...) ...) * agda-mode: Avoid using 'equal' where unnecessary 'Equal' is used for structural equality, which is not necessary for atomic objects like symbol or numbers. In that case referential equality, 'eq' or a specialised procedure like 'zerop' or 'null' is preferred. * agda-mode: Add a custom setter to 'agda2-mode-abbrevs-use-defaults' * agda-mode: Replace 'agda2-command-table' with regular maps * agda-mode: Replace agda2-queue with a regular buffer * agda-mode: Use more consistent outlines in agda2-mode.el * agda-mode: Use more consistent outlines in agda2-highlight.el * agda-mode: Use more consistent outlines in agda2-input.el * agda-mode: Use 'with-silent-modifications' * agda-mode: Only use exec-path as a function if fboundp * agda-mode: Modify 'file-coding-system-alist' directly * agda-mode: Move add-to-list autoloads to agda2.el to avoid duplication * agda-mode: Use a "hidden name" for the Agda process buffer * agda-mode: Use 'apply' instead of 'eval' It is not necessary to use 'eval' to invoke a function with an argument list of unknown length. * agda-mode: Add a "Code" header to agda2.el * agda-mode: Do not disable cl-function warnings * agda-mode: Enable debug-on-error for agda-mode when compiling * agda-mode: Use 'barf-if-buffer-read-only' instead of checking manually * agda-mode: Avoid usage of deprecated 'window-system' variable * agda-mode: Do not control evaluation using buffer-local values * agda-mode: Further simplify process filter This change builds on c7492c0, dropping the need for any queue (of string or a buffer), by inserting the process output directly into the process buffer and operating on thereon. We avoid the overhead of consing lists and strings, while simplifying the logic by relying more on Lisp primitives.
This reverts commit 90d82ae.
This was formerly part of #6123 (see #5917), but has been restricted to just fixing superficial issues related to Elisp conventions.