agda-mode on Atom

For people who don't wanna use Emacs for whatever reasons.

Feel free to open issues!!!!

Requirements

Binaries: agda

Installation

Install this package:

from the editor: Atom > Preferences... > Install, search for agda-mode and install
or from a shell: apm install agda-mode

Ensure you have agda properly installed (check this in your console, type agda and see if it's in the PATH).

Syntax Highlighting

Unlike on Emacs, agda-mode on Atom doesn't come with syntax highlighting bundled, nor does it highlight your code dynamically on load (yet).

To have your code highlighted:

Install language-agda:

from the editor: Atom > Preferences... > Install, search for language-agda and install
or from a shell: apm install language-agda

Extra perk: with language-agda installed, commands such as input-symbol, go-to-definition can be invoked without having to load first.

Recommanded Settings

Enable Scroll Past End

Go to Settings > Editor > Scroll Past End and enable it to allow the editor to be scrolled past the end of the last line. The reason is that the height of the "panel" at the bottom is constantly changing, and it's pretty annoying to have the editor jumping up and down with the panel.

Commands

C-c stands for "press Ctrl and c at the same time"
When it comes to combos like C-c C-l, you can often slur them into "hold Ctrl while pressing c and then l"

This is an (not so) exhaustive list of available commands:

Keymap	Command	Global	Goal-specific
`C-c` `C-l`	load a file	✓
`C-c` `C-x` `C-q`	quit	✓
`C-c` `C-x` `C-r`	kill and restart Agda	✓
`C-c` `C-x` `C-c`	compile	✓
`C-c` `C-x` `C-a`	abort	✓
`C-c` `C-x` `C-h`	toggle display of implicit arguments	✓
`C-c` `C-=`	show constraints	✓
`C-c` `C-s`	solve constraints	✓
`C-c` `C-?`	show goals	✓
`C-c` `C-f`	next goal (forward)	✓
`C-c` `C-b`	previous goal (back)	✓
`C-alt-\` or `alt-cmd-\`	go to definition	✓
`C-c` `C-x` `C-d`	toggle panel docking	✓
`C-c` `C-n`	compute normal form	✓	✓
`C-u` `C-c` `C-n`	compute normal form (ignoring abstract)	✓	✓
`C-u` `C-u` `C-c` `C-n`	compute normal form (use show instance)	✓	✓
`C-c` `C-w`	why in scope	✓	✓
`C-c` `C-SPC`	give		✓
`C-c` `C-r`	refine		✓
`C-c` `C-a`	auto		✓
`C-c` `C-c`	case		✓

Commands listed below support 3 different levels of normalization.

Keymap	Command	Global	Goal-specific
`C-c` `C-z`	search about	✓
`C-c` `C-d`	infer type	✓	✓
`C-c` `C-o`	module contents	✓	✓
`C-c` `C-t`	goal type		✓
`C-c` `C-e`	context		✓
`C-c` `C-,`	goal type and context		✓
`C-c` `C-.`	goal type and inferred type		✓

Levels of normalization

Prefix	Normalization
	Simplified
`C-u`	No normalization
`C-u` `C-u`	Full normalization

For example, C-u C-c C-d if you want to infer a type without normalizing it. See Agda:Issue 850 for more discussion.

Unicode input method

To invoke the input method, press \ or alt-/ in .agda or .lagda files. The key mapping of symbols are the same as in Emacs. For example: \bN for ℕ, \all for ∀, \r or \to for →, etc.

Keymap	Command
`\` or `alt-/`	input symbol
`C-u` `C-x` `C-=`	lookup the key mapping of a symbol

To customize the keymap, open the settings tab (at the bottom right) and go to Input Method > Keymap extensions

Trouble shooting

Windows 10

If you are having trouble using agda-mode on Windows 10 (symptoms: #97, #98, #110) Please consider follow these instructions and see if it works:

Go to the system's Language settings
Select Administrative language settings
Click Change system locale...
Check Beta: Use Unicode UTF-8 for worldwide language support

Contribute

See HACKING