db3fb47109
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. |
||
|---|---|---|
| .. | ||
| alloc.h | ||
| ascii.cpp | ||
| ascii.h | ||
| bit_tricks.cpp | ||
| bit_tricks.h | ||
| CMakeLists.txt | ||
| escaped.cpp | ||
| escaped.h | ||
| exception_with_pos.h | ||
| ffi.cpp | ||
| freset.h | ||
| init_module.cpp | ||
| init_module.h | ||
| io.h | ||
| kvmap.cpp | ||
| kvmap.h | ||
| lbool.cpp | ||
| lbool.h | ||
| list.h | ||
| list_fn.cpp | ||
| list_fn.h | ||
| macros.h | ||
| map_foreach.cpp | ||
| map_foreach.h | ||
| message_definitions.h | ||
| name.cpp | ||
| name.h | ||
| name_generator.cpp | ||
| name_generator.h | ||
| name_hash_map.h | ||
| name_hash_set.h | ||
| name_map.h | ||
| name_set.cpp | ||
| name_set.h | ||
| nat.h | ||
| null_ostream.h | ||
| option_declarations.cpp | ||
| option_declarations.h | ||
| options.cpp | ||
| options.h | ||
| output_channel.h | ||
| pair.h | ||
| path.cpp | ||
| path.h | ||
| rb_map.h | ||
| rb_tree.h | ||
| rc.h | ||
| shell.cpp | ||
| test.h | ||
| timeit.cpp | ||
| timeit.h | ||
| timer.cpp | ||
| timer.h | ||
| unit.h | ||
| unlock_guard.h | ||