The compiler moves to Idris2
The stage-0 compiler has been ported from Haskell (lscz) to Idris2 (lscz2). With a dependently typed host language we can express Serene's type theory directly rather than encoding it.
This phase brought an elaborator from the high-level surface language down to the corett core, a bidirectional type checker for Kernel.TT, and the Parser and compiler Pipeline ported over to Idris2. Serene is now being built on Quantitative Type Theory — see the language report.