Jean-Christophe Léchenet
Jean-Christophe Léchenet
> Not sure, it says ask JC If I recall correctly, Benjamin wrote that when he and I tried to write elpi alone (and it didn't work well :grin: )....
> one thing that worries me a little is that the new eqb function apparently don't move when you call simpl. I guess it is the bug that if you...
> I did not try. `cbn` seems to work. And it seems you can use `Arguments eqb_body _ _ _ _ _ _ _ _ _ /.` to make `eqb_body`...
> looks good now. Still I've one question, and IIRC you have this in Jasmin: > > ```coq > Definition alias := list nat. > derive alias. > ``` >...
Benjamin thought about it : it seems like a bad idea in the end, because in the second version `p` remains live during the call of `f`.
I encountered the same bug. Here is another example ``` export fn main () -> reg u64 { reg u64 x; stack u64 y; x = 0; y = #MOV(x);...
Maybe related to https://github.com/jasmin-lang/jasmin/issues/601?
The second example reveals a real problem in the allocator if I'm not mistaken: the fact that registers and extra registers can conflict. The problem does not happen with large...
For example 1, it depends whether we want to be able to write code working both for ARM and x86. If we do not care, there is no problem rejecting...
No, the conflict may arise also if there are extra registers available. If we use all of them, we end up in this case too. This is just a bit...