fix: misc build improvements, removal of opam env from build

[difcsi]

As discussed, we don't need to maintain our opam environment, we trust the builder to be competent enough to do that.

We also don't install any artifact we produce. We still need opam to install build dependencies for us. Theoretically, that could also be left to the user, but the dependencies are listed by cil, which might change, so we attempt to install them / ensure they exist.

Overhead should be very little for subsequent builds.

This PR also removes old Dockerfiles that weren't maintained, opting to provide a single Dockerfile to anyone interested.

A devcontainer config is also bundled, enabling IDEs to automatically pick up on our suggested development environment. It is a tiny wrapper around the dockerfile.

At present, we only have build-dependencies.txt and test-dependencies.txt.

As this is distribution specific, these should technically be scoped (ubuntu26.04-build-dependencies.txt and friends), but as other distros were unmaintained anyways, I think the names are okay for now. In the future, we hope to be more flexible with support

[difcsi]

This CI failure exposes a latent instance of #149.

Presently, the test runner relies on the build configure-time hardcoded paths to find tools for testing, instead of liballocs correctly making itself available through the system. I'd argue that the test runner should represent a 'post-install' state, where liballocs tools are reachable from the env path. 'cilly' should resolve, though I'll push a fix that uses the full path as with other tools for now.

In an ideal scenario, the test runner would only have runtime dependencies available. This is blocked by make install not working correctly, and also because #178: lib-test relies on rebuilding liballocs, thus it needs some build-time dependencies: presently, this is solved by over-equipping the test runner. This defeats the point of having the two separate CI stages: why waste time persisting a workspace when we could run tests within the build job?

(I have a fix for #149 somewhere on my fork, part of the Debian package build system. I'll bring that up-to-date one day: now we can actually run with commonly-bundled compiler versions: fairly modern gcc and clang with dwarf4. )

I suppose the right path here is to patch the makefile so Cilly's absolute path is used within the tests; that much is clear. But I don't see the point of maintaining two jobs (build -> test) if both need the same environment (persisted build artefacts and build-time dependencies). We could just merge them into one build&test, save some CI time and the complexity of having two dependency lists.

@stephenrkell, what do you think?

[difcsi]

@stephenrkell we should either set the CIL branch to goblint-develop+srk within the .gitmodules here, or you can set that as the default branch on your fork for @dependabot to pick up the CIL updates

[stephenrkell]

I am fine with moving the lib-test step into the build job.

For the other tests, we should always test with the cilly that we were configured with.

I am confused about the current state of this PR regarding opam. The patch currently removes opam things in some places but adds them in others.

[difcsi]

Sorry, I edited the name of the PR, my bad.

Opam can maintain OCaml versions and packages separately, much like a Python virtual environment. We don't do that anymore.

But we still need opam, as goblint-cil has OCaml packages as build dependencies that we need to install somehow. With disabled sandboxing (as is here), this amounts to a system-wide install.

Alternatively, we could use apt, by installing packages such as libzarith-ocaml-dev. Ubuntu repositories seem to have the necessary packages. But leaving it to opam makes our build resilient to upstream dependency changes.

Happy to switch to a fully apt-based building.

Also, the Dockerfile still has a sandboxed opam, which is genuinely something I missed

[stephenrkell]

Thanks for explaining!

I definitely favour maximising the use of apt and minimising use of opam (ideally to zero, or else to the smallest degree feasible). The fewer distinct sources of "stuff from the Internet" that we have in the build, the better for reliability, transparency, supply chain integrity, etc... and also a general preference for fewer distinct tools involved in the build.

[difcsi]

I definitely favour maximising the use of apt and minimising use of opam (ideally to zero, or else to the smallest degree feasible). The fewer distinct sources of "stuff from the Internet" that we have in the build, the better for reliability, transparency, supply chain integrity, etc... and also a general preference for fewer distinct tools involved in the build.

Unfortunately, it seems not everything is available from apt on ubuntu. I'll push a patch that moves all we can to apt

[difcsi]

@stephenrkell stripped out opam as requested, this one is ready to merge