v0.3.15

• build: Update Lean to v4.29.1

v0.3.14

• build: Update Lean to v4.28.0

v0.3.13

• build: Update Lean to v4.27.0
• fix(delab): Add recursion depth limiter in instantiateDelayedMVars
• fix(repl): Use side branch id in subsume

v0.3.11

• fix: Delayed assigned mvar visit set bug
• feat(environment): Output the result of env.catalog to file
• build: Update Lean to v4.25.2

v0.3.7

• chore: Update Lean to v4.22.0
• fix: Instance capturing with sorry tactic and its related mechanisms

v0.3.6

• feat(frontend): Restructure load_sorry so it can distil multiple sorrys into a single search target. This is called "search target distillation"
• feat(frontend): check_track can check if one Lean file conforms to the specifications of another
• fix: Improve error handling
• doc: Add documentation about new functions
• fix: Panic when executing draft tactics in captured sorrys due to auxiliary declarations

Features from v0.3.5:

• feat(goal): Now goal_tactic can execute multiple tactics in one go. have or lets are fine as well.
• feat(frontend): env_parse function divides a tactic sequence into multiple tactics
• fix: Pickling errored mvar crashes server