v4.23.0
·
1287 commits
to master
since this release
refactor: port more of `shell.cpp` to Lean (#10086) This PR ports more of the post-initialization C++ shell code to Lean. All that remains is the initialization of the profiler and task manager. As initialization tasks rather than main shell code, they were left in C++ (where the rest of the initialization code currently is). The `max_memory` and `timeout` Lean options used by the the `--memory` and `--timeout` command-line options are now properly registered. The server defaults for max memory and max heartbeats (timeout) were removed as they were not actually used (because the `server` option that was checked was neither set nor exists). This PR also makes better use of the module system in `Shell.lean` and fixes a minor bug in a previous port where the file name check was dependent on building the `.ilean` rather than the `.c` file (as was originally the case). Fixes #9879. (cherry picked from commit db3fb47109de07fcfbb3e493d387086b0b8c01ae)