Server crashes when evaluating missing `extern` definitions

[tydeu]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

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 --plugin.~~ (EDIT: this only occurs if the symbol is missing). This only happens with the --server mode of lean -- 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:

@[extern "my_add"] constant myAdd : UInt32 → UInt32 → UInt32

plugin/Bug..lean:

import Add
#eval myAdd 1 2 -- works as expected when run with normal `lean`; causes server to crash if the symbol is missing

Here is an example .c, and Makefile that can be used to build a plugin to test:

plugin/add.c:

#include <stdint.h>

uint32_t my_add(uint32_t a, uint32_t b) {
    return a + b;
}

plugin/Makefile:

all: Add.dll

test: test-plugin test-noplugin

add.o: add.c
	cc -c -o add.o add.c

libAddC.a: add.o
	ar rcs libAddC.a add.o

../build/lib/libAdd.a:
	cd .. && leanmake lib

Add.dll: libAddC.a ../build/lib/libAdd.a
	leanc -shared -o Add.dll -L../build/lib -Wl,--whole-archive -lAdd -Wl,--no-whole-archive -L. -lAddC

# Should produce: 3
test-plugin: Add.dll
	LEAN_PATH=../build lean --plugin Add.dll Bug.lean

# Should produce: 
# could not find native implementation of external declaration 
# 	'myAdd' (symbols 'l_myAdd___boxed' or 'l_myAdd')`
test-noplugin: ../build/lib/libAdd.a
	-LEAN_PATH=../build lean Bug.lean

Run with:

make -C plugin test

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.

[tydeu]

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).

[tydeu]

The hanging that occurs when trying to evaluate a missing symbol appears to be caused by the bug described in #640.

[Kha]

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.

[tydeu]

@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.

[leodemoura]

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.