Release 2025.02

Release 2025.02

What's Changed

• internal: stable ordering of globals components by @strub in #612
• internals: user-defined rules can be headed by a projection by @strub in #616
• cloning: do not allow realizing a non-axiomatic lemma by @strub in #618
• runtest: lint code + fix warnings by @strub in #619
• user reduction: fix some incompleteness issues by @strub in #623
• ci: compile with warning as errors by @strub in #627
• runtest: properly restore the terminal on (exceptional) exit by @strub in #620
• pretty-printer/parser: improve reparsability of the pretty-printer output by @strub in #622
• make runtest fail reasonably on bad config filename by @fdupress in #643
• split SmtMap into SMT Array and finite map by @fdupress in #605
• Fix set_set_swap statement and proof. by @MM45 in #651
• proc rewrite now supports the /= rule by @strub in #648
• Propagate extended code positions to more tactics by @strub in #649
• The tactic swap now takes generalized code position. by @strub in #650
• no user defined rule in op comparison by @strub in #653
• New tactic to alias a subexpression of an instruction by @strub in #647
• lexer: do not lex decimal numbers when the parser won't accept them by @strub in #655
• unroll for: constant-propagate the counter by @strub in #656
• fix "unroll for" failure (InvalidCPos) by @strub in #657
• Fix deep code positions parsing by @strub in #658
• Improve code positions (match + extended assignments) by @Cameron-Low in #654
• Fix include-path management regarding duplicate paths by @strub in #663
• add alt-ergo 2.6 to the docker image by @fdupress in #662
• Track more precisely tuple to tuple assignments in sim by @cassiersg in #667
• Fixing code blocks display in readme by @aubertc in #673
• Merge typing of expressions and formulas by @strub in #671
• Some basic facts on polynomials + fix theory cloning by @strub in #679
• Tactic split with break position by @lyonel2017 in #675
• get rid of axiomatized by in favor of [opaque] with trivial lemma by @oskgo in #681
• Better operators overloading inference by @strub in #665
• PP: various fixes by @strub in #664
• Fine Grained Module Definitions by @Cameron-Low in #661
• Exposed the tp_nothing typolicy of EcTyping by @alleystoughton in #684
• More results on floor/ceil (isint) by @strub in #678
• Service commit (docker / nix / dune) by @strub in #686
• Service commit (expain flag for menhir) by @strub in #687
• runtest: ignore Emacs lock files (.#XXX) by @strub in #688
• Better printing of hint DBs by @strub in #689
• Rigid unification option for hint solve/exact by @strub in #680
• FMap: add lemmas on range after update by @fdupress in #690
• Add PKE libraries (both standard model and ROM) by @MM45 in #677
• KEM libraries (non-ROM and ROM) by @MM45 in #672
• Upgrade to why3 1.8 by @strub in #674
• [external CI] use dev branch for XSalsa checks by @fdupress in #693
• Improve transitivity* and replace* by @Cameron-Low in #692
• Apply cloning substitution to datatype ctor types by @strub in #695
• nix: add a dependency to git so that dune-site works correctly by @strub in #706
• In matching, forbid the capture of all variables by @strub in #708
• New code-position variants: ^()<-, and ^(x)<- to match tuples. by @Cameron-Low in #707
• revert subtype theory + syntactic sugar for cloning it by @strub in #691

New Contributors

• @cassiersg made their first contribution in #667
• @aubertc made their first contribution in #673

Full Changelog: r2024.09...r2025.02