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 verify hangs #13

Closed
vzaliva opened this issue May 4, 2021 · 2 comments
Closed

make verify hangs #13

vzaliva opened this issue May 4, 2021 · 2 comments

Comments

@vzaliva
Copy link
Contributor

vzaliva commented May 4, 2021

make verify pass 8-bit tests but hangs on 16-bit.
Coq 8.12.2 and OCaml 4.07.1.

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.
@vzaliva
Copy link
Contributor Author

vzaliva commented May 5, 2021

From the paper[1]: "The execution of the OCaml-extracted test takes 4 seconds for to cover all 8-bits integers. The equivalent test for 16-bit integers did not complete after several hours"

I left the test running overnight to see if it ever completes for 16-bit integers on my machine. Has it ever been successfully run? If not, perhaps it is worth mentioning in README.

[1] https://hal.archives-ouvertes.fr/hal-01251943/document

@vzaliva vzaliva closed this as completed May 5, 2021
@vzaliva
Copy link
Contributor Author

vzaliva commented May 5, 2021

Finished overnight. The diff is still failing but I will address this in PR

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