diff --git a/INSTALL.md b/INSTALL.md index faeefdf67662b2f90fabe927ba476dd588b69bca..d9d7b24ec340bd1746b2f1a9b9a17114e6126f7b 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -34,15 +34,12 @@ First you need to install opam, then you may install Frama-C using opam. Several Linux distributions already include an `opam` package. -**Note:** make sure your opam version is >= 2.0.0. - macOS has opam through Homebrew. Windows users can install opam via WSL (Windows Subsystem for Linux). -If your system does not have an opam package >= 2.0.0, you can -[compile it from source](#compiling-from-source), -or use the provided opam binaries available at: +If your system does not have an opam package >= 2, you can use the provided +opam binaries available at: http://opam.ocaml.org/doc/Install.html @@ -62,15 +59,16 @@ its `depext` plug-in: issuing the two commands will install the appropriate system packages (this of course requires administrator rights on the system). -If your system is not supported by `depext`, you will need to install -Gtk, GtkSourceView, GnomeCanvas and GMP, including development libraries, -separately. If you do so, please consider providing the system name and list of -packages (e.g. via a [Gitlab issue](https://git.frama-c.com/pub/frama-c/issues/new)) -so that we can add it to the Frama-C `depext` package. +If your system is not supported by `depext`, you can simply try: - # install Frama-C opam install frama-c +If there are errors due to missing external dependencies, opam may emit a +message indicating which packages to install. If this is not sufficient, +there may be missing dependencies in opam's `depext` tool. In this case, +you may [create a Gitlab issue](https://git.frama-c.com/pub/frama-c/issues/new) +indicating your distribution and error message. + ### Configuring provers for Frama-C/WP Frama-C/WP uses the [Why3](http://why3.lri.fr/) platform to run external provers @@ -86,13 +84,13 @@ Most provers are available on all platforms. After their installation, Why3 must be configured to make them available for Frama-C/WP: ```shell -why3 config --detect +why3 config detect ``` ### Reference configuration See file [reference-configuration.md](reference-configuration.md) -for a set of packages that is known to work with Frama-C 22 (Titanium). +for a set of packages that is known to work with Frama-C 23 (Vanadium). ### Installing Custom Versions of Frama-C diff --git a/README.md b/README.md index afae47f12d44ad2c2cefc5b26cfe7f5034592ec3..4a1fe8a9a018f880768f07f52f5aee199367bac5 100644 --- a/README.md +++ b/README.md @@ -28,23 +28,36 @@ properties. Plug-ins can also collaborate via their APIs. ## Installation -For more detailed information about installing opam/Frama-C, -see [INSTALL.md](INSTALL.md). - Frama-C is available through [opam](http://opam.ocaml.org/), the -OCaml package manager. This is the preferred installation method. Be sure -to install opam v2.0 or higher. Then the following sequence of commands -should install frama-c and its gui: +OCaml package manager. If you have it, simply run: - opam init - opam install depext - opam depext frama-c - opam install frama-c + opam install depext # handles external (non-OCaml) dependencies + opam depext frama-c --install Frama-C is developed mainly in Linux, often tested in macOS (via Homebrew), and occasionally tested on Windows (via the Windows Subsystem for Linux). +For detailed installation instructions and troubleshooting, +see [INSTALL.md](INSTALL.md). + +### Development branch + +To install the development branch of Frama-C (updated nightly): + + opam pin add frama-c https://git.frama-c.com/frama-c#master + +This command will *pin* the development version of Frama-C and try to install it. +If installation fails due to missing external dependencies, try using +the same commands from the [Installation](#installation) section to get the +external dependencies and then install Frama-C. + +### Distribution packages + +Some Linux distributions have a `frama-c` package, kindly provided by +distribution packagers. Note that they may not correspond to the latest +Frama-C release. + ## Usage Frama-C can be run from the command-line, or via its graphical interface. diff --git a/bin/check-reference-configuration.sh b/bin/check-reference-configuration.sh index 1c718e5ce4badcea43a6177eb253d446b85950f9..6557c2eca7defd285aebdb24afa512ccad39385e 100755 --- a/bin/check-reference-configuration.sh +++ b/bin/check-reference-configuration.sh @@ -65,5 +65,5 @@ if [ $has_any_diffs -ne 0 ]; then echo " opam switch create ${working_ocaml}" echo " opam install depext" echo " opam depext --install$all_packages" - echo " rm -f ~/.why3.conf && why3 config --detect" + echo " rm -f ~/.why3.conf && why3 config detect" fi