Merge branch 'feature/build/dune-configurator' into 'master'

Improves build and install process

Closes #1149

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

.force-reconfigure

-2

.gitlab-ci.yml

@@ -185,7 +185,7 @@ build-distrib-tarball:
     CI_LINK: "yes"
     HDRCK: "frama-c-hdrck"
   script:
-    - ./nix/shell-checkers.sh "autoconf && ./dev/make-distrib.sh"
+    - ./nix/shell-checkers.sh "./dev/make-distrib.sh"
   artifacts:
     paths:
       - ./*.tar.gz
@@ -279,6 +279,7 @@ ocaml-versions-nightly:
   stage: compatibility
   image: 'ocaml/opam:ubuntu-20.04-ocaml-$OCAML'
   script:
+    - sudo apt update
     - opam pin . -n
     - opam depext frama-c --with-test
     - opam install --jobs 2 frama-c --with-test
@@ -295,7 +296,6 @@ opam-pin-nightly:
   <<: *opam_template
   only:
     - schedules
-  allow_failure: true
 
 # TODO: Enable this rule later:
 #

Makefile

@@ -26,6 +26,10 @@ MAKECONFIG_DIR=share
 
 include share/Makefile.common
 
+##############################################################################
+# DUNE OPTIONS
+################################
+
 DUNE_BUILD_OPTS?=
 
 RELEASE?=no
@@ -39,95 +43,53 @@ endif
 DUNE_DISPLAY?=progress
 DUNE_BUILD_OPTS+=--display $(DUNE_DISPLAY)
 
+##############################################################################
 # PTESTS SRC
+################################
+
 FRAMAC_PTESTS_SRC:=tools/ptests
 
+##############################################################################
 # HDRCK SRC
-FRAMAC_HDRCK_SRC:=tools/hdrck
+################################
 
-###################
-# Frama-C Version #
-###################
+FRAMAC_HDRCK_SRC:=tools/hdrck
 
-VERSION:=$(shell $(CAT) VERSION)
-VERSION_CODENAME:=$(shell $(CAT) VERSION_CODENAME)
+##############################################################################
+# Frama-C
+################################
 
 .PHONY: all
 
-all: config.sed
+all:
+ifneq ($(DISABLED_PLUGINS),)
+	dune clean
+	rm -rf _build .merlin
+	./dev/disable-plugins.sh ${DISABLED_PLUGINS}
+endif
 	dune build $(DUNE_BUILD_OPTS) @install
 
-MAJOR_VERSION=$(shell $(SED) -E 's/^([0-9]+)\..*/\1/' VERSION)
-MINOR_VERSION=$(shell $(SED) -E 's/^[0-9]+\.([0-9]+).*/\1/' VERSION)
-VERSION_CODENAME=$(shell $(CAT) VERSION_CODENAME)
-
-# File used by dune to build src/kernel_internals/runtime/fc_config.ml
-config.sed: VERSION share/Makefile.config share/Makefile.common Makefile configure.ac
-	@echo "# generated file" > $@
-	@echo "s|@VERSION@|$(VERSION)|" >> $@
-	@echo "s|@VERSION_CODENAME@|$(VERSION_CODENAME)|" >> $@
-	@echo "s|@MAJOR_VERSION@|$(MAJOR_VERSION)|g" >> $@
-	@echo "s|@MINOR_VERSION@|$(MINOR_VERSION)|g" >> $@
-	@echo "s|@FRAMAC_DEFAULT_CPP@|$(FRAMAC_DEFAULT_CPP)|" >> $@
-	@echo "s|@FRAMAC_DEFAULT_CPP_ARGS@|$(FRAMAC_DEFAULT_CPP_ARGS)|" >> $@
-	@echo "s|@FRAMAC_GNU_CPP@|$(FRAMAC_GNU_CPP)|" >> $@
-	@echo "s|@DEFAULT_CPP_KEEP_COMMENTS@|$(DEFAULT_CPP_KEEP_COMMENTS)|" >> $@
-	@echo "s|@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@|$(DEFAULT_CPP_SUPPORTED_ARCH_OPTS)|" >> $@
-
 clean:: purge-tests # to be done before a "dune" command
 	dune clean
 	dune clean --root $(FRAMAC_PTESTS_SRC)
 	dune clean --root $(FRAMAC_HDRCK_SRC)
-	rm -rf _build .merlin config.sed autom4te.cache
-
-########################################################################
-# Makefile.config is rebuilt whenever configure.ac is modified         #
-########################################################################
-
-share/Makefile.config: share/Makefile.config.in config.status
-	$(PRINT_MAKING) $@
-	./config.status --file $@
-
-share/Makefile.dynamic_config: share/Makefile.dynamic_config.internal
-	$(PRINT_MAKING) $@
-	$(RM) $@
-	$(CP) $< $@
-	$(CHMOD_RO) $@
-
-config.status: configure
-	$(PRINT_MAKING) $@
-	./config.status --recheck
-
-configure: configure.ac .force-reconfigure
-	$(PRINT_MAKING) $@
-	autoconf -f
-
-# If 'make clean' has to be performed after 'git pull':
-# change '.make-clean-stamp' before 'git commit'
-.make-clean: .make-clean-stamp
-	$(TOUCH) $@
-	$(QUIET_MAKE) clean
+	rm -rf _build .merlin
 
-include .make-clean
-
-# force "make clean" to be executed for all users of GIT
-force-clean:
-	expr `$(CAT) .make-clean-stamp` + 1 > .make-clean-stamp
-
-# force a reconfiguration for all git users
-force-reconfigure:
-	expr `$(CAT) .force-reconfigure` + 1 > .force-reconfigure
+##############################################################################
+# HELP
+################################
 
+help::
+	@echo "Build configuration variables"
+	@echo "  - RELEASE: compile in release mode if set to 'yes'"
+	@echo "  - DUNE_DISPLAY: parameter transmitted to dune --display option"
+	@echo "  - DISABLED_PLUGINS: disable these plugins before (re)building"
+	@echo "    (none for enabling all plugins)"
 
 ##############################################################################
 # INSTALL/UNINSTALL
 ################################
 
-sinclude config.prefix
-FRAMAC_INSTALLDIR?=
-
-INSTALLDIR:=$(FRAMAC_INSTALLDIR)
-
 include share/Makefile.installation
 
 ###############################################################################
