install

Additional install commands

macOS

Homebrewverified · 100%

brew install cornelis

local Homebrew formula metadata

Linux

Nixverified · 92%

nix profile install nixpkgs#cornelis

nixpkgs package indexes · pkgs/by-name/co/cornelis/package.nix · source: api.github.com

overview

Package summary

Neovim support for Agda

Project links

Commands and aliases

cornelis

history

Project history and usage

Cornelis is a Neovim interface for Agda, positioning itself as agda-mode for Neovim. It is written in Haskell and exposes Agda interactions through Vim commands for loading, goals, refinement, case splitting, normalization, and navigation.

Project history

The upstream README still describes Cornelis in relation to Emacs agda-mode and documents installation through common Vim and Neovim plugin managers. The current repository under the Agda organization was created in 2022, and its README states that the repository is currently unmaintained while asking interested maintainers to contact the Agda community.

Adoption history

Cornelis serves the smaller intersection of Agda users and Neovim users. Its adoption significance is mainly editorial and workflow-based: it gives dependently typed programming a modal-editor path rather than requiring the traditional Emacs-centered Agda workflow.

How it is used

Users install Cornelis as a Neovim plugin, build it with Stack, and configure Vimscript or Lua variables for behavior such as rewrite mode, Agda input prefix, disabling default bindings, and debug logging.

Why package nerds care

Cornelis is interesting to package maintainers because it is both an editor integration and a Haskell-built executable. Distribution needs to account for Neovim plugin layout, Stack/Haskell build expectations, and compatibility with Agda versions.

Timeline

2022: Current agda/cornelis GitHub repository created.
2026: Repository metadata shows recent activity while the README marks the project as unmaintained.
Present: Tags in the official repository include v2.7.0, v2.7.1, and v2.8.0.

Related projects

Related projects include Agda, agda-mode for Emacs, nvim-hs.vim, vim-textobj-user, and Neovim plugin managers such as vim-plug and lazy.nvim.

Sources

security posture

Risk level: green

narrow executable package without higher-risk signals.

Risk classifier

green risk · low confidence · appliance

Why

narrow executable package without higher-risk signals

Signals

metadata:no-higher-risk-signals

Install behavior

No Homebrew post-install hook is recorded in formula metadata.
Homebrew bottle metadata is available for 6 platform targets.
Installs with 1 runtime dependencies.
Build metadata lists 3 build dependencies.

Recommended review

Before unattended agent use, check whether the tool reads plaintext credentials, writes remote state, publishes artifacts, or shells out to plugins.

executables

Installed executables

Command	Kind	Exposure	Note
`cornelis`	cli	global executable

freshness

Version and freshness

These signals separate page generation age, package-manager activity, and upstream release comparison. Version lag is warned only when an evidence URL and comparable versions are present.

page generated2026-08-04

manager version2.8.0

manager updated2026-07-22

local dataok

upstreamcurrent

latest detectedv2.8.0

https://github.com/agda/cornelis

okNo freshness warnings were generated.

install metadata

Package metadata

Package key	brew:cornelis
Version	2.8.0
Package manager	Homebrew
Package manager page	https://formulae.brew.sh/formula/cornelis
Homepage	https://github.com/agda/cornelis
Repository	https://github.com/agda/cornelis
License	BSD-3-Clause
Source archive	https://github.com/agda/cornelis/archive/refs/tags/v2.8.0.tar.gz
Last updated	2026-07-22T05:23:36Z
Pulse	updated
Dependencies	gmp
Build dependencies	cabal-install, ghc, hpack
Uses from macOS	libffi
Bottle	available (on arm64_linux, arm64_sequoia, arm64_sonoma, arm64_tahoe, sonoma, x86_64_linux)
Homebrew post-install	not defined
Service	none declared

registry facts

Source database details

Source Database	Homebrew formula API
Tap	homebrew/core
Full Name	cornelis
Version Scheme	0
Revision	0
Head Version	HEAD
Bottle Stable Root URL	https://ghcr.io/v2/homebrew/core
Deprecated	no
Disabled	no
Keg Only	no
URL Keys	head stable

source database matches

Other package-manager records

Matches are pulled from external package-manager indexes and kept separate from local Automic Vault package links.

Nix95%

cornelis

nix profile install nixpkgs#cornelis

normalized package name match
Matched by: Cornelis

nixpkgs package indexes · api.github.com · nixpkgs package indexes: pkgs/by-name/co/cornelis/package.nix from https://api.github.com/repos/NixOS/nixpkgs/git/trees/master?recursive=1

package graph

Links come from deterministic package relationships, av.db category and tag curation, ecosystem matches, and package hub membership.

source trail

Generated from repository data

This page is generated by av-web from the private package SQLite artifact built by scripts/generate-pkg-sqlite.py.

Combined YAML source

View the package source record on GitHub.

combined/cornelis.yml

Used sources

Geiger risk classifier
cross-ecosystem install command graph
curated package history
external package-manager database matches
package relationship graph
package version freshness
package-page enrichment
pkg.so package database
pkgdb category and tag curation

Install cornelis with Homebrew, Nix