Repository files navigation

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

cornelis isagda-mode, but for neovim. It's written in Haskell, which meansit's maintainable and significantly less likely to bit-rot like anyvimscript/lua implementations.

It supports highlighting, goal listing, type-context, refinement, auto, solving,case splitting, go-to definition, normalization, and helper functions. These areexposed via vim commands. Most commands have an equivalent inagda-mode.

These commands can be used in context of a hole:

Commands with an<RW> argument take an optional normalization mode argument,one ofAsIs,Instantiated,HeadNormal,Simplified orNormalised. Whenomitted, defaults toNormalised.This default may be specified in vimrc asg:cornelis_rewrite_mode.

Commands with a<CM> argument take an optional compute mode argument:

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 canrestart everything via:CornelisRestart.

There is reasonably good support for agda-input via your<LocalLeader> ininsert mode. Seeagda-input.vimfor available bindings.

If you'd like to use a prefix other than your<LocalLeader>, add the followingto your.vimrc:

letg:cornelis_agda_prefix="<Tab>"" Replace with your desired prefix

If you'd like an interactive prompt for choosing unicode characters,additionally installvim-which-key:

Plug'liuchengxu/vim-which-key'

and map a call tocornelis#prompt_input() in insert mode:

inoremap<localleader><C-O>:callcornelis#prompt_input()<CR>

If you don't want any of the default bindings, add the following to your.vimrc:

letg:cornelis_no_agda_input=1

Custom bindings can be added by calling thecornelis#bind_input function in.vimrc. For example:

callcornelis#bind_input("nat","ℕ")

will add<LocalLeader>nat as an input remapping forℕ.

If you'd prefer to manage agda-input entirely on your own (perhaps in a snippetsystem), you can set the following:

function!MyCustomHook(key,character)" do somethingendfunctionletg:cornelis_bind_input_hook="MyCustomHook"

You can invokecornelis#standard_bind_input with the same arguments if you'dlike to run your hook in addition to the standard one.

Use theiz/az text objects to operate on text between⟨ and⟩. Somewhatsurprisingly for i/a text objects,iz targets thespaces between thesebrackets, andaz targets the spaces. Neither textobj targets the bracketsthemselves.

Alsoii/ai will operate on⦃ and⦄, but in the way you'd expecttext objects to behave.

ih/ah will operate on{! and!}.

Make sure you havestack on your PATH!

Forvim-plug:

Plug'kana/vim-textobj-user'Plug'neovimhaskell/nvim-hs.vim'Plug'isovector/cornelis', {'do':'stack build','tag':'*' }

forlazy.nvim:

{'isovector/cornelis',name='cornelis',ft='agda',build='stack install',dependencies= {'neovimhaskell/nvim-hs.vim','kana/vim-textobj-user'},version='*',}

If you are having issues, try using a tag which matches your agda major version(e.g. for Agdav2.7.0.1 use cornelisv2.7.*). If there is no matchingversion that is working for a new version of agda, please create an issue.

You can install both the vim plugin and the cornelis binary using nix flakes!You can access the binary ascornelis.packages.<my-system>.cornelis and thevim plugin ascornelis.packages.<my-system>.cornelis-vim. Below is a sampleconfiguration to help you understand where everything plugs in.

# 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 dependenciesplugin=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 whennvim-hs tries to run stack,which it will do if the global binary option isn't enabled.

Vimscript:

letg:cornelis_use_global_binary=1

Lua:

vim.g.cornelis_use_global_binary=1

Once you havecornelis installed, you'll probably want to add some keybindingsfor it! This is enough to get you started:

auBufRead,BufNewFile*.agdacallAgdaFiletype()auQuitPre*.agda :CornelisCloseInfoWindowsfunction!AgdaFiletype()nnoremap<buffer><leader>l:CornelisLoad<CR>nnoremap<buffer><leader>r:CornelisRefine<CR>nnoremap<buffer><leader>d:CornelisMakeCase<CR>nnoremap<buffer><leader>,:CornelisTypeContext<CR>nnoremap<buffer><leader>.:CornelisTypeContextInfer<CR>nnoremap<buffer><leader>n:CornelisSolve<CR>nnoremap<buffer><leader>a:CornelisAuto<CR>nnoremap<buffer>gd:CornelisGoToDefinition<CR>nnoremap<buffer>[/:CornelisPrevGoal<CR>nnoremap<buffer>]/:CornelisNextGoal<CR>nnoremap<buffer><C-A>:CornelisInc<CR>nnoremap<buffer><C-X>:CornelisDec<CR>endfunction

Feeling spicy? Automatically runCornelisLoad every time you save the file.

auBufWritePost*.agdaexecute"normal! :CornelisLoad\<CR>"

If you'd like to automatically load files when you open them too, try this:

function!CornelisLoadWrapper()ifexists(":CornelisLoad")==#2    CornelisLoadendifendfunctionauBufReadPre*.agdacallCornelisLoadWrapper()auBufReadPre*.lagda*callCornelisLoadWrapper()

This won't work on the first Agda file you open due to a bug, but it willsuccessfully load subsequent files.

The max height and width of the info window can be set via:

letg:cornelis_max_size=30

and

letg:cornelis_max_width=40

If you'd prefer your info window to appear somewhere else, you can setg:cornelis_split_location (previouslyg:cornelis_split_direction), e.g.

letg:cornelis_split_location='vertical'

The following configuration options are available:

• horizontal: The default, opens in a horizontal split respectingsplitbelow.
• vertical: Opens in a vertical split respectingsplitright.
• 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.

Set default rewrite mode to use in commands which take an optionalnormalization mode argument

letg:cornelis_rewrite_mode='HeadNormal'

The following configuration options are available:

• AsIs
• Instantiated
• HeadNormal
• Simplified
• Normalised

If you're interested in automatically aligning your reasoning justifications,also install the following plugin:

Plug'junegunn/vim-easy-align'

and add the following configuration for it:

vmap<leader><space><Plug>(EasyAlign)letg:easy_align_delimiters= {\'r': {'pattern':'[≤≡≈∎]','left_margin':2,'right_margin':0 },\}

You can now align justifications by visually selecting the proof, and thentyping<leader><space>r.

Syntax highlighting is controlled by syntax groups namedCornelis*,defined insyntax/agda.vim.These groups are linked to default highlighting groups(:h group-name),and can be customized by overriding them in user configuration.

" Highlight holes with a yellow undercurl/underline:highlight CornelisHole ctermfg=yellow ctermbg=NONE cterm=undercurl" Highlight "generalizables" (declarations in `variable` blocks) like constants:highlightlinkCornelisGeneralizableConstant

I'm a noob at Agda, and I don't know what I don't know. If this plugin doesn'thave 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 tolearn 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 andsend a PR. I'd love to have you on board!

Cornelis spins up a newBufferStuff for each Agda buffer it encounters.BufferStuff contains a handle to a uniqueagda instance, which can be usedto send commands. It also tracks things like the information window buffer,in-scope goals, and whatever the lastDisplayInfo response fromagda was.

For eachBufferStuff, we also spin up a new thread, blocking on responsesfromagda. These responses all get redirected to a global worker thread, whichis responsible for dispatching on each command. Commands are typesafe, parsedfrom JSON, and associated with the buffer they came from.