Skip to content
Snippets Groups Projects
Commit 1e806051 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'feature/ci/manuals' into 'feature/bobot/jbuilder' 

Allow building manuals in CI

See merge request frama-c/frama-c!3646
parents 3856ce30 4e21a24c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
.gitlab-ci.yml
+ 22
− 0
View file @ 1e806051
......@@ -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
......
doc/aorai/.gitignore
+ 2
− 1
View file @ 1e806051
/transf
\ No newline at end of file
/transf
/transf.cm*
doc/build-manuals.sh
+ 55
− 27
View file @ 1e806051
#! /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
nix/headache.nix 0 → 100644
+ 32
− 0
View file @ 1e806051
{ 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 = [ ];
};
}
nix/manuals.nix 0 → 100644
+ 53
− 0
View file @ 1e806051
{ 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
'';
}
nix/pkgs.nix
+ 3
− 0
View file @ 1e806051
......@@ -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;
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment