-
Notifications
You must be signed in to change notification settings - Fork 1.2k
Closed
Description
Dear OCaml devs,
when compiling coq-serapi in 32bit OCaml we are seeing this:
$ dune build -p coq-serapi
File "serlib/.serlib.objs/native/_unknown_", line 1, characters 0-0:
(cd _build/default && /home/egallego/.opam/jscoq+32bit/bin/ocamlopt.opt -w -40 -rectypes -g -ppx '.ppx/341932708445810a638020e478ebc4f1/ppx.exe --as-ppx --cookie '\''library-name="serlib"'\''' -I serlib/.serlib.objs/byte -I serlib/.serlib.objs/native -I /home/egallego/.opam/jscoq+32bit/lib/base -I /home/egallego/.opam/jscoq+32bit/lib/base/base_internalhash_types -I /home/egallego/.opam/jscoq+32bit/lib/base/caml -I /home/egallego/.opam/jscoq+32bit/lib/base/shadow_stdlib -I /home/egallego/.opam/jscoq+32bit/lib/findlib -I /home/egallego/.opam/jscoq+32bit/lib/ocaml/threads -I /home/egallego/.opam/jscoq+32bit/lib/parsexp -I /home/egallego/.opam/jscoq+32bit/lib/ppx_compare/runtime-lib -I /home/egallego/.opam/jscoq+32bit/lib/ppx_deriving/runtime -I /home/egallego/.opam/jscoq+32bit/lib/ppx_deriving_yojson/runtime -I /home/egallego/.opam/jscoq+32bit/lib/ppx_hash/runtime-lib -I /home/egallego/.opam/jscoq+32bit/lib/ppx_sexp_conv/runtime-lib -I /home/egallego/.opam/jscoq+32bit/lib/result -I /home/egallego/.opam/jscoq+32bit/lib/seq -I /home/egallego/.opam/jscoq+32bit/lib/sexplib -I /home/egallego/.opam/jscoq+32bit/lib/sexplib0 -I /home/egallego/.opam/jscoq+32bit/lib/yojson -I /home/egallego/.opam/jscoq+32bit/lib/zarith -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/boot -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/clib -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/config -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/coqworkmgrapi -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/engine -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/gramlib -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/interp -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/kernel -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/lib -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/library -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/parsing -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/pretyping -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/printing -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/proofs -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/stm -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/sysinit -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/tactics -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/vernac -I /home/egallego/external/coq-master/_build/install/default/lib/coq-core/vm -intf-suffix .ml -no-alias-deps -open Serlib -o serlib/.serlib.objs/native/serlib__Ser_glob_term.cmx -c -impl serlib/ser_glob_term.ml)
/tmp/build_15c8bd_dune/camlasmcddc6e.s: Assembler messages:
/tmp/build_15c8bd_dune/camlasmcddc6e.s:10336: Error: operand size mismatch for `movzb'
File "serlib/ser_glob_term.ml", line 1:
Error: Assembler error, input left in file /tmp/build_15c8bd_dune/camlasmcddc6e.s
this was first detected by opam CI system. To reproduce try to build coq-serapi as above. Note that a dune build with the dev profile doesn't trigger this error. I can reproduce in 4.12 and 4.14
cc #10626 cc @kit-ty-kate
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels