From 16dfce7e6e523addf852139695df8a8b05d641c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9ana=20=E6=B1=9F?= Date: Sun, 25 Jan 2026 11:49:00 +0100 Subject: [PATCH 1/5] nvim: move out cornelis autocommands to avoid duplication --- .config/nvim/ftplugin/agda.vim | 21 +-------------------- .config/nvim/plugin/cornelis.vim | 17 +++++++++++++++++ 2 files changed, 18 insertions(+), 20 deletions(-) create mode 100644 .config/nvim/plugin/cornelis.vim diff --git a/.config/nvim/ftplugin/agda.vim b/.config/nvim/ftplugin/agda.vim index 74a49940..3c80e715 100644 --- a/.config/nvim/ftplugin/agda.vim +++ b/.config/nvim/ftplugin/agda.vim @@ -150,26 +150,7 @@ imap \Chi Χ imap \Psi Ψ imap \Omega Ω -" autoload -function! CornelisLoadWrapper() - if exists(":CornelisLoad") ==# 2 - CornelisLoad - endif -endfunction - -au BufReadPre *.agda call CornelisLoadWrapper() -au BufReadPre *.lagda* call CornelisLoadWrapper() - -au BufRead,BufNewFile *.agda call AgdaFiletype() -au BufRead,BufNewFile *.lagda* call AgdaFiletype() -au QuitPre *.agda :CornelisCloseInfoWindows -au QuitPre *.lagda* :CornelisCloseInfoWindows - -" autoreload at file write -au BufWritePost *.agda execute "normal! :CornelisLoad\" -au BufWritePost *.lagda* execute "normal! :CornelisLoad\" - -" default cornelis config +" default cornelis mapping nnoremap l :CornelisLoad nnoremap r :CornelisRefine nnoremap d :CornelisMakeCase diff --git a/.config/nvim/plugin/cornelis.vim b/.config/nvim/plugin/cornelis.vim new file mode 100644 index 00000000..27930283 --- /dev/null +++ b/.config/nvim/plugin/cornelis.vim @@ -0,0 +1,17 @@ +" agda related autocommands + +function! CornelisLoadWrapper() + if exists(":CornelisLoad") ==# 2 + CornelisLoad + endif +endfunction + +au BufReadPre *.agda call CornelisLoadWrapper() +au BufReadPre *.lagda* call CornelisLoadWrapper() + +au QuitPre *.agda :CornelisCloseInfoWindows +au QuitPre *.lagda* :CornelisCloseInfoWindows + +" autoreload at file write +au BufWritePost *.agda execute "normal! :CornelisLoad\" +au BufWritePost *.lagda* execute "normal! :CornelisLoad\" From d2ebdb007336b182e9c6f1799c6c31c9f94b0ff9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9ana=20=E6=B1=9F?= Date: Sun, 25 Jan 2026 14:43:13 +0100 Subject: [PATCH 2/5] nvim/agda: add bindings for PFLA chapter "Induction" --- .config/nvim/ftplugin/agda.vim | 40 ++++++++++++++++++++-------------- 1 file changed, 24 insertions(+), 16 deletions(-) diff --git a/.config/nvim/ftplugin/agda.vim b/.config/nvim/ftplugin/agda.vim index 3c80e715..9038d60a 100644 --- a/.config/nvim/ftplugin/agda.vim +++ b/.config/nvim/ftplugin/agda.vim @@ -3,22 +3,30 @@ " (Link is dead so use wayback machine) " Superscripts -imap ^0 ⁰ -imap ^1 ¹ -imap ^2 ² -imap ^3 ³ -imap ^4 ⁴ -imap ^5 ⁵ -imap ^6 ⁶ -imap ^7 ⁷ -imap ^8 ⁸ -imap ^9 ⁹ -imap ^+ ⁺ -imap ^- ⁻ -imap ^= ⁼ -imap ^( ⁽ -imap ^) ⁾ -imap ^n ⁿ +imap \^0 ⁰ +imap \^1 ¹ +imap \^2 ² +imap \^3 ³ +imap \^4 ⁴ +imap \^5 ⁵ +imap \^6 ⁶ +imap \^7 ⁷ +imap \^8 ⁸ +imap \^9 ⁹ +imap \^+ ⁺ +imap \^- ⁻ +imap \^= ⁼ +imap \^( ⁽ +imap \^) ⁾ +imap \^n ⁿ + +imap \^l ˡ +imap \^r ʳ + +imap \' ′ +imap \'' ″ +imap \''' ‴ +imap \'''' ⁗ " Subscripts imap \_0 ₀ From e538cf1fdfbe2a85e264530e577a7a55e32c0c17 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9ana=20=E6=B1=9F?= Date: Sun, 25 Jan 2026 15:24:17 +0100 Subject: [PATCH 3/5] nvim/agda: document how to find new symbols --- .config/nvim/ftplugin/agda.vim | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.config/nvim/ftplugin/agda.vim b/.config/nvim/ftplugin/agda.vim index 9038d60a..6a5dbec8 100644 --- a/.config/nvim/ftplugin/agda.vim +++ b/.config/nvim/ftplugin/agda.vim @@ -2,6 +2,9 @@ " https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VIMEditing#:~:text=agda%2Dutf8%2Evim " (Link is dead so use wayback machine) +" To add more +" https://www.compart.com/en/unicode/ + " Superscripts imap \^0 ⁰ imap \^1 ¹ From cc9a1be62f55738915fc2a24d9560796acde719e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9ana=20=E6=B1=9F?= Date: Sun, 25 Jan 2026 22:01:04 +0100 Subject: [PATCH 4/5] npins/cornelis: use 2.7.1 due to agda's interface change --- nix/overlays/cornelis.nix | 5 +++++ npins/sources.json | 9 +++++---- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/nix/overlays/cornelis.nix b/nix/overlays/cornelis.nix index 7ae3c175..3008001b 100644 --- a/nix/overlays/cornelis.nix +++ b/nix/overlays/cornelis.nix @@ -2,4 +2,9 @@ let sources = import ../../npins; in + +# If this is updated, we break split on case support for PLFA. +# PLFA uses 2.7.0 +# https://github.com/agda/cornelis/issues/169 +assert sources.cornelis.version == "v2.7.1"; sources.cornelis.asFlake.overlays.cornelis diff --git a/npins/sources.json b/npins/sources.json index 929ec7c3..c6de909e 100644 --- a/npins/sources.json +++ b/npins/sources.json @@ -27,10 +27,11 @@ "version_upper_bound": null, "release_prefix": null, "submodules": false, - "version": "v2.8.0", - "revision": "67137c76fe0d4a8bb899eea46afaa370993d3556", - "url": "https://api.github.com/repos/agda/cornelis/tarball/refs/tags/v2.8.0", - "hash": "sha256-dGS6De3EtTirgEMDMSjA+iBNc670W7pG4eA02Nq7Azo=" + "version": "v2.7.1", + "revision": "40298eed11eb877526b3ab3f648d8a7bff9e2f50", + "url": "https://api.github.com/repos/agda/cornelis/tarball/refs/tags/v2.7.1", + "hash": "sha256-h18AeggnOSSjy0RLJIkWsSID1BJTarOV9F1APKusIrE=", + "frozen": true }, "disko": { "type": "GitRelease", From edf313dfb3b6fe68f2f8f7e52ff812113ad40e98 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9ana=20=E6=B1=9F?= Date: Sun, 25 Jan 2026 22:39:53 +0100 Subject: [PATCH 5/5] overlays/iosevka: useless refactor --- nix/overlays/iosevka/default.nix | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/nix/overlays/iosevka/default.nix b/nix/overlays/iosevka/default.nix index 236e7059..bae060fa 100644 --- a/nix/overlays/iosevka/default.nix +++ b/nix/overlays/iosevka/default.nix @@ -29,18 +29,18 @@ let identityOverlay = _: _: { }; overlays = - lib.crossLists - ( - spacingCfg: variantCfg: - lib.composeManyExtensions [ - spacingCfg - variantCfg - ] - ) - [ + let + # Useless complexity just for the fun + n-airyToList = acc: x: { + value = acc ++ [ x ]; + __functor = self: n-airyToList self.value; + }; + combinations = lib.crossLists (n-airyToList [ ]) [ (import ./spacings.nix) ([ identityOverlay ] ++ import ./variants.nix) ]; + in + map ({ value, ... }: lib.composeManyExtensions value) combinations; iosevkas = lib.genAttrs' overlays ( overlay: