RHEL8 Install

[lwli11]

Please feel free to ignore this if CN is not intended to support RHEL.

Installing on CN works according to: https://github.com/rems-project/cerberus/blob/master/backend/cn/INSTALL.md until 'make install'.

$ make install
[DUNE] cerberus
[DUNE] install cerberus
Error: The mandir installation directory is unknown.
Hint: It can be specified with '--prefix' or by setting '--mandir'
make: *** [Makefile:294: install] Error 1

[podhrmic]

Would running CN in a docker container work for you? See https://github.com/rems-project/cerberus?tab=readme-ov-file#docker-image

[lwli11]

It should! To confirm, which of deps/release/dev-env should I pick?

$ make -f Makefile_docker
targets: deps|release|dev-env

Thanks!

[podhrmic]

We have been using the release image:

make -f Makefile_docker release

[lwli11]

Thanks! I seem to run into an issue. Have you seen this before?:
STEP 12/13: RUN eval opam env && make install && make install_cn
WARN[0012] Failed to mount subscriptions, skipping entry in /usr/share/containers/mounts.conf: getting host subscription data: failed to read subscriptions from "/usr/share/rhel/secrets": open /usr/share/rhel/secrets/rhsm/rhsm.conf: permission denied
[WARNING] Running as root is not recommended
[DUNE] cerberus
Warning: one state has shift/reduce conflicts.
Warning: one state has reduce/reduce conflicts.
Warning: one shift/reduce conflict was arbitrarily resolved.
Warning: 4 reduce/reduce conflicts were arbitrarily resolved.
Warning: one state has shift/reduce conflicts.
Warning: one state has reduce/reduce conflicts.
Warning: one shift/reduce conflict was arbitrarily resolved.
Warning: 4 reduce/reduce conflicts were arbitrarily resolved.
Read 1186 sample input sentences and 1186 error messages.
Read 1186 sample input sentences and 1186 error messages.
Warning: one state has shift/reduce conflicts.
Warning: one state has reduce/reduce conflicts.
Warning: one shift/reduce conflict was arbitrarily resolved.
Warning: 4 reduce/reduce conflicts were arbitrarily resolved.
Read 1186 sample input sentences and 1186 error messages.
Warning: one state has shift/reduce conflicts.
Warning: one state has reduce/reduce conflicts.
Warning: one shift/reduce conflict was arbitrarily resolved.
Warning: 3 reduce/reduce conflicts were arbitrarily resolved.
Warning: one state has shift/reduce conflicts.
Warning: one state has reduce/reduce conflicts.
Warning: one shift/reduce conflict was arbitrarily resolved.
Warning: 4 reduce/reduce conflicts were arbitrarily resolved.
(debug 0): constructValue_aux: is WRONG for union ==> always assigning the first member
[DUNE] install cerberus
[DUNE] cn
File "backend/cn/report.ml", line 689, characters 10-30:
689 | Some (In_channel.input_all ic)
^^^^^^^^^^^^^^^^^^^^
Error: Unbound module In_channel
make: *** [Makefile:79: cn] Error 1
Error: building at STEP "RUN eval opam env && make install && make install_cn": while running runtime: exit status 2

[cp526]

I suspect this is due to too old an OCaml version. Which version of OCaml do you have?
We depend on an OCaml version of at least 4.14.0 (This information was previously missing in CN's build machinery, I just added that.)

[lwli11]

Thanks, the docker image now builds.

I also see the image:
docker image ls
Emulate Docker CLI using podman. Create /etc/containers/nodocker to quiet msg.
REPOSITORY TAG IMAGE ID CREATED SIZE
localhost/cerberus release 635ba847a591 19 minutes ago 2.96 GB

However, when I run the docker run command:
docker run --volume PWD:/data/ cerberus:0.1 tests/tcc/00_assignment.c --pp=core
bash: PWD: command not found...
Similar command is: 'pwd'
Emulate Docker CLI using podman. Create /etc/containers/nodocker to quiet msg.
? Please select an image:
▸ registry.access.redhat.com/cerberus:0.1
registry.redhat.io/cerberus:0.1
docker.io/library/cerberus:0.1

Or when I replace 'PWD' with 'pwd':
docker run --volume pwd:/data/ cerberus:0.1 tests/tcc/00_assignment.c --pp=core
Emulate Docker CLI using podman. Create /etc/containers/nodocker to quiet msg.
? Please select an image:
▸ registry.access.redhat.com/cerberus:0.1
registry.redhat.io/cerberus:0.1
docker.io/library/cerberus:0.1

[podhrmic]

@cp526 maybe this issue could be a gentle nudge to add the missing token to rems-project/cerberus#323 and actually publish the docker image so it doesn't need to be built locally?

We have our cerberus image published in the VERSE registry, but sadly I cannot make it public yet...

[lwli11]

I think I've found the command that works!

docker run --volume pwd:/data -it cn /data/tests/tcc/00_assignment.c
Emulate Docker CLI using podman. Create /etc/containers/nodocker to quiet msg.
WARN[0000] Failed to mount subscriptions, skipping entry in /usr/share/containers/mounts.conf: getting host subscription data: failed to read subscriptions from "/usr/share/rhel/secrets": open /usr/share/rhel/secrets/rhsm/rhsm.conf: permission denied
[WARNING] Running as root is not recommended
/root/.opam/default/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
^~~~~~~

[septract]

The docker container is now built in CI. Could we close this issue @lwli11 ?