search

AbsInt / CompCert

The CompCert formally-verified C compiler
https://compcert.org
Other
1.88k stars 228 forks source link

Build fails on macOS Sierra 10.12.1 #152

Closed mattam82 closed 7 years ago

mattam82 commented 7 years ago

I'm trying to install compcert 2.7.1 (opam package) on OS X and I get this:


gcc -m32 -c -DMODEL_sse2 -DABI_standard -DSYS_linux -o i64_dtos.o ia32/i64_dtos.S
ia32/i64_dtos.S:59:1: error: unknown directive
.type __i64_dtos, @function; .size __i64_dtos, . - __i64_dtos
^
ia32/i64_dtos.S:59:30: error: unknown directive
.type __i64_dtos, @function; .size __i64_dtos, . - __i64_dtos
                             ^
make[2]: *** [i64_dtos.o] Error 1

More info:

#=== ERROR while installing coq-compcert.2.7.1 ================================#
# opam-version 1.2.1
# os           darwin
# command      make -j4
# path         /Users/mat/.opam/coq.8.5.1/build/coq-compcert.2.7.1
# compiler     system (4.02.1)
# exit-code    2
# env-file     /Users/mat/.opam/coq.8.5.1/build/coq-compcert.2.7.1/coq-compcert-11320-d0f245.env
# stdout-file  /Users/mat/.opam/coq.8.5.1/build/coq-compcert.2.7.1/coq-compcert-11320-d0f245.out
# stderr-file  /Users/mat/.opam/coq.8.5.1/build/coq-compcert.2.7.1/coq-compcert-11320-d0f245.err
### stdout ###
# [...]
# OCAMLOPT cparser/Parse.ml
# OCAMLOPT driver/Frontend.ml
# OCAMLOPT driver/Driver.ml
# Linking ccomp
# /Applications/Xcode.app/Contents/Developer/usr/bin/make runtime
# /Applications/Xcode.app/Contents/Developer/usr/bin/make -C runtime
# gcc -m32 -c -DMODEL_sse2 -DABI_standard -DSYS_linux -o i64_dtos.o ia32/i64_dtos.S
# gcc -m32 -c -DMODEL_sse2 -DABI_standard -DSYS_linux -o i64_dtou.o ia32/i64_dtou.S
# gcc -m32 -c -DMODEL_sse2 -DABI_standard -DSYS_linux -o i64_sar.o ia32/i64_sar.S
# gcc -m32 -c -DMODEL_sse2 -DABI_standard -DSYS_linux -o i64_sdiv.o ia32/i64_sdiv.S
### stderr ###
# r   __i 64_  sdi , .  - _ _i64_ v
# [...]
#       ^
#                         ^
# make[2]: *** [i64_sdiv.o] Error 1
# make[2]: *** Waiting for unfinished jobs....
# make[2]: *** [i64_sar.o] Error 1
# make[2]: *** [i64_dtou.o] Error 1
# make[2]: *** [i64_dtos.o] Error 1
# make[1]: *** [runtime] Error 2
# make: *** [all] Error 2

# gcc -v
Configured with: --prefix=/Applications/Xcode.app/Contents/Developer/usr --with-gxx-include-dir=/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.11.sdk/usr/include/c++/4.2.1
Apple LLVM version 7.0.0 (clang-700.0.72)
Target: x86_64-apple-darwin16.1.0
Thread model: posix

