Jonathan Protzenko

icon indicating a website link https://jonathan.protzenko.fr

icon company Microsoft icon location Redmond, WA icon location This is my professional GitHub account to record my contributions with my @Microsoft (MS) employee hat on. My open-source work is done with the @protz hat on

Results 404 comments of Jonathan Protzenko

Introduction.rst claims to be literate F*

Can you clarify your bug report? I still see the file here: https://github.com/FStarLang/karamel/blob/master/book/Introduction.rst

Specify functions that must extract?

The idea was that if something failed to extract, you'd get a warning 2 in krml (which if I recall correctly is set as an error, by default). This is...

Specify functions that must extract?

Yeah in that case an attribute (not forwarded to krml) is your best bet. How about `assert_lowstar`?

Deeply nested conditionals and branch polarity flips

I think this: https://github.com/FStarLang/karamel/blob/master/lib/Simplify.ml#L888-L899 is probably preventing the -fnoreturn-else from triggering afterwards. If this is important, you could make this optimization disabled under -fnoreturn-else...?

Performance monitoring of the Everest build

If we are talking about adding this to Everest regressions, then I suspect the plan of action would be: - modify the everest script to package runlim (if applicable) -...

Performance monitoring of the Everest build

Thanks Guido! Regarding PR on HACL: you should be able to submit a PR onto the hacl-star/hacl-star repository from an external fork (the usual GitHub fork + pr workflow). Your...

Performance monitoring of the Everest build

Ok, thanks for pointing that out -- let's not bother with relative paths into obj/, I think the rule is fine as-is and having .runlim files for the .depend files...

Rust: support for std::option without monomorphization? (and possibly more)

(as discussed privately) Disabling monomorphization for the Rust backend is a pretty big feature request, since monomorphization happens early on in the pipeline, and I do not know whether the...

Fatal error: exception Failure("[mk_expr m]: op should've been caught")

Can you post the crash details?

Dependencies in karamel.opam seem quite out of date

I'm happy to remove this dependency if CI comes back green (and also ulex and batteries). Want to submit a PR?