lean4-htt/tests/pkg
Mac Malone ad5ec0e196
feat: user-specified init fn when loading plugins (#13510)
This PR adds the ability to specify a name for the initialization
function of a Lean plugin on load.

* The `Lean.loadPlugin` API has gained a `initFn?` argument that
defaults to `none`. When `none`, the initialization function name will
be inferred from the shared library's name (as before).
* The CLI `--plugin` option can now have a initialization function
specified via `--plugin=path:initFn`.
* The `--setup` JSON configuration now also accepts`{"path": ...,
"initFn": ...}` for plugins.
2026-05-05 20:20:54 +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
homo feat: add E-matching diagnostics to grind (#13558) 2026-04-29 12:17:55 +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: prevent private default instances from leaking into public scope (#13596) 2026-05-02 07:53:44 +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 refactor: move Async and Http from Internal to Std (#13511) 2026-04-23 19:55:22 +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 feat: user-specified init fn when loading plugins (#13510) 2026-05-05 20:20:54 +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