mach update deletes necessary file

[pnmadelaine]

Running mach update deletes ocaml/lib/Lib_RandomBuffer_System_bindings.ml which is necessary to build the OCaml bindings.

[pnmadelaine]

@victor-dumitrescu is this file actually needed? as @franziskuskiefer noticed, the function exposed there is deprecated anyway https://github.com/hacl-star/hacl-star/blob/3e283efd721ceff6fc11eef4c4908662287a6ff9/lib/c/Lib_RandomBuffer_System.c#L56

[victor-dumitrescu]

The file is needed to bind to Lib_RandomBuffer_System. I haven't seen that randombytes is now deprecated, it seems that we should switch over to crypto_random in the OCaml bindings. In any case, the .ml file would still be required.

AFAIK this file is handwritten (since the C file it provides the bindings for is not generated by karamel. Maybe that's why it gets deleted?

[franziskuskiefer]

Yeah, I think we need change the HACL makefile. @protz had some ideas but I never got around to trying them.
Let's get this fixed before merging #410.

[msprotz]

• Several functions still rely on randombytes, so we can't exactly get rid of this file.
• The bindings for this file are not auto-generated by krml like the others, they are hand-written and live in hacl-star/lib/ml/
• A version of this file used to exist in dist/gcc-compatible/lib
• It was removed in commit d0c3db3538c32f2f8033bc9db8396abc9b9630e2 (by @pnmadelaine)
• The logic that copied the file from lib/ml to dist/gcc-compatible was also removed by @pnmadelaine in 7789f9bd858d9028364a8637a5306b5a3159f126

Excerpt of the logic removed by 7789f9bd858d9028364a8637a5306b5a3159f126:jjjkj

-dist/gcc-compatible/Makefile.basic: HAND_WRITTEN_ML_BINDINGS += \
-  $(wildcard lib/ml/*_bindings.ml)

-       [ x"$(HAND_WRITTEN_ML_BINDINGS)" != x ] && mkdir -p $(dir $@)/lib && cp $(HAND_WRITTEN_ML_BINDINGS) $(dir $@)lib/ || true

If these rules are not replicated by mach, then they should. That is, mach should pull that file from lib/ml and move it to the corresponding folder.

[franziskuskiefer]

fixed in #411