Tahina Ramananandro (professional account)

Yes, in a container running from the Docker image, I can successfully compile and run a `__int128_t` function that computes 2^(2^n): ``` docker run -i -t tahina/20200318ocamlstdint ContainerAdministrator@52e7a61f5bdc /cygdrive/c/test/ocaml-stdint $...

Thank you for the update. However, that doc reads (emphasis mine): > *Beginning in Dune 3.0*, it’s possible to use the ctypes stanza to generate bindings for C libraries without...

Thank you for your suggestion. Alas, it does not seem to help: ```fstar let my_preferred_name1 = test (btest U8.t) let w1 (x: my_preferred_name1) : HST.Stack U8.t (fun h -> B.live...

cc @R1kM

While this issue still remains at large, I managed to work around it for most of my use cases involving Steel.ST arrays by changing the representation of universe lifting for...

I hope this constraint can be lifted thanks to FStarLang/FStar#2205, which should allow me to correctly perform structural recursion on `bitsum_t`

> The quackyducky/3d Makefile does not pass the clean target down to 3d/ocaml, so the 3d/ocaml/_build directory was not removed, resulting in a dirty build. This particular issue should be...

I wrote a documentation page to build EverParse from its sources, now at https://project-everest.github.io/everparse/build.html or, equivalently, `doc/build.rst`. I managed to build and run EverParse on FreeBSD 12.2 (but then, C...

Thank you @landonf for testing on your side! > Building against a non-writable OCaml installation (using `make everparse`) failed in `install-hacl-star-raw` when attempting to modify `ld.conf` to include the new...

> Building against a user-writable opam installation got to the packaging stage, but failed in `package.sh` when attempting to discover `libffi`: Thank you for reporting! Yes, I learnt how to...