Reed Mullanix totbwf · He/Him
  • Hamilton, ON
  • https://reedmullanix.com

  • PhD student at McMaster University working on proof assistants

  • Joined on 2026年04月20日
totbwf deleted branch fix-issue-146 from totbwf/mikan 2026年06月29日 17:05:18 +02:00
totbwf pushed to main at 1lab/mikan 2026年06月29日 17:05:17 +02:00
f1e3544f31 fix: invalidate source text cache before token highlighting
e777c0cdd0 test: add reproducer for #146
b566748d04 test: sanitize emacs test output
Compare 3 commits »
totbwf merged pull request 1lab/mikan#147 2026年06月29日 17:05:17 +02:00
Invalidate source text cache before computing token-based highlighting
totbwf closed issue 1lab/mikan#146 2026年06月29日 17:05:17 +02:00
Error warning from the Emacs mode when opening and editing an already loaded file
totbwf created pull request 1lab/mikan#147 2026年06月29日 16:22:37 +02:00
Invalidate source text cache before computing token-based highlighting
totbwf pushed to fix-issue-146 at totbwf/mikan 2026年06月29日 16:21:02 +02:00
f1e3544f31 fix: invalidate source text cache before token highlighting
totbwf commented on issue 1lab/mikan#146 2026年06月29日 15:48:53 +02:00
Error warning from the Emacs mode when opening and editing an already loaded file

I suspect this might have something to do with 1lab/mikan#129, which caches the text of each source module. We currently only evict the cache in cmd_load', but token...

totbwf commented on issue 1lab/mikan#146 2026年06月29日 15:41:02 +02:00
Error warning from the Emacs mode when opening and editing an already loaded file

I've got a reproducer up at https://codeberg.org/totbwf/mikan/src/branch/fix-issue-146. Looks like the problem is that agda2-highlight-tokens is using a stale version of the file for some reason.

totbwf pushed to fix-issue-146 at totbwf/mikan 2026年06月29日 15:24:24 +02:00
e777c0cdd0 test: add reproducer for #146
b566748d04 test: sanitize emacs test output
a3beab3c1e fix reference to Mikan (instead of Agda) in cabal.project.ghc-9.14.1
1515b8739c chore: make fix-whitespace
0f415fe6d1
 with display: always reconstruct head term
Compare 10 commits »
totbwf created branch fix-issue-146 in totbwf/mikan 2026年06月29日 15:24:24 +02:00
totbwf commented on pull request 1lab/mikan#136 2026年06月26日 14:11:38 +02:00
chore/fix: unbreak larger parts of make test

Yeah, that seems like a good idea to me!

totbwf commented on pull request 1lab/mikan#136 2026年06月25日 17:20:40 +02:00
chore/fix: unbreak larger parts of make test

I can confirm that plan is to work towards a makefile-free future. Currently, all the tests do run and pass under cabal test, so these makefile targets are no longer needed. I'd be inclined to...

totbwf deleted branch emacs-fixes from totbwf/mikan 2026年06月25日 17:04:22 +02:00
totbwf merged pull request 1lab/mikan#143 2026年06月25日 17:04:21 +02:00
Add golden tests for the emacs mode, fix a bunch of bugs
totbwf pushed to main at 1lab/mikan 2026年06月25日 17:04:21 +02:00
f268b2ecea emacs: Initialize the mikan process after major mode starts
ed2c8ae4b5 test: add emacs regression tests for goal detection
5248c93df5 tests: Add tasty infrastructure for testing the emacs mode
298541a087 emacs: Fix race condition in agda2-restart
5a5e4cc156 emacs: fix issues with goal detection introduced in #8498
Compare 5 commits »
totbwf closed issue 1lab/mikan#142 2026年06月25日 17:04:20 +02:00
agda2-program-name cannot be set as a directory-local variable and cannot be influenced by global minor modes
totbwf commented on pull request 1lab/mikan#143 2026年06月25日 16:48:10 +02:00
Add golden tests for the emacs mode, fix a bunch of bugs

Right now, CI will skip over all of the emacs tests, as we don't have emacs inside of the flake. I don't know if we want to include emacs in the flake though; perhaps a separate CI pipeline...

totbwf created pull request 1lab/mikan#143 2026年06月25日 16:47:06 +02:00
Add golden tests for the emacs mode, fix a bunch of bugs
totbwf pushed to emacs-fixes at totbwf/mikan 2026年06月25日 16:36:18 +02:00
f268b2ecea emacs: Initialize the mikan process after major mode starts
ed2c8ae4b5 test: add emacs regression tests for goal detection
5248c93df5 tests: Add tasty infrastructure for testing the emacs mode
298541a087 emacs: Fix race condition in agda2-restart
5a5e4cc156 emacs: fix issues with goal detection introduced in #8498
Compare 10 commits »
totbwf created branch emacs-fixes in totbwf/mikan 2026年06月25日 16:36:17 +02:00