search

Stevendeo / Pilat

Invariant generator for polynomial loops
GNU Lesser General Public License v2.1
8 stars 2 forks source link

Extended installation instructions #8

Closed Sorata8428 closed 5 months ago

Sorata8428 commented 2 years ago

While installing pilat onto a wsl Ubuntu 20.04 image, I have encountered some issues that could be avoided by giving inexperienced users more thorough instructions for the installation.

  1. When someone has already initialized opam according to the official frama-c installtion guide, the ocaml version will not be set to 4.04.1 but to a more recent version, 4.08.1 in my case. When someone tries to install pilat in this configuration, opam will install pilat 1.2. Trying to run frama-c now leads to the error:

    [kernel] User Error: cannot load plug-in 'frama-c-pilat': cannot load module
  Details: The module `Lacaml__Common' is already loaded (either by the main program or a previously-dynlinked library) 
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.      
[kernel] Frama-C aborted: invalid user input.

    In this case, the user can first install ocaml 4.04.1 onto a new switch using switch create NAME_OF_SWITCH 4.04.1 where they may properly install pilat using opam depext --install -y pilat.

  2. If the user is working within a virtual environment built on wsl, such as wsl itself or docker for windows, installing pilat from scratch using the instructions results in an error, since wsl does not support sandboxing and therefore opam cannot create a switch. To correctly install and initialize opam, the user can combine the pilat and frama-c instructions:

    sudo apt install make m4 gcc opam
opam init --disable-sandboxing --shell-setup --comp 4.04.1

    This once again yields an environment where pilat can be installed with opam depext --install -y pilat.

I have verified that the two processes I have described work on Ubuntu 20.04 on wsl and docker for windows. While the second point is a wsl specific problem, the first one should apply to linux users as well, but I have not tested this specifically. I think extending the installation instructions with this information should be helpful to users, especially those with little expierience using opam or linux in general.

Stevendeo commented 2 years ago

  1. I am updating the pilat opam package for compatibility with the latest version of frama-c. It should be compatible with the ocaml.4.12.0 as well, so unless you are forced to use ocaml.4.04.1 (which is incompatible with frama-c.22.0 and does not enter the scope of this new version of Pilat) it should be easier. I am not sure why opam wants you to install pilat.1.2 as the version 1.3 is compatible with the constraints you gave (ocaml >= 4.08.1). What version of frama-c do you use ?

  2. I will only answer about the Ubuntu installation procedure, I do not indent to maintain nor check compatibility for windows. This issue is not specifically linked to pilat in particular but to opam's functionning. I could describe in the INSTALL file the details on how to properly install opam, but the pilat repository is not the place to do so. Maybe the best way would be to use a docker image with opam already installed.