Vadim Zaliva (May 04 2021 at 17:57): Vadim Zaliva (May 04 2021 at 17:57):I am trying to update coq-bits to work with recent version of Coq and OCaml. I've did some cosmetic changes and it compiles OK. However make verify pass 8 bit tests but hangs on 16 bit. I first thought it is regression, but I tried to make verify with Coq 8.12.2 and OCaml 4.07.1 and it also hangs. I see that verify target is not invoked during OPAM package built, so I suspect OPAM package is built without passing these tests. @Anton Trunov , perhaps as the maintainer, you can weight in on this? Is it a bug?
Vadim Zaliva (May 04 2021 at 17:58):Here is a branch with my fixes. Once make verify problem is resolved I will make a pull request. https://github.com/vzaliva/bits/tree/coq813
Vadim Zaliva (May 04 2021 at 18:02):src/extraction/verif.sh
patching file axioms8.ml
Hunk #1 succeeded at 159 (offset 5 lines).
Hunk #2 FAILED at 836.
1 out of 2 hunks FAILED -- saving rejects to file axioms8.ml.rej
patching file axioms16.ml
Hunk #1 succeeded at 159 (offset 5 lines).
Hunk #2 FAILED at 836.
1 out of 2 hunks FAILED -- saving rejects to file axioms16.ml.rej
Verifying 8bit
Finished, 8 targets (8 cached) in 00:00:00.
... Ok
Verifying 16bit
Finished, 8 targets (8 cached) in 00:00:00.
I've opened an issue: https://github.com/coq-community/bits/issues/13 for further discussion.
Last updated: Jun 06 2023 at 23:01 UTC