Open tydeu opened 3 years ago
Oops! I discovered that I had provided the wrong plugin when testing this (which was thus missing the symbol). Providing a plugin with the proper symbol does work (the server doesn't crash and the extern is evaluated). However, the fact that hangs/crashes with no error when the symbol is missing is still a problem in my view (for one, it would have avoid this mix-up of mine).
The hanging that occurs when trying to evaluate a missing symbol appears to be caused by the bug described in #640.
The unhandled exception in server mode is likely because the #eval
is not executed on the main thread, so main
's try-catch doesn't trigger. evalConst
has its own try-catch, but that doesn't trigger either because a closure is returned and the exception is triggered only when that closure is run. If we want to make this kind of error recoverable, we should extend evalConst
with support for an arguments array so that the exception is triggered within evalConst
's try-catch block.
@Kha While I would prefer the error being recoverable, I would at the very least hope it would actually kill the worker than exist in a zombie state that persists even once VS Code is closed.
I am marking this issue as "low priority". I am also considering closing it with "wontfix" because better FFI support for loading external shared libraries will minimize the impact of this problem.
Prerequisites
Description
The Lean 4 server hangs and crashes (with no error) when evaluating (via
#eval
) a (non-builtin) definition/constant that is defined externally.This happens irrespective of whether or not the external symbol has in fact been provided through a(EDIT: this only occurs if the symbol is missing). This only happens with the--plugin
.--server
mode oflean
-- executing the program directly with Lean either results in a proper error (if no external symbol is provided via a plugin) or runs correctly (if one is).Steps to Reproduce
Running the following program with or without a plugin to provide
my_add
causes the crash:Add.lean:
plugin/Bug..lean:
Here is an example
.c
, andMakefile
that can be used to build a plugin to test:plugin/add.c:
plugin/Makefile:
Run with:
Expected behavior:
The server returns an error when the symbol is missing or evaluates the definition correctly when a plugin is provided (like Lean does when run directly).
Actual behavior:
The server hangs/crashes with no error message if the symbol is missing.
Reproduces how often:
Always.
Versions
OS: Windows 20H2
Lean (version 4.0.0-nightly-2021-08-20, commit 1624e42a5d6d, Release)
Additional Information
I discussed this issue in a Zulip thread with @Kha and he stated that it sounds like a bug with Lean.