Martin Karup Jensen

I have to go back on my statement: I currently don't have the time to investigate this, so take the above code as the full bug report.

@JasonGross I reported this a while back, so I can't quite remember what the versions were at the time. I also haven't tested whether the issue is still present. For...

Sorry for the late, late reply. It seems to happen when trying to pretty print anything that is an in-memory data structure (using pointers) (which is basically what CertiCoq translates...

Sorry for the late reply. Adding the `-O1` flag fixes the issue with too many locals, so it's only about the incorrect behavior. If I compile with `emcc -O1 -fsanitize=undefined...

Sorry for the late, late reply. Adding -O1 and specifying a large enough stack size and initial memory produces the correct result, so that's a mistake on my part. As...

I'm investigating different ways of extracting Coq programs to WebAssembly binaries. One way to do this is to extract to OCaml, and from there use [wasm_of_ocaml](https://github.com/ocaml-wasm/wasm_of_ocaml). This uses the standard...

My apologies for the radio silence, vacation time. > I had a go at this in #43 . There are some instructions to try it out in the PR description,...

The bytecode compilation in the PR works for my purposes! (I haven't tested anything other than running the bytecode and compiling it to Wasm) I don't know if it will...

> @mkarup I tried to implement your suggested fixes, indeed the C code I wrote departs quite a bit from the ml code in Coq's kernel. Could you give it...

The PR fixes the issues I reported, but of course the tests are by no means exhaustive (insert Dijkstra quote here). One more thing that I forgot to add to...