Release v1.0.1

This patch fixes a bug where z3 processes were not terminated when users
modified their code while blaster was actively solving goals. This could
lead to memory exhaustion as orphaned z3 instances accumulated in the
background.

What's Changed

• Killing external running Smt process when blaster command/tactic has changed in editor by @etiennejf in #47

Full Changelog: v1.0.0...v1.0.1

Release v1.0.0

Blaster v1.0.0 Release Notes

This constitutes the first release of Blaster. A lot of the early development was performed on a private repository sc-fvt.
Future development will be performed on this repository and release notes will reference commits and PRs from this repository.

Core Features & Architecture

• SMT Translation and Advanced Optimizations - Foundational SMT-LIB translation infrastructure for Lean 4 expressions with Z3 integration (sc-fvt#238)
• Tactic Interface - Added lean_blaster tactic with comprehensive option parsing for seamless integration into Lean 4 proof workflows (sc-fvt#504)
• Stack-based Recursion - Implemented stack-based recursion approach during optimization phase for improved performance (sc-fvt#418)

Optimization & Simplification Rules

Normalization Rules

• Initial normalization and simplification rules (sc-fvt#65)
• Match to if-then-else normalization (sc-fvt#71)
• Recursive function normalization and structural equivalence (sc-fvt#74)
• Decidable simplification rules and codebase optimization (sc-fvt#77)
• Removal of Decidable instance from Ite, Dite and Decidable.decide (sc-fvt#427)
• Normalizing ite and dite to Solver.dite' (Lean-blaster#25)

Arithmetic Simplification

• Basic simplification rules for Nat.mul, Nat.div, Nat.mod (sc-fvt#68)
• Basic simplification rules for Int.add, Int.neg, Int.mul, Int.negSucc (sc-fvt#69)
• Int and Nat division and modulo simplification rules (sc-fvt#298)
• Arithmetic equality simplification rules (sc-fvt#325)
• Advanced simplification rules for relational operators (sc-fvt#297)
• Additional equality/relational arithmetic optimization rules (Lean-blaster#35)

Control Flow Optimization

• Advanced optimization rules on Match and ITE (sc-fvt#270)
• Match elimination rules (sc-fvt#346)
• Generalized ite and match over constructor propagation rules (sc-fvt#274)
• Ite and DIte factorization rules (sc-fvt#312)
• Projection propagation rules (sc-fvt#331)

Context & Hypothesis Management

• COI (Cone of Influence) reduction rules (sc-fvt#75)
• Hypothesis context simplification rules (sc-fvt#296)

Solver Improvements

Function Handling

• Considering extensionality assertions for higher-order functions (sc-fvt#421)
• Handling axioms in solver optimization (sc-fvt#508)
• Handling opaque definitions as free variables (Lean-blaster#33)
• Co-domain restriction for undeclared/axiom functions and axioms for global lambdas (Lean-blaster#29)

Bug Fixes

• Fixed Mvar and typeclass issues when invoking blaster (sc-fvt#525, Lean-blaster#15)
• Fixed predicate qualifier generated twice bug (sc-fvt#370)
• Fixed lean_copy_expand_array issue (sc-fvt#286)
• Deactivated maxRecDepth check during term elaboration (Lean-blaster#36)
• Activated omitted relational rules with bug fix optimizations (sc-fvt#394)

Testing & Infrastructure

Test Suite

• Test cases for normalize ite and match function application (sc-fvt#391)
• Integration of all tests from sc-fvt repository (Lean-blaster#7)
• Lean-Blaster integration and adjusted test suite (sc-fvt#565)

CI/CD

• Z3 added to CI pipeline (sc-fvt#196)
• Z3 lookup in WSL and error display improvements (sc-fvt#266)
• Nightly build infrastructure (Lean-blaster#17)

Build System

• Make with all targets (sc-fvt#268)

Documentation

• Added description of the tool in README (Lean-blaster#9)
• Added Z3 installation instructions to README (Lean-blaster#38)

Full Changelog:

https://github.com/input-output-hk/Lean-blaster/commits/v1.0.0