runtime
@kha The runtime folder includes what is needed to link a standalone Lean program. It is still contains some unnecessary files. We will be able to remove them after we release Lean4.
The frontend is still using the old "let-expression macros". We will use the new let-expressions to implement the new tactic framework.