Zenith

Zenith is a Lean 4 library inspired by ZIO.

Right now the main goals are pedagogical:

• Explore how to translate certain OO patterns into Lean
• Simple implementation of ZIO better suited for high level analysis
• Visualization of program execution
• etc

But once the library matures enough it should be usable for regular programming.

Features

• Dependency Injection
• Error handling
• Asynchronous and Concurrent programming
• Program execution diagram

Status

• Core data type and interpreter ✅
• Fibers ✅
• Environment ✅
• Layers ❌

Future plans

• Find a workaround for the limitation that Z Services can't be used in environment.
• Scopes and FiberRefs
• Fiber supervision
• Concurrency primitives
• Better integration with Lean features

Building and running examples

• Elan is needed to install lake, which will in turn download project dependencies (i.e. the specific Lean 4 version).
• VSCode + Lean 4 plugin is the recommended editor.

Compile everything once

lake build

Recompile on chage

Using the entr file monitor

find . -name "*.lean" | entr -s 'lake build'

Run example programs

./build/bin/z

Regenerate svg diagrams

(Graphviz needs to be installed)

for f in $(find diagrams -name "*.dot"); do echo $f; dot -Tsvg $f -o diagrams/$(basename $f .dot).svg; done

This will (re)create a bunch of svg files under diagrams/*.

Internal documentation

• Interpreter
• Module dependencies
• Variance
• Problems