Jonathan Protzenko

Preliminary investigation indicates that the WASM memory is auto-resized (which is expected behavior) because at some point we exhaust the available space (why not), but then this possibly results in...

(on my end, increasing the initial page size just makes the problem go away, I'm tempted to put a very large number and argue that with virtual memory it's all...

https://developer.mozilla.org/en-US/docs/WebAssembly/JavaScript_interface/Memory/grow#detachment_upon_growing

Here are some other places that would need to be fixed to properly handle memory regrow: - reserve does not account for any stack space so typically it doesn't save...

> Could you confirm whether replacing `initial: 16` with `initial: 32` in `loader.js` fixes your issue? This is the workaround -- increase initial memory size (possibly to an even larger...

No objection for me, maybe this ties in to your other PR (or discussion) about having something like `assert_lowstar` or something that *then* would always print out an error if...

@mtzguido can you remind me what's up with using the most recent z3 version? what I'd like to understand is what happens to people like @R1kM and I for whom...

@karthikbhargavan can you recall if you upgraded something else in your setup then? could it be that you now have `z3` resolve to 4.13.3 instead of the old 4.8.5? F*...

yeah I'm roughly in favor of merging (modulo putting the flag directly in $(FSTAR)), with the caveat that some users may not realize that the right thing to do is...

My intuition is that I'm wary of taking a dependency on F*, and I'm afraid that I'll eventually end up debugging F*'s logic for building *and* OCaml's build logic should...