The idea is to prevent unwanted type information at lean-mode.
For example, before this commit, we would get "list.nil : ..." type
info whenever we hovered over the "end" of a "begin...end" block.
When we check whether the dependencies for a task have already been
evaluated and then accordingly move the task from waiting to queued, we
do not remove it from the reverse dependency lists it appears in.
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.
