FFI: extern opaque fails to compile

[ydewit]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

I have an FFI project that needs to access an extern variable (not a function), but compilation fails with the following error:

info: bug: no previous manifest, creating one from scratch
ℹ [1/4] Built bug/ffi.o
info: stdout/stderr:
 ==> Building targer Main.ffi.cpp ...
trace: .> c++ -c -o ././.lake/build/Main.ffi.o ./././Main.ffi.cpp -I /Users/yuri/.elan/toolchains/leanprover--lean4---nightly/include
ℹ [2/4] Built Main
trace: .> LEAN_PATH=././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/build/lib /Users/yuri/.elan/toolchains/leanprover--lean4---nightly/bin/lean ././././Main.lean -R ./././. -o ././.lake/build/lib/Main.olean -i ././.lake/build/lib/Main.ilean -c ././.lake/build/ir/Main.c --json
✖ [3/4] Building Main:c.o (with exports)
trace: .> /Users/yuri/.elan/toolchains/leanprover--lean4---nightly/bin/leanc -c -o ././.lake/build/ir/Main.c.o.export ././.lake/build/ir/Main.c -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
././.lake/build/ir/Main.c:33:25: error: called object type 'uint16_t' (aka 'unsigned short') is not a function or function pointer
x_1 = this_ffi_type_void();
      ~~~~~~~~~~~~~~~~~~^
././.lake/build/ir/Main.c:109:1: error: use of undeclared identifier 'l_ffi__type__void'
l_ffi__type__void = _init_l_ffi__type__void();
^
././.lake/build/ir/Main.c:109:21: warning: call to undeclared function '_init_l_ffi__type__void'; ISO C99 and later do not support implicit function declarations [-Wimplicit-function-declaration]
l_ffi__type__void = _init_l_ffi__type__void();
                    ^
1 warning and 2 errors generated.
error: external command '/Users/yuri/.elan/toolchains/leanprover--lean4---nightly/bin/leanc' exited with code 1
Some builds logged failures:
- Main:c.o (with exports)
error: build failed

This is the line causing it:

@[extern "this_ffi_type_void"]
opaque ffi_type_void : UInt16 := 0

I also tried the following but got the same problem:

@[extern "this_ffi_type_void"]
opaque ffi_type_void : UInt16 := 0

Steps to Reproduce

1. download and unzip the project: bug.zip
2. cd bug
3. lake build

Expected behavior: generated code compiles

Actual behavior: generated code does not compilke

Versions

"4.9.0-nightly-2024-06-02"

Darwin merrix.local 23.5.0 Darwin Kernel Version 23.5.0: Wed May 1 20:13:18 PDT 2024; root:xnu-10063.121.3~5/RELEASE_ARM64_T6030 arm64 arm Darwin