# ld -v
@(#)PROGRAM:ld  PROJECT:ld64-253.3.3
configured to support archs: armv6 armv7 armv7s arm64 i386 x86_64 x86_64h armv6m armv7k armv7m armv7em
LTO support using: Apple LLVM 7.0.0 (clang-700.0.72)

# opam list
base-bigarray         base  Bigarray library distributed with the OCaml compiler
base-bytes            base  Bytes library distributed with the OCaml compiler
base-ocamlbuild       base  OCamlbuild binary and libraries distributed with the OCaml compiler
base-threads          base  Threads library distributed with the OCaml compiler
base-unix             base  Unix library distributed with the OCaml compiler
biniou              1.0.12  Binary data format designed for speed, safety, ease of use and backward compatibility as protocols evolve
camlp5                6.16 (pinned)  Preprocessor-pretty-printer of OCaml
conf-m4                  1  Virtual package relying on m4
conf-which               1  Virtual package relying on which
coq                  8.5.2 (pinned)  Formal proof management system.
coq-color            1.2.0  A library on rewriting theory and termination.
coq-ext-lib          0.9.4  A library of Coq definitions, theorems, and tactics.
coq-squiggle-eq        dev  A formalization of Howe's Squiggle equality
coq-template-coq   8.5.dev (pinned)  A quoting library for Coq.
cppo                 1.4.1  Equivalent of the C preprocessor for OCaml programs
easy-format          1.2.0 (pinned)  High-level and functional interface to the Format module of the OCaml standard library
menhir            20161115  LR(1) parser generator
merlin               2.5.3  Editor helper, provides completion, typing and source browsing in Vim and Emacs
ocamlbuild               0  Build system distributed with the OCaml compiler since OCaml 3.10.0
ocamlfind            1.6.2 (pinned)  A library manager for OCaml
yojson               1.3.2 (pinned)  Yojson is an optimized parsing and printing library for the JSON format 

cat /Users/mat/.opam/coq.8.5.1/build/coq-compcert.2.7.1/coq-compcert-11320-d0f245.err

Warning: you are using the standard library and/or the %inline keyword. We
recommend switching on --infer in order to avoid obscure type error messages.
Built an LR(0) automaton with 595 states.
Built an LR(1) automaton with 595 states.
2 shift/reduce conflicts were silently solved.
Extra reductions on error were added in 101 states.
Priority played a role in 0 of these states.
Built an LR(0) automaton with 426 states.
Built an LR(1) automaton with 426 states.
5851 shift/reduce conflicts were silently solved.
Built an LR(0) automaton with 595 states.
Built an LR(1) automaton with 595 states.
2 shift/reduce conflicts were silently solved.
Extra reductions on error were added in 101 states.
Priority played a role in 0 of these states.
Read 211 sample input sentences and 157 error messages.
/var/folders/6t/3bgdwycx7hzgfpqcl07f_z2w0000gp/T/camlasmdad9c5.s:2224:30: warning: trigraph ignored [-Wtrigraphs]
        .ascii  "FFEEEDDDDCBBBAAAAA@@??>>==<<;;:998887766554433221100//..--,,++**))((''&&%%$$##\42\42"
                                     ^
1 warning generated.
ia32/i64_sdiv.Sia32/i64_dtou.S:ia32/i64_dtos.S73:ia32/i64_sar.S1::8759: error: unknown directive:1:
:.ty: 159p:: e1error: : error: unknown directiveunknown directive
error: 
unknown directive.ty
. _pt.typype _ee ___ __iii_6464__i64_sad6tr4_, sdouivdtos, @fun, @fu@ctincto,ni fo; .u@functnncst; iion; izone _.;s.sizize _i__i64e_sd __i64_6 dti.4osvs,,_dtou,  . i ze ._.-_ i 64_sar,-  __i64_sdi -v__. - i 
^
64ia32/i64_sdiv.S___:__id6t734:30ou
i: _s64_dtoerror: ^sunknown directive
aia32/i64_dtou.S:87:
r30: 
^^

.terror: yia32/i64_dtos.S:pe59:30unknown directive
 _.t
ype ia32/i64_sar.S:_i__i6: error: 59:4_unknown directive
dtou, @function; .s.ti6y429ze __i6: error: 4_unknown directivedpe __i6t_s4_didtv
o.tu,, os@yf pe, @fuu _n._nctc tion- i6__ii; 4._ss64_diztoare , u_@
_o      n; fi64.   sun_dtos, . - _  ct  _iioni 64ze __; .sid to_ze _i6_s4i6_      s d4    i
 _ v, .       s^ -a
r   __i 64_  sdi , .  - _ _i64_ v
      s      a r    
                       ^ 
      ^
                        ^
make[2]: *** [i64_sdiv.o] Error 1
make[2]: *** Waiting for unfinished jobs....
make[2]: *** [i64_sar.o] Error 1
make[2]: *** [i64_dtou.o] Error 1
make[2]: *** [i64_dtos.o] Error 1
make[1]: *** [runtime] Error 2
make: *** [all] Error 2

/Users/mat/.opam/coq.8.5.1/build/coq-compcert.2.7.1/coq-compcert-11320-d0f245.out
...
OCAMLOPT extraction/Selection.ml
OCAMLOPT extraction/Compiler.ml
OCAMLOPT cparser/Lexer.ml
OCAMLOPT cparser/Parse.ml
OCAMLOPT driver/Frontend.ml
OCAMLOPT driver/Driver.ml
Linking ccomp
/Applications/Xcode.app/Contents/Developer/usr/bin/make runtime
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C runtime
gcc -m32 -c -DMODEL_sse2 -DABI_standard -DSYS_linux -o i64_dtos.o ia32/i64_dtos.S
gcc -m32 -c -DMODEL_sse2 -DABI_standard -DSYS_linux -o i64_dtou.o ia32/i64_dtou.S
gcc -m32 -c -DMODEL_sse2 -DABI_standard -DSYS_linux -o i64_sar.o ia32/i64_sar.S
gcc -m32 -c -DMODEL_sse2 -DABI_standard -DSYS_linux -o i64_sdiv.o ia32/i64_sdiv.S

cat /Users/mat/.opam/coq.8.5.1/build/coq-compcert.2.7.1/coq-compcert-11320-d0f245.env
PATH=/Users/mat/.opam/coq.8.5.1/bin:/usr/local/bin:/usr/local/sbin:/opt/local/bin:/Users/mat/research/coq/v8.4/bin:/Users/mat/bin:/Users/mat/usr/bin:/sbin/:/usr/sbin:/usr/local/sbin:/opt/bin:/sw/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin:/opt/X11/bin:/Library/TeX/texbin
OCAML_TOPLEVEL_PATH=/Users/mat/.opam/coq.8.5.1/lib/toplevel
PERL5LIB=/Users/mat/.opam/coq.8.5.1/lib/perl5:
MANPATH=:/Users/mat/.opam/coq.8.5.1/man
OPAMSWITCH=coq.8.5.1
OPAMUTF8MSGS=1
CAML_LD_LIBRARY_PATH=/Users/mat/.opam/coq.8.5.1/lib/stublibs:/usr/local/lib/ocaml/stublibs
BIBINPUTS=/Users/mat/me/publication/bib:.:
TERM_PROGRAM=Apple_Terminal
BSTINPUTS=/Users/mat/me/publication/bibstyles:
SHELL=/bin/bash
TERM=xterm-256color
HISTSIZE=5000
PGPPATH=/Users/mat/.gnupg
TMPDIR=/var/folders/6t/3bgdwycx7hzgfpqcl07f_z2w0000gp/T/
Apple_PubSub_Socket_Render=/private/tmp/com.apple.launchd.wEJkkO363b/Render
TERM_PROGRAM_VERSION=387
DEBUGGER=gdb
TERM_SESSION_ID=00BE3091-6A80-43F4-B459-2A934634E51D
LC_ALL=fr_FR.UTF-8
USER=mat
PROMPT_HOSTNAME=swag
LD_LIBRARY_PATH=/Users/mat/usr/lib:
SSH_AUTH_SOCK=/private/tmp/com.apple.launchd.zRnRj4WZ7J/Listeners
__CF_USER_TEXT_ENCODING=0x1F6:0x0:0x0
T1LIB_CONFIG=/Users/mat/.t1config
PWD=/Users/mat/research/certicoq/theories
EDITOR=/usr/bin/vim
XPC_FLAGS=0x0
XPC_SERVICE_NAME=0
TEXINPUTS=/Users/mat/me/publication/styles:/Users/mat/me/publication/figures::/Users/mat/.latex:/usr/lib/ocaml/ocamldoc/:/usr/share/texmf/advi:
COLORFGBG=default;default
SHLVL=1
HOME=/Users/mat
LATEXINPUTS=/Users/mat/me/publication/styles:/Users/mat/.latex:
LOGNAME=mat
HOMEPATHLENGTH=11-1
PROFILE_LOADED=1
LC_CTYPE=UTF-8
PROMPT_COMMAND=prompt_cmd
CVSEDITOR=vim
DISPLAY=:0
RSYNC_RSH=ssh
SECURITYSESSIONID=186a7
_=/usr/local/bin/opam
OLDPWD=/Users/mat/research/certicoq/libraries
OPAM_PACKAGE_VERSION=2.7.1
OPAM_PACKAGE_NAME=coq-compcert
MAKELEVEL=
MAKEFLAGS=
bschommer commented 7 years ago

The problem is that your system gcc, which is used to compile the 64 bit runtime library and later as linker/assembler by CompCert, is configured for x86_64-apple-darwin16.1.0 but CompCert expects a gcc for x86_32-linux. I'm not quite that familiar with opam but maybe one could add a check for a x86_32-linux-gcc.

m-schmidt commented 7 years ago

I can reproduce this on my El Capitan machine when CompCert is configured for target 'x86_32-linux'. To solve the problem, you currently have to compile CompCert yourself. The necessary target then is 'x86_32-macosx'.

maximedenes commented 7 years ago

@mattam82 hasn't this been fixed by your PR on the Coq OPAM repo?

mattam82 commented 7 years ago

Yes it has been fixed for OS X

On Wed, Dec 7, 2016 at 3:56 PM Maxime Dénès notifications@github.com wrote:

@mattam82 https://github.com/mattam82 hasn't this been fixed by your PR on the Coq OPAM repo?

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://github.com/AbsInt/CompCert/issues/152#issuecomment-265467993, or mute the thread https://github.com/notifications/unsubscribe-auth/AAGARdVf5DT8mW1eKKBs677H4GlZ-P-Pks5rFsj1gaJpZM4LBREx .