cryspen/hacl-packages

`mach update` deletes necessary file

Closed this issue · 5 comments

pnmadelaine commented

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

victor-dumitrescu commented

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 commented

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 commented
  • 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.

  • ❤️1