This PR fixes fallout of the closure allocator changes in #10982. As far
as we know
this bug only meaningfully manifests in non default build configurations
without mimalloc such as:
`cmake --preset release -DUSE_MIMALLOC=OFF`
The issue is that I forgot to update the deallocation functions for
closures. However, this only
seems to matter if we disable mimalloc which is why this slipped through
testing.
This PR implements the `#grind_lint` command, a diagnostic tool for
analyzing the behavior of theorems annotated for theorem instantiation.
The command helps identify problematic theorems that produce excessive
or unbounded instance generation during E-matching, which can lead to
performance issues.
The main entry point is:
```
#grind_lint check
```
which analyzes all theorems marked with the `@[grind]` attribute.
For each theorem, it creates an artificial goal and runs `grind`,
collecting statistics about the number of instances produced.
Results are summarized using info messages, and detailed breakdowns are
shown for lemmas exceeding a configurable threshold.
Additional subcommands are provided for targeted inspection and control:
* `#grind_lint inspect thm`: analyzes one or more specific theorems in
detail
* `#grind_lint mute thm`: excludes a theorem from instantiation during
analysis
* `#grind_lint skip thm`: omits a theorem from being analyzed by
`#grind_lint check`
This PR renames `String.endPos` to `String.rawEndPos`, as in a future
release the name `String.endPos` will be taken by the function that is
currently called `String.endValidPos`.
This PR improves the release automation. We link to CI output for
building the release tag, don't give instructions for bumping downstream
repositories until the release it ready, and improve documentation and
prompts.
This PR improves the scripts assisting with cutting Lean releases (by
reporting CI status of open PRs, and adding documentation), and adds a
`.claude/commands/release.md` prompt file so Claude can assist.
This PR adds the necessary infrastructure for recording elaboration
dependencies that may not be apparent from the resulting environment
such as notations and other metaprograms. An adapted version of `shake`
from Mathlib is added to `script/` but may be moved to another location
or repo in the future.
This PR introduces a simple script that adjusts module headers in a
package for use of the module system, without further minimizing import
or annotation use.
---------
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
This PR includes some improvements to the release process, making the
updating of `stable` branches more robust, and including `cslib` in the
release checklist.
This PR reviews the expected-to-fail-right-now tests for `grind`, moving
some (now passing) tests to the main test suite, updating some tests,
and adding some tests about normalisation of exponents.
This PR make some minor changes to the grind annotation analysis script,
including sorting results and handling errors. Still need to add an
external UI.
This PR adds a script for analyzing `grind` E-matching annotations. The
script is useful for detecting matching loops. We plan to add
user-facing commands for running the script in the future.
This PR updates `release_repos.yml` to reflect that `import-graph` no
longer depends on `batteries`, and reorders the repositories to better
reflect dependencies.
This PR further improves release automation, automatically incorporating
material from `nightly-testing` and `bump/v4.X.0` branches in the bump
PRs to downstream repositories.
This PR further updates release automation. The per-repository update
scripts `script/release_steps.py` now actually performs the tests,
rather than outputting a script for the release manager to run line by
line. It's been tested on `v4.21.0` (i.e. the easy case of a stable
release), and we'll debug its behaviour on `v4.22.0-rc1` tonight.
This PR changes the CI setup to generate `lean-pr-testing-NNNN` branches
for Mathlib on the `leanprover-community/mathlib4-nightly-testing` fork,
rather than on the main repo.
This PR removes an old workaround around non-implemented C++11 features
in the thread finalization.
This `ifdef` dates back to approximately 2015 as can be seen
[here](https://github.com/leanprover/lean3/blame/master/src/util/thread.cpp#L177),
the comments mention that it was originally implemented because not all
compilers at the time were able to support the C++11 `thread_local`
keyword. 10 years later this is hopefully the case and we can remove
this workaround.
There is an additional motivation for doing this,
`lean::initialize_thread` contains the following allocation:
```cpp
g_thread_finalizers_mgr = new thread_finalizers_manager;
```
this is supposed to be freed at some point but:
```cpp
// TODO(gabriel): race condition with thread finalizers
void delete_thread_finalizer_manager() {
// delete g_thread_finalizers_mgr;
// g_thread_finalizers_mgr = nullptr;
}
```
so `g_thread_finalizers_mgr` leaks upon repeated invocation of
`lean::initialize_thread`.
Note that Windows has already been using this alternative implementation
for a while so the alternative implementation has (hopefully) not rotten
away in the meantime.
This PR improves the release checklist and scripts:
* Check that the release's commit hash is not all-numeric starting with
0 (this can break SemVer, which [required us to release
v4.21.0-rc2](https://github.com/leanprover/lean4/releases/tag/v4.21.0-rc2)).
* Check that projects being bumped to a release tag do not reference
`nightly-testing` anymore.
* Clarify how to create subsequent release candidates if an `-rc1`
already exists.
* Fix typos in the release checklist documentation.
This PR adjusts the experimental module system to not export the bodies
of `def`s unless opted out by the new attribute `@[expose]` on the `def`
or on a surrounding `section`.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR ensures that for modules opted into the experimental module
system, we do not import module docstrings or declaration ranges.
Excluding declaration docstrings as well would require some more work to
make `[inherit_doc]` leave a mere reference to the other declaration
instead of copying its docstring eagerly.
This PR adds further automation to the release process, taking care of
tagging, and creating new `bump/v4.X.0` branches automatically, and
fixing some bugs.
---------
Co-authored-by: Johan Commelin <johan@commelin.net>
This PR fixes a number of bugs in the release automation scripts, adds a
script to merge tags into remote `stable` branches, and makes the main
`release_checklist.py` script give suggestions to call the
`merge_remote.py` and `release_steps.py` scripts when needed.
---------
Co-authored-by: Johan Commelin <johan@commelin.net>
