Yong Kiam

Hi Ramana, Thanks for pointing this out! top_case_tac seems very useful. As a related question: do you also know if there is a way to force the case splitter to...

I've tried this on x64: ``` .globl cdecl(cml_main) .globl cdecl(argc) .globl cdecl(argv) cdecl(cml_main): movabs $cdecl(argc), %rdx movabs $cdecl(argv), %rcx movq %rdi, 0(%rdx) # %rdi stores argc movq %rsi, 0(%rcx) #...

I think this was intended more for `cml_main` itself to be a callable C function rather than requiring a set_jmp long_jmp loop around it. i.e., so that e.g. `int foo...

Probably a naive question: is this referring to the "r12" and "r13" as exposed by the encoder to CakeML? I'm guessing not since I don't think r12/r13 have those special...

My understanding is that the bignum library already tries pretty hard to use small num operations where possible. So the overhead that would be eliminated here would be the checks...

Suggestion from @myreen for improving robustness of astPP: 1. Given a CakeML program `foo` in HOL, call the sexpr generator on `foo` to get `foo_sexpr_1` 2. Call astPP on `foo`...

That makes sense! I guess the proposal is more if we'd want to prototype outside of HOL/`process_topdecs` by modifying concrete syntax right away.

Just to clarify: Do you mean compiling the 64-bit CakeML compiler sexpr using the x64 compiler with --target=arm8? If so that seems extremely weird.

I suspect it's not actually running out of heap -- that's a misleading error message. Instead, I think the ARM8 encoder is actually failing to compute a jump that is...

Specifically, see https://github.com/CakeML/cakeml/pull/721 and the issues inside.