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.

Sign up for GitHub

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

Jump to bottom

primitive/uint63/* tests fail on 32bit architectures #11624

Closed
treinen opened this issue Feb 18, 2020 · 2 comments · Fixed by #11805
Closed

primitive/uint63/* tests fail on 32bit architectures #11624

treinen opened this issue Feb 18, 2020 · 2 comments · Fixed by #11805
Labels
part: kernel part: ocaml
Milestone
8.11.1

Comments

@treinen
Copy link
Contributor

treinen commented Feb 18, 2020

The test suite fails on primitive/uint63/* on 32-bit architectures , see https://gitlab.com/coq/coq/-/jobs/436836250.
I have observed the same on an i386 porterbox, using ocaml 4.08.1. @ejgallego says it
looks like a bug, so here we go ..

Coq Version

8.11.0
@treinen
Copy link
Contributor Author

treinen commented Feb 21, 2020

For the record: I got the same test failures, plus a few additional ones, on the debian armel architecture. This is a 32bit ARM architecture, bytecode-only.

@ejgallego
Copy link
Member

Note this also fails generally on our CI if we use OCaml >= 4.08

proux01 added a commit to proux01/coq that referenced this issue Mar 11, 2020
@proux01
Fix coqchk for primitive integers on 32bit arch with OCaml >= 4.08 (c…
dfa74b2 
…oq#11624)
@proux01 proux01 mentioned this issue Mar 11, 2020
Merged
ppedrot added a commit that referenced this issue Mar 13, 2020
@ppedrot
Merge PR #11805: Fix coqchk for primitive integers on 32bit arch with…
3449c8a 
… OCaml >= 4.08 (#11624)

Reviewed-by: ppedrot
@coqbot coqbot added this to the 8.11.1 milestone Mar 13, 2020
ppedrot pushed a commit to ppedrot/coq that referenced this issue Mar 20, 2020
@proux01 @ppedrot
Fix coqchk for primitive integers on 32bit arch with OCaml >= 4.08 (c…
f2895d0 
…oq#11624)

(cherry picked from commit dfa74b2)
ppedrot added a commit to ppedrot/coq that referenced this issue Mar 20, 2020
@ppedrot
Backport PR coq#11805: Fix coqchk for primitive integers on 32bit arc…
f1c272b 
…h with OCaml >= 4.08 (coq#11624)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
part: kernel part: ocaml
Projects
None yet
Milestone
8.11.1
Development

Successfully merging a pull request may close this issue.

Fix coqchk for primitive integers on 32bit arch with OCaml >= 4.08 (#11624) proux01/coq
3 participants
@treinen @ejgallego @coqbot