diff --git a/INSTALL.md b/INSTALL.md index 281258aac8f3cf08ad6b696376928a33ca5c7efc..260097eb65bc937c250882e90d0e9aba46c38277 100644 --- a/INSTALL.md +++ b/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. diff --git a/share/Makefile.common b/share/Makefile.common index b3c6d6eb692e91d0cb53cf9bd87f3b06d05a4019..8754621da7b77f997fcd326615908992472087f9 100644 --- a/share/Makefile.common +++ b/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)