Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

make should not run coq and cc when there's nothing to be done #298

Open
JasonGross opened this issue Nov 21, 2022 · 0 comments
Open

make should not run coq and cc when there's nothing to be done #298

JasonGross opened this issue Nov 21, 2022 · 0 comments

Comments

@JasonGross
Copy link
Contributor

Fiat-Crypto's start-up make is slow because make bedrock2_ex; make compiler_noex runs

COQFLAGS="-Q src/bedrock2 bedrock2 -Q src/bedrock2Examples bedrock2Examples  -Q /home/jgross/Documents/GitHub/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil " ../etc/bytedump.py bedrock2.PrintListByte.allBytes > special/BytedumpTest.out.tmp
COQFLAGS="-Q src/bedrock2 bedrock2 -Q src/bedrock2Examples bedrock2Examples  -Q /home/jgross/Documents/GitHub/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil " ../etc/bytedump.py bedrock2.ToCStringExprTypecheckingTest.test > special/TypecheckExprToCString.c
hexdump < /dev/null && \
        hexdump -C special/BytedumpTest.golden.bin > special/BytedumpTest.golden.hex && \
        hexdump -C special/BytedumpTest.out.tmp > special/BytedumpTest.out.hex && \
        diff -u special/BytedumpTest.golden.hex special/BytedumpTest.out.hex && \
        rm special/BytedumpTest.golden.hex special/BytedumpTest.out.hex || true
diff -u special/BytedumpTest.golden.bin special/BytedumpTest.out.tmp
mv special/BytedumpTest.out.tmp special/BytedumpTest.out
COQFLAGS="-Q src/bedrock2 bedrock2 -Q src/bedrock2Examples bedrock2Examples  -Q /home/jgross/Documents/GitHub/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil " ../etc/bytedump.py bedrock2.ToCStringStackallocLoopTest.main_cbytes > special/stackloop.c
COQFLAGS="-Q src/bedrock2 bedrock2 -Q src/bedrock2Examples bedrock2Examples  -Q /home/jgross/Documents/GitHub/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil " ../etc/bytedump.py bedrock2Examples.stackalloc.stacknondet_c > special/stacknondet.c
cc -fsyntax-only special/TypecheckExprToCString.c
cc -O0 special/stackloop.c -o special/stackloop
special/stackloop
cc special/stacknondet.c -o special/stacknondet
special/stacknondet

twice, even if it's already been run.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant