New option --no-autodetect-provers to disable prover auto-detection (!195) Environment variable WHY3FIND_AUTODECTECT_PROVERS=no have the same effect
New command why3find dap [OPTIONS] (!185)
IDE Integration
VSCode debugger client
Bug Fixes
Allow preprocessing tactics to leave the goal unchanged (#141, !187)
1.2.0 - 2025-08-01
Command Line Interface
New option -X to print failed tasks in extenso (!165)
New option --show-progress=(never|auto|always) to control when progress is shown (#128, !170)
Bug Fixes
Truncated float printing introduced in (!81) caused imprecise calibration values on reruns which could lead to spurious cache misses. Cache entries are now printed with sufficient precision. (#125, !169)
Fix a failure when saving a new session (#137, !174)
Removed duplicated symbols from val function in generated doc and LSP server (!176)
Fixed missing symbol from let rec in generated doc and LSP server (!179)
Cleanup sessions on success (!173, !180)
Remove old theories from proof.json files (#130, !184)
1.1.1 - 2025-01-10
Bug Fixes
Fix the proving strategy to try only the first applicable tactic as stated in the doc. It would previously "backtrack" to the following tactic under certain circumstances (#121, !164).
Fix dev-repo URI in opam file (!163).
1.1.0 - 2024-12-18
Notable New Features
Make the timeout of the fast sequential proof step an independent fast parameter instead of using 1/5 * time. See option --fast and README.md (!144).
Introduce option --preprocess <tactic> to run a tactic before starting the proof strategy (!142).
Add a LSP server and VSCode extension for the WhyML language. See the corresponding section below for detailed features.
Improve cache efficiency by hashing tasks earlier in the Why3 processing (#93, !91).
Command Line Interface
Renamed option -m into --master (#99, !127)
Renamed option -v into --velocity (#99, !127)
New option -l for detailed statistics (!83, !146)
New option -g <name> to select goal(s) to be proven (!114)
New option -H n to run the proof strategy up to step n (!118)
New option --log-prover-results to dump JSON prover results (!92)
New option --list-provers to list available provers (!96)
New option --list-tactics to list available tactics (!96)
New option --strict to pin provers to their current version (#90, !86)
New option --relax to un-pin provers from their configured version (#90, !86)
New option --update to update provers' pins to latest version (!143)
New option --why3-debug to enable Why3 debug flags (#88, !80)
New option --why3-warn-off to disable Why3 warnings (#88, !80)