search

mit-plv / riscv-coq

RISC-V Specification in Coq
BSD 3-Clause "New" or "Revised" License
109 stars 17 forks source link

[coq-platform] Smoke test broken #37

Open rtetley opened 8 months ago

rtetley commented 8 months ago

This commit breaks the smoke test in the platform: https://github.com/coq/platform/actions/runs/8391869140/job/22983180597 Could you offer a new test ?

rtetley commented 8 months ago

This breakage concerns the ~8.19~2024.01+beta1 pick

rtetley commented 8 months ago

I used the src/riscv/Examples/Fib.v file. If this is alright could you please close this issue ?

samuelgruetter commented 8 months ago

I used the src/riscv/Examples/Fib.v file. If this is alright could you please close this issue ?

That looks like a good "smoke test" to me (even though I don't know anything specific about requirements on smoke tests in the coq platform). One thing to note is that this file doesn't need anything of the src/riscv/Proofs/ directory, if that is desired, src/riscv/Proofs/DecodeEncode.v could be used, but that one doesn't need anything from the src/riscv/Platform/ directory.