Jonathan Protzenko

Results 404 comments of Jonathan Protzenko

actually, is there any way that fslit could generate the equivalent of ``` .. code-block:: fstar ``` ? I'm enjoying syntax higlighting via `pygments` for code-blocks I manually wrote, but...

Can you say more about why you want to clone from Vale? If the specs are there and are ok, can we make sure there's no copy-paste?

I think the custom extraction rules are in FStar.Extraction.Krml.fs and as long as you can still pattern-match just like before, it should be good. I think before the `new` keyword...

sadly HACL* has not been switched over to use sizet so I'm not surprised there's no diff there -- ping @cmovcc though for the starmalloc diff

or, more precisely: it won't launch the cygwin setup it just downloaded

Yes, and also see https://github.com/FStarLang/FStar/blob/master/contrib/CoreCrypto/INSTALL.md for extra packages and more detailed instructions. If you have a patch I'll gladly take it, but I think we're both short on time :)

Urgh. I can't rely on OPAM to install camlp4 properly because you _still_ need a silly patch to make camlp4 compile on Windows... see https://github.com/ocaml/camlp4/issues/41#issuecomment-55229048 Or maybe you can try...

huh. the dynloader should try to load a `cmxs`, shouldn't it?

Can you submit a pull request? (I'm short on time right now.) Thanks, Jonathan

"opam add merlin" works for "32-bit ocaml + cygwin-32 opam", but not for "64-bit ocaml + 64-bit opam"