Vincent Laporte

I guess the annotation should be ignored, with a warning.

Thanks. This crash (`Fatal error: exception Not_found`) of the second example is addressed by #694.

To begin with, I’d like to remind that “unsafe” means: reasoning about the run-time behaviors is invalid. Therefore the phrase “the stack usage of the function” makes no sense (worse,...

The first example now gives a proper error message (after #313). The second example is still bad. One possible fix would be to have a pass before lowering that checks...

Nice work! Thanks for your contribution. It would be nice if you could write a few example Jasmin programs to better illustrate the intended uses of these syscalls. You should...

Thanks for the example. IMHO, you should put the zero terminator in your global constants. There is no need to copy from global to stack. Are you sure, when calling...

Sure. Thanks for your help. I’ve just rebased and launched CI.

The CI machine ran out of memory. Is this just bad luck or the sign of a real regression?

> Indeed, apparently it's much better. How do you know? What’s a good way to measure time & memory consumption of `coqc`?

What’s the meaning of all these new warnings? Should we pay attention to them or just silence them?