Merge branch '1171-install-dune' into 'master'

Removed obsolete installation commands in INSTALL.md

Closes #1171

See merge request frama-c/frama-c!3929

INSTALL.md

@@ -320,13 +320,13 @@ Arch Linux: `pikaur -S frama-c`
 
 2. On Linux-like distributions:
 
-        ./configure && make && sudo make install
+        ./make RELEASE=yes && make install
 
     See section *Configuration* below for options.
 
 3. On Windows+Cygwin:
 
-        ./configure --prefix="$(cygpath -a -m <installation path>)" && make && make install
+        ./make RELEASE=yes && make install
 
 4. The binary `frama-c` (and `frama-c-gui` if you have lablgtk2) is now installed.
 
@@ -338,51 +338,66 @@ See the `opam` file, section `depends`, for compatible OCaml versions and
 required dependencies (except for those related to `lablgtk`, which are
 required for the GUI but otherwise optional).
 
-Section `depopts` lists optional dependencies.
+To install the required dependencies, you can use opam v2.1
+or higher to do the following (assuming you are in frama-c
+root source folder):
 
-#### Configuration
+1. `opam switch create frama-c ocaml-base-compiler.4.13.1`
+   to create a compatible opam switch
+1. `opam pin . -n` to pin to the latest development version
+1. `opam install --deps-only` will fetch and build all
+   relevant dependencies
 
-Frama-C is configured by `./configure [options]`.
-
-`configure` is generated by `autoconf`, so that the standard options for setting
-installation directories are available, in particular `--prefix=/path`.
-
-A plugin can be enabled by `--enable-plugin` and disabled by `--disable-plugin`.
-By default, all distributed plugins are enabled, unless some optional
-dependencies are not met.
-
-See `./configure --help` for the current list of plugins, and available options.
-
-##### Under Cygwin
+#### Compilation
 
-Use `./configure --prefix="$(cygpath -a -m <installation path>)"`.
+There are basically two compilation modes: development and release.
 
-(using Unix-style paths without the drive letter will probably not work)
+Typing `make` builds in development mode, this is a shortcut for:
+```
+dune build @install
+```
 
+Typing `make RELEASE=yes` builds in release mode, this is a shortcut for:
+```
+dune build @install --release --promote-install-files=false
+```
 
-#### Compilation
+For more precise build configuration, use directly the `dune` command.
 
-Type `make` (you can use `-j` for parallelization).
+#### Testing
 
-Some Makefile targets of interest are:
-- `doc`      generates the API documentation.
-- `oracles`  sets up the Frama-C test suite oracles for your own configuration.
-- `tests`    performs Frama-C's own tests.
+Basic tests can be executed using:
 
+```
+make run-ptests
+make default-tests
+```
 
 #### Installation
 
-Type `make install`
-(depending on the installation directory, this may require superuser
-privileges. The installation directory is chosen through `--prefix`).
+Type `make install` (depending on the installation directory, this may require
+superuser privileges. The installation directory is chosen through the variable
+`PREFIX`). This is a shortcut for:
 
+```
+dune install
+```
 
 #### API Documentation
 
 For plugin developers, the API documentation of the Frama-C kernel and
-distributed plugins is available in the file `frama-c-api.tar.gz`, after running
-`make doc-distrib`.
+distributed plugins is available in the `_build/default/_doc/_html` directory
+after running:
+
+```
+make doc
+```
 
+or:
+
+```
+dune build @doc
+```
 
 #### Uninstallation
 
@@ -422,9 +437,9 @@ available:
 - `frama-c`
 - `frama-c-gui`       if available
 - `frama-c-config`    lightweight wrapper used to display configuration paths
-- `frama-c.byte`      bytecode version of frama-c
-- `frama-c-gui.byte`  bytecode version of frama-c-gui, if available
-- `ptests.opt`        testing tool for Frama-c
+- `frama-c-hdrck`     header checking tool for Frama-C
+- `frama-c-ptests`    testing tool for Frama-c
+- `frama-c-wtests`    testing tool for Frama-c
 - `frama-c-script`    utilities related to analysis parametrization
 
 ## Shared files: (in `/INSTALL_DIR/share/frama-c` and subdirectories)
@@ -438,10 +453,6 @@ available:
 - an annotated C standard library (with ACSL annotations) in `libc`
 - plugin-specific files (in directories `wp`, `e-acsl`, etc.)
 
-## Documentation files: (in `/INSTALL_DIR/share/frama-c/doc`)
-
-- files used to generate dynamic plugin documentation
-
 ## Object files: (in `/INSTALL_DIR/lib/frama-c`)
 
 - object files used to compile dynamic plugins
@@ -461,7 +472,7 @@ Plugins may be released independently of Frama-C.
 
 The standard way for installing them should be:
 
-    ./configure && make && make install
+    dune build @install && dune install
 
 Plugins may have their own custom installation procedures.
 Consult their specific documentation for details.

share/Makefile.common

@@ -34,7 +34,7 @@ DUNE_BUILD_OPTS?=
 
 RELEASE?=no
 ifeq ($(RELEASE),yes)
-DUNE_BUILD_OPTS+=--release
+DUNE_BUILD_OPTS+=--release --promote-install-files=false
 endif
 
 # DUNE_DISPLAY: chose Dune build verbosity (see '--display' dune option)