# cornelis ![Cornelis in Action](https://raw.githubusercontent.com/isovector/cornelis/master/cast.gif) ## Dedication > I'll ask to stand up \ > With a show about a rooster, \ > Which was old and worn out, \ > Impotent and weathered. \ > The chickens complained and whined \ > Because he did not satisfy them. > > -- [Cornelis Vreeswijk](https://www.youtube.com/watch?v=oKUscEWPVAM) ## Overview `cornelis` is [agda-mode], but for neovim. It's written in Haskell, which means it's maintainable and significantly less likely to bit-rot like any vimscript/lua implementations. [agda-mode]: https://agda.readthedocs.io/en/latest/tools/emacs-mode.html ## Features It supports highlighting, goal listing, type-context, refinement, auto, solving, case splitting, go-to definition, normalization, and helper functions. These are exposed via vim commands. Most commands have an equivalent in [agda-mode]. ### Global commands | Vim command | Description | Equivalent agda-mode keybinding | | :--- | :--- | :--- | | `:CornelisLoad` | Load and type-check buffer | C-cC-l | | `:CornelisGoals` | Show all goals | C-cC-? | | `:CornelisRestart` | Kill and restart the `agda` process | C-cC-xC-r | | `:CornelisAbort` | Abort running command | C-cC-xC-a | | `:CornelisSolve ` | Solve constraints | C-cC-s | | `:CornelisGoToDefinition` | Jump to definition of name at cursor | M-. or middle mouse button | | `:CornelisPrevGoal` | Jump to previous goal | C-cC-b | | `:CornelisNextGoal` | Jump to next goal | C-cC-f | | `:CornelisQuestionToMeta` | Expand `?`-holes to `{! !}` | _(none)_ | | `:CornelisInc` | Like `` but also targets sub- and superscripts | _(none)_ | | `:CornelisDec` | Like `` but also targets sub- and superscripts | _(none)_ | | `:CornelisCloseInfoWindows` | Close (all) info windows cornelis has opened | _(none)_ | ### Commands in context of a goal These commands can be used in context of a hole: | Vim command | Description | Equivalent agda-mode keybinding | | :--- | :--- | :--- | | `:CornelisGive` | Fill goal with hole contents | C-cC-SPC | | `:CornelisRefine` | Refine goal | C-cC-r | | `:CornelisElaborate ` | Fill goal with normalized hole contents | C-cC-m | | `:CornelisAuto` | [Automatic proof search] | C-cC-a | | `:CornelisMakeCase` | Case split | C-cC-c | | `:CornelisTypeContext ` | Show goal type and context | C-cC-, | | `:CornelisTypeInfer ` | Show inferred type of hole contents | C-cC-d | | `:CornelisTypeContextInfer ` | Show goal type, context, and inferred type of hole contents | C-cC-. | | `:CornelisNormalize ` | Compute normal of hole contents | C-cC-n | | `:CornelisWhyInScope` | Show why given name is in scope | C-cC-w | | `:CornelisHelperFunc ` | Copy inferred type to register `"` | C-cC-h | [Automatic proof search]: https://agda.readthedocs.io/en/latest/tools/auto.html#auto Commands with an `` argument take an optional normalization mode argument, one of `AsIs`, `Instantiated`, `HeadNormal`, `Simplified` or `Normalised`. When omitted, defaults to `Normalised`. Commands with a `` argument take an optional compute mode argument: | `` | Description | Equivalent agda-mode prefix | | :--- | :--- | :--- | | `DefaultCompute` | default, used if `` is omitted | no prefix, default | | `IgnoreAbstract` | compute normal form, ignoring `abstract`s | C-u | | `UseShowInstance` | compute normal form of print using `show` instance | C-uC-u | | `HeadCompute` | compute weak-head normal form | C-uC-uC-u | If Agda is stuck executing a command (e.g. if normalization takes too long), abort the command with `:CornelisAbort`. If you need to restart the plugin (eg if Agda is stuck in a loop), you can restart everything via `:CornelisRestart`. ### Agda Input There is reasonably good support for agda-input via your `` in insert mode. See [agda-input.vim](https://github.com/isovector/cornelis/blob/master/agda-input.vim) for available bindings. If you'd like to use a prefix other than your ``, add the following to your `.vimrc`: ```viml let g:cornelis_agda_prefix = "" " Replace with your desired prefix ``` #### Interactive Unicode Selection If you'd like an interactive prompt for choosing unicode characters, additionally install `vim-which-key`: ```viml Plug 'liuchengxu/vim-which-key' ``` and map a call to `cornelis#prompt_input()` in insert mode: ```viml inoremap :call cornelis#prompt_input() ``` #### Disabling Default Bindings If you don't want any of the default bindings, add the following to your `.vimrc`: ```viml let g:cornelis_no_agda_input = 1 ``` #### Adding Bindings Custom bindings can be added by calling the `cornelis#bind_input` function in `.vimrc`. For example: ```viml call cornelis#bind_input("nat", "ℕ") ``` will add `nat` as an input remapping for `ℕ`. #### Custom Hooks If you'd prefer to manage agda-input entirely on your own (perhaps in a snippet system), you can set the following: ```viml function! MyCustomHook(key, character) " do something endfunction let g:cornelis_bind_input_hook = "MyCustomHook" ``` You can invoke `cornelis#standard_bind_input` with the same arguments if you'd like to run your hook in addition to the standard one. ### Text Objects Use the `iz`/`az` text objects to operate on text between `⟨` and `⟩`. Somewhat surprisingly for i/a text objects, `iz` targets the _spaces_ between these brackets, and `az` targets the spaces. Neither textobj targets the brackets themselves. Also `ii`/`ai` will operate on `⦃` and `⦄`, but in the way you'd expect text objects to behave. `ih`/`ah` will operate on `{!` and `!}`. ## Installation Make sure you have [`stack`](https://docs.haskellstack.org/en/stable/install_and_upgrade/) on your PATH! ```viml Plug 'kana/vim-textobj-user' Plug 'neovimhaskell/nvim-hs.vim' Plug 'isovector/cornelis', { 'do': 'stack build' } ``` ### Agda Version `cornelis` is tested only against `agda-2.6.3`. If you run into weird error messages from vim, it's probably because you're running an old version of `agda`. If possible, try upgrading, if not, file a bug and I'll see if I can help. In addition, there are some bugs in the most recent version of `agda` that negatively affect `cornelis`. For best results, build from head, ensuring you have the following patches: - https://github.com/agda/agda/pull/5752 - https://github.com/agda/agda/pull/5776 ### Installation with Nix You can install both the vim plugin and the cornelis binary using nix flakes! You can access the binary as `cornelis.packages..cornelis` and the vim plugin as `cornelis.packages..cornelis-vim`. Below is a sample configuration to help you understand where everything plugs in.
Nix details ```nix # flake.nix { description = "my-config"; inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable"; home-manager = { url = "github:nix-community/home-manager"; inputs.nixpkgs.follows = "nixpkgs"; }; cornelis.url = "github:isovector/cornelis"; cornelis.inputs.nixpkgs.follows = "nixpkgs"; }; outputs = { home-manager , nixpkgs , cornelis , ... }: { nixosConfigurations = { bellerophon = nixpkgs.lib.nixosSystem { system = "x86_64-linux"; modules = [ home-manager.nixosModules.home-manager { nixpkgs.overlays = [cornelis.overlays.cornelis]; home-manager.useGlobalPkgs = true; home-manager.useUserPackages = true; home-manager.users.my-home = import ./my-home.nix; } ]; }; }; }; } # my-home.nix {pkgs, ...}: { home.packages = [ pkgs.agda ]; programs.neovim = { enable = true; extraConfig = builtins.readFile ./init.vim; plugins = [ { # plugin packages in required Vim plugin dependencies plugin = pkgs.vimPlugins.cornelis; config = "let g:cornelis_use_global_binary = 1"; } ]; extraPackages = [ pkgs.cornelis ]; }; } ```
Make sure you enable the global binary option in your vim config. Since `/nix/store` is immutable cornelis will fail when `nvim-hs` tries to run stack, which it will do if the global binary option isn't enabled. #### Use global binary instead of stack Vimscript: ```viml let g:cornelis_use_global_binary = 1 ``` Lua: ```lua vim.g.cornelis_use_global_binary = 1 ``` ## Example Configuration Once you have `cornelis` installed, you'll probably want to add some keybindings for it! This is enough to get you started: ```viml au BufRead,BufNewFile *.agda call AgdaFiletype() au QuitPre *.agda :CornelisCloseInfoWindows function! AgdaFiletype() nnoremap l :CornelisLoad nnoremap r :CornelisRefine nnoremap d :CornelisMakeCase nnoremap , :CornelisTypeContext nnoremap . :CornelisTypeContextInfer nnoremap n :CornelisSolve nnoremap a :CornelisAuto nnoremap gd :CornelisGoToDefinition nnoremap [/ :CornelisPrevGoal nnoremap ]/ :CornelisNextGoal nnoremap :CornelisInc nnoremap :CornelisDec endfunction ``` Feeling spicy? Automatically run `CornelisLoad` every time you save the file. ```viml au BufWritePost *.agda execute "normal! :CornelisLoad\" ``` If you'd like to automatically load files when you open them too, try this: ```viml function! CornelisLoadWrapper() if exists(":CornelisLoad") ==# 2 CornelisLoad endif endfunction au BufReadPre *.agda call CornelisLoadWrapper() au BufReadPre *.lagda* call CornelisLoadWrapper() ``` This won't work on the first Agda file you open due to a bug, but it will successfully load subsequent files. ### Configuring Cornelis' Behavior The max height and width of the info window can be set via: ```viml let g:cornelis_max_size = 30 ``` and ```viml let g:cornelis_max_width = 40 ``` If you'd prefer your info window to appear somewhere else, you can set `g:cornelis_split_location` (previously `g:cornelis_split_direction`), e.g. ```viml let g:cornelis_split_location = 'vertical' ``` The following configuration options are available: - `horizontal`: The default, opens in a horizontal split respecting `splitbelow`. - `vertical`: Opens in a vertical split respecting `splitright`. - `top`: Opens at the top of the window. - `bottom`: Opens at the bottom of the window. - `left`: Opens at the left of the window. - `right`: Opens at the right of the window. ### Aligning Reasoning Justification If you're interested in automatically aligning your reasoning justifications, also install the following plugin: ```viml Plug 'junegunn/vim-easy-align' ``` and add the following configuration for it: ```viml vmap (EasyAlign) let g:easy_align_delimiters = { \ 'r': { 'pattern': '[≤≡≈∎]', 'left_margin': 2, 'right_margin': 0 }, \ } ``` You can now align justifications by visually selecting the proof, and then typing `r`. ### Customizing Syntax Highlighting Syntax highlighting is controlled by syntax groups named `Cornelis*`, defined in [`syntax/agda.vim`](./syntax/agda.vim). These groups are linked to default highlighting groups ([`:h group-name`](https://neovim.io/doc/user/syntax.html#group-name)), and can be customized by overriding them in user configuration. ```viml " Highlight holes with a yellow undercurl/underline: highlight CornelisHole ctermfg=yellow ctermbg=NONE cterm=undercurl " Highlight "generalizables" (declarations in `variable` blocks) like constants: highlight link CornelisGeneralizable Constant ``` ## Contributing I'm a noob at Agda, and I don't know what I don't know. If this plugin doesn't have some necessary feature for you to get work done, please file a bug, including both what's missing, and how you use it in your workflow. I'd love to learn how to use Agda better! I can move quickly on feature requests. If you'd like to get involved, feel free to tackle an issue on the tracker and send a PR. I'd love to have you on board! ## Architecture Cornelis spins up a new `BufferStuff` for each Agda buffer it encounters. `BufferStuff` contains a handle to a unique `agda` instance, which can be used to send commands. It also tracks things like the information window buffer, in-scope goals, and whatever the last `DisplayInfo` response from `agda` was. For each `BufferStuff`, we also spin up a new thread, blocking on responses from `agda`. These responses all get redirected to a global worker thread, which is responsible for dispatching on each command. Commands are typesafe, parsed from JSON, and associated with the buffer they came from.