Idris2Doc : lscz

lscz, the Serene bootstrap interpreter

An interpreter for a frozen subset of Serene, written in Idris2. Its only job is to run stage1, the real Serene compiler written in Serene, until stage1 can compile itself.

The interpreter parses type annotations and drops them. It never checks types.

Build and test

All commands run from inside lscz/ (use nix develop for the toolchain):

    idris2 --typecheck lscz.ipkg              # fastest check
    idris2 --build tests.ipkg                 # build the test suite
    ./build/exec/lscz-tests                   # run it

The pipeline




Package lscz - Namespaces