CakeML/cakeml

Make chars_to_nums tail-recursive?

Open

#1,392 opened on May 18, 2026

View on GitHub
 (1 comment) (0 reactions) (0 assignees)Standard ML (98 forks)auto 404
dev experiencegood first issuehelp wanted

Repository metrics

Stars
 (1,169 stars)
PR merge metrics
 (PR metrics pending)

Description

When I tried to perf Candle using a custom version of the compiler that "simulates" the calls in CakeML by adjusting the C stack (pushing/popping two addresses), I ran into segfaults:

warning: failed to parse execution context from corefile: Cannot access memory at address 0x7ffede486ff0
Failed to read a valid object file image from memory.
Core was generated by `./cake --candle'.
Program terminated with signal SIGSEGV, Segmentation fault.
#0  0x00005618030e23f8 in cml_decodeProg_chars_to_nums_9849 ()
#0  0x00005618030e23f8 in cml_decodeProg_chars_to_nums_9849 ()
Backtrace stopped: Cannot access memory at address 0x7ffeda487000
rsp            0x7ffeda487000      0x7ffeda487000
rbp            0x7ffeda487000      0x7ffeda487000
rip            0x5618030e23f8      0x5618030e23f8 <cml_decodeProg_chars_to_nums_9849+38>

Note that this happens on startup and also happens with --repl.

Claude suggests that this is because chars_to_nums is not tail-recursive (which it isn't):

Definition chars_to_nums_def:
  chars_to_nums ns =
    if NULL ns then [] else
      let (k,ks) = dec_next 0 1 ns in
        k :: chars_to_nums ks

The "fix" was to bump up my ulimit -s to something larger. Claude suggests that it needs to be ~80MB with the current definition.

Contributor guide