search

banacorn / agda-mode

agda-mode on Atom
https://atom.io/packages/agda-mode
MIT License
58 stars 14 forks source link
agda agda-mode atom

readme

agda-mode on Atom

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

⚠️ Project status ⏸️

Sorry, people on Atom. Please consider using the new agda-mode on VS Code.

Requirements

Installation

  1. Install this package:
    • from the editor: Atom > Preferences... > Install, search for agda-mode and install
    • or from a shell: apm install agda-mode
  2. 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:

  1. 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

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:

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

Contribute

See HACKING