Commit 1e5a4ec5 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'fix/doc-makefile' into 'master'

[Doc] Update the doc Makefile

See merge request frama-c/frama-c!3463
parents dc74109d 14f0da39
......@@ -91,6 +91,7 @@ autom4te.cache
/doc/*/*.fls
/doc/*/*.fdb_latexmk
/doc/*/*.synctex.gz
/doc/*/frama-c-affiliation.tex
/doc/acsl/
......
......@@ -20,10 +20,8 @@
# #
##########################################################################
# This file just download the manuals in the released version
all:download
# default when make is invoked without target
default:
FRAMAC_SRC=..
MAKECONFIG_DIR=$(FRAMAC_SRC)/share
......@@ -33,23 +31,26 @@ include $(FRAMAC_SRC)/share/Makefile.common
DOCDIR ?= "$(DESTDIR)${prefix}/share/doc"
FRAMAC_DOCDIR ?= $(DOCDIR)/frama-c
.PHONY: .force
###################
# Frama-C Version #
###################
VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' $(FRAMAC_SRC)/VERSION)
VERSION_CODENAME=$(shell cat $(FRAMAC_SRC)/VERSION_CODENAME)
VERSION_SAFE=$(subst ~,-,$(VERSION))
ifeq ($(findstring +dev,$(VERSION)),+dev)
DEVELOPMENT=yes
else
DEVELOPMENT=no
endif
###
# Developpement version, generate the manuals
default: all
.PHONY: force
else
# Distributed version, download the manuals by default
default: download
MANUALS=acsl
......@@ -63,22 +64,131 @@ FILES= $(addprefix manuals/, \
$(addsuffix .pdf, $(MANUALS)) \
)
ifeq ($(DEVELOPMENT),yes)
download: force
@echo "You can't download the manuals in this way for the development version"
else
download: force
download: .force
$(MKDIR) manuals
wget -nv -N -P manuals \
$(addprefix http://frama-c.com/download/,$(addsuffix -$(VERSION).pdf, $(VERSIONED_MANUALS))) \
$(addprefix http://frama-c.com/download/,$(addsuffix .pdf, $(MANUALS)))
endif
install:
$(MKDIR) $(FRAMAC_DOCDIR)
$(CP) $(FILES) $(FRAMAC_DOCDIR)
endif
###################
# Generation #
###################
FC_SUFFIX=$(VERSION_SAFE)-$(VERSION_CODENAME)
clean::
$(RM) manuals/*.pdf
$(RM) manuals/*.tgz
$(MAKE) -C userman clean
$(MAKE) -C developer clean
$(MAKE) -C rte clean
$(MAKE) -C aorai clean
$(MAKE) -C value clean
$(MAKE) -C metrics clean
$(MAKE) -C ../src/plugins/wp/doc/manual clean
all: \
manuals/user-manual-$(FC_SUFFIX).pdf \
manuals/plugin-development-guide-$(FC_SUFFIX).pdf \
manuals/rte-manual-$(FC_SUFFIX).pdf \
manuals/aorai-manual-$(FC_SUFFIX).pdf \
manuals/aorai-example-$(FC_SUFFIX).tgz \
manuals/eva-manual-$(FC_SUFFIX).pdf \
manuals/metrics-manual-$(FC_SUFFIX).pdf \
manuals/wp-manual-$(FC_SUFFIX).pdf \
manuals/%:
mkdir --parent manuals
$(CP) $< $@
%.pdf:
$(PRINT) Generating $@
$(MAKE) -C $(@D) $(@F)
%.tgz:
$(PRINT) Generating $@
$(MAKE) -C $(@D) $(@F)
manuals/user-manual-$(FC_SUFFIX).pdf: userman/userman.pdf
manuals/plugin-development-guide-$(FC_SUFFIX).pdf: developer/developer.pdf
manuals/rte-manual-$(FC_SUFFIX).pdf: rte/main.pdf
manuals/aorai-manual-$(FC_SUFFIX).pdf: aorai/main.pdf
manuals/aorai-example-$(FC_SUFFIX).tgz: aorai/aorai-example.tgz
manuals/eva-manual-$(FC_SUFFIX).pdf: value/main.pdf
manuals/metrics-manual-$(FC_SUFFIX).pdf: metrics/metrics.pdf
manuals/wp-manual-$(FC_SUFFIX).pdf: ../src/plugins/wp/doc/manual/wp.pdf
###################
# ACSL #
###################
ifeq ($(wildcard acsl),)
# ACSL and E-ACSL manuals requires a clone of the acsl repository
$(info 'acsl' not in doc; try: git clone https://github.com/acsl-language/acsl.git)
else
ACSL_SUFFIX=$(shell grep acslversion acsl/version.tex | sed 's/.*{\([^{}\\]*\).*/\1/')
clean::
$(MAKE) -C acsl clean
all: \
manuals/acsl-implementation-$(FC_SUFFIX).pdf \
manuals/acsl-$(ACSL_SUFFIX).pdf \
manuals/acsl-implementation-$(FC_SUFFIX).pdf: acsl/acsl-implementation.pdf
manuals/acsl-$(ACSL_SUFFIX).pdf: acsl/acsl.pdf
###################
# E-ACSL #
###################
EACSL_DOC=../src/plugins/e-acsl/doc
EACSL_SUFFIX=$(shell grep 'newcommand{\\eacsllangversion' $(EACSL_DOC)/refman/main.tex | sed 's/.*{\([^{}\\]*\).*/\1/')
ifeq ($(EACSL_SUFFIX),)
$(info could not retrieve E-ACSL version from ../src/plugins/e-acsl/doc/refman/main.tex")
else
# Sanity check: version differences between Frama-C, and E-ACSL
ifneq ($(ACSL_SUFFIX),$(EACSL_SUFFIX))
$(info WARNING: different versions for ACSL and E-ACSL manuals: $(ACSL_SUFFIX) versus $(EACSL_SUFFIX))
endif
clean::
$(MAKE) -C $(EACSL_DOC)/refman/ clean
$(MAKE) -C $(EACSL_DOC)/userman/ clean
all: \
manuals/e-acsl-implementation-$(FC_SUFFIX).pdf \
manuals/e-acsl-manual-$(FC_SUFFIX).pdf \
manuals/e-acsl-$(EACSL_SUFFIX).pdf \
manuals/e-acsl-implementation-$(FC_SUFFIX).pdf: $(EACSL_DOC)/refman/e-acsl-implementation.pdf
manuals/e-acsl-manual-$(FC_SUFFIX).pdf: $(EACSL_DOC)/userman/main.pdf
manuals/e-acsl-$(EACSL_SUFFIX).pdf: $(EACSL_DOC)/refman/e-acsl.pdf
endif
# 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): we have to wait for one to complete
# before making the other
acsl/acsl-implementation.pdf: | acsl/acsl.pdf
$(EACSL_DOC)/refman/e-acsl-implementation.pdf: | $(EACSL_DOC)/refman/e-acsl.pdf
endif
#! /usr/bin/env bash
# GNU parallel needs to be installed
if ! command -v parallel >/dev/null 2>/dev/null; then
echo "parallel is required"
exit 127
fi
# latexmk needs to be installed
if ! command -v latexmk >/dev/null 2>/dev/null; then
echo "latexmk is required"
exit 127
fi
cd $(dirname $0)
usage () {
echo "usage: $(basename $0) [help|clean|build] (default: build)"
}
if test $# -gt 1; then usage; exit 2; fi;
if test $# -eq 1; then
case $1 in
"help") usage; exit 0;;
"clean") rm -f manuals/*.pdf; exit 0;;
"build") ;;
*) usage; exit 2;;
esac
fi
set -e
if [ ! -e acsl ]; then
echo "error: 'acsl' not in doc; try: git clone git@github.com:acsl-language/acsl.git"
exit 1
fi
mkdir -p manuals
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
echo "error: could not retrieve E-ACSL version from ../src/plugins/e-acsl/doc/refman/main.tex"
exit 1
fi
build () {
echo "##### Building $1"
set +e
make -C $(dirname $1) $(basename $1)
ret=$?
if [ $ret -eq 0 ]; then
echo "##### $1 done"
else
echo "######### $1 failed"
exit 1
fi
# extract extension, add suffix, re-append extension
MANUAL=${2%.*}-$3.${2##*.}
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
# Sanity check: version differences between Frama-C, ACSL and E-ACSL
if [ "$ACSL_SUFFIX" != "$EACSL_SUFFIX" ]; then
echo "WARNING: different versions for ACSL and E-ACSL manuals: $ACSL_SUFFIX versus $EACSL_SUFFIX"
fi
if [ "$ACSL_IMPLEM_VERSION" != "$FC_VERSION" ]; then
echo "WARNING: ACSL implementation refers to a different Frama-C version: $ACSL_IMPLEM_VERSION versus $FC_VERSION"
fi
......@@ -163,25 +163,10 @@ manuals.
%\texttt{doc/manuals} in order to update the manuals (required by the
%\texttt{install} target below).
Run the script \texttt{doc/build-manuals.sh} to compile and install all manuals,
even for E-ACSL. Note that this script requires \texttt{GNU parallel}.
Otherwise, if you want to do it \textbf{manually}, in each directory:
\begin{shell}
make
make install
\end{shell}
The result is installed in \texttt{doc/manuals/}.
For E-ACSL, the \textbf{manual} steps (ignore if you used the script)
are slightly different: \texttt{make} and
\texttt{make install} must be run in the following directories:
\begin{itemize}
\item \texttt{src/plugins/e-acsl/doc/refman}
\item \texttt{src/plugins/e-acsl/doc/userman}
\end{itemize}
In the \texttt{doc} directory, just run \texttt{make} to compile
and install all manuals, together with some final coherence checks with
respect to the current Frama-C implementation (notably
for the developer manual and ACSL implementation manual).
% No longer use git annex (as recommended by VP)
%\paragraph{Getting the manuals on the web (ultimately)}
......
Supports Markdown
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