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

Make Emacs mode available as a normal package via MELPA #3360

Closed
mrkkrp opened this issue Nov 2, 2018 · 10 comments
Closed

Make Emacs mode available as a normal package via MELPA #3360

mrkkrp opened this issue Nov 2, 2018 · 10 comments
Labels
type: enhancement Issues and pull requests about possible improvements ux: emacs Issues relating to the Emacs agda2-mode
Milestone

Comments

@mrkkrp
Copy link

mrkkrp commented Nov 2, 2018

The title says it all. All these manual manipulations are not nice if there is a proper package manager and a repo with packages (MELPA).

@gallais
Copy link
Member

gallais commented Nov 2, 2018

Is this #3234?

@ice1000
Copy link
Member

ice1000 commented Nov 2, 2018

@mrkkrp You should first understand that different Agda versions has different agda2-mode for them. You should be aware that if you want to have agda2-mode in melpa you'll need to publish many many agda2-mode at the same time to ensure compatibility.

@ice1000 ice1000 added the ux: emacs Issues relating to the Emacs agda2-mode label Nov 2, 2018
@mrkkrp
Copy link
Author

mrkkrp commented Nov 3, 2018

All right, but then it is certainly not very handy. Even proof general is now on MELPA. Perhaps Agda has its own reasons to do things this way...

@ice1000
Copy link
Member

ice1000 commented Nov 3, 2018

@mrkkrp The API changes! This is a huge problem.

For me, it's acceptable to create different agda2-mode on melpa for different versions of Agda

@nad
Copy link
Contributor

nad commented Nov 4, 2018

I think it would be great if the Agda mode could be available via MELPA. For some further discussion, see #3234.

@ice1000
Copy link
Member

ice1000 commented Nov 13, 2018

Is like to put the input method minor mode on melpa first.

@jespercockx
Copy link
Member

This is a great idea. I'm assigning icebox not because I want to shoot it down, but because this doesn't have to be linked to a specific release of Agda.

@jespercockx jespercockx added this to the icebox milestone Nov 15, 2018
@jespercockx jespercockx added the type: enhancement Issues and pull requests about possible improvements label Nov 15, 2018
jappeace added a commit to jappeace/melpa that referenced this issue Aug 17, 2020
Is part of the main agda repository: https://github.com/agda/agda
Has been used a long time but nobody bothered to add to melpa.
I wish to use nix for emacs config management and adding this
to melpa, adds it to nix.

My association is that I'm writing a blog post about agda at the moment,
but while doing that I wish to leave the state of agda
better and more accisable than I found it in.

There is an issue to do this upstream:
agda/agda#3360
I'm doing this because it looked easy and I have reasonable
gains out of it.
@jappeace jappeace mentioned this issue Aug 17, 2020
7 tasks
@jappeace
Copy link
Contributor

melpa/melpa#7080

@jappeace
Copy link
Contributor

@ice1000
Melpa will version this automatically by date:

image

So if agda upgrades, this repository upgrade, the melpa will also upgrade automatically.
The entry file also contains a revision to whatever agda mode version is being used (for this repository):

image

So the big gain here is that this probably will work with whatever agda you have on your system, or you have a way of figuring it out, otherwise you can simply choose to not use melpa.
But most users will just get a working setup and forget about upgrading for a year or 2.

riscy added a commit to melpa/melpa that referenced this issue Sep 11, 2020
* Add agda mode

Is part of the main agda repository: https://github.com/agda/agda
Has been used a long time but nobody bothered to add to melpa.
I wish to use nix for emacs config management and adding this
to melpa, adds it to nix.

My association is that I'm writing a blog post about agda at the moment,
but while doing that I wish to leave the state of agda
better and more accisable than I found it in.

There is an issue to do this upstream:
agda/agda#3360
I'm doing this because it looked easy and I have reasonable
gains out of it.

* Rename to agda2-mode instead

Upstream also calls it agda2-mode

* Add eri mode

* Add annotation mode

* Modify recipe to only include agda2 mode files

* Update agda2-mode

Co-authored-by: Chris Rayner <riscy@users.noreply.github.com>
@jappeace
Copy link
Contributor

This is finished melpa/melpa#7080

I'm available for any questions or concerns on this.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
type: enhancement Issues and pull requests about possible improvements ux: emacs Issues relating to the Emacs agda2-mode
Projects
None yet
Development

No branches or pull requests

7 participants