AndrasKovacs

I investigated resilient parsing (meaning that we want to parse as much of the source as possible and produce multiple errors) and arrived at the following thing: https://andraskovacs.github.io/posts/2026/09/resilient-parsing/ I'm quite happy with this iteration. The most interesting thing I learned is probably the following: every parsing error should have *three* positions. The position where the parser actually failed, and a span around it which indicates the *error node* being produced in the AST. These error nodes are carried further into elaboration and behave the same way as error nodes produced from elaboration errors, i.e. we can report multiple parsing and elaboration errors at the same time.

@ncf@types.pl @jonmsterling@mathstodon.xyz @totbwf@types.pl @jeanas@mathstodon.xyz All of IR, II and HII types can be specified in terms of eliminators. The only relevant thing that's missing from literature is HII eliminators in cubical TTs.

@zyang Cool stuff!

• This paper is about NbE with term sharing: https://arxiv.org/pdf/2603.21949 Based on this, I attempted a simple Haskell implementation: https://gist.github.com/AndrasKovacs/0e1bc2532e071cef5974ca582f8090ad I'm not completely sure about the correctness of my version, but in the case it's wrong it would be fixed by using global "gensym", like in the paper.
• This paper uses a similar evaluator, but since it's a conversion checker, it's quite a bit more complicated: https://hal.science/hal-05322705/document
• Another direction of NbE optimization is to reduce space usage by "trimming" environments; this is well-known in closed evaluators but it's been used in normalizers too, e.g. in https://depositonce.tu-berlin.de/items/512ba4cd-ff0c-4f33-a5c2-a8fdc66dc03c and probably in the Rocq VM (not sure).

@MartinEscardo @liamoc @jonmsterling I used Ubuntu for 10 years or so, because it was supposed to Work and I didn't have interest in tweaking and tinkering. But my experience has never been great, and it got so bad last year that I switched to CachyOS in anger. And it was positively shocking how much better it was in every way that's relevant to my usual activities. Now I think that Ubuntu plainly sucks. Its popularity is basically also steadily dropping and I barely see it being recommended to new users.

@zwarich @MartinEscardo For positivity checking we need to check how definitions and arguments occur in definitions. We do this for a mutual block at once. The old code used a naive cubic transitive closure of the occurrence graph. The new code is a quadratic depth-first search that's more specific for the work and also more optimized. https://github.com/agda/agda/commit/4e481bf79340e0e58a99818e20dbf377d1acae90