Comments (4)
JasonGross
commented on September 22, 2024
Though also I don't want to see
coqc -q -Q src/bedrock2 bedrock2 -Q ../deps/coqutil/src/coqutil coqutil special/BytedumpTest.v > special/BytedumpTest.out.tmp0
head -c $(($(wc -c < special/BytedumpTest.out.tmp0 | xargs) - 1)) special/BytedumpTest.out.tmp0 > special/BytedumpTest.out.tmp
rm special/BytedumpTest.out.tmp0
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
every single time I build
from bedrock2.
samuelgruetter
commented on September 22, 2024
@andres-erbsen could you please take care of the BytedumpTest.out related stuff? I don't understand it well and why it's so many commands...
from bedrock2.
JasonGross
commented on September 22, 2024
Note that you can just hide them all except when VERBOSE=1, and simply print out testing bytedump or something
from bedrock2.
JasonGross
commented on September 22, 2024
Note that there is also the issue of
coq_makefile -f _CoqProject INSTALLDEFAULTROOT = bedrock2 /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Scalars.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/NotationsCustomEntry.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/MetricLogging.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/BasicC64Semantics.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Syntax.v /home/$gross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/BasicCSyntax.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/FE310CSemantics$v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Lift1Prop.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/ZNamesSyn$ax.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/TailRecursion.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Tr$cePredicate.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/string2ident.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bed$ock2/Map/SeparationLogic.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Map/Separation.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/b$drock2/src/bedrock2/Map/FDSepLog.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Byte.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bed$ock2/src/bedrock2/Markers.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Memory.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2$src/bedrock2/Examples/ArrayLoadStore.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/ARPResponder.v /home/jgross/Documents/repos/fia$-crypto/bedrock2/bedrock2/src/bedrock2/Examples/lightbulb_spec.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/MultipleReturnValues.$ /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/Trace.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examp$es/bsearch.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/SPI.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedr$ck2/Examples/chacha20.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/StructAccess.v /home/jgross/Documents/repos/fiat-crypto/bedroc$2/bedrock2/src/bedrock2/Examples/LAN9250.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/FE310CompilerDemo.v /home/jgross/Documents/$epos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/lightbulb.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/Demos.v /home/jgr$ss/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/ipow.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/ARPRespo$derProofs.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/swap.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedr$ck2/Semantics.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Array.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2$ProgramLogic.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/AbsintWordToZ.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/b$drock2/StringNamesSyntax.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/ToCString.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedroc$2/src/bedrock2/StructNotations.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/ptsto_bytes.v /home/jgross/Documents/repos/fiat-crypto/bedrock$/bedrock2/src/bedrock2/ReversedListNotations.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/WeakestPrecondition.v /home/jgross/Documents/rep$s/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Hexdump.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/div10.v /home/jgross/Documents/repos/fia$
-crypto/bedrock2/bedrock2/src/bedrock2/Variables.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/BasicC32Semantics.v /home/jgross/Documents/r$
pos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Structs.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Bytedump.v /home/jgross/Documents/repo$
/fiat-crypto/bedrock2/bedrock2/src/bedrock2/NotationsInConstr.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Notations.v /home/jgross/Docume$
ts/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/WeakestPreconditionProperties.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/ChangeSeman$
icsParams.v -o Makefile.coq.all
which could use a similar fix as in mit-plv/coqutil@079ca2b
from bedrock2.
Related Issues (20)
- Using multiple return values HOT 2
- Why does bedrock2 use `Load`? HOT 2
- Please create a tag for Coq 8.16 in Coq Platform 2022.09 HOT 6
- bedrock2 fails with a syntax error on Windows HOT 9
- bedrock2 lightbulb example is incompatible with native_compute HOT 5
- Less Memory-Hungry, More Principled Solution for Decidable Side-Conditions HOT 2
- Failing in coq CI HOT 1
- `make` should not run `coq` and `cc` when there's nothing to be done
- Update tested is failing with rate limits HOT 2
- Bedrock2 is broken on Coq's CI HOT 1
- Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 HOT 2
- Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 HOT 2
- design: outputting bitwidth-generic code? HOT 7
- design: core functionality of RecordPredicates? HOT 4
- Unbound value Int.land HOT 2
- Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10 [coq-bedrock2] HOT 2
- Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10 [coq-bedrock2-compiler] HOT 2
- install target is unusable when sudo doesn't have access to coqc HOT 4
- [coq-bedrock2] Please create a tag for Coq 8.19 in Coq Platform 2024.01
- [coq-bedrock2-compiler] Please create a tag for Coq 8.19 in Coq Platform 2024.01
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from bedrock2.