Skip to content

v4.23.0

Choose a tag to compare

@github-actions github-actions released this 14 Sep 14:52
· 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)