This commit is contained in:
Nathan McCarty 2025-02-07 06:54:36 -05:00
parent b095fe356b
commit bbf7b4f6c8

View file

@ -65,6 +65,10 @@ calls to make interaction between lazy and strict code Just Work™:
had initially thought I had discovered just _one_ compiler bug, but it turns out had initially thought I had discovered just _one_ compiler bug, but it turns out
I also stumbled into an unrelated issue in the termination checker![^8] I also stumbled into an unrelated issue in the termination checker![^8]
I also found a convoluted hole in the case generator that I had to reach out to
the community for help minimizing (thank you
dunhamsteve!):[idris-lang/Idris2#3466](https://github.com/idris-lang/Idris2/issues/3466)[^9]
I broke the [pack](https://github.com/stefan-hoeck/idris2-pack) package manager I broke the [pack](https://github.com/stefan-hoeck/idris2-pack) package manager
by, apparently, being the first person to try and upload a library to `pack-db` by, apparently, being the first person to try and upload a library to `pack-db`
with library code in literate files, in my with library code in literate files, in my
@ -96,3 +100,5 @@ ecosystem.
subset of the language for which termination is a 'trivial' property, which subset of the language for which termination is a 'trivial' property, which
includes most code I've written in the language so far, but not nearly all includes most code I've written in the language so far, but not nearly all
of it. of it.
[^9]: It's me, I'm the user on the discord