1lab/mikan
13
52
Fork
You've already forked mikan
9

agda2-program-name cannot be set as a directory-local variable and cannot be influenced by global minor modes #142

Closed
opened 2026年06月25日 15:28:52 +02:00 by totbwf · 1 comment

If you have a .dir-locals.el like

((nil . ((agda2-program-name . "some-other-mikan")

then it will be clobbered during initializtaion of agda2-mode. The root of the problem is that agda2-mode is transitively a derived mode of fundamental-mode, which calls kill-all-local-variables as part of mode initialization, and only restores them using hack-local-variables after we've started the mode.

A similar bug impacts users of envrc.el: global minor modes are initialized as a part of after-change-major-mode-hook, which gets called after we've started the mode.

If you have a `.dir-locals.el` like ```emacs-lisp ((nil . ((agda2-program-name . "some-other-mikan") ``` then it will be clobbered during initializtaion of `agda2-mode`. The root of the problem is that `agda2-mode` is transitively a derived mode of `fundamental-mode`, which calls `kill-all-local-variables` as part of mode initialization, and only restores them using `hack-local-variables` *after* we've started the mode. A similar bug impacts users of `envrc.el`: global minor modes are initialized as a part of `after-change-major-mode-hook`, which gets called after we've started the mode.
Author
Owner
Copy link

There are some baroque solutions for setting local variables before mode initialization is complete, but the correct move here is probably to move the initial call to agda2-restart outside of agda2-mode.

There are a couple of ways to do this, but the best solution is to add use after-change-major-mode-hook or change-major-mode-after-body-hook to start initializing the agda process after all minor modes have been started.

There are some baroque solutions for setting local variables before mode initialization is complete, but the correct move here is probably to move the initial call to `agda2-restart` outside of `agda2-mode`. There are a couple of ways to do this, but the best solution is to add use `after-change-major-mode-hook` or `change-major-mode-after-body-hook` to start initializing the agda process after all minor modes have been started.
Sign in to join this conversation.
No Branch/Tag specified
main
aliao/occurs-opt
aliao/rec-con
fix-license
aliao/oopsie
aliao/strengthen-iapply
No results found.
Labels
Clear labels
1 - scope
language
 Backwards-compatible changes to the surface language, such as adding new features.
1 - scope
language change
 Breaking changes to a documented part of the surface language. These should be documented and specifically called out in the changelog.
1 - scope
performance
 Semantics-preserving performance work.
1 - scope
task
 Changes that are not apparent to the user, e.g. developer documentation and refactors, which do not need to be documented.
A: dead-code
Dead code elimination and --save-metas.
A: errors
Reporting of error and warning messages.
A: highlighting
Highlighting during interaction & literate compilation
A: imports
Handling of imports and interface file de/serialization.
A: infra
Iinfrastructure (e.g. CI, developer documentation, the build system, or the repository itself)
A: instance
Instance declarations, arguments, and resolution
A: lhs
LHS checking, coverage checking, and clause compilation
A: modules
Declaration and instantiation of parametrised modules.
A: parallel
Parallel typechecking.
A: positivity
Positivity checking
A: printing
Pretty-printing, display forms, and the wording of diagnostic messages
A: records
Record declarations, record expressions and copattern matching
A: scoping
Scope checking (ConcreteToAbstract)
A: termination
Termination checking
0 - type
bug
 Issues describing an incorrect behaviour in the project, typos in the documentation, etc.
0 - type
discussion
 An issue raised to gather opinions on a proposed change, or a suggested language change.
0 - type
question
 An issue raised to ask a question.
9 - status
duplicate
 This issue or pull request already exists.
9 - status
info needed
 More information is needed from the submitter to decide how to proceed with the issue report.
9 - status
invalid
 The issue report or pull request does not describe an actual bug, or does otherwise does not meet the contributing guidelines.
good first issue
Interested in contributing? Get started here.
upstream
Related to an upstream repository, already reported there
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
1lab/mikan#142
Reference in a new issue
1lab/mikan
No description provided.
Delete branch "%!s()"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?