Jonathan Protzenko
Jonathan Protzenko
Companion PR in https://github.com/FStarLang/karamel/pull/273 You can override the definition of `KRML_HOST_IGNORE` with something more suitable if need be by invoking `krml` with `-add-early-include '"mydefs.h"'`, then defining `KRML_HOST_IGNORE` in `mydefs.h` before...
- [x] move the Low\* libraries under the LowStar prefix (instead of FStar) - [x] remove old libraries from ulib/ - [x] F\* doc (the tool) (#634) - [x] write,...
The following snippet doesn't work: ``` module JH type vec (a: Type): nat -> Type = | Nil: vec a 0 | Cons: hd:a -> n:nat -> tl:vec a n...
Trying to complete an identifier with Ctrl-x Ctrl-o, I get this error: ``` Error detected while processing function merlin#Complete: line 38: Traceback (most recent call last): Press ENTER or type...
With https://github.com/FStarLang/karamel/pull/273 there is now a way to forcefully "ignore" a variable, in order to silence a compiler warning for an unused variable. If I compile dist/gcc-compatible *without* `-Wno-unused-variable`, these...
https://github.com/FStarLang/karamel/pull/274 contains a potential improvement to remove the amount of unused variables This is not necessarily a slam dunk. I'll comment on specific bits of the diff to point out...
@franziskuskiefer reported that our usage of `__has_include` was yet one more oddity that made support across compiler versions difficult. I believe this *used* to be a an issue but with...
I had fun this afternoon and monitored a full build of HACL* on my machine to see who were the worst offenders in terms of memory usage... this is a...
Hi Natalia, I just noticed that your recent addition of SHA3 to dist/mozilla breaks the build on OSX with this: ``` /Library/Developer/CommandLineTools/usr/bin/ranlib: file: libevercrypt.a(Vale.o) has no symbols Undefined symbols for...
Just making a note of this. This is quite extreme and I wonder if there's anything specific in this file causing this. This is triggering other issues in e.g. CI...