Fix error in configuring/building x86_32 Compcert compiler bridges

This task fixes an error in configuring/building x86_32 Comcpert compiler bridges.

See original thread at:

Linked PRs:

Merges:

Sure thing. PR submitted. I think the issue was just related to having an apt-get install without an apt-get update in the same RUN statement (this PR just merges the 2 apt-get installs into a single RUN statement). This is a Docker cacheing issue and can cause the install to fail (https://docs.docker.com/develop/develop-images/dockerfile_best-practices/).

1 Like

Thanks @Cap!

Linked PR to OP.

Would you mind rebasing the PR w.r.t current uberspark/uberspark.git:develop? There was a PR merge that changed the build docker container to use a new version of doxygen.

PR rebased, ready for review.

Hmm. Am getting error #137 with the same message as mentioned in the OP. I am using WSL + Ubuntu 16.04x LTS 64bits + Docker 19.03.2

Also, can you please remove the ls -lR command within the docker container that seems to just list the entire container directory recursively and makes generating build logs impossible due to terminal size buffers (at least on WSL).

Thanks!

I’m not sure why you are getting that error. Though the changes I pushed didn’t address it, so it makes sense that the error is persisting.

Do you have enough system resources available? After I build the container, the image is ~2.6GB (and I have another ~2+GB of cached intermediate images). Do you have enough free disk space?

My build environment is an Ubuntu 16.04x VM, with Docker 19.03.12.

Have you tried running the docker build using the -m to increase the memory available to the docker container?

Alternatively, it seems that WSL might limit the memory accessible (https://github.com/MicrosoftDocs/WSL/blob/live/WSL/release-notes.md#build-18945). As a note, my development VM has 10 GB of RAM.

It definitely is related to the container memory. Just tweaked my WSL + docker setup to increase the container RAM and it seems to be moving along…Fingers crossed…:stuck_out_tongue:

1 Like

Ok just built successfully :smiley:

@Cap. Can you make the following revisions to the PR:

  1. Revise installation documentation for next generation toolkit and mention to have at least 4GB-6GB container memory configuration. Mention as a note that you could receive bridge build errors (#137) and you might want to tweak memory to get past it.
  2. Remove the ls -lR within compiler_script.sh for all the compcert cc-bridges.

I can merge once the aforementioned are in place.

Thanks!

PR updated as requested. Glad that you got it working!

I’m getting some strange docker errors when I switched to the compcert bridge (v3.7) trying to build the x86 uxmhf uobjcoll. I just reinstalled uberspark with the pr too, not sure if this is a problem on my end.

When running uberspark uobjcoll build, I get the following error:
uberspark >> [docker] /bin/sh: 1: cd: /root/src: Permission denied

I tried a couple of things, and managed to get rid of the permission error by changing the mount directory from /root/src to /mnt/src, but now I get uberspark >> [docker] /bin/sh: 1: ccomp: not found

This might be something on my end, since I’m getting errors even when using the gcc bridge now, when I didn’t before. I’ve already tried reinstalling uberspark and restarting docker a couple of times.

Edit: gcc works

Help is appreciated.
Thanks!

Is this error with the PR linked to the OP in this topic?

Yeah. I haven’t confirmed with the pre-pr bridges.
Just tested with v3.3 and I’m getting the same errors

Seems like a container uid/gid issue. Are you using WSL? You can take a look at build-trusses/build-x86_64.Dockerfile and see how this is solved by using build-trusses/docker-entrypoint.sh script. Try to see if adapting that approach to the compcert bridge solves the problem.

but now I get uberspark >> [docker] /bin/sh: 1: ccomp: not found

This seems to imply that CompCert is not in the $PATH.

Found the problem! Not sure how you guys were able to build and install it, but I noticed that the ./compiler_script.sh had these lines:

./configure x86_32-linux
make -j4 all
exit
make install

It ran exit before make install so compcert was never actually installed…
Removing the exit line fixed the issue. I’m getting some preprocessor errors that I’ll try to debug but ccomp works.

Still unsure about the /root/src permissions though. Changing it to /mnt/src works well enough, is there a reason why we use /root?

@yeeb,

Thanks! I removed the exit from compiler_script.sh and updated the PR to have this removed in all version of the compcert bridge.

I’m not sure about your permissions issues and the directory.
@amitvasudevan, any insights?

1 Like

Thanks @Cap and @yeeb,

Still unsure about the /root/src permissions though. Changing it to /mnt/src works well enough, is there a reason why we use /root ?

Nope, we can use /mnt/src but that has to be reflected within the tool-chain which currently uses /root/src.

However, am not sure how gccworks with /root/src while compcert does not. Is the compcert container switching to a different user other than root?

Sorry, didn’t specify. I modified the frontend toolchain to use /mnt/src. gcc only worked after the modification (i was getting the same permission error).

However, am not sure how gcc works with /root/src while compcert does not. Is the compcert container switching to a different user other than root?

The CompCert bridge changes the user to ubuntu

Wierd. What development environment are you using?