Wojciech Różowski 9aad86a576 feat: allow deprecating options (#13195) ... This PR adds support for marking options as deprecated. When a deprecated option is used via `set_option`, a warning is emitted (controlled by `linter.deprecated.options`). An `OptionDeprecation` structure with a required `since` field and an optional `text?` field is added to `OptionDecl`. Each `set_option` elaborator (command, term, tactic, grind) calls `checkDeprecatedOption` to emit warnings. The C++ `register_option` is updated to account for the new field. As a first use, `backward.eqns.nonrecursive` and `backward.eqns.deepRecursiveSplit` are marked deprecated. Continues earlier work done in #11096.		2026-04-02 14:44:11 +00:00
..
builtin_attr	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
cbv_attr	chore: disable cbv usage warning (#12986)	2026-03-19 14:12:04 +00:00
collectAxioms	feat: support #print axioms under the module system (#13117)	2026-03-27 10:15:49 +00:00
debug	fix: lake: error on executables with duplicate root module names (#13028)	2026-03-23 18:10:10 +00:00
def_clash	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
deprecated_arg	feat: add deprecated_arg attribute (#13011)	2026-03-30 10:20:44 +00:00
deprecated_module	feat: add deprecated_module (#13002)	2026-04-01 14:40:43 +00:00
deprecated_option	feat: allow deprecating options (#13195)	2026-04-02 14:44:11 +00:00
deriving	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
frontend	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
initialize	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
issue12825	fix: re-privatize constant name prefix in realizeConst to avoid diamond import collisions (#12964)	2026-03-18 13:54:50 +00:00
leanchecker	refactor: remove Lean.Environment.replay from core (#12972)	2026-03-18 22:11:42 +00:00
linter_set	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
misc	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
mod_clash	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
module	fix: namespace used in private import and current module vanishes dowstream (#12840)	2026-03-20 13:27:26 +00:00
path with spaces	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
prv	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
rebuild	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
setup	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
signal	fix: use process signal numbers from correct architecture (#12900)	2026-03-17 13:33:13 +00:00
structure_docstrings	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
sym_ext	feat: add extensible state mechanism for SymM (#13080)	2026-03-24 03:58:45 +00:00
sym_simp_attr	feat: add Sym.simp theorem set attributes (#13018)	2026-03-21 03:53:39 +00:00
test_extern	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
user_attr	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
user_attr_app	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
user_ext	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
user_opt	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
user_plugin	chore: improve how test suite interacts with stages (#12913)	2026-03-16 15:20:03 +00:00
ver_clash	chore: clean up old test artifacts (#13179)	2026-03-30 08:02:52 +00:00
.gitignore	chore: migrate pkg tests (#12889)	2026-03-11 18:55:46 +00:00