@@ -153,12 +115,9 @@ FRAMAC_WTESTS:=$(FRAMAC_PTESTS_SRC)/wtests.exe
 # Frama-C also have ptest directories in plugins, so we do not use default
 PTEST_ALL_DIRS:=tests $(wildcard src/plugins/*/tests)
 
-# Test aliasing definition allowing ./configure --disable-<plugin> 
+# Test aliasing definition allowing ./configure --disable-<plugin>
 PTEST_ALIASES:=@tests/ptests @src/plugins/ptests
 
-# Ptests needs config.sed so that dune can build Frama-C (if it is not built)
-PTEST_DEPS:=config.sed
-
 # WP tests need WP cache
 PTEST_USE_WP_CACHE:=yes
 

bin/rebuild.sh

@@ -21,4 +21,4 @@
 #                                                                        #
 ##########################################################################
 
-autoconf -f && ./configure && make -k clean && make -k
+make -k clean && make -k

configurator.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+module C = Configurator.V1
+
+module Temp = struct (* Almost copied from configurator *)
+  let (^/) a b = a ^ "/" ^ b
+
+  let rec rm_rf dir =
+    Array.iter (fun fn ->
+        let fn = dir ^/ fn in
+        if Sys.is_directory fn then rm_rf fn else Unix.unlink fn)
+      (Sys.readdir dir);
+    Unix.rmdir dir
+
+  let prng = lazy (Random.State.make_self_init ())
+
+  let gen_name ~dir ~prefix ~suffix =
+    let rnd = Random.State.bits (Lazy.force prng) land 0xFFFFFF in
+    dir ^/ Printf.sprintf "%s%06x%s" prefix rnd suffix
+
+  let create_dir () =
+    let dir =
+      gen_name ~dir:(Filename.get_temp_dir_name ()) ~prefix:"" ~suffix:"" in
+    Unix.mkdir dir 0o700 ;
+    at_exit (fun () -> rm_rf dir) ;
+    dir
+
+  let create ?(dir=create_dir ()) ?(prefix="") ?(suffix="") mk =
+    let rec try_name counter =
+      let name = gen_name ~dir ~prefix ~suffix in
+      match mk name with
+      | () -> name
+      | exception Unix.Unix_error _ when counter < 1000 -> try_name (counter + 1)
+    in
+    try_name 0
+end
+
+module C_compiler = struct (* This could be put in Dune? *)
+  type t =
+    { compiler: string
+    ; is_gnu: bool
+    }
+
+  let find_compiler configurator =
+    let cc_env = try Sys.getenv "CC" with Not_found -> "" in
+    if cc_env <> "" then cc_env
+    else
+      let finder compiler = C.which configurator compiler |> Option.is_some in
+      try List.find finder [ "gcc"; "cc"; "cl.exe" ]
+      with Not_found -> C.die "Could not find a C compiler"
+
+  let write_file name code =
+    let out = open_out name in
+    Printf.fprintf out "%s" code ;
+    close_out out
+
+  let call configurator compiler options code =
+    let dir = Temp.create_dir () in
+    let file =
+      Temp.create ~dir ~suffix:".c" (fun name -> write_file name code) in
+    C.Process.run configurator ~dir compiler (options @ [ file ])
+
+
+  let preprocess_flag = "-E"
+
+  let is_gnu configurator compiler =
+    let code = {|#ifndef __GNUC__
+      this is not a gnuc compiler
+#endif
+|}
+    in
+    (call configurator compiler ["-c"] code).exit_code = 0
+
+  let get configurator =
+    let compiler = find_compiler configurator in
+    let is_gnu = is_gnu configurator compiler in
+    { compiler ; is_gnu }
+
+  let preprocess configurator t options =
+    call configurator t.compiler (preprocess_flag :: options)
+
+  let _compile configurator t options =
+    call configurator t.compiler ("-c" :: options)
+end
+
+(* Frama-C specific part *)
+
+module Cpp = struct
+  module GnuLike = struct
+    let code = {|
+#define foo 0
+/* foo */
+int main(){}
+|}
+
+    let check configurator compiler =
+      let options = ["-dD" ; "-nostdinc"] in
+      (C_compiler.preprocess configurator compiler options code).exit_code = 0
+  end
+
+  module KeepComments = struct
+    let code =
+      {|/* Check whether comments are kept in output */|}
+
+    let check configurator compiler options =
+      let result = C_compiler.preprocess configurator compiler options code in
+      result.exit_code = 0 &&
+      let re = Str.regexp_string "kept" in
+      try ignore (Str.search_forward re result.stdout 0); true
+      with Not_found -> false
+  end
+
+  module Archs = struct
+    let opt_m_code value =
+      Format.asprintf {|/* Check if preprocessor supports option -m%s */|} value
+
+    let check configurator compiler arch =
+      let code = opt_m_code arch in
+      let options = [ Format.asprintf "-m%s" arch ] in
+      if (C_compiler.preprocess configurator compiler options code).exit_code = 0
+      then Some arch else None
+
+    let supported_archs configurator compiler archs =
+      let check = check configurator compiler in
+      List.map (fun s -> "-m" ^ s) @@ List.filter_map check archs
+  end
+
+  type t =
+    { compiler : C_compiler.t
+    ; default_args : string list
+    ; is_gnu_like : bool
+    ; keep_comments : bool
+    ; supported_archs_opts : string list
+    }
+
+  let get configurator =
+    let compiler = C_compiler.get configurator in
+    let default_args = [ "-C" ; "-I." ] in
+    let is_gnu_like = GnuLike.check configurator compiler in
+    let keep_comments = KeepComments.check configurator compiler [ "-C" ] in
+    let supported_archs_opts =
+      Archs.supported_archs configurator compiler [ "16" ; "32" ; "64" ] in
+    { compiler; default_args; is_gnu_like; keep_comments; supported_archs_opts }
+
+  let pp_flags fmt =
+    let pp_sep fmt () = Format.fprintf fmt " " in
+    Format.pp_print_list ~pp_sep Format.pp_print_string fmt
+
+  let pp_default_cpp fmt cpp =
+    Format.fprintf fmt "%s %a"
+      cpp.compiler.compiler
+      pp_flags (C_compiler.preprocess_flag :: cpp.default_args)
+
+  let pp_archs fmt cpp =
+    let pp_arch fmt arch = Format.fprintf fmt "\"%s\"" arch in
+    let pp_sep fmt () = Format.fprintf fmt "; " in
+    Format.fprintf fmt
+      "%a" (Format.pp_print_list ~pp_sep pp_arch) cpp.supported_archs_opts
+
+  let pp_sed fmt cpp =
+    Format.fprintf fmt
+      "s|@FRAMAC_DEFAULT_CPP@|%a|\n" pp_default_cpp cpp ;
+    Format.fprintf fmt
+      "s|@FRAMAC_DEFAULT_CPP_ARGS@|%a|\n" pp_flags cpp.default_args ;
+    Format.fprintf fmt
+      "s|@FRAMAC_GNU_CPP@|%b|\n" cpp.is_gnu_like ;
+    Format.fprintf fmt
+      "s|@DEFAULT_CPP_KEEP_COMMENTS@|%b|\n" cpp.keep_comments ;
+    Format.fprintf fmt
+      "s|@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@|%a|" pp_archs cpp
+end
+
+module Fc_version = struct
+  type t =
+    { major: string
+    ; minor: string
+    ; ext: string
+    ; name: string
+    }
+
+  let get configurator =
+    let out_VERSION =
+      let out = C.Process.run configurator "cat" ["VERSION"] in
+      if out.exit_code <> 0 then C.die "Can't read VERSION." ;
+      out.stdout
+    in
+    let re_version =
+      Str.regexp {|\([1-9][0-9]\)\.\([0-9]\)\(.*\)|}
+    in
+    let major, minor, ext =
+      if Str.string_match re_version out_VERSION 0 then
+        Str.matched_group 1 out_VERSION,
+        Str.matched_group 2 out_VERSION,
+        try Str.matched_group 3 out_VERSION with Not_found -> ""
+      else
+        C.die "Can't read VERSION."
+    in
+    let name =
+      let out = C.Process.run configurator "cat" ["VERSION_CODENAME"] in
+      if out.exit_code <> 0 then
+        C.die "Can't read VERSION_CODENAME." ;
+      String.sub out.stdout 0 (String.length out.stdout - 1)
+    in
+    { major; minor; ext; name }
+
+  let pp_sed fmt version =
+    Format.fprintf fmt
+      "s|@VERSION@|%s.%s%s|\n" version.major version.minor version.ext ;
+    Format.fprintf fmt
+      "s|@VERSION_CODENAME@|%s|\n" version.name ;
+    Format.fprintf fmt
+      "s|@MAJOR_VERSION@|%s|\n" version.major ;
+    Format.fprintf fmt
+      "s|@MINOR_VERSION@|%s|" version.minor
+end
+
+let python_available configurator =
+  let result = C.Process.run configurator "python3" ["--version"] in
+  if result.exit_code <> 0 then false
+  else
+    let out = result.stdout in
+    let re_version =
+      Str.regexp {|.* \([0-9]\)\.\([0-9]+\).[0-9]+|}
+    in
+    try
+      let maj, med =
+        if Str.string_match re_version out 0 then
+          int_of_string @@ Str.matched_group 1 out,
+          int_of_string @@ Str.matched_group 2 out
+        else raise Not_found
+      in
+      if maj <> 3 || med < 7 then raise Not_found ;
+      true
+    with Not_found | Failure _ -> false
+
+let configure configurator =
+  let version = Fc_version.get configurator in
+  let cpp = Cpp.get configurator in
+  let config_sed = open_out "config.sed" in
+  let fmt = Format.formatter_of_out_channel config_sed in
+  Format.fprintf fmt "%a\n%a\n" Fc_version.pp_sed version Cpp.pp_sed cpp ;
+  close_out config_sed ;
+  let python = open_out "python-3.7-available" in
+  Printf.fprintf python "%b" (python_available configurator) ;
+  close_out python
+
+let () =
+  C.main ~name:"frama_c_config" configure

configure.ac

-##########################################################################
-#                                                                        #
-#  This file is part of Frama-C.                                         #
-#                                                                        #
-#  Copyright (C) 2007-2022                                               #
-#    CEA   (Commissariat à l'énergie atomique et aux énergies            #
-#           alternatives)                                                #
-#    INRIA (Institut National de Recherche en Informatique et en         #
-#           Automatique)                                                 #
-#                                                                        #
-#  you can redistribute it and/or modify it under the terms of the GNU   #
-#  Lesser General Public License as published by the Free Software       #
-#  Foundation, version 2.1.                                              #
-#                                                                        #
-#  It is distributed in the hope that it will be useful,                 #
-#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
-#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
-#  GNU Lesser General Public License for more details.                   #
-#                                                                        #
-#  See the GNU Lesser General Public License version 2.1                 #
-#  for more details (enclosed in the file licenses/LGPLv2.1).            #
-#                                                                        #
-##########################################################################
-
-# autoconf input for Objective Caml programs
-# Copyright (C) 2001 Jean-Christophe Filliâtre
-#   from a first script by Georges Mariano
-
-# the script generated by autoconf from this input will set the following
-# variables:
-#   OCAMLC        "ocamlc" if present in the path, or a failure
-#                 or "ocamlc.opt" if present with same version number as ocamlc
-#   OCAMLOPT      "ocamlopt" (or "ocamlopt.opt" if present), or "no"
-#   OCAMLBEST     either "byte" if no native compiler was found,
-#                 or "opt" otherwise
-#   OCAMLDEP      "ocamldep"
-#   OCAMLLEX      "ocamllex" (or "ocamllex.opt" if present)
-#   OCAMLYACC     "ocamlyacc"
-#   OCAMLLIB      the path to the ocaml standard library
-#   OCAMLVERSION  the ocaml version number
-#   OCAMLWIN32    "yes"/"no" depending on Sys.os_type = "Win32"
-#   PLATFORM      "Win32", "Cygwin", "MacOS" or "Unix"
-#   EXE           ".exe" if PLATFORM=Win32 (or Cygwin), "" otherwise
-#   DLLEXT        ".dll" if PLATFORM=Win32 (or Cygwin), ".so" otherwise
-
-AC_INIT
-AC_CONFIG_SRCDIR([src/init/boot/boot.ml])
-
-define([FRAMAC_MAIN_AUTOCONF])
-m4_include(share/configure.ac)
-
-AC_SUBST([FRAMAC_VERSION],[`cat VERSION`])
-
-# export CYGWIN=nobinmode
-
-##########################
-# Check for Make version #
-##########################
-
-new_section "configure make"
-
-AC_CHECK_PROGS(MAKE,gmake make,make,)
-AC_MSG_CHECKING([version of make])
-MAKE_DISTRIB=`sh -c "$MAKE -v | sed -n -e 's/\(.*\) Make.*$/\1/p'"`
-MAKE_MAJOR=`sh -c "$MAKE -v | sed -n  -f bin/sed_get_make_major"`
-MAKE_MINOR=`sh -c "$MAKE -v | sed -n -f bin/sed_get_make_minor"`
-AC_MSG_RESULT($MAKE_MAJOR.$MAKE_MINOR)
-if test "$MAKE_DISTRIB" != GNU -o "$MAKE_MAJOR" -lt 3 \
-   -o "$MAKE_MAJOR" = 3 -a "$MAKE_MINOR" -lt 81
-then
-   AC_MSG_ERROR([unsupported version; GNU Make version 3.81
-                 or higher is required.]);
-fi
-
-# verbosemake feature
-AC_ARG_ENABLE(
-  verbosemake,
-  [  --enable-verbosemake    verbose makefile commands],
-  VERBOSEMAKE=$enableval,
-  VERBOSEMAKE=no
-)
-
-if test "$VERBOSEMAKE" = yes ; then
-  AC_MSG_RESULT(Make will be verbose.)
-fi
-
-##########################################
-# Check for invalid command-line options #
-##########################################
-case $prefix in
-  *\'*|*\"* ) AC_MSG_ERROR(quotes not allowed in --prefix argument: $prefix);;
-  NONE )
-    # no prefix: remove existing config.prefix if any
-    rm -f config.prefix
-    ;;
-  * )
-    echo "FRAMAC_INSTALLDIR?=\"$prefix\"" > config.prefix
-    ;;
-esac
-
-#############################
-# Check for Ocaml compilers #
-#############################
-
-new_section "configure ocaml compilers"
-
-# we first look for ocamlc in the path; if not present, we fail
-AC_CHECK_PROG(OCAMLC,ocamlc,ocamlc,no)
-if test "$OCAMLC" = no ; then
-        AC_MSG_ERROR(Cannot find ocamlc.)
-fi
-
-# we extract Ocaml version number and library path
-# "sed -n" is the posix version of "sed --quiet"
-AC_MSG_CHECKING(version of OCaml)
-OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version *\(.*\)$|\1|p' `
-AC_MSG_RESULT($OCAMLVERSION)
-case $OCAMLVERSION in
-  0.*|1.*|2.*|3.*|4.00.*|4.01.*|4.02.*|4.03.*|4.04.*|4.05.*|4.06.*|4.07.*|4.08.0)
-     AC_MSG_ERROR(Incompatible OCaml version; use 4.08.1+.);;
-   *)
-     OCAML_ANNOT_OPTION="-bin-annot";;
-esac
-
-AC_SUBST(OCAMLMAJORNB)
-AC_SUBST(OCAMLMINORNB)
-AC_SUBST(OCAMLPATCHNB)
-
-AC_SUBST(HAS_OCAML409)
-AC_SUBST(HAS_OCAML410)
-
-OCAMLMAJORNB=$(echo $OCAMLVERSION | cut -f 1 -d .)
-OCAMLMINORNB=$(echo $OCAMLVERSION | cut -f 2 -d .)
-OCAMLPATCHNB=$(echo $OCAMLVERSION | cut -f 3 -d .)
-
-if test $OCAMLMAJORNB -gt 4; then
-  HAS_OCAML409=yes;
-  HAS_OCAML410=yes;
-else
-  HAS_OCAML409=no;
-  HAS_OCAML410=no;
-  if test $OCAMLMINORNB -ge 9; then
-    HAS_OCAML409=yes;
-  fi;
-  if test $OCAMLMINORNB -ge 10; then
-    HAS_OCAML410=yes;
-  fi;
-fi;   # MAJORNB -gt 4
-
-# Ocaml library path
-AC_MSG_CHECKING(OCaml library path)
-OCAMLLIB=`$OCAMLC -where | tr -d '\\r'`
-AC_MSG_RESULT($OCAMLLIB)
-
-# then we look for ocamlopt; if not present, we issue a warning
-# if the version or the stdlib directory is not the same, we also discard it
-# we set OCAMLBEST to "opt" or "byte", whether ocamlopt is available or not
-AC_CHECK_PROG(OCAMLOPT,ocamlopt,ocamlopt,no)
-OCAMLBEST=byte
-if test "$OCAMLOPT" = no ; then
-        AC_MSG_WARN(Cannot find ocamlopt; bytecode compilation only.)
-else
-        AC_MSG_CHECKING(ocamlopt version and standard library)
-        TMPVERSION=`$OCAMLOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p'`
-        if test "$TMPVERSION" != "$OCAMLVERSION" \
-                -o `$OCAMLOPT -where | tr -d '\\r'` != "$OCAMLLIB"; then
-            AC_MSG_RESULT(differs from ocamlc; ocamlopt discarded.)
-            OCAMLOPT=no
-        else
-            AC_MSG_RESULT(ok)
-            OCAMLBEST=opt
-        fi
-fi
-
-# In case we have a native compiler, check that native dynlink works.
-# Otherwise, fall back to bytecode-only compilation
-
-if test "$OCAMLBEST" = opt; then
-  echo "let f x y =" > test_dynlink.ml
-  echo "  Dynlink.loadfile \"foo\"; " >> test_dynlink.ml
-  echo "  ignore (Dynlink.is_native);" >> test_dynlink.ml
-  echo "  abs_float (x -. y)" >> test_dynlink.ml
-  if ($OCAMLOPT -shared -linkall -o test_dynlink.cmxs test_dynlink.ml) \
-    2> /dev/null ; \
-then
-  AC_MSG_RESULT([native dynlink works fine. Great.])
-else
-  AC_MSG_WARN([Native dynlink does not work, disabling native compilation.])
-  OCAMLBEST=byte
-fi
-rm -f test_dynlink.*
-fi
-
-if test "$OCAMLBEST" = "opt"; then
-   LIB_SUFFIX=cmxa
-   DYN_SUFFIX=cmxs
-   OBJ_SUFFIX=cmx;
-else
-   LIB_SUFFIX=cma
-   DYN_SUFFIX=cma
-   OBJ_SUFFIX=cmo;
-fi
-
-# checking for ocamlfind
-
-AC_CHECK_PROG(DUNE,dune,dune,no)
-if test "$DUNE" != no ; then
-   true
-else
-        AC_MSG_ERROR(Cannot find dune.)
-fi
-
-###################################################
-# Select devel compilation (warnings, warn-error) #
-###################################################
-
-# It is inherited by the plugins
-
-if test -e ".for_devel"; then
-   DEFAULT_DEVEL_MODE=yes
-else
-   DEFAULT_DEVEL_MODE=no
-fi
-
-AC_ARG_ENABLE(
-  devel-mode,
-  [  --enable-devel-mode     force the devel mode (warnings and warn-error).
-  --disable-devel-mode    force the distrib mode (no warnings and no warn-error).
-],
-  DEVELOPMENT=$enableval,
-  DEVELOPMENT=$DEFAULT_DEVEL_MODE, # default value
-)
-
-if test "$DEVELOPMENT" = "yes" ; then
-   AC_MSG_NOTICE(Development mode: warnings and warn-errors are activated)
-else
-   AC_MSG_NOTICE(Distribution mode: all warnings are deactivated)
-fi
-
-
-# landmarks (profiling tool, for developers)
-########
-
-dnl AC_ARG_ENABLE(
-dnl   landmarks,
-dnl   [  --enable-landmarks      enable landmarks profiling (default: yes if package installed)],
-dnl   ENABLE_LANDMARKS=$enableval,
-dnl   ENABLE_LANDMARKS=yes)
-
-dnl if test "$ENABLE_LANDMARKS" = yes ; then
-dnl   AC_MSG_CHECKING(for Landmarks)
-dnl   LANDMARKS_PATH=$($OCAMLFIND query landmarks 2>/dev/null | tr -d '\r\n')
-dnl   LANDMARKS_PPX_PATH=$($OCAMLFIND query landmarks.ppx 2>/dev/null | tr -d '\r\n')
-dnl   if test -f "$LANDMARKS_PATH/landmark.$DYN_SUFFIX" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks.$DYN_SUFFIX"; then
-dnl     HAS_LANDMARKS="yes";
-dnl     AC_MSG_RESULT(found)
-dnl   else
-dnl     HAS_LANDMARKS="no";
-dnl     AC_MSG_RESULT(not found.)
-dnl   fi;
-dnl else
-dnl   AC_MSG_RESULT(Landmarks profiling disabled);
-dnl   HAS_LANDMARKS="no"
-dnl fi
-
-# Python >=3.7 (for analysis-scripts and several tests: compliance, jcdb, ...)
-########
-
-AC_MSG_CHECKING(for python3)
-
-PYTHON3_VERSION=$(python3 --version 2>/dev/null || echo "")
-if test -z "$PYTHON3_VERSION" ; then
-  AC_MSG_RESULT(not found. Some non-regression tests will be disabled.)
-  HAS_PYTHON37="no"
-else
-  AC_MSG_RESULT(found)
-  AC_MSG_CHECKING(for python3 >= 3.7)
-  PYTHON3_VERSION=$(echo "$PYTHON3_VERSION" | cut -d' ' -f2-)
-  case $PYTHON3_VERSION in
-  2.*|3.[[0-6]].*)
-     AC_MSG_RESULT(found $PYTHON3_VERSION (too old); some non-regression tests will be disabled)
-     HAS_PYTHON37="no"
-     ;;
-   *)
-     AC_MSG_RESULT(ok)
-     HAS_PYTHON37="yes"
-     ;;
-  esac
-fi
-
-############
-# Platform #
-############
-
-new_section "configure platform"
-
-AC_MSG_CHECKING(platform)
-# get Sys.os_type as OCAML_OS_TYPE
-echo "let () = print_string Sys.os_type;;" > test_os_type.ml
-$OCAMLC -o test_os_type test_os_type.ml
-OCAML_OS_TYPE=$(./test_os_type)
-rm -f test_os_type.cmi  test_os_type.cmo  test_os_type.ml test_os_type
-
-if test "$OCAML_OS_TYPE" = "Win32"; then
-  AC_MSG_RESULT(Win32)
-  AC_CHECK_PROG(CYGPATH,cygpath,cygpath,no)
-  PLATFORM=Win32
-  OCAMLWIN32=yes
-  EXE=.exe
-  DLLEXT=.dll
-else
-  OCAMLWIN32=no
-  if test "$OCAML_OS_TYPE" = "Cygwin"; then
-    AC_MSG_WARN([Compilation using Cygwin is unsupported;
-                 consider using a MinGW-based compiler.])
-    AC_MSG_RESULT(Cygwin)
-    PLATFORM=Cygwin
-    EXE=.exe
-    DLLEXT=.dll
-  else
-    if test $(uname -s) = "Darwin"; then
-      AC_MSG_RESULT(MacOS)
-      PLATFORM=MacOS
-    else
-      AC_MSG_RESULT(Unix)
-      PLATFORM=Unix
-    fi
-    EXE=
-    DLLEXT=.so
-  fi
-fi
-
-# C and POSIX standard headers used by C bindings.
-AC_LANG([C])
-
-AC_ARG_WITH(cc,[specifies a custom C compiler and pre-processor],[CC=$withval])
-
-AC_PROG_CC
-
-AC_CHECK_HEADERS(stdlib.h)
-AC_CHECK_HEADERS(assert.h)
-AC_CHECK_HEADERS(float.h)
-AC_CHECK_HEADERS(math.h)
-
-AC_CHECK_HEADERS(signal.h)
-
-AC_CHECK_HEADERS(unistd.h)
-
-# Local machdep feature (to generate new platforms)
-AC_ARG_ENABLE(
-  localmachdep,
-  [  --enable-localmachdep   enable local machdep configuration],
-  LOCAL_MACHDEP=$enableval,
-  LOCAL_MACHDEP=no)
-
-if test "$LOCAL_MACHDEP" = yes ; then
-
-AC_CONFIG_HEADERS([config.h])
-AC_CHECK_HEADERS(wchar.h)
-
-# Find out the true definitions of some integer types
-# checkIntegerype(size_t) will echo "int" or "long"
-checkIntegerType() {
-  fn="testtype.c"
-  fo="testtype.o"
-  for t in "int" "unsigned int" "long" "unsigned long" "short" "unsigned short" "char" "unsigned  char" ;do
-     echo "#include <stddef.h>" >$fn
-     echo "#include <wchar.h>" >>$fn
-     # We define a prototype with one type and the function with
-     # another type. This will result in compilation error
-     # unless the types are really identical
-     echo "$t foo($t x);"      >>$fn
-     echo "$1 foo($1 x) { return x;}" >>$fn
-     if gcc -c $fn 2>/dev/null ;then
-        # Found it
-        echo $t
-        rm -f $fn $fo
-        return
-     fi
-  done
-  rm -f $fn $fo
-}
-
-AC_MSG_CHECKING([definition of size_t])
-TYPE_SIZE_T=`checkIntegerType "size_t"`
-if test "x$TYPE_SIZE_T" = "x" ;then
-  AC_MSG_ERROR([Cannot find definition of size_t])
-fi
-AC_DEFINE_UNQUOTED(TYPE_SIZE_T, "$TYPE_SIZE_T")
-AC_MSG_RESULT([$TYPE_SIZE_T])
-
-AC_MSG_CHECKING([definition of wchar_t])
-TYPE_WCHAR_T=`checkIntegerType "wchar_t"`
-if test "x$TYPE_WCHAR_T" = "x" ;then
-  AC_MSG_ERROR([Cannot find definition of wchar_t])
-fi
-AC_DEFINE_UNQUOTED(TYPE_WCHAR_T, "$TYPE_WCHAR_T")
-AC_MSG_RESULT([$TYPE_WCHAR_T])
-
-AC_MSG_CHECKING([definition of ptrdiff_t])
-TYPE_PTRDIFF_T=`checkIntegerType "ptrdiff_t"`
-if test "x$TYPE_PTRDIFF_T" = "x" ;then
-  AC_MSG_ERROR([Cannot find definition of ptrdiff_t])
-fi
-AC_DEFINE_UNQUOTED(TYPE_PTRDIFF_T, "$TYPE_PTRDIFF_T")
-AC_MSG_RESULT([$TYPE_PTRDIFF_T])
-
-AC_MSG_CHECKING([for gcc version])
-AC_CHECK_TYPE(__builtin_va_list,
-              HAVE_BUILTIN_VA_LIST=true,
-              HAVE_BUILTIN_VA_LIST=false)
-if test "$HAVE_BUILTIN_VA_LIST" = "true" ;then
-   AC_DEFINE_UNQUOTED(HAVE_BUILTIN_VA_LIST, 1)
-fi
-
-# Does gcc add underscores to identifiers to make assembly labels?
-# (I think MSVC always does)
-AC_MSG_CHECKING([if gcc adds underscores to assembly labels.])
-AC_LINK_IFELSE([AC_LANG_SOURCE([int main() { __asm__("jmp _main"); }])],
-                  UNDERSCORE_NAME=true,
-                  UNDERSCORE_NAME=false)
-AC_MSG_RESULT($UNDERSCORE_NAME)
-if test "$UNDERSCORE_NAME" = "true" ;then
-   AC_DEFINE_UNQUOTED(UNDERSCORE_NAME, 1)
-fi
-
-fi # local machdep configuration
-
-###################################
-# Frama-C's pre-processor support #
-###################################
-
-# Specific preprocessor support
-AC_ARG_WITH(
-        cpp,
-        [  --with-cpp             customize default preprocessor for Frama-C],
-        [FRAMAC_DEFAULT_CPP=$withval],
-        [FRAMAC_DEFAULT_CPP=])
-
-# if no specific pre-processor has been given, check whether we can use
-# $CC. Note that we want to keep comments in the output, so that AC_PROG_CPP
-# alone is not sufficient.
-  if test -z "$FRAMAC_DEFAULT_CPP"; then
-    AC_PROG_CPP
-    CPPFLAGS="-C -I.";
-    if test -n "$GCC"; then FRAMAC_GNU_CPP=true; else FRAMAC_GNU_CPP=false; fi
-  else
-    CPP=$FRAMAC_DEFAULT_CPP;
-    FRAMAC_GNU_CPP=true;
-    CPPFLAGS="-dD -nostdinc"
-    AC_PREPROC_IFELSE(
-        [AC_LANG_SOURCE([#define foo 0
-                         /* foo */
-                         ])],
-        FRAMAC_GNU_CPP=true,
-        FRAMAC_GNU_CPP=false)
-    CPPFLAGS=
-  fi
-  AC_PREPROC_IFELSE(
-    [AC_LANG_SOURCE([/* Check whether comments are kept in output */])],
-    [if test -e conftest.i; then
-      if grep -e kept conftest.i; then
-      FRAMAC_DEFAULT_CPP="$CPP $CPPFLAGS";
-      DEFAULT_CPP_KEEP_COMMENTS=true;
-     else
-      AC_MSG_WARN([Default pre-processing command '$CPP' do not preserve
-                     comments. Please define an appropriate pre-processor
-                   with --with-cpp, or you will only be able to use ACSL
-                   annotations in already pre-processed files])
-      FRAMAC_DEFAULT_CPP=$CPP;
-      DEFAULT_CPP_KEEP_COMMENTS=false;
-      fi;
-      else # handling old version of autoconf (<2.67) that does not keep
-           # preprocessor result in conftest.i
-        AC_MSG_WARN([Unable to check whether $CPP preserves comments.
-                     Assuming everything is fine])
-        FRAMAC_DEFAULT_CPP="$CPP $CPPFLAGS";
-        DEFAULT_CPP_KEEP_COMMENTS=true;
-      fi
-    ],
-     [AC_MSG_WARN([Unable to find a working pre-processor.
-                   Please define one with --with-cpp, or you will be able
-                   to launch Frama-C only on pre-processed files])];
-      FRAMAC_DEFAULT_CPP="";
-      DEFAULT_CPP_KEEP_COMMENTS=false;
-    )
-
-AC_MSG_RESULT(Default preprocessor is '$FRAMAC_DEFAULT_CPP'.)
-
-FRAMAC_DEFAULT_CPP_ARGS=$CPPFLAGS
-
-# Test if preprocessor supports options such as -m16/-m32/-m64
-
-DEFAULT_CPP_SUPPORTED_ARCH_OPTS=
-
-# Store original value of CPPFLAGS before doing tests
-OLD_CPPFLAGS=$CPPFLAGS
-
-rm -f conftest.i
-CPPFLAGS="$OLD_CPPFLAGS -m32"
-AC_PREPROC_IFELSE(
-  [AC_LANG_SOURCE([/* Check if preprocessor supports option -m32 */])],
-  [if test -e conftest.i; then
-    DEFAULT_CPP_SUPPORTED_ARCH_OPTS+='\"-m32\"; ';
-  fi], [])
-
-rm -f conftest.i
-CPPFLAGS="$OLD_CPPFLAGS -m64"
-AC_PREPROC_IFELSE(
-  [AC_LANG_SOURCE([/* Check if preprocessor supports option -m64 */])],
-  [if test -e conftest.i; then
-    DEFAULT_CPP_SUPPORTED_ARCH_OPTS+='\"-m64\"; ';
-  fi], [])
-
-rm -f conftest.i
-CPPFLAGS="$OLD_CPPFLAGS -m16"
-AC_PREPROC_IFELSE(
-  [AC_LANG_SOURCE([/* Check if preprocessor supports option -m16 */])],
-  [if test -e conftest.i; then
-    DEFAULT_CPP_SUPPORTED_ARCH_OPTS+='\"-m16\"; ';
-  fi], [])
-
-# revert CPPFLAGS to original value
-CPPFLAGS=$OLD_CPPFLAGS
-
-AC_MSG_RESULT(Default preprocessor supported architecture-related options: $DEFAULT_CPP_SUPPORTED_ARCH_OPTS)
-
-############################
-# Substitutions to perform #
-############################
-
-AC_SUBST(VERBOSEMAKE)
-AC_SUBST(DEVELOPMENT)
-AC_SUBST(HAS_APRON)
-AC_SUBST(HAS_MPFR)
-AC_SUBST(HAS_LANDMARKS)
-AC_SUBST(HAS_PYTHON37)
-AC_SUBST(LABLGTK_VERSION)
-AC_SUBST(OCAMLBEST)
-AC_SUBST(OCAMLVERSION)
-AC_SUBST(OCAMLLIB)
-AC_SUBST(OCAMLWIN32)
-AC_SUBST(OCAML_ANNOT_OPTION)
-AC_SUBST(EXE)
-AC_SUBST(DLLEXT)
-
-AC_SUBST(HAVE_STDLIB_H)
-AC_SUBST(HAVE_WCHAR_H)
-AC_SUBST(HAVE_PTRDIFF_H)
-AC_SUBST(HAVE_BUILTIN_VA_LIST)
-AC_SUBST(UNDERSCORE_NAME)
-AC_SUBST(CYCLES_PER_USEC)
-AC_SUBST(LOCAL_MACHDEP)
-AC_SUBST(datarootdir)
-AC_SUBST(FRAMAC_DEFAULT_CPP)
-AC_SUBST(FRAMAC_DEFAULT_CPP_ARGS)
-AC_SUBST(DEFAULT_CPP_SUPPORTED_ARCH_OPTS)
-AC_SUBST(FRAMAC_GNU_CPP)
-AC_SUBST(DEFAULT_CPP_KEEP_COMMENTS)
-AC_SUBST(CC)
-
-AC_SUBST(LABLGTK_PATH)
-
-# used by some share/Makefile.xxx
-AC_SUBST(PLATFORM)
-
-################################################
-# Finally create the Makefile from Makefile.in #
-################################################
-
-new_section "creating makefile"
-
-AC_CONFIG_FILES([share/Makefile.config], [chmod a-w share/Makefile.config])
-
-AC_OUTPUT
-
-###########
-# Plugins #
-###########
-
-rm -f src/plugins/.disabled
-rm -f src/plugins/dune
-
-m4_foreach_w([__plugin],m4_esyscmd([ls src/plugins]),
-  [
-    m4_define([plugin_dir],[src/plugins/__plugin])
-    m4_syscmd(test -d plugin_dir)
-    m4_define([is_plugin],m4_sysval)
-    m4_if(is_plugin,0,[
-      AC_ARG_ENABLE(
-        __plugin,
-        AS_HELP_STRING([--disable-__plugin],[Disable __plugin]),
-        [ENABLE___plugin=$enableval],
-        [ENABLE___plugin=yes]
-      )
-      if test "$ENABLE___plugin" = no ; then
-        echo "__plugin" >> src/plugins/.disabled
-      fi
-    ],)
-  ])
-
-if test -f src/plugins/.disabled ; then
-  echo ";; File generated by ./configure --disable-<PLUGIN>" > src/plugins/dune
-  echo "(include_subdirs no)" >> src/plugins/dune
-  echo ";; Disabled plugin list:" >> src/plugins/dune
-  echo "(data_only_dirs $(cat src/plugins/.disabled))" >> src/plugins/dune
-  cat src/plugins/.disabled | sed -n -e 's|^\(.*\)$|(rule (alias "frama-c-configure") (deps (universe)) (action (echo "Disabled plug-in: src/plugins/\1\n")))|p' >> src/plugins/dune
-  echo ";; Test" >> src/plugins/dune
-  echo "(alias (name ptests) (deps (alias ptests_config)))" >> src/plugins/dune
-# "sed -n" is the posix version of "sed --quiet"
-  cat src/plugins/.disabled | sed -n -e 's|^\(.*\)$|(rule (alias "ptests_config") (deps (universe)) (action (echo "Testing with disabled plug-in: src/plugins/\1\n")))|p' >> src/plugins/dune
-  chmod a-w src/plugins/dune
-  rm src/plugins/.disabled
-fi
-
-###########
-# Summary #
-###########
-
-new_section "summary: plug-ins available"
-
-$DUNE build -j1 --display quiet @frama-c-configure

share/Makefile.config.in → dev/disable-plugins.sh

+#!/usr/bin/env bash
 ##########################################################################
 #                                                                        #
 #  This file is part of Frama-C.                                         #
@@ -20,70 +21,68 @@
 #                                                                        #
 ##########################################################################
 
-##########################################################################
-#                                                                        #
-# Define variables from configure.                                       #
-# These variables may be redefined later.                                #
-#                                                                        #
-##########################################################################
-
-######################
-# Installation paths #
-######################
+case "$1" in
+  "-h"|"--help")
+    echo "Usage: $0 <plugin directories>"
+    echo "  - directories are given without prefix src/plugins"
+    echo "  - if no directory is given all plugins are enabled (alternative: none)"
+    exit 0
+esac
 
-CYGPATH         ?=@CYGPATH@
+if [ ! -f VERSION ]; then
+  echo "This script is meant to be run from the root directory of Frama-C"
+  exit 2
+fi
 
-DESTDIR         ?=
-prefix          ?=@prefix@
-exec_prefix     ?=@exec_prefix@
-datarootdir     ?=@datarootdir@
-datadir         ?=@datadir@
-BINDIR          ?=$(DESTDIR)@bindir@
-LIBDIR          ?=$(DESTDIR)@libdir@
-DATADIR         ?=$(DESTDIR)@datarootdir@
-MANDIR          ?=$(DESTDIR)@mandir@
-BASHCOMPDIR     ?=$(DESTDIR)@datarootdir@/bash-completion/completions
+if [[ "$#" == "0" || ( "$#" == "1" && "$1" == "none" ) ]]; then
+  rm -f src/plugins/dune
+  echo "All plugins enabled"
+  echo "Make sure to \"dune clean\" the Frama-C directory before rebuilding"
+  exit 0
+fi
 
-FRAMAC_LIBDIR ?=$(LIBDIR)/frama-c
-FRAMAC_PLUGINDIR ?=$(FRAMAC_LIBDIR)/plugins
-FRAMAC_DATADIR ?=$(DATADIR)/frama-c
-EMACS_DATADIR ?=$(DATADIR)/emacs/site-lisp
+IFS='\, ' read -a DISABLED_PLUGINS <<< "$@"
 
-FRAMAC_DEFAULT_CPP ?=@FRAMAC_DEFAULT_CPP@
-FRAMAC_DEFAULT_CPP_ARGS ?= @FRAMAC_DEFAULT_CPP_ARGS@
-FRAMAC_GNU_CPP ?=@FRAMAC_GNU_CPP@
-DEFAULT_CPP_KEEP_COMMENTS?=@DEFAULT_CPP_KEEP_COMMENTS@
-DEFAULT_CPP_SUPPORTED_ARCH_OPTS?=@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@
+PLUGINS=
+for PLUGIN in "${DISABLED_PLUGINS[@]}" ; do
+  if [ -d "src/plugins/$PLUGIN" ]; then
+    PLUGINS="$PLUGINS $PLUGIN"
+  else
+    echo "Error: src/plugins/$PLUGIN is not a directory"
+    exit 2
+  fi
+done
 
-###########################
-# Miscellaneous variables #
-###########################
+cat > src/plugins/dune <<EOL
+;; File generated by ./dev/disable-plugins.sh <PLUGINS>
+(include_subdirs no)
+;; Disabled plugin list:
+(data_only_dirs ${PLUGINS})
+(rule
+ (alias "frama-c-configure")
+ (deps (universe))
+ (action (progn
+  (echo "Disabled plug-in(s):\n")
+EOL
 
-# Used by Makefile.common
-PLATFORM	?=@PLATFORM@
+for PLUGIN in "${DISABLED_PLUGINS[@]}" ; do
+  echo "  (echo \"- src/plugins/$PLUGIN\n\")" >> src/plugins/dune
+done
 
-# Used by Makefile.common
-VERBOSEMAKE	?=@VERBOSEMAKE@
+cat >> src/plugins/dune <<EOL
+)))
+;; Test
+(alias (name ptests) (deps (alias ptests_config)))
+(rule
+ (alias "ptests_config")
+ (deps (universe))
+ (action (progn
+  (echo "Testing with disabled plug-in(s):\n")
+EOL
+for PLUGIN in "${DISABLED_PLUGINS[@]}" ; do
+  echo "  (echo \"- src/plugins/$PLUGIN\n\")" >> src/plugins/dune
+done
+echo ")))" >> src/plugins/dune
 
-#######################
-# Working directories #
-#######################
-
-ifeq ($(OCAMLWIN32),yes)
-ifneq ($(CYGPATH),no)
-# Note: using quotes in the line below leads to weird garbled characters
-# in some versions of Cygwin.
-winpath=$(shell $(CYGPATH) -m $(1))
-else
-winpath=$(1)
-endif #CYGPATH
-else
-winpath=$(1)
-endif #OCAMLWIN32
-
-FRAMAC_ROOT_SRCDIR 	?= $(call winpath,@abs_top_srcdir@)
-
-##########################################################################
-# Local Variables:
-# mode: makefile
-# End:
+echo "Disabled plug-ins: $PLUGINS"
+echo "Make sure to clean the current directory before rebuilding"

dev/make-distrib.sh

@@ -23,11 +23,6 @@
 
 set -euxo pipefail
 
-if [ ! -f configure ] ; then
-  echo "No 'configure' file, you should first run 'autoconf'"
-  exit 2
-fi
-
 ################################################################################
 # Configuration
 
@@ -83,7 +78,6 @@ for plugin in $EXTERNAL_PLUGINS ; do
 done
 
 tar --concatenate --file=$TAR_ACC
-tar rf $FRAMAC_TAR configure --transform "s,^,$FRAMAC/,"
 
 ################################################################################
 # Prepare header options

doc/Makefile

@@ -28,12 +28,10 @@ MAKECONFIG_DIR=$(FRAMAC_SRC)/share
 
 include $(FRAMAC_SRC)/share/Makefile.common
 
-DOCDIR ?= "$(DESTDIR)${prefix}/share/doc"
 FRAMAC_DOCDIR ?= $(DOCDIR)/frama-c
 
 .PHONY: .force
 
-
 ###################
 # Frama-C Version #
 ###################
@@ -201,3 +199,13 @@ acsl/acsl-implementation.pdf: | acsl/acsl.pdf
 $(EACSL_DOC)/refman/e-acsl-implementation.pdf: | $(EACSL_DOC)/refman/e-acsl.pdf
 
 endif
+
+##############################################################################
+# HELP
+################################
+
+help::
+	@echo "Documentation installation configuration variable"
+	@echo "  - PREFIX: documentation will be in PREFIX/share/doc/frama-c"
+	@echo "  - DOCDIR: (overrides previous variable) documentation will be in DOCDIR/frama-c"
+	@echo "  - FRAMAC_DOCDIR: (overrides previous variable) documentation will be in FRAMAC_DOCDIR"

doc/developer/Makefile

@@ -43,7 +43,9 @@ DEPENDENCIES= $(FRAMAC_MODERN) $(GENERATED) frama-c-book.cls
 
 all: developer.pdf # check << restore check later
 
-FC_BINDIR:=$(FRAMAC_ROOT_SRCDIR)/bin
+# This variable does not exist anymore.
+# FC_BINDIR:=$(FRAMAC_ROOT_SRCDIR)/bin
+# Thus TODO: use `dune exec -- frama-c` for the following commands
 
 .PHONY: clean-tuto
 clean-tuto:

dune

@@ -21,4 +21,13 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (alias (name default) (deps (alias install)))
-(dirs src tools tests headers share bin)
+(dirs bin headers man share src tools tests)
+
+(executable
+ (name configurator)
+ (libraries dune-configurator str))
+
+(rule
+ (deps VERSION VERSION_CODENAME)
+ (targets config.sed python-3.7-available)
+ (action (run ./configurator.exe)))

ivette/INSTALL.md

@@ -43,8 +43,6 @@ command to run the server.
 From the `Frama-C` main directory, simply type:
 
 ```
-$ autoconf -f
-$ ./configure
 $ make -C ivette dist
 $ [sudo] make -C ivette install
 ```

ivette/Makefile

@@ -60,6 +60,14 @@ tsc: dome-pkg dome-templ
 	yarn run typecheck
 	yarn run lint --fix --cache --cache-location .eslint-cache
 
+# --------------------------------------------------------------------------
+# --- Help
+# --------------------------------------------------------------------------
+
+help::
+	@echo "Ivette installation configuration variables"
+	@echo "  - PREFIX: used to customize installation path"
+
 # --------------------------------------------------------------------------
 # --- Ivette Package Loader
 # --------------------------------------------------------------------------
@@ -159,7 +167,8 @@ include $(DOME)/template/makefile
 # --- Ivette Installation
 # --------------------------------------------------------------------------
 
-sinclude ../share/Makefile.config
+BINDIR=$(PREFIX)/bin
+LIBDIR=$(PREFIX)/lib
 
 dist-dir:
 	@echo "Cleaning dist"

man/dune

+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                                                        ;;
+;;  This file is part of Frama-C.                                         ;;
+;;                                                                        ;;
+;;  Copyright (C) 2007-2022                                               ;;
+;;    CEA (Commissariat à l'énergie atomique et aux énergies              ;;
+;;         alternatives)                                                  ;;
+;;                                                                        ;;
+;;  you can redistribute it and/or modify it under the terms of the GNU   ;;
+;;  Lesser General Public License as published by the Free Software       ;;
+;;  Foundation, version 2.1.                                              ;;
+;;                                                                        ;;
+;;  It is distributed in the hope that it will be useful,                 ;;
+;;  but WITHOUT ANY WARRANTY; without even the implied warranty of        ;;
+;;  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         ;;
+;;  GNU Lesser General Public License for more details.                   ;;
+;;                                                                        ;;
+;;  See the GNU Lesser General Public License version 2.1                 ;;
+;;  for more details (enclosed in the file licenses/LGPLv2.1).            ;;
+;;                                                                        ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(rule
+ (target frama-c.1.generated)
+ (deps frama-c.1.md)
+ (enabled_if %{bin-available:pandoc})
+ (action (run pandoc -s -t man %{deps} -o %{target}))
+)
+
+(rule
+ (alias check-man)
+ (deps frama-c.1 frama-c.1.generated)
+ (action (diff frama-c.1 frama-c.1.generated))
+)
+
+(install
+ (package frama-c)
+ (section man)
+ (files frama-c.1)
+)

nix/api-doc.nix

@@ -20,7 +20,6 @@ stdenv.mkDerivation rec {
   preConfigure = frama-c.preConfigure;
 
   buildPhase = ''
-    make config.sed
     dune build -j1 @doc
 
     cp -r _build/default/_doc/_html frama-c-api

nix/frama-c-checkers-shell.nix

 { lib
 , stdenv
-, autoconf
 , clang_10
 , frama-c-hdrck
 , git
@@ -11,7 +10,6 @@
 stdenv.mkDerivation rec {
   name = "frama-c-checkers-shell";
   buildInputs = [
-    autoconf
     clang_10
     frama-c-hdrck
     git

nix/frama-c.nix

@@ -8,12 +8,12 @@
 , wrapGAppsHook
 , writeText
 # Generic
-, autoconf
 , findlib
 # Frama-C build
 , apron
 , camlzip
 , dune_3
+, dune-configurator
 , dune-site
 , gcc9
 , graphviz
@@ -56,7 +56,6 @@ stdenvNoCC.mkDerivation rec {
     else gitignoreSource ./.. ;
 
   nativeBuildInputs = [
-    autoconf
     which
     wrapGAppsHook
   ];
@@ -65,6 +64,7 @@ stdenvNoCC.mkDerivation rec {
     apron
     camlzip
     dune_3
+    dune-configurator
     dune-site
     findlib
     gcc9
@@ -93,9 +93,10 @@ stdenvNoCC.mkDerivation rec {
 
   outputs = [ "out" "build_dir" ];
 
-  preConfigure = (if release_mode then "" else "autoconf \n") + ''
+  preConfigure = ''
     patchShebangs src/plugins/eva/gen-api.sh
     chmod +x src/plugins/eva/gen-api.sh
+    dune build @frama-c-configure
   '';
 
   # Do not use default parallel building, but allow 2 cores for Frama-C build
@@ -103,14 +104,13 @@ stdenvNoCC.mkDerivation rec {
   dune_opt = if release_mode then "--release" else "" ;
 
   buildPhase = ''
-    make config.sed
     dune build -j2 --display short $release_mode @install
     make tools/ptests/ptests.exe
     make tools/ptests/wtests.exe
   '';
 
   installFlags = [
-    "FRAMAC_INSTALLDIR=$(out)"
+    "INSTALLDIR=$(out)"
   ];
 
   # Simpler for our test target
@@ -121,9 +121,14 @@ stdenvNoCC.mkDerivation rec {
     tar -cf $build_dir/dir.tar .
   '';
 
-  # Required so that tests of external plugins can be excuted
+  # Nix moves these directories after they have been installed by Dune and
+  # compress manuals ...
+  # Note: Required so that tests of external plugins can be executed. Don't know
+  # why tests fail without them.
   postFixup = ''
     cp -r $out/share/doc $out/doc
+    cp -r $out/share/man $out/man
+    gzip -d $out/man/man1/*
   '';
 
   # Allow loading of external Frama-C plugins

nix/internal-tests.nix

@@ -10,12 +10,12 @@
 , wrapGAppsHook
 , writeText
 # Generic
-, autoconf
 , findlib
 # Frama-C build
 , apron
 , camlzip
 , dune_3
+, dune-configurator
 , dune-site
 , gcc9
 , graphviz
@@ -58,7 +58,6 @@ stdenvNoCC.mkDerivation rec {
   src = gitignoreSource ./..;
 
   nativeBuildInputs = [
-    autoconf
     which
     wrapGAppsHook
   ];
@@ -68,6 +67,7 @@ stdenvNoCC.mkDerivation rec {
     alt-ergo
     camlzip
     dune_3
+    dune-configurator
     dune-site
     findlib
     gcc9
@@ -101,15 +101,14 @@ stdenvNoCC.mkDerivation rec {
   outputs = [ "out" ];
 
   preConfigure = ''
-    autoconf
     patchShebangs src/plugins/eva/gen-api.sh
     chmod +x src/plugins/eva/gen-api.sh
+    dune build @frama-c-configure
   '';
 
   # Do not use default parallel building, but allow 2 cores for Frama-C build
   enableParallelBuilding = false;
   buildPhase = ''
-    make config.sed
     dune build -j2 --display short @install
     make tools/ptests/ptests.exe
     make tools/ptests/wtests.exe
@@ -134,7 +133,7 @@ stdenvNoCC.mkDerivation rec {
   '';
 
   installFlags = [
-    "FRAMAC_INSTALLDIR=$(out)"
+    "INSTALLDIR=$(out)"
   ];
 
   meta = {

nix/src-distrib.nix

@@ -19,10 +19,6 @@ stdenv.mkDerivation rec {
     git
   ];
 
-  configurePhase = ''
-    autoconf
-  '';
-
   preBuild = ''
     patchShebangs ./devel_tools/make-distrib.sh
   '';

opam/opam

@@ -87,16 +87,13 @@ tags: [
 ]
 
 build: [
-  ["autoconf"] {dev}
-  ["./configure" "--prefix" prefix]
-  [make "config.sed"]
   ["dune" "build" "-j%{jobs}%" "--release" "@install"]
   [make "-C" "doc" "download"] {with-doc}
 ]
 
 install: [
-  [make "install"]
-  [make "-C" "doc" "install"] {with-doc}
+  [make "INSTALLDIR=%{prefix}%" "MANDIR=%{mandir}%" "install"]
+  [make "PREFIX=%{prefix}%" "-C" "doc" "install"] {with-doc}
 ]
 
 run-test: [
@@ -112,7 +109,6 @@ depends: [
   "dune-configurator"
   "dune-private-libs"
   "dune-site"
-  "conf-autoconf" { build }
   ( ( "lablgtk" { >= "2.18.8" } & "conf-gnomecanvas" & "conf-gtksourceview"
       & ("ocamlgraph" { < "2.0" } | "ocamlgraph_gtk" ))
     | ( "lablgtk3" { >= "3.1.0" & os!="macos" }