UInt64 ref counting error

Stream: lean4

[Sam Burnham]

On Lean v4.23.0, when using a UInt64 that sets the most significant bit (0x8000000000000000 and above), the compiler errors if lean_inc is called on that value when used more than once.

MWE:

def gSize : UInt64 := 0x8000000000000000
def mwe : UInt64 :=
    let x := gSize
    let y := gSize
    x + y

errors with

❯ lake build
✖ [7/8] Building Main:c.o
trace: .> /home/sam/.elan/toolchains/leanprover--lean4---v4.23.0/bin/cc -c -o /home/sam/lean-mwe/.lake/build/ir/Main.c.o.export /home/sam/lean-mwe/.lake/build/ir/Main.c -I /home/sam/.elan/toolchains/leanprover--lean4---v4.23.0/include -fstack-clash-protection -fwrapv -fPIC -fvisibility=hidden -Wno-unused-command-line-argument -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
/home/sam/lean-mwe/.lake/build/ir/Main.c: In function ‘_init_l_mwe___closed__0’:
/home/sam/lean-mwe/.lake/build/ir/Main.c:39:10: error: passing argument 1 of ‘lean_inc’ makes pointer from integer without a cast [-Wint-conversion]
   39 | lean_inc(x_1);
      |          ^~~
      |          |
      |          uint64_t {aka long unsigned int}
In file included from /home/sam/lean-mwe/.lake/build/ir/Main.c:4:
/home/sam/.elan/toolchains/leanprover--lean4---v4.23.0/include/lean/lean.h:512:62: note: expected ‘lean_object *’ but argument is of type ‘uint64_t’ {aka ‘long unsigned int’}
  512 | static inline void LEAN_ALWAYS_INLINE lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_ref(o); }
      |                                                ~~~~~~~~~~~~~~^
At top level:
cc1: note: unrecognized command-line option ‘-Wno-unused-command-line-argument’ may have been intended to silence earlier diagnostics
error: external command '/home/sam/.elan/toolchains/leanprover--lean4---v4.23.0/bin/cc' exited with code 1
Some required targets logged failures:
- Main:c.o
error: build failed

Using numeric symbols for 9223372036854775808 and above also causes the error, while using an exponent 2^64-1 does not. The error also doesn't occur if there's only one reference to gSize. I tested that v4.22.0 and earlier don't have this behavior.

[Sebastian Ullrich]

Could you please file an issue?

[Sam Burnham]

Sebastian Ullrich said:

Could you please file an issue?

Done: lean#10443

[Henrik Böving]

fixed lean#10444

[Sam Burnham]

Thanks for the quick fix!