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 foragda-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 forlanguage-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 would be annoying if the editor jumps 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-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.
.agda
or .lagda
)
Unicode input method (only invokable under 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 = | lookup the key mapping of a symbol |
How specify options to Agda
Go to Settings > Packages > agda-mode
, put the options after the path of Agda in the Settings
(exactly like what you would do in CLI). For example:
How to contribute
Environment Setup
- clone the repo and load it as a development package
- open the repo in the development mode
- install dependencies
- checkout to the
dev
branch. Themaster
branch is for stable releases.
apm develop agda-mode
atom -d ~/github/agda-mode
cd ~/github/agda-mode
npm install
git checkout dev
The project is written in TypeScript so you would probably need these:
npm install -g typescript@2.9.2
To keep the TypeScript transpiler running while developing:
tsc --watch