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

Z3 4.8.5 build on Cygwin fails on flexlink -fopenmp #1

Open
btj opened this issue Jul 23, 2019 · 2 comments
Open

Z3 4.8.5 build on Cygwin fails on flexlink -fopenmp #1

btj opened this issue Jul 23, 2019 · 2 comments

Comments

@btj
Copy link
Member

btj commented Jul 23, 2019

Build https://travis-ci.org/verifast/vfdeps-win/builds/562820769 fails here:

ocamlmklib -o api/ml/z3ml -I api/ml api/ml/z3native_stubs.o api/ml/z3enums.cmo api/ml/z3native.cmo api/ml/z3.cmo  -cclib -lz3 -cclib -fopenmp -cclib -static-libgcc -cclib -static-libstdc++
ocamlfind ocamlopt -package num  -I api/ml -o api/ml/z3enums.cmx -c ../src/api/ml/z3enums.ml
ocamlfind ocamlopt -package num  -I api/ml -o api/ml/z3native.cmx -c ../src/api/ml/z3native.ml
ocamlfind ocamlopt -package num  -I api/ml -o api/ml/z3.cmx -c ../src/api/ml/z3.ml
ocamlmklib -o api/ml/z3ml -I api/ml api/ml/z3native_stubs.o  api/ml/z3enums.cmx api/ml/z3native.cmx api/ml/z3.cmx -cclib -lz3 -cclib -fopenmp -cclib -static-libgcc -cclib -static-libstdc++
ocamlfind ocamlopt -package num  -linkall -shared -o api/ml/z3ml.cmxs -I . -I api/ml api/ml/z3ml.cmxa
make[1]: Leaving directory '/cygdrive/c/Users/travis/build/verifast/vfdeps-win/z3-Z3-4.8.5/build'
flexlink: unknown option '-fopenmp'.
File "caml_startup", line 1:
Error: Error during linking
make[1]: *** [Makefile:4464: api/ml/z3ml.cmxs] Error 2

I'm guessing that the -cclib -fopenmp arguments to ocamlmklib should be -cclib -link -cclib -fopenmp to ensure the -fopenmp is passed to the actual linker. Of course, the question is whether the -fopenmp flag is compatible with Cygwin at all.

@btj btj closed this as completed in 6e77b53 Jul 23, 2019
@btj btj reopened this Jul 23, 2019
@btj
Copy link
Member Author

btj commented Jul 24, 2019

Z3's build/Makefile file is generated by scripts/mk_util.py. Search for ocamlmklib. It's in the mk_makefile method of class MLComponent:

            OCAMLMKLIB = 'ocamlmklib'

            LIBZ3 = '-cclib -l' + z3link
            if is_cygwin() and not(is_cygwin_mingw()):
                LIBZ3 = z3linkdep

            LIBZ3 = LIBZ3 + ' ' + ' '.join(map(lambda x: '-cclib ' + x, LDFLAGS.split()))

            if DEBUG_MODE and not(is_cygwin()):
                # Some ocamlmklib's don't like -g; observed on cygwin, but may be others as well.
                OCAMLMKLIB += ' -g'

            z3mls = os.path.join(self.sub_dir, 'z3ml')

            out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3linkdep))
            out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3))
            out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3linkdep, z3mls))
            out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3))
            out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
            out.write('\t%s -linkall -shared -o %s.cmxs -I . -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))

            out.write('\n')
            out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls))
            out.write('\n')

Interestingly, when I try the build locally, it fails with a different error:

flexlink: unknown option -static-libgcc

In this build, the -fopenmp flag is not included in the command line:

api/ml/z3ml.cma: api/ml/z3enums.cmo api/ml/z3native.cmo api/ml/z3.cmo  api/ml/z3native_stubs$(OBJ_EXT) libz3$(SO_EXT)
        ocamlmklib -o api/ml/z3ml -I api/ml api/ml/z3native_stubs$(OBJ_EXT) api/ml/z3enums.cmo api/ml/z3native.cmo api/ml/z3.cmo  -cclib -lz3 -cclib -static-libgcc -cclib -static-libstdc++
api/ml/z3ml.cmxa:  api/ml/z3enums.cmx api/ml/z3native.cmx api/ml/z3.cmx api/ml/z3native_stubs$(OBJ_EXT) libz3$(SO_EXT) api/ml/z3ml.cma
        ocamlmklib -o api/ml/z3ml -I api/ml api/ml/z3native_stubs$(OBJ_EXT)  api/ml/z3enums.cmx api/ml/z3native.cmx api/ml/z3.cmx -cclib -lz3 -cclib -static-libgcc -cclib -static-libstdc++
api/ml/z3ml.cmxs: api/ml/z3ml.cmxa
        ocamlfind ocamlopt -package num  -linkall -shared -o api/ml/z3ml.cmxs -I . -I api/ml api/ml/z3ml.cmxa

@btj
Copy link
Member Author

btj commented Jul 24, 2019

I confirmed that replacing -cclib -static-libgcc by -cclib -link -cclib -static-libgcc causes the subsequent ocamlopt call (which calls flexlink) to succeed.

btj added a commit that referenced this issue Jul 24, 2019
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