4 ms·

> At the time of writing, it is only really feasible to edit Agda code using Emacs. Why?

by shocks 11y ago

sordina 11y ago
Writing Agda is a very interactive experience. The only IDE that provides this interactivity at present is Emacs. If you take a look at some Youtube clips of people editing Agda you'll see why you would want an IDE. Not that this can't be done elsewhere, just that it hasn't been done yet.
semi-extrinsic 11y ago
I think this is (at least part of) why: "Another thing that sets Agda apart from other languages is its extensive use of unicode to make mathematical constructs more natural."
- drivingmenuts 11y ago
  APL called and is a bit miffed.
  - SamReidHughes 11y ago
    They didn't have Unicode back then :-)
CHY872 11y ago
It's really just basic editor support. Agda is quite an interactive programming language, so you need lots of shortcuts, syntax highlighting, autofilling etc in order to get productivity at all (especially since you're constantly moving stuff in and out of a repl) https://youtu.be/pP7ynVdVY9A?t=13m https://youtu.be/pP7ynVdVY9A?t=13m gives a decent example. As to why support isn't in other editors, it's probably a combination of: more code to support, no one wants to write it, and the fact that Agda is less amenable to being sped up by efficient usage of editors (as it is a more interactive process with less copy pasting).
- black_knight 11y ago
  I have to disagree to that one needs syntax highlighting and autofilling to be productive in Agda. I have written a fair amount of agda code in Acme, which has neither. Rather I find these bells and whistles distracting — and prefer giving my complete attention to the task at hand. I think that writing agda code interactively in Emacs is fine, but it is certainly not the only way to write good agda code. In fact writing without the interactive support encourages better code structure. One is more likely to factor a complicated line into several help terms (using 'where', for example), which makes the code more readable.
black_knight 11y ago
Emacs is the only officially supported interactive Agda environment, as other people have noted. However, I have written a lot of Agda code in other editors (acme and vim). It is certainly feasable to do! In fact I find that it improves my code quality not to use the interactive features. When in interactive mode, I blindly chase the goal trying to get the correct type, and often end up going long detours. When I am on my own I get a better overview of the situation, and can often see the shortest path. That said, I wish they would continue to support agda interactive mode on the command line, as it is nice to be able to evaluate expressions in context of a hole. Writing unicode is a breeze with XCompose, in any UTF8-enabled editor. I found a nice XCompose file based on the Plan 9 keyboard file, by Pmarin. It can be downloaded from «Greg 'Groggy' Lehey»'s site: http://www.lemis.com/grog/programs/XCompose http://www.lemis.com/grog/programs/XCompose

> At the time of writing, it is only really feasible to edit Agda code using Emacs. Why?

by shocks 11y ago

> At the time of writing, it is only really feasible to edit Agda code using Emacs. Why?

Writing Agda is a very interactive experience. The only IDE that provides this interactivity at present is Emacs. If you take a look at some Youtube clips of people editing Agda you'll see why you would want an IDE. Not that this can't be done elsewhere, just that it hasn't been done yet.

semi-extrinsic 11y ago

I think this is (at least part of) why: "Another thing that sets Agda apart from other languages is its extensive use of unicode to make mathematical constructs more natural."

drivingmenuts 11y ago
APL called and is a bit miffed.
- SamReidHughes 11y ago
  They didn't have Unicode back then :-)

CHY872 11y ago

It's really just basic editor support. Agda is quite an interactive programming language, so you need lots of shortcuts, syntax highlighting, autofilling etc in order to get productivity at all (especially since you're constantly moving stuff in and out of a repl) https://youtu.be/pP7ynVdVY9A?t=13m https://youtu.be/pP7ynVdVY9A?t=13m gives a decent example. As to why support isn't in other editors, it's probably a combination of: more code to support, no one wants to write it, and the fact that Agda is less amenable to being sped up by efficient usage of editors (as it is a more interactive process with less copy pasting).

black_knight 11y ago
I have to disagree to that one needs syntax highlighting and autofilling to be productive in Agda. I have written a fair amount of agda code in Acme, which has neither. Rather I find these bells and whistles distracting — and prefer giving my complete attention to the task at hand. I think that writing agda code interactively in Emacs is fine, but it is certainly not the only way to write good agda code. In fact writing without the interactive support encourages better code structure. One is more likely to factor a complicated line into several help terms (using 'where', for example), which makes the code more readable.

black_knight 11y ago

Emacs is the only officially supported interactive Agda environment, as other people have noted. However, I have written a lot of Agda code in other editors (acme and vim). It is certainly feasable to do! In fact I find that it improves my code quality not to use the interactive features. When in interactive mode, I blindly chase the goal trying to get the correct type, and often end up going long detours. When I am on my own I get a better overview of the situation, and can often see the shortest path. That said, I wish they would continue to support agda interactive mode on the command line, as it is nice to be able to evaluate expressions in context of a hole. Writing unicode is a breeze with XCompose, in any UTF8-enabled editor. I found a nice XCompose file based on the Plan 9 keyboard file, by Pmarin. It can be downloaded from «Greg 'Groggy' Lehey»'s site: http://www.lemis.com/grog/programs/XCompose http://www.lemis.com/grog/programs/XCompose