make bedrock2-files is broken
Closed this issue · 1 comments
I tried to run make bedrock2-files and was met with the error /bin/sh: --lang: command not found. Indeed, when I have the Makefile target print out the command it's trying to run, I see:
( --lang bedrock2 --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select '25519' 64 '(auto)' '2^255 - 19' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes carry_scmul121666 && touch fiat-bedrock2/src/curve25519_64.c.ok) > fiat-bedrock2/src/curve25519_64.c.tmp
The Makefile line generating this line is:
($(TIMER) $($(BEDROCK2_$*_BINARY_NAME)) --lang bedrock2 $(BEDROCK2_ARGS) $($*_DESCRIPTION) $($*_ARGS) $($*_FUNCTIONS) && touch $@.ok) > $@.tmp
I can conclude that there's something going wrong with finding the right binary file, but there's too much Makefile magic for me to determine what exactly is going wrong. I think this might have happened in 890de05 . @JasonGross , can you fix it?
Other than regenerating the bedrock2 output, the change putting output pointers before input in the bedrock2 backend is ready to go.
Ah, indeed. Does changing $($(BEDROCK2_$*_BINARY_NAME)) to $(BEDROCK2_$($*_BINARY_NAME)) (and $$($$(BEDROCK2_$$*_BINARY_NAME)) to $$(BEDROCK2_$$($$*_BINARY_NAME)) in the rule dependency) fix things?