Stream: coq-community devs & users

Topic: coq-bits


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Vadim Zaliva (May 05 2021 at 02:25):

I've opened an issue: https://github.com/coq-community/bits/issues/13 for further discussion.


Last updated: Feb 04 2023 at 01:03 UTC