Jonathan Protzenko

Results 404 comments of Jonathan Protzenko

Hi Landon, Unfortunately I don't think you can achieve this as-is. Let me try to explain a little bit. After processing all of the inline_for_extraction's (let's ignore refinements which are...

Thanks for testing. We can probably ditch the `-march=native` and just rely on `-O2` or whatever makes sense. It's not like there's any performance-critical code in kremlib anyhow. For the...

I'm all in favor of moving everything to Dune, so 👍 for me. Can we do something about the ctypes test? Dune folks promised an easier way to build ctypes...

There is some relevant discussion here: https://github.com/project-everest/hacl-star/pull/426

I see that https://github.com/ocaml/dune/pull/3905 was merged and there is now very nice documentation here: https://dune.readthedocs.io/en/latest/foreign-code.html#ctypes-stubgen Is there any chance we could try to use this to finish this PR?

I need to investigate, but in the meanwhile, have you tried provided a custom naming hint? Try adding: ``` let my_favorite_name = btest U8.t let my_preferred_name = test (btest U8.t)...

Hi XVilka, Thanks for the bug report! A few points to keep in mind: - unless ocamlbuild breaks in a catastrophic manner, it's unlikely that I'll find cycles to upgrade...

Thanks for your contribution! Could you tell us a little bit why this is important? I buy the changes related to `which`, but why get rid of `bash`? This complicates...

Is this using the combination of `-fmerge` and `-ftail-calls`? Thanks for the repro. From the Changelog, ```markdown ### Jan 13th, 2020 - New *experimental* option: `-fmerge`, to merge variables, i.e....

I pushed a fix. With your test file, I now get: ``` /* This file was generated by KaRaMeL KaRaMeL invocation: krml out.krml -skip-compilation -fmicrosoft -d c-names F* version: ce8b1957...