diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index ae0d387ea3276a2613dace64ddc957e2820b6172..e5be8a656f1cb8216b2c675115c034930444412a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -93,6 +93,28 @@ volatile:
 ################################################################################
 ### DISTRIB
 
+manuals: # TODO: restore doc companions
+  stage: distrib_and_compatibility
+  script:
+    - nix-build nix/pkgs.nix -A ocamlPackages.manuals
+  tags:
+    - nix
+  when: manual
+  artifacts:
+    paths:
+      - result/acsl-implementation.pdf
+      - result/acsl.pdf
+      - result/aorai-manual.pdf
+      - result/e-acsl-implementation.pdf
+      - result/e-acsl-manual.pdf
+      - result/e-acsl.pdf
+      - result/eva-manual.pdf
+      - result/metrics-manual.pdf
+      - result/plugin-development-guide.pdf
+      - result/rte-manual.pdf
+      - result/user-manual.pdf
+      - result/wp-manual.pdf
+
 ################################################################################
 ### PUBLIC
 
diff --git a/doc/aorai/.gitignore b/doc/aorai/.gitignore
index 7af91cd419db82b54ead3e68b22a67a87ef72b18..4a1902eddb22e656993e3d067f609a7bc4dc4180 100644
--- a/doc/aorai/.gitignore
+++ b/doc/aorai/.gitignore
@@ -1 +1,2 @@
-/transf
\ No newline at end of file
+/transf
+/transf.cm*
diff --git a/doc/build-manuals.sh b/doc/build-manuals.sh
index 72d8a48ea72ec8f2e2459243fec599dd233debef..3f330a4ea60ce67b3216d7da404d3af2b932f8f6 100755
--- a/doc/build-manuals.sh
+++ b/doc/build-manuals.sh
@@ -1,9 +1,10 @@
 #! /usr/bin/env bash
 
-# GNU parallel needs to be installed
+# Look for GNU parallel
+PARALLEL=1
 if ! command -v parallel >/dev/null 2>/dev/null; then
-    echo "parallel is required"
-    exit 127
+    echo "parallel not found, building in sequential"
+    PARALLEL=0
 fi
 
 # latexmk needs to be installed
@@ -43,7 +44,6 @@ FC_SUFFIX=$(cat ../VERSION)-$(cat ../VERSION_CODENAME)
 FC_SUFFIX="$(echo ${FC_SUFFIX} | sed -e "s/~/-/")"
 ACSL_SUFFIX=$(grep acslversion acsl/version.tex | sed 's/.*{\([^{}\\]*\).*/\1/')
 FC_VERSION=$(cat ../VERSION)
-ACSL_IMPLEM_VERSION=$(grep fcversion acsl/version.tex | sed 's/.*{\([^{}\\]*\).*/\1/')
 EACSL_SUFFIX=$(grep 'newcommand{\\eacsllangversion' ../src/plugins/e-acsl/doc/refman/main.tex | sed 's/.*{\([^{}\\]*\).*/\1/')
 # sanity check
 if [ "$EACSL_SUFFIX" = "" ]; then
@@ -63,42 +63,70 @@ build () {
         echo "######### $1 failed"
         exit 1
     fi
-    # extract extension, add suffix, re-append extension
-    MANUAL=${2%.*}-$3.${2##*.}
+    if [ "$NO_SUFFIX" == "yes" ] ; then
+        MANUAL=$2
+    else
+        # extract extension, add suffix, re-append extension
+        MANUAL=${2%.*}-$3.${2##*.}
+    fi
     cp -f $1 manuals/$MANUAL
     echo "##### $MANUAL copied"
-    
+
 }
 
 EACSL_DOC=../src/plugins/e-acsl/doc
 
 export -f build
 
-# Note: The makefiles of ACSL/E-ACSL are not parallelizable when producing both
-# acsl.pdf and acsl-implementation.pdf (race conditions in intermediary files,
-# leading to non-deterministic errors).
-# Therefore, we perform a second call to parellel for these files.
-SHELL=(type -p bash) parallel --halt soon,fail=1 --csv build {1} {2} {3} ::: \
-userman/userman.pdf,user-manual.pdf,$FC_SUFFIX \
-developer/developer.pdf,plugin-development-guide.pdf,$FC_SUFFIX \
-rte/main.pdf,rte-manual.pdf,$FC_SUFFIX \
-aorai/main.pdf,aorai-manual.pdf,$FC_SUFFIX \
-aorai/aorai-example.tgz,aorai-example.tgz,$FC_SUFFIX \
-value/main.pdf,eva-manual.pdf,$FC_SUFFIX \
-metrics/metrics.pdf,metrics-manual.pdf,$FC_SUFFIX \
-../src/plugins/wp/doc/manual/wp.pdf,wp-manual.pdf,$FC_SUFFIX \
-acsl/acsl-implementation.pdf,acsl-implementation.pdf,$FC_SUFFIX \
-$EACSL_DOC/refman/e-acsl-implementation.pdf,e-acsl-implementation.pdf,$FC_SUFFIX \
-$EACSL_DOC/userman/main.pdf,e-acsl-manual.pdf,$FC_SUFFIX \
-
-SHELL=(type -p bash) parallel --halt soon,fail=1 --csv build {1} {2} {3} ::: \
-acsl/acsl.pdf,acsl.pdf,$ACSL_SUFFIX \
-$EACSL_DOC/refman/e-acsl.pdf,e-acsl.pdf,$EACSL_SUFFIX
+if [[ $PARALLEL -eq 1 ]]; then
+    # Note: The makefiles of ACSL/E-ACSL are not parallelizable when producing both
+    # acsl.pdf and acsl-implementation.pdf (race conditions in intermediary files,
+    # leading to non-deterministic errors).
+    # Therefore, we perform a second call to parellel for these files.
+    SHELL=(type -p bash) parallel --halt soon,fail=1 --csv build {1} {2} {3} ::: \
+    userman/userman.pdf,user-manual.pdf,$FC_SUFFIX \
+    developer/developer.pdf,plugin-development-guide.pdf,$FC_SUFFIX \
+    rte/main.pdf,rte-manual.pdf,$FC_SUFFIX \
+    aorai/main.pdf,aorai-manual.pdf,$FC_SUFFIX \
+    aorai/aorai-example.tgz,aorai-example.tgz,$FC_SUFFIX \
+    value/main.pdf,eva-manual.pdf,$FC_SUFFIX \
+    metrics/metrics.pdf,metrics-manual.pdf,$FC_SUFFIX \
+    ../src/plugins/wp/doc/manual/wp.pdf,wp-manual.pdf,$FC_SUFFIX \
+    acsl/acsl-implementation.pdf,acsl-implementation.pdf,$FC_SUFFIX \
+    $EACSL_DOC/refman/e-acsl-implementation.pdf,e-acsl-implementation.pdf,$FC_SUFFIX \
+    $EACSL_DOC/userman/main.pdf,e-acsl-manual.pdf,$FC_SUFFIX \
+
+    SHELL=(type -p bash) parallel --halt soon,fail=1 --csv build {1} {2} {3} ::: \
+    acsl/acsl.pdf,acsl.pdf,$ACSL_SUFFIX \
+    $EACSL_DOC/refman/e-acsl.pdf,e-acsl.pdf,$EACSL_SUFFIX
+else
+    build userman/userman.pdf user-manual.pdf $FC_SUFFIX
+    build developer/developer.pdf plugin-development-guide.pdf $FC_SUFFIX
+    build rte/main.pdf rte-manual.pdf $FC_SUFFIX
+    build aorai/main.pdf aorai-manual.pdf $FC_SUFFIX
+    build aorai/aorai-example.tgz aorai-example.tgz $FC_SUFFIX
+    build value/main.pdf eva-manual.pdf $FC_SUFFIX
+    build metrics/metrics.pdf metrics-manual.pdf $FC_SUFFIX
+    build ../src/plugins/wp/doc/manual/wp.pdf wp-manual.pdf $FC_SUFFIX
+    build acsl/acsl.pdf acsl.pdf $ACSL_SUFFIX
+    build acsl/acsl-implementation.pdf acsl-implementation.pdf $FC_SUFFIX
+    build $EACSL_DOC/refman/e-acsl-implementation.pdf e-acsl-implementation.pdf $FC_SUFFIX
+    build $EACSL_DOC/userman/main.pdf e-acsl-manual.pdf $FC_SUFFIX
+    build $EACSL_DOC/refman/e-acsl.pdf e-acsl.pdf $EACSL_SUFFIX
+fi
 
 # Sanity check: version differences between Frama-C, ACSL and E-ACSL
+FAIL=0
 if [ "$ACSL_SUFFIX" != "$EACSL_SUFFIX" ]; then
     echo "WARNING: different versions for ACSL and E-ACSL manuals: $ACSL_SUFFIX versus $EACSL_SUFFIX"
+    FAIL=1
 fi
+
+# The file fc_version.tex is created by the compilation of the implementation manual
+ACSL_IMPLEM_VERSION=$(grep fcversion acsl/fc_version.tex | sed 's/.*{\([^{}\\]*\).*/\1/')
+
 if [ "$ACSL_IMPLEM_VERSION" != "$FC_VERSION" ]; then
     echo "WARNING: ACSL implementation refers to a different Frama-C version: $ACSL_IMPLEM_VERSION versus $FC_VERSION"
+    FAIL=1
 fi
+exit $FAIL
diff --git a/nix/headache.nix b/nix/headache.nix
new file mode 100644
index 0000000000000000000000000000000000000000..258016810ddcf07992f3c430e46afd05c8b05135
--- /dev/null
+++ b/nix/headache.nix
@@ -0,0 +1,32 @@
+{ lib
+, camomile
+, fetchFromGitHub
+, buildDunePackage
+, cmdliner
+}:
+
+buildDunePackage rec {
+  version = "v1.05";
+  pname = "headache";
+
+  src = fetchFromGitHub {
+    owner = "Frama-C";
+    repo = pname;
+    rev = version;
+    sha256 = "036lrcxh23j2rrj91wlgq9piyyv1vh82wjy63z1l1ggkkhfs7d8r";
+  };
+
+  useDune2 = true;
+
+  buildInputs = [
+    cmdliner
+    camomile
+  ];
+
+  meta = with lib; {
+    homepage = https://github.com/Frama-C/headache/;
+    description = "Automatic generation of files headers";
+    license = licenses.gpl2;
+    maintainers = [ ];
+  };
+}
diff --git a/nix/manuals.nix b/nix/manuals.nix
new file mode 100644
index 0000000000000000000000000000000000000000..e6883788152d7578ac4fac1fc04fa22b5e119a0a
--- /dev/null
+++ b/nix/manuals.nix
@@ -0,0 +1,53 @@
+{ lib
+, stdenv
+, frama-c
+, headache
+, texlive
+} :
+
+stdenv.mkDerivation rec {
+  pname = "manuals";
+  version = frama-c.version;
+  slang = frama-c.slang;
+
+
+  build_dir = frama-c.build_dir + "/dir.tar";
+  acsl = fetchGit {
+    url = "https://github.com/acsl-language/acsl.git";
+    name = "acsl";
+  };
+  srcs = [
+    build_dir
+    acsl
+  ] ;
+
+  sourceRoot = ".";
+
+  buildInputs = frama-c.buildInputs ++ [
+    frama-c
+    headache
+    texlive.combined.scheme-full
+  ];
+
+  postUnpack = ''
+    mv acsl doc
+  '' ;
+
+  postPatch = ''
+    patchShebangs .
+  '' ;
+
+  # Keep main configuration
+  configurePhase = ''
+    true
+  '';
+
+  buildPhase = ''
+    NO_SUFFIX="yes" ./doc/build-manuals.sh
+  '';
+
+  installPhase = ''
+    mkdir -p $out
+    cp ./doc/manuals/*.pdf $out
+  '';
+}
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
index a36dae2d38ba4a13c5e468cbf5f9248b222761a2..46ce47e4a8d02653f768db37cd34e3835380861d 100644
--- a/nix/pkgs.nix
+++ b/nix/pkgs.nix
@@ -4,6 +4,7 @@ let
     # External Packages
     alt-ergo = oself.callPackage ./alt-ergo.nix {};
     camlzip = oself.callPackage ./camlzip.nix {};
+    headache = oself.callPackage ./headache.nix {};
     ocp-indent = oself.callPackage ./ocp-indent.nix {};
     psmt2-frontend = oself.callPackage ./psmt2-frontend.nix {};
     why3 = oself.callPackage ./why3.nix {};
@@ -13,6 +14,8 @@ let
     # Tests
     main-tests = oself.callPackage ./main-tests.nix {};
     plugins-tests = oself.callPackage ./plugins-tests.nix {};
+    # Release
+    manuals = oself.callPackage ./manuals.nix {};
   };
   overlay = self: super: {
     niv = (import sources.niv {}).niv;