The build does not work on Ubuntu LInux 19.10

I followed the documentation and found that CompCert and Frama-C do not build as prescribed in the build instructions.
After coq was installed successfully it can’t be found. There seem to be problems with menhir also:

cd ~/CompCert-3.1
./configure x86_32-linux
Testing assembler support for CFI directives… yes
Testing linker support for ‘-no-pie’ option… yes
Testing Coq… NOT FOUND
Error: make sure Coq version 8.6 is installed.
Testing OCaml… version 4.05.0 – good!
Testing OCaml .opt compilers… yes
Testing Menhir… NOT FOUND
Error: make sure Menhir version 20161201 or later is installed.
Testing GNU make… version 4.2.1 (command ‘make’) – good!
One or several required tools are missing or too old. Aborting.

I know that the documentation suggests to have Linux 16.04, but at this point when Linux 20.04 is to be released 16.04 is fairly old.

I was having this problem. I think that if you run: eval `opam config env` These errors will go away.

This helped, but I had to reinstall menhir again, because some of the steps downgrade it.
I wonder if the order of installation of opam packages is correct.
We need to update the documentation and add this step at least:
‘opam config env’

@Anton, I am guessing you are trying to install the current generation toolkit.

I know that the documentation suggests to have Linux 16.04, but at this point when Linux 20.04 is to be released 16.04 is fairly old.

16.04 LTS EOL is April 2021, so we have a little time before we need to migrate.

We need to update the documentation and add this step at least:
‘opam config env’

This has already been done. Please see task:

Also, please do note that the current generation toolkit will be deprecated soon in favor of the next generation toolkit which leverages coss bridges and docker containers to conceal such dependencies elegantly.

We should ideally be using and refining the next generation toolkit moving forward. However, what @Cap and you have discovered so far with frama-c and compcert could definitely be bought in as verification and coss compiler “bridges” within the new framework.

Please let me know if you are interested in creating these bridges (essentially docker containers with überSpark manifest descriptions) for the “next generation toolkit” and I can add relevant tasks for us to take the discussion there.

Thanks!