TakeV/spacemacs
1
0
Fork 0
Code Issues Pull requests Packages Projects Releases Wiki Activity
spacemacs/layers/+lang/agda
History
syl20bnr ebe4c60264 Revert "Defer packages by default using use-package-always-defer" 
This reverts commit 29c78ce841 and all other fixes
that have been made afterwards.

The motivation is that use-package is seen by many as a replacement for
`require`. Is use-package always defer the loading of packages then is breaks
this use case, this does not respect POLA so even if it was making Spacemacs
loading faster (up to 3s faster on some startup on my machine) we just cannot
use it, it would be irresponsible. Spacemacs should be easy to use, loading
performance will come with time but it is not a priority.
2018-03-03 23:40:10 -05:00
..
config.el Happy New Year 2018! 2018-01-04 02:00:25 -05:00
packages.el Revert "Defer packages by default using use-package-always-defer" 2018-03-03 23:40:10 -05:00
README.org Fix features format in misc README.org's 2017-08-22 21:27:13 +03:00

README.org

Agda layer

Description

This layer adds support for the Agda programming language.

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 configuration layer, add it to your ~/.spacemacs. You will need to add agda to the existing dotspacemacs-configuration-layers list in this file.

Agda

Quick instructions to install Agda assuming you have cabal installed:

  cabal install alex happy "cpphs < 1.19" agda

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

By default the agda-mode executable bundled with most agda installations is used to locate the agda-mode package. If you don't have it and want to use a local agda-mode package, you can customize the layer variable agda-mode-path to your needs. Set it to nil if agda2.el is already discoverable in Emacs’ load path, otherwise set it to the path at which agda2.el can be found. For example,

  (agda2 :variables agda-mode-path "/some/path/to/agda2.el")

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