spacemacs/layers/+lang/agda/README.org

#+TITLE: Agda layer
#+HTML_HEAD_EXTRA: <link rel="stylesheet" type="text/css" href="../../../css/readtheorg.css" />

* Table of Contents                                         :TOC_4_org:noexport:
 - [[Description][Description]]
   - [[Some features:][Some features:]]
 - [[Install][Install]]
   - [[Layer][Layer]]
   - [[Agda][Agda]]
 - [[Key bindings][Key bindings]]

* Description
This layer adds support for the [[http://wiki.portal.chalmers.se/agda/pmwiki.php][Agda]] programming language.

** Some features:
- Faces redefined to correctly play with themes.
- Spacemacs bindings to Agda's interactive tools.

*This layer is in construction, it needs your contributions and bug reports.*

* Install
** Layer
To use this contribution add it to your =~/.spacemacs=

#+BEGIN_SRC emacs-lisp
  (setq-default dotspacemacs-configuration-layers '(agda))
#+END_SRC

** Agda
Quick instructions to install Agda assuming you have cabal installed:

#+BEGIN_SRC sh
  cabal install alex happy "cpphs < 1.19" agda
#+END_SRC

Then check that =agda= is available on your =$PATH= and seen by Emacs. For
information about setting up =$PATH=, check out the corresponding section in the
FAQ (~SPC h SPC $PATH RET~).

* Key bindings
The key bindings of this layer don't follow the Spacemacs conventions,
we opted to a simple transcription of stock Agda mode key bindings to
Spacemacs leader key.

All Agda specific bindings are prefixed with the major-mode leader
~SPC m~.

| Key Binding | Description                                                                                                                               |
|-------------+-------------------------------------------------------------------------------------------------------------------------------------------|
| ~SPC m =~   | Show constraints.                                                                                                                         |
| ~SPC m ?~   | Show all goals.                                                                                                                           |
| ~SPC m ,~   | Shows the type of the goal at point and the currect context.                                                                              |
| ~SPC m .~   | Shows the context, the goal and the given expression's inferred type.                                                                     |
| ~SPC m a~   | Simple proof search.                                                                                                                      |
| ~SPC m b~   | Go to the previous goal, if any and activate goal-navigation micro-state.                                                                 |
| ~SPC m c~   | Refine the pattern variables given in the goal.                                                                                           |
| ~SPC m d~   | Infers the type of the given expression.                                                                                                  |
| ~SPC m e~   | Show the context of the goal at point.                                                                                                    |
| ~SPC m f~   | Go to the next goal, if any and activate goal-navigation micro-state.                                                                     |
| ~SPC m h~   | Compute the type of a hypothetical helper function.                                                                                       |
| ~SPC m l~   | Load current buffer.                                                                                                                      |
| ~SPC m n~   | Computes the normal form of the given expression, using the scope of the current goal or, if point is not in a goal, the top-level scope. |
| ~SPC m p~   | Shows all the top-level names in the given module.                                                                                        |
| ~SPC m r~   | Refine the goal at point.                                                                                                                 |
| ~SPC m s~   | Solves all goals that are already instantiated internally.                                                                                |
| ~SPC m t~   | Show the type of the goal at point.                                                                                                       |
| ~SPC m x c~ | Compile current module.                                                                                                                   |
| ~SPC m x d~ | Removes buffer annotations (overlays and text properties).                                                                                |
| ~SPC m x h~ | Toggle display of implicit arguments.                                                                                                     |
| ~SPC m x q~ | Quit and clean up after agda2.                                                                                                            |
| ~SPC m x r~ | Kill and restart the *agda2* buffer and load =agda2-toplevel-module=.                                                                     |
| ~SPC m w~   | Explains why a given name is in scope.                                                                                                    |
Fix some documentation bugs - CSS links - GIFS in published version - Unify layer doc titles - Change emoji layer emojis to an image 2015-12-02 14:23:39 +00:00			`#+TITLE: Agda layer`
Documentation update - Add #+HTML_HEAD_EXTRA options to all org files - HTMLize published documentation via CSS 2015-11-08 18:04:44 +00:00			`#+HTML_HEAD_EXTRA: <link rel="stylesheet" type="text/css" href="../../../css/readtheorg.css" />`
Org conversion of all READMEs ! 2015-06-10 16:44:30 +00:00
Convert documentation to publishable format 2015-10-30 11:20:58 +00:00			`* Table of Contents :TOC_4_org:noexport:`
			`- [[Description][Description]]`
			`- [[Some features:][Some features:]]`
			`- [[Install][Install]]`
			`- [[Layer][Layer]]`
			`- [[Agda][Agda]]`
			`- [[Key bindings][Key bindings]]`
Org conversion of all READMEs ! 2015-06-10 16:44:30 +00:00
			`* Description`
			`This layer adds support for the [[http://wiki.portal.chalmers.se/agda/pmwiki.php][Agda]] programming language.`

Fix various issues with org markup - lists were not correctly indented sometimes - note and such things do not exist in org - Note and Important - Change Feature list to heading - Change TODOS to actual org TODOS - Add TOC to python layer - list indentation - some typos I could not leave unchanged - TODO formatting - List indentation - typos - wrong markup fix conversion issues 2015-06-10 21:16:01 +00:00			`** Some features:`
Org conversion of all READMEs ! 2015-06-10 16:44:30 +00:00			`- Faces redefined to correctly play with themes.`
			`- Spacemacs bindings to Agda's interactive tools.`
add note about setting up $PATH 2015-10-27 10:59:05 +00:00
Fix various issues with org markup - lists were not correctly indented sometimes - note and such things do not exist in org - Note and Important - Change Feature list to heading - Change TODOS to actual org TODOS - Add TOC to python layer - list indentation - some typos I could not leave unchanged - TODO formatting - List indentation - typos - wrong markup fix conversion issues 2015-06-10 21:16:01 +00:00			`This layer is in construction, it needs your contributions and bug reports.`
Org conversion of all READMEs ! 2015-06-10 16:44:30 +00:00
			`* Install`
			`** Layer`
			`To use this contribution add it to your =~/.spacemacs=`

			`#+BEGIN_SRC emacs-lisp`
			`(setq-default dotspacemacs-configuration-layers '(agda))`
			`#+END_SRC`

			`** Agda`
			`Quick instructions to install Agda assuming you have cabal installed:`

			`#+BEGIN_SRC sh`
			`cabal install alex happy "cpphs < 1.19" agda`
			`#+END_SRC`

add note about setting up $PATH 2015-10-27 10:59:05 +00:00			`Then check that =agda= is available on your =$PATH= and seen by Emacs. For`
Clean up PATH documentation 2015-10-29 12:41:05 +00:00			`information about setting up =$PATH=, check out the corresponding section in the`
Change `SPC f e h` to `SPC h SPC` for helm-spacemacs default binding This make `SPC h SPC` as default binding for accessing `helm-spacemacs`, by either A) changing all the documentation; and B) adding a deprecation message for `SPC f e h`. The deprecation use a warning, because if a message is used it's hidden directly when the helm buffer is shown, making it nearly unnoticeable for the user. 2015-12-21 13:50:36 +00:00			`FAQ (~SPC h SPC $PATH RET~).`
Org conversion of all READMEs ! 2015-06-10 16:44:30 +00:00
			`* Key bindings`
			`The key bindings of this layer don't follow the Spacemacs conventions,`
			`we opted to a simple transcription of stock Agda mode key bindings to`
			`Spacemacs leader key.`

			`All Agda specific bindings are prefixed with the major-mode leader`
			`~SPC m~.`

			`\| Key Binding \| Description \|`
			`\|-------------+-------------------------------------------------------------------------------------------------------------------------------------------\|`
			`\| ~SPC m =~ \| Show constraints. \|`
			`\| ~SPC m ?~ \| Show all goals. \|`
			`\| ~SPC m ,~ \| Shows the type of the goal at point and the currect context. \|`
			`\| ~SPC m .~ \| Shows the context, the goal and the given expression's inferred type. \|`
			`\| ~SPC m a~ \| Simple proof search. \|`
			`\| ~SPC m b~ \| Go to the previous goal, if any and activate goal-navigation micro-state. \|`
			`\| ~SPC m c~ \| Refine the pattern variables given in the goal. \|`
			`\| ~SPC m d~ \| Infers the type of the given expression. \|`
			`\| ~SPC m e~ \| Show the context of the goal at point. \|`
			`\| ~SPC m f~ \| Go to the next goal, if any and activate goal-navigation micro-state. \|`
			`\| ~SPC m h~ \| Compute the type of a hypothetical helper function. \|`
			`\| ~SPC m l~ \| Load current buffer. \|`
			`\| ~SPC m n~ \| Computes the normal form of the given expression, using the scope of the current goal or, if point is not in a goal, the top-level scope. \|`
Make SPC m o reserved for user 2015-08-17 18:25:48 +00:00			`\| ~SPC m p~ \| Shows all the top-level names in the given module. \|`
Org conversion of all READMEs ! 2015-06-10 16:44:30 +00:00			`\| ~SPC m r~ \| Refine the goal at point. \|`
			`\| ~SPC m s~ \| Solves all goals that are already instantiated internally. \|`
			`\| ~SPC m t~ \| Show the type of the goal at point. \|`
			`\| ~SPC m x c~ \| Compile current module. \|`
			`\| ~SPC m x d~ \| Removes buffer annotations (overlays and text properties). \|`
			`\| ~SPC m x h~ \| Toggle display of implicit arguments. \|`
			`\| ~SPC m x q~ \| Quit and clean up after agda2. \|`
			`\| ~SPC m x r~ \| Kill and restart the agda2 buffer and load =agda2-toplevel-module=. \|`
			`\| ~SPC m w~ \| Explains why a given name is in scope. \|`