Error in configuring/building x86_32 Compcert compiler bridges

I am trying to build/configure the Compcert compiler bridge for x86_32 via the following command:

uberspark bridge config --cc-bridge --build amd64/x86_32/generic/compcert/v3.1

However, the above command produces the following error during the bridge build/configuration process.

uberspark >> [docker] COQC cfrontend/Csharpminor.v
uberspark >> [docker] COQC common/Determinism.v
uberspark >> [docker] COQC cfrontend/Ctyping.v
uberspark >> [docker] Makefile:202: recipe for target 'cparser/Parser.vo' failed
uberspark >> [docker] Killed
uberspark >> [docker] make[1]: *** [cparser/Parser.vo] Error 137
uberspark >> [docker] make[1]: *** Waiting for unfinished jobs....
uberspark >> [docker] make[1]: Leaving directory '/tmp/CompCert-3.1'
uberspark >> [docker] Makefile:136: recipe for target 'all' failed
uberspark >> [docker] make: *** [all] Error 2
uberspark >> [docker] The command '/bin/sh -c . ./compiler_script.sh' returned a non-zero code: 2
uberspark >> ERROR: could not build cc-bridge!

uberspark: could not build cc-bridge!

I tried with Compcert v3.1, v3.2and v3.7 and all of them halt at the error above. I have not tried the other versions yet.

Anyone else experiencing this issue?

Hello, Amit. It appears the primary failure message is the one from the Coq compiler, “Makefile:202: recipe for target ‘cparser/Parser.vo’ failed”, which of course makes compiler_script.sh fail. Did you run these when the pull request was accepted or did Cap? Just a real quick guess, maybe one of the build dependencies is not downloading correctly? I had initially placed all build deps in the repository with the scripts, but was asked to remove those. If any of the downloads are failing from the build environment, it would have downstream effects, such as these. Coq, in particular, has a lot of dependencies. Do you have the full build logs?

Hey David,

Good to hear from you!

Did you run these when the pull request was accepted or did Cap?

I am not sure if we/who tested this on the pull request.

I had initially placed all build deps in the repository with the scripts, but was asked to remove those.

I remember we had to remove some README but was not sure about the build deps. Does the build deps get sourced during the container build?

Just a real quick guess, maybe one of the build dependencies is not downloading correctly?

I did not see any download errors, but will double check.

Do you have the full build logs?

Generating one for you right now. It takes a while to build the entire container, so will post back on this thread when its done :slight_smile:

Thanks!

Build log attached for cc bridge build for Compcert v3.1

I did not see any immediate errors within the log except for the Compcert build error as reported before. One thing I did notice was it installed Coq v8.6 which I am not sure is compatible with Compcert v3.1

cc-bridge-compcert-buildlog.txt (141.1 KB)

[docker] make[1]: *** [cparser/Parser.vo] Error 137

I believe that an Error 137 == Out of Memory Error.

Hah. Really? So the Compcert v3.1 cc-bridge builds successfully on your side?

@amitvasudevan,
Yes, I can successfully build. It did require a slight tweak to the Dockerfile. I needed to add another apt-get update at line 25 for the following apt-get install items.

Hmm…can you submit a PR for this fix? Also, does this mean that in the future such apt updates might be needed or could break the dependencies?

24 posts were merged into an existing topic: Fix error in configuring/building x86_32 Compcert compiler bridges