Jean-Christophe Léchenet comments

Results 173 comments of


                                            Jean-Christophe Léchenet

Bad interaction of async proofs and HB

Never mind, this is an occurrence of https://github.com/LPCIC/coq-elpi/issues/543, closing.

Opam fails to install in directory with spaces in the name.

On Linux, even with opam 2.2~alpha2, I get an error ``` /tmp/dir with spaces% opam switch create toto --packages ocaml.4.14.1 --jobs=1 Installing new switch packages Switch invariant: ["ocaml" {= "4.14.1"}]...

add something to exit while and for loop

Yes

Risc v constants if while

I took the liberty to rename the pass ("prelowering" was unclear). If you agree with the changes I did, I'll merge.

Risc v constants if while

One side note: maybe it would make sense not to print the program after the pass when actually the pass is not called (on x86 and arm), but this is...

Risc v constants if while

Ok, I'm merging then.

Make constant-propagation stronger

The inlining of global variables was not done in #541 for the bounds of `for` loops. Is this feature desirable? We expect the bounds of a `for` loop to be...

Combination of flags passed as an argument triggers an internal error

I think in some cases, this can be useful. At least, this is tested in the test-suite.

Combination of flags passed as an argument triggers an internal error

But it does not seem to be used in libjade at the moment.

With option returnaddress=stack, the compiler can use LR/ra as a result register

I thought about it, and I think the fact that adding RA to the callee_save registers avoids the problem on our examples is more or less luck. Indeed, callee_save registers...