diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index cd88e35ba6..6f9f5370d3 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -796,7 +796,7 @@ private: } if (object * const * o = g_init_globals->find(fn)) { // persistent, so no `inc` needed - return *o; + return type_is_scalar(t) ? unbox_t(*o, t) : *o; } symbol_cache_entry e = lookup_symbol(fn); diff --git a/tests/pkg/initialize/.gitignore b/tests/pkg/initialize/.gitignore new file mode 100644 index 0000000000..bfb30ec8c7 --- /dev/null +++ b/tests/pkg/initialize/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/tests/pkg/initialize/Initialize.lean b/tests/pkg/initialize/Initialize.lean new file mode 100644 index 0000000000..e205e2493a --- /dev/null +++ b/tests/pkg/initialize/Initialize.lean @@ -0,0 +1,5 @@ +import Initialize.Basic + +/-- info: 42 -/ +#guard_msgs in +#eval initNat diff --git a/tests/pkg/initialize/Initialize/Basic.lean b/tests/pkg/initialize/Initialize/Basic.lean new file mode 100644 index 0000000000..d25d1eed68 --- /dev/null +++ b/tests/pkg/initialize/Initialize/Basic.lean @@ -0,0 +1 @@ +initialize initNat : Nat ← pure 42 diff --git a/tests/pkg/initialize/lakefile.toml b/tests/pkg/initialize/lakefile.toml new file mode 100644 index 0000000000..069562dfd3 --- /dev/null +++ b/tests/pkg/initialize/lakefile.toml @@ -0,0 +1,5 @@ +name = "initialize" +defaultTargets = ["Initialize"] + +[[lean_lib]] +name = "Initialize" diff --git a/tests/pkg/initialize/test.sh b/tests/pkg/initialize/test.sh new file mode 100755 index 0000000000..b1c0671e59 --- /dev/null +++ b/tests/pkg/initialize/test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +rm -rf .lake/build +lake build