The task result state now distinguishes created/waiting/queued, which is
useful for debugging. mt_task_queue now also correctly waits for all
tasks during destruction.
This is useful if you're debugging lean-server in an IDE which cannot
redirect stdin, and also if you want to run `gdb --args lean
--server=some.file`.
@gebner I was getting the following error with valgrind:
==9902== Invalid read of size 1
==9902== at 0xAD209B: lean::module_mgr::mark_out_of_date(std::string const&, lean::buffer<std::string, 16u>&) (module_mgr.cpp:24)
==9902== by 0xAD3EF5: lean::module_mgr::invalidate(std::string const&) (module_mgr.cpp:286)
==9902== by 0x986A84: lean::server::handle_sync(nlohmann::basic_json<std::map, std::vector, std::string, bool, long, unsigned long, double, std::allocator> const&) (server.cpp:141)
==9902== by 0x986603: lean::server::handle_request(nlohmann::basic_json<std::map, std::vector, std::string, bool, long, unsigned long, double, std::allocator> const&) (server.cpp:105)
==9902== by 0x986313: lean::server::run() (server.cpp:90)
==9902== by 0x975E98: main (lean.cpp:383)
==9902== Address 0x0 is not stack'd, malloc'd or (recently) free'd
==9902==
==9902==
==9902== Process terminating with default action of signal 11 (SIGSEGV)
==9902== Access not within mapped region at address 0x0
==9902== at 0xAD209B: lean::module_mgr::mark_out_of_date(std::string const&, lean::buffer<std::string, 16u>&) (module_mgr.cpp:24)
==9902== by 0xAD3EF5: lean::module_mgr::invalidate(std::string const&) (module_mgr.cpp:286)
==9902== by 0x986A84: lean::server::handle_sync(nlohmann::basic_json<std::map, std::vector, std::string, bool, long, unsigned long, double, std::allocator> const&) (server.cpp:141)
==9902== by 0x986603: lean::server::handle_request(nlohmann::basic_json<std::map, std::vector, std::string, bool, long, unsigned long, double, std::allocator> const&) (server.cpp:105)
==9902== by 0x986313: lean::server::run() (server.cpp:90)
==9902== by 0x975E98: main (lean.cpp:383)
Now, Ctrl-c-Ctrl-g also works when hovering the beginning of the tactic
instead of the beginning of the `by` token.
The idea is to make the behavior consistent with `begin...end` blocks.
