Feature: Preliminary Docker-ization test of the tool-chain/build process

Description:

Referencing this discussion thread:
https://forums.uberspark.org/t/error-on-build-ubersparklibs/29/29

it appears that docker-izing the tool-chain/build process will make it easier in terms of resolving various tool dependencies and allow easy use of the base tool-chain

Assigned to:
@jrs322

So far I have a working base image that meets our need with ocaml and opam installed. The problem I was running into involved the make process for Coq.8.6.1 but has since been resolved.
Currently I am stuck on automating the process for installing the correct versions of Frama-c and Compcert as both ./configure scripts are unable to locate ocamlc, but inside the container work well.

The current DockerFile is here : Dockerfile (470 Bytes)

I am a little confused. So Frama-C and Compcert are working within the container?

They are working when manually built inside the container. At the moment the Dockerfile itself has issues running the configure scripts for both packages. When using Docker run and the cmd line both Frama-C and Compcert can be built. It is very confusing, both ./configure scripts say they cannot find ocamlc when run in the Dockerfile, but are able to find it when inside the container.

Can we just persist the changes to the container somehow, so we have to install it just once?

Are you switching to the correct version within opam and initializing the environment prior to running the ./configure scripts?

opam switch 4.02.3
eval `opam config env`

Yes I am, but it seems that the ./configure scripts are run either by a different user or something else, as switching and evaluating the env does not effect the ./configure scripts.

Can you try using the CMD directive to execute the configure scripts instead of the RUN directive within your dockerfile?

Yeah I can try that, current version is tested to work manually building compcert + frama-c

Sounds good. Please fork off of latest develop and submit a pull request when you are ready. Thanks!

Pull request submitted for dockerfile without CMD calls. Will work on those today.

Referencing: https://github.com/hypcode/uberspark/pull/3
The Dockerfile should be within the src/ folder; can you make this change? We can tweak the Makefile later for build/installation.

You should be able to continue your commits to jrs322:feature_add_dockerfile and we can merge once you test the CMD calls as well.

Thanks!

So only one CMD call can be issued in a Dockerfile and is used to open a cmd terminal at the time. At this point I think writing a bash script to perform the configurations and makes, adding it to the container at build time, and then running the script once inside the container is one solution I have.

Do you know how much slower this is compared to a static build-time setup?

Another option might be to run the ./configure command using RUN but with the exec form as opposed to the shell form. The following link gives you an example: https://goinbigdata.com/docker-run-vs-cmd-vs-entrypoint/

I suspect running the ./configure via a shell might be causing some environment issues…

The post below describes a similar issue confirming that every RUN command seems to have a different context when executed using shell form:

Oh, that makes alot of sense, I can try to submit a change this week.

@jrs322: Let me know when you have this ready; you will likely need to rebase your pull request off latest develop branch, following the recent release. Thanks!

Hey Amit, I’ve been working on this for a bit without much progress. The solution here doesnt seem to apply to the issues with opam and ./configure

Can we try the above route for the time being and see how fast/slow the container spins up? Thanks!