.. _editing-lambdapi-source-code-with-emacs-melpamelpa-badgemelpa-link: Emacs ===== `MELPA package `_ Lambdapi source code can be edited with the `emacs`_ editor with the major mode ``lambdapi-mode``. It requires Emacs 26.1 or higher and provides: * Syntax highlighting for Lambdapi (``*.lp`` files) and Dedukti (``*.dk`` files) * Auto indentation for Lambdapi * Easier unicode input * Completion for Lambdapi * Typing of symbol at point (in minibuffer) * Type checking declarations Short-cuts ------------------ * ``C-c C-c``: jump to cursor position * ``C-c C-n``: next tactic or command * ``C-c C-p``: previous tactic or command * ``C-c C-f``: next proof * ``C-c C-b``: previous proof * ``C-c C-e``: toggle electric mode * ``M-;`` : (un)comment region * ``C-x RET C-\``: enter unicode characters in minibuffer using LaTeX * ``M-.`` : goto definition * ``M-x customize-group lambdapi``: customize window layout * ``C-c C-r``: refresh window layout * ``C-c C-k``: shutdown LSP server * ``C-c C-r``: reconnect LSP server * Click on a symbol to discover its type in the bottom line As always with emacs, if you were to be dissatisfied with these keybindings, you can change them easily! Installation ------------ The ``lambdapi-mode`` is distributed through `MELPA `__, so you can use any package manager for Emacs. Or, provided that MELPA is correctly `configured `__, use the following command inside Emacs:: M-x package-install RET lambdapi-mode RET where ``M-x`` is usually Alt+x and ``RET`` denotes the Return or Enter key. Usage ----- Make sure you have a `lambdapi.pkg `__ file in your folder when editing a Lambdapi file in it. Commenting regions ^^^^^^^^^^^^^^^^^^ Lambdapi handles single-line and multi-line comments with ``//`` and ``/* ... */`` respectively. To comment a region in Emacs, select it and use ``M-;``. Entering unicode ^^^^^^^^^^^^^^^^ Company: if `company`_ and `company-math`_ are installed, LaTeX commands are autocompleted with the latter tool. Any (or at least a lot of) LaTeX symbol can be entered via its LaTeX command: start typing it, and an autocompletion tooltip should suggest the unicode symbol. This method is the more complete and easier to use, but depends on ``company``. LambdaPi input method: if `company`_ or `company-math`_ is not installed, LaTeX characters can be entered via the LambdaPi input method. Greek characters can be accessed using backquoted letters (as done in `cdlatex`_), or with the LaTeX command: α can be accessed with :literal:`\`a` or ``\alpha``, β with :literal:`\`b` or ``\beta``, and similarly for other Greek letters. *NOTE on the interaction between the input method and company:* the dropdown window of company-math will not appear as long as the current word is a candidate for a completion of the input method. To favour company over the input method, the input method can be disabled setting the variable ``lambdapi-unicode-prefer-company`` to a non-nil value in ``~/.emacs`` or ``~/.emacs.d/init.el``: .. code:: emacs-lisp (setq lambdapi-unicode-prefer-company 1) abbrev mode: the ``abbrev`` mode is an emacs minor mode allowing the user to define abbreviations. For instance, one may define “btw” to be an abbreviation of “by the way” with, ``add-global-abbrev``. Doing so will cause the sequence “btw” to be automatically expanded when the user hits ``SPC`` or ``TAB``. The expansion can be inhibited by hitting ``C-q`` before ``SPC``. The function ``lambdapi-local-abbrev`` can be called when the cursor is at the end of a word to define the word as an abbreviation. When called, the user can input the expanded form in the minibuffer. Additionnally, the abbreviation is added as a directory local variable, so it will be available the next time a file of the project is opened. The function ``lambdapi-local-abbrev`` is bound to ``C-c a``. To enter unicode characters in the minibuffer using LaTeX, the TeX input method can be used, for this, once in the minibuffer, enter ``C-x RET C-\`` and select ``TeX`` in the list. LSP server ^^^^^^^^^^ Navigating goals '''''''''''''''' On lambdapi-mode startup, the window is split into three buffers: * the top buffer contains the Lambdapi file, * the middle ``*Goals*`` buffer is where goals are displayed, * the bottom ``*lp-logs*`` buffer is where Lambdapi messages are displayed. It is possible to print the goals to solve at some point in the file by using the following short-cuts or the navigation buttons "Prev" and "Next": * ``C-c C-c``: jump to cursor position * ``C-c C-n`` or button "Next": next tactic or command * ``C-c C-p`` or button "Prev": previous tactic or command * ``C-c C-f``: next proof * ``C-c C-b``: previous proof The part of the file up to the current goal is displayed with a green background. In case of error, the background gets red. If an edition occurs in the green zone, the green zone is automatically shrinked and the goals buffer updated. It is possible to make the green zone expand automatically each time a new command is typed by toggling the electric mode with ``C-c C-e``. Clicking on the ``i``-th goal of the ``*Goals*`` buffer puts the focus on it by inserting a ``focus i`` tactic in the proof script. Electric Terminator mode '''''''''''''''''''''''' You can toggle electric terminators either from the toolbar or using ``C-c C-e``. This will evaluate the region till the cursor whenever you type the ``;`` terminator or ``begin``. Customize window layout ''''''''''''''''''''''' The window layout can be customized in the LambdaPi customization group (Do ``M-x customize-group lambdapi``). The layout can be refreshed with ``C-c C-r``. CPU usage and deactivation '''''''''''''''''''''''''' If for any reason the LSP server consumes too much power (e.g. if a non-terminating rewrite system is edited), it can be disabled with ``M-x eglot-shutdown``. Other relevant packages ----------------------- * `company`_: auto-completion * `company-math`_: unicode symbols auto completion * `unicode-fonts `__: to configure correctly Emacs’ unicode fonts * `rainbow-delimiters `__: to appreciate having a lot of parentheses * paredit: to help keeping the parentheses balanced * `quickrun`_: for code evaluation To have everything configured using `use-package`_, use .. code:: emacs-lisp (use-package lambdapi-mode :hook (paredit-mode rainbow-delimiters-mode-enable)) .. _elpa: https://elpa.gnu.org .. _eglot: https://github.com/joaotavora/eglot .. _company: http://company-mode.github.io .. _company-math: https://github.com/vspinu/company-math .. _use-package: https://github.com/jwiegley/use-package .. _cdlatex: https://www.gnu.org/software/emacs/manual/html_node/org/CDLaTeX-mode.html .. _quickrun: https://github.com/emacsorphanage/quickrun .. _emacs: https://www.gnu.org/software/emacs/ .. _opam: http://opam.ocaml.org .. _highlight: https://www.emacswiki.org/emacs/HighlightLibrary .. _math-symbol-lists: https://elpa.gnu.org/packages/math-symbol-lists.html