aegis-iisc / catalyst_ocaml

Ocaml version of the Relational Refinement Type
Other
1 stars 0 forks source link

Trouble building on newer glibc #1

Open david-christiansen opened 4 years ago

david-christiansen commented 4 years ago

It seems that the transitive dependencies of the build process are incompatible with newer glibc versions (including on the latest Fedora).

Here's a Dockerfile that works for me, in the parent directory of a checkout:

FROM ubuntu:16.04

RUN apt-get update && apt-get -y install libgmp-dev python m4 curl build-essential git zip unzip rsync z3 libz3-dev

RUN curl -sL -O https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh

RUN echo "" | sh install.sh

RUN opam init --disable-sandboxing

RUN eval $(opam env)

RUN opam switch create 4.03.0

RUN opam update

RUN opam pin -y add menhir 20180905

RUN opam install -y core

RUN opam pin -y add z3 4.7.1

RUN mkdir -p ~/tmp

RUN sed s/linkopts\ =\ /linkopts\(native\)\ =\ /g < ~/.opam/4.03.0/lib/z3/META > ~/tmp/META

RUN echo "linkopts(byte) = \"-custom -cclib -lz3\"" >> ~/tmp/META

RUN cp ~/tmp/META ~/.opam/4.03.0/lib/z3/META

COPY catalyst_ocaml catalyst_ocaml

WORKDIR catalyst_ocaml

RUN eval $(opam env) && ocamlbuild -use-menhir -tag thread -use-ocamlfind -pkg core -pkg z3 -Is typing,parsing,utils,speclang,specparser,specelab,specverify,vcencode,driver main/ocatalyst.byte

RUN eval $(opam env) && ocamlbuild -use-menhir -tag thread -use-ocamlfind -pkg core -pkg z3 -Is typing,parsing,utils,speclang,specparser,specelab,specverify,vcencode,driver main/ocatalyst.native

ENTRYPOINT LD_LIBRARY_PATH=~/.opam/4.03.0/lib/z3 bash

Here's one that exhibits the issue:

FROM debian:buster

RUN apt-get update && apt-get -y install opam libgmp-dev m4

RUN opam init --disable-sandboxing

RUN eval $(opam env)

RUN opam switch create 4.03.0

RUN opam update

RUN opam pin -y add menhir 20180905

RUN opam install -y core

RUN opam pin -y add z3 4.7.1

RUN mkdir -p ~/tmp

RUN sed s/linkopts\ =\ /linkopts\(native\)\ =\ /g < ~/.opam/4.03.0/lib/z3/META > ~/tmp/META

RUN echo "linkopts(byte) = \"-custom -cclib -lz3\"" >> ~/tmp/META

RUN cp ~/tmp/META ~/.opam/4.03.0/lib/z3/META

COPY catalyst_ocaml catalyst_ocaml

WORKDIR catalyst_ocaml

RUN eval $(opam env) && ocamlbuild -use-menhir -tag thread -use-ocamlfind -pkg core -pkg z3 -Is typing,parsing,utils,speclang,specparser,specelab,specverify,vcencode,driver main/ocatalyst.byte

Concretely, I get this message:

/home/dtc/.opam/4.03.0/.opam-switch/build/core.v0.9.1/_build/default/src/unix_stubs.c:558: undefined reference to `makedev'

(this was generated outside of Docker for reasons of time, but I believe that the Docker script that I posted reproduces this - it's running right now and I'll report back)

david-christiansen commented 4 years ago

Update: it does indeed fail in the expected way.

david-christiansen commented 4 years ago

This problem still occurs after pulling the latest version. What can be done?

david-christiansen commented 4 years ago

It looks like updating a dependency will help: https://github.com/janestreet/core/pull/114