Skip to content

GitLab

F
frama-c
Commit f4c58515 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files
Options

Merge branch 'feature/andre/release-script-and-manuals' into 'stable/scandium' 

Feature/andre/release script and manuals

See merge request frama-c/frama-c!2648
parents 03334023 0d5315d6
Hide whitespace changes
Inline Side-by-side
Showing with 213 additions and 290 deletions
bin/build-src-distrib.sh
View file @ f4c58515
......@@ -54,57 +54,51 @@ run () {
fi
}
GITHUB_DIR=./Frama-C-snapshot
GITHUB_GIT="git@github.com:Frama-C/Frama-C-snapshot.git"
GITLAB_DIR=./pub-frama-c
GITLAB_GIT="git@git.frama-c.com:pub/frama-c.git"
if test ! -d $GITHUB_DIR/.git; then
echo "WARNING: $GITHUB_DIR/.git directory not found; do you want to clone it? (y/n)"
if test ! -d $GITLAB_DIR/.git; then
echo "WARNING: $GITLAB_DIR/.git directory not found; do you want to clone it? (y/n)"
read CHOICE
case "${CHOICE}" in
"Y"|"y")
run "git clone $GITHUB_GIT"
run "git clone $GITLAB_GIT $GITLAB_DIR"
;;
*)
echo "github's Frama-C-snapshot project must be linked at $GITHUB_DIR \
echo "gitlab's public Frama-C project must be linked at $GITLAB_DIR \
(clone or symbolic link)"
exit 1
;&
esac
fi
GITHUB_BRANCH=$(git --git-dir=$GITHUB_DIR/.git rev-parse --abbrev-ref HEAD)
if test "$FINAL_RELEASE" = "yes" -a "$GITHUB_BRANCH" != "master"; then
echo "WARNING: your setup will commit (locally) a final release on a non-master branch of Frama-C-snapshot";
fi
if test "$FINAL_RELEASE" = "no" -a "$GITHUB_BRANCH" = "master";
then
echo "WARNING: your setup will commit (locally) an intermediate release on the master branch of Frama-C-snapshot"
GITLAB_BRANCH=$(git --git-dir=$GITLAB_DIR/.git rev-parse --abbrev-ref HEAD)
if test "$FRAMAC_BRANCH" != "$GITLAB_BRANCH"; then
echo "WARNING: switching pub-frama-c to current branch $FRAMAC_BRANCH"
run "git -C $GITLAB_DIR checkout -b $FRAMAC_BRANCH"
fi
GITHUB_WIKI_GIT="git@github.com:Frama-C/Frama-C-snapshot.wiki.git"
GITHUB_WIKI=./Frama-C-snapshot.wiki
if test ! -d $GITHUB_WIKI/.git; then
echo "WARNING: $GITHUB_WIKI/.git directory not found; do you want to clone it? (y/n)"
GITLAB_WIKI_GIT="git@git.frama-c.com:pub/frama-c.wiki"
GITLAB_WIKI=./frama-c.wiki
if test ! -d $GITLAB_WIKI/.git; then
echo "WARNING: $GITLAB_WIKI/.git directory not found; do you want to clone it? (y/n)"
read CHOICE
case "${CHOICE}" in
"Y"|"y")
run "git clone $GITHUB_WIKI_GIT"
run "git clone $GITLAB_WIKI_GIT"
;;
*)
echo "Frama-C-snapshot wiki must be linked at $GITHUB_WIKI \
echo "pub/frama-c wiki must be linked at $GITLAB_WIKI \
(clone or symbolic link)"
exit 1
;&
esac
fi
GITHUB_WIKI_BRANCH=$(git --git-dir=$GITHUB_WIKI/.git rev-parse --abbrev-ref HEAD)
GITLAB_WIKI_BRANCH=$(git --git-dir=$GITLAB_WIKI/.git rev-parse --abbrev-ref HEAD)
if test "$GITHUB_WIKI_BRANCH" != "master"; then
echo "WARNING: Frama-C-snapshot's wiki is not on the master branch";
if test "$GITLAB_WIKI_BRANCH" != "master"; then
echo "WARNING: pub/frama-c's wiki is not on the master branch";
fi
ACSL_GIT="git@github.com:acsl-language/acsl.git"
ACSL_GIT="git@gitlab.com:acsl-language/acsl.git"
ACSL_DIR="./doc/acsl"
if test \! -d $ACSL_DIR/.git ; then
echo "WARNING: $ACSL_DIR/.git directory not found; do you want to clone it? (y/n)"
......@@ -125,12 +119,6 @@ fi
MANUALS_DIR="./doc/manuals"
#if test \! -d $MANUALS_DIR/.git ; then
# echo "ERROR: $MANUALS_DIR/.git directory not found"
# echo "The Frama-C manuals repository must linked at $MANUALS_DIR (clone or symbolic link)"
# exit 1
#fi
#MANUALS_BRANCH=`git --git-dir=$MANUALS_DIR/.git rev-parse --abbrev-ref HEAD`
# push on frama-c.com only for final releases
if test "$FINAL_RELEASE" = "yes"; then
......@@ -149,11 +137,10 @@ BUILD_DIR="$BUILD_DIR_ROOT/frama-c"
echo "Frama-C Version : $FRAMAC_VERSION"
echo "Frama-C Branch : $FRAMAC_BRANCH"
echo "Final release : $FINAL_RELEASE"
echo "Frama-C-snapshot dir : $GITHUB_DIR"
echo "Frama-C-snapshot branch : $GITHUB_BRANCH"
echo "Frama-C-snapshot wiki : $GITHUB_WIKI"
echo "pub/frama-c dir : $GITLAB_DIR"
echo "pub/frama-c branch : $GITLAB_BRANCH"
echo "pub/frama-c wiki : $GITLAB_WIKI"
echo "Manuals Dir : $MANUALS_DIR"
#echo "Manuals Branch : $MANUALS_BRANCH"
if test "$FINAL_RELEASE" = "yes"; then
echo "Website Dir : $WEBSITE_DIR"
echo "Website Branch : $WEBSITE_BRANCH"
......@@ -198,15 +185,18 @@ case "${STEP}" in
run "doc/build-manuals.sh"
;&
1)
run "git -C $GITHUB_DIR reset --hard"
run "git -C $GITHUB_WIKI reset --hard"
run "git -C $GITLAB_DIR reset --hard"
run "git -C $GITLAB_WIKI reset --hard"
if test "$FINAL_RELEASE" = "yes"; then
run "git -C $WEBSITE_DIR reset --hard"
fi
;&
2)
step 2 "BUILDING THE SOURCE DISTRIBUTION"
if ! git diff-index --quiet HEAD --; then
# WARNING! MUST RUN git update-index BEFORE git diff-index!
# See: https://stackoverflow.com/questions/36367190/git-diff-files-output-changes-after-git-status
run "git update-index --refresh"
if ! git diff-index HEAD --; then
echo ""
echo "### WARNING: uncommitted git changes will be discarded when creating archive!"
echo "Proceed anyway? [y/N]"
......@@ -227,15 +217,9 @@ case "${STEP}" in
run "cd $BUILD_DIR; make -j OPEN_SOURCE=yes src-distrib"
# sanity check: markdown-report must be distributed
run "tar tf $BUILD_DIR/$TARGZ_FILENAME | grep -q src/plugins/markdown-report"
# cleanup Frama-C-snapshot
for file in $(git -C $GITHUB_DIR ls-files); do
run "rm $GITHUB_DIR/$file";
done
run "git -C $GITHUB_DIR clean -fx"
run "cd $GITHUB_DIR; tar --strip-components=1 -xzvf $BUILD_DIR/$TARGZ_FILENAME"
run "git -C $GITHUB_DIR add -A"
run "mkdir -p $GITHUB_WIKI/downloads"
run "cp $BUILD_DIR/$TARGZ_FILENAME $GITHUB_WIKI/downloads/"
# populate release assets in wiki
run "mkdir -p $GITLAB_WIKI/downloads"
run "cp $BUILD_DIR/$TARGZ_FILENAME $GITLAB_WIKI/downloads/"
if test "$FINAL_RELEASE" = "yes"; then
SPEC_FILE="$DOWNLOAD_DIR/$TARGZ_FILENAME"
run "rm -f $WEBSITE_DIR/$SPEC_FILE"
......@@ -284,83 +268,32 @@ case "${STEP}" in
5)
step 5 "COPYING AND STAGING THE DISTRIBUTED MANUALS"
PAGE_NAME=Frama-C-${FRAMAC_VERSION_AND_CODENAME}.md
WIKI_PAGE=$GITHUB_WIKI/$PAGE_NAME
run "mkdir -p $GITHUB_WIKI/manuals"
WIKI_PAGE=$GITLAB_WIKI/$PAGE_NAME
run "mkdir -p $GITLAB_WIKI/manuals"
run "sed -i -e '/<!-- LAST RELEASE -->/a \
- [${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})](Frama-C-${FRAMAC_VERSION_AND_CODENAME})' $GITHUB_WIKI/Home.md"
- [${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})](Frama-C-${FRAMAC_VERSION_AND_CODENAME})' $GITLAB_WIKI/Home.md"
echo "# Frama-C release ${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})" > $WIKI_PAGE
echo "## Sources" >> $WIKI_PAGE
echo " - [$TARGZ_FILENAME](downloads/$TARGZ_FILENAME)" >> $WIKI_PAGE
echo "" >> $WIKI_PAGE
echo "## Manuals" >> $WIKI_PAGE
for f in "user-manual" "acsl-implementation" "eva-manual" "plugin-development-guide" "rte-manual" "wp-manual" "metrics-manual" "aorai-manual"; do
echo "- [$f](manuals/$f-${FRAMAC_VERSION_AND_CODENAME}.pdf)" >> $WIKI_PAGE
run "cp $MANUALS_DIR/$f.pdf $GITHUB_WIKI/manuals/$f-${FRAMAC_VERSION_AND_CODENAME}.pdf"
run "git -C $GITHUB_WIKI add manuals/$f-${FRAMAC_VERSION_AND_CODENAME}.pdf"
if test "$FINAL_RELEASE" = "yes"; then
SPEC_FILE="$DOWNLOAD_DIR/$f-${FRAMAC_VERSION_AND_CODENAME}.pdf"
RELE_FILE="$DOWNLOAD_DIR/frama-c-$f.pdf"
run "rm -f $WEBSITE_DIR/$SPEC_FILE $WEBSITE_DIR/$RELE_FILE"
run "cp $MANUALS_DIR/$f.pdf $WEBSITE_DIR/$SPEC_FILE";
run "ln -s $f-${FRAMAC_VERSION_AND_CODENAME}.pdf $WEBSITE_DIR/$RELE_FILE";
run "git -C $WEBSITE_DIR add $SPEC_FILE"
run "git -C $WEBSITE_DIR add $RELE_FILE"
fi
done
for f in "aorai-example"; do
if test "$FINAL_RELEASE" = "yes"; then
SPEC_FILE="$DOWNLOAD_DIR/$f-${FRAMAC_VERSION_AND_CODENAME}.tgz"
RELE_FILE="$DOWNLOAD_DIR/frama-c-$f.tgz"
run "rm -f $WEBSITE_DIR/$SPEC_FILE $WEBSITE_DIR/$RELE_FILE"
run "cp $MANUALS_DIR/$f.tgz $WEBSITE_DIR/$SPEC_FILE";
run "ln -s $f-${FRAMAC_VERSION_AND_CODENAME}.tgz $WEBSITE_DIR/$RELE_FILE";
run "git -C $WEBSITE_DIR add $SPEC_FILE"
run "git -C $WEBSITE_DIR add $RELE_FILE"
fi
done
for fpath in $MANUALS_DIR/*; do
f=$(basename $fpath)
f_no_ext=${f%.*}
if [[ $f =~ ^frama-c ]]; then
echo "Skipping adding link to $f in wiki"
continue
fi
if [[ $f_no_ext = *${FRAMAC_VERSION_AND_CODENAME} ]]; then
echo "Skipping adding link to $f in wiki"
continue
fi
echo "- [$f](manuals/$f)" >> $WIKI_PAGE
run "cp $fpath $GITLAB_WIKI/manuals/"
run "git -C $GITLAB_WIKI add manuals/$f"
done
for f in "acsl"; do
ACSL_VERSION=`cat doc/acsl/ACSL_VERSION`
if test "$FINAL_RELEASE" = "yes"; then
SPEC_FILE="$DOWNLOAD_DIR/${f}-${ACSL_VERSION}.pdf"
RELE_FILE="$DOWNLOAD_DIR/$f.pdf"
run "rm -f $WEBSITE_DIR/$SPEC_FILE $WEBSITE_DIR/$RELE_FILE"
run "cp $MANUALS_DIR/$f.pdf $WEBSITE_DIR/$SPEC_FILE";
run "ln -s ${f}-${ACSL_VERSION}.pdf $WEBSITE_DIR/$RELE_FILE";
run "git -C $WEBSITE_DIR add $SPEC_FILE"
run "git -C $WEBSITE_DIR add $RELE_FILE"
fi
done
for f in "e-acsl-manual" "e-acsl-implementation"; do
echo "- [$f](manuals/${f}-${FRAMAC_VERSION_AND_CODENAME}.pdf)" >> $WIKI_PAGE
run "cp src/plugins/e-acsl/doc/manuals/$f.pdf $GITHUB_WIKI/manuals/${f}-${FRAMAC_VERSION_AND_CODENAME}.pdf"
run "git -C $GITHUB_WIKI add manuals/${f}-${FRAMAC_VERSION_AND_CODENAME}.pdf"
if test "$FINAL_RELEASE" = "yes"; then
SPEC_FILE="$DOWNLOAD_DIR/e-acsl/${f}-${FRAMAC_VERSION_AND_CODENAME}.pdf"
RELE_FILE="$DOWNLOAD_DIR/e-acsl/$f.pdf"
run "rm -f $WEBSITE_DIR/$SPEC_FILE $WEBSITE_DIR/$RELE_FILE"
run "cp src/plugins/e-acsl/doc/manuals/$f.pdf $WEBSITE_DIR/$SPEC_FILE"
run "ln -s ${f}-${FRAMAC_VERSION_AND_CODENAME}.pdf $WEBSITE_DIR/$RELE_FILE";
run "git -C $WEBSITE_DIR add $SPEC_FILE"
run "git -C $WEBSITE_DIR add $RELE_FILE"
fi
done
# E-ACSL manuals based on ACSL version number
for f in "e-acsl"; do
echo "- [$f](manuals/${f}-${ACSL_VERSION}.pdf)" >> $WIKI_PAGE
run "cp src/plugins/e-acsl/doc/manuals/$f.pdf $GITHUB_WIKI/manuals/${f}-${ACSL_VERSION}.pdf"
run "git -C $GITHUB_WIKI add manuals/${f}-${ACSL_VERSION}.pdf"
if test "$FINAL_RELEASE" = "yes"; then
SPEC_FILE="$DOWNLOAD_DIR/e-acsl/${f}-${ACSL_VERSION}.pdf"
RELE_FILE="$DOWNLOAD_DIR/e-acsl/$f.pdf"
run "rm -f $WEBSITE_DIR/$SPEC_FILE $WEBSITE_DIR/$RELE_FILE"
run "cp src/plugins/e-acsl/doc/manuals/$f.pdf $WEBSITE_DIR/$SPEC_FILE"
run "ln -s ${f}-${ACSL_VERSION}.pdf $WEBSITE_DIR/$RELE_FILE";
run "git -C $WEBSITE_DIR add $SPEC_FILE"
run "git -C $WEBSITE_DIR add $RELE_FILE"
fi
done
run "git -C $GITHUB_WIKI add $PAGE_NAME"
run "git -C $GITLAB_WIKI add $PAGE_NAME"
;;
*)
echo "Bad entry: ${STEP}"
......
doc/build-manuals.sh
View file @ f4c58515
......@@ -2,41 +2,79 @@
cd $(dirname $0)
set -e
build () {
if test -z "$2" ; then export NAME="$1"; else export NAME="$2"; fi
echo "##### Building $NAME"
cd $1
make $3 || (echo "######### $NAME failed" ; exit 1)
make install
echo "##### $NAME done"
cd ..
usage () {
echo "usage: $(basename $0) [help|clean|build] (default: build)"
}
mkdir -p manuals
if test $# -gt 1; then usage; exit 2; fi;
build userman
build developer "Developer manual" developer.pdf
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
build rte
build aorai
build metrics
build value
if [ ! -e acsl ]; then
echo "error: 'acsl' not in doc; clone git@github.com:acsl-language/acsl.git"
exit 1
fi
build acsl "ACSL manuals" all
cd ../src/plugins/wp/doc/
mkdir -p manuals
build manual WP
cd ../../e-acsl/doc
FC_SUFFIX=$(cat ../VERSION)-$(cat ../VERSION_CODENAME)
ACSL_SUFFIX=$(grep acslversion 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 retrive E-ACSL version from ../src/plugins/e-acsl/doc/refman/main.tex"
exit 1
fi
build () {
echo "##### Building $1"
make -C $(dirname $1) $(basename $1) || \
(echo "######### $1 failed" ; exit 1)
echo "##### $1 done"
# extract extension, add suffix, re-append extension
MANUAL=${2%.*}-$3.${2##*.}
cp -f $1 manuals/$MANUAL
echo "##### $MANUAL copied"
ln -srf manuals/$MANUAL manuals/$2
}
EACSL_DOC=../src/plugins/e-acsl/doc
build userman "E-ACSL userman"
export -f build
build refman "E-ACSL reference"
# 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 \
cd ../../../..
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
doc/release/branch.tex
View file @ f4c58515
......@@ -16,8 +16,8 @@ $\rightarrow$ Repository $\rightarrow$ Protected Branches.
\textbf{The \texttt{master} branch must be protected \emph{at all times}.
Parameters
\texttt{Allowed to merge} and \texttt{Allowed to push} must be set to
\texttt{Developers + Masters} during non-freeze times, and to
\texttt{Masters} during freeze time.}
\texttt{Developers + Maintainers} during non-freeze times, and to
\texttt{Maintainers} during freeze time.}
\section{Creating the branch}
......@@ -41,14 +41,14 @@ These branches are directly created on the gitlab server.
\end{enumerate}
What can be committed in this branch must follow the release schedule,
and go through Merge-requests. Everything else should go in \texttt{master},
which can then be reset to standard-level protection (Developers + Masters
which can then be reset to standard-level protection (Developers + Maintainers
allowed to push/merge).
\section{Creating the milestones}
Create the milestones for the next release on \textsf{Mantis}
\expertise{Julien, Boris} and \textsf{Gitlab}
\expertise{François, Julien, Boris}
\expertise{Julien} and \textsf{Gitlab}
\expertise{François, Julien}
\section{BTS}
......
doc/release/build.tex
View file @ f4c58515
......@@ -2,6 +2,16 @@
The procedure for creating the source distribution.
\section{Prerequisites}
\begin{itemize}
\item All tools needed to compile Frama-C (that you should have anyways)
\item \texttt{bash} v4.0 or higher
\item \texttt{git-lfs}
\item GNU \texttt{parallel}
\item a \TeX distribution
\end{itemize}
\section{Final checks}
\begin{itemize}
......@@ -137,7 +147,7 @@ manuals.
%\texttt{install} target below).
Run the script \texttt{doc/build-manuals.sh} to compile and install all manuals,
even for E-ACSL.
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}
......
doc/release/intro.tex
View file @ f4c58515
......@@ -21,7 +21,7 @@ roles, and we must distinguish between:
%% of the release for a specific architecture \expertise{none currently}.
\item[Web Site Maintainers:] they are responsible for updating the web site,
during the release and for possible later updates \expertise{Florent}.
\item[Release Manager:] he is responsible for the organisation of the
\item[Release Manager:] they are responsible for the organisation of the
release process
\end{description}
......
doc/userman/Makefile
View file @ f4c58515
......@@ -17,8 +17,8 @@ else
SILENT = -silent
endif
all: pdf
pdf: $(TARGET).tex $(FRAMAC_MODERN)
all: $(TARGET).pdf
$(TARGET).pdf: $(TARGET).tex $(FRAMAC_MODERN)
latexmk $(SILENT) -f -pdf $<
install:
......
opam/opam
View file @ f4c58515
opam-version: "2.0"
name: "frama-c"
synopsis: "Platform dedicated to the analysis of source code written in C"
version: "20.0"
version: "21.0-beta"
maintainer: "francois.bobot@cea.fr"
authors: [
"Michele Alberti"
......@@ -50,7 +50,7 @@ authors: [
homepage: "http://frama-c.com/"
license: "GNU Lesser General Public License version 2.1"
dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
doc: "http://frama-c.com/download/user-manual-20.0-Calcium.pdf"
doc: "http://frama-c.com/download/user-manual-21.0-Scandium.pdf"
bug-reports: "https://bts.frama-c.com/"
tags: [
"deductive"
......
src/plugins/e-acsl/doc/Makefile.common 0 → 100644
View file @ f4c58515
# Common makefile for both refman and userman
VERSION_FILE=$(wildcard ../../../../../VERSION)
EACSL_VERSION=$(shell cat $(VERSION_FILE))
FC_VERSION=$(shell cat $(VERSION_FILE))
include $(EACSL_DIR)/doc/support/MakeLaTeXModern
#################
# Generic rules #
#################
eacslversion.tex: Makefile
rm -f $@
printf '\\newcommand{\\eacslpluginversion}{$(EACSL_VERSION)\\xspace}\n' > $@
printf '\\newcommand{\\fcversion}{$(FC_VERSION)\\xspace}\n' >> $@
chmod a-w $@
%.1: %.mp
mpost -interaction=batchmode $<
%.mps: %.1
mv $< $@
%.pp: %.tex pp
./pp -utf8 $< > $@
%.pp: %.c pp
./pp -utf8 -c $< > $@
%.tex: %.ctex pp
rm -f $@
./pp $< > $@
chmod a-w $@
%.bnf: %.tex transf
rm -f $@
./transf $< > $@
chmod a-w $@
%_modern.bnf: %.tex transf
rm -f $@
./transf -modern $< > $@
chmod a-w $@
%.ml: %.mll
ocamllex $<
%.pdf: %.tex
pdflatex $*
makeindex $*
bibtex $*
pdflatex $*
pdflatex $*
%.cmo: %.ml
ocamlc -c $<
src/plugins/e-acsl/doc/refman/Makefile
View file @ f4c58515
default: all
EACSL_DIR=../..
include $(EACSL_DIR)/doc/Makefile.common
##########
# Inputs #
##########
VERSION_FILE=$(wildcard ../../../../../VERSION)
EACSL_VERSION=$(shell cat $(VERSION_FILE))
MAIN=main
DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
intro_modern.tex speclang_modern.tex \
......@@ -22,7 +24,6 @@ DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
##############
.PHONY: all e-acsl default
default: all
e-acsl: e-acsl-implementation.pdf e-acsl.pdf
all: e-acsl
......@@ -42,7 +43,6 @@ e-acsl.tex: e-acsl-implementation.tex Makefile
$(MAIN).pdf: $(DEPS_MODERN)
EACSL_DIR=../..
DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
install: e-acsl-implementation.pdf e-acsl.pdf
mkdir -p $(EACSL_DIR)/doc/manuals
......@@ -50,11 +50,6 @@ install: e-acsl-implementation.pdf e-acsl.pdf
include $(EACSL_DIR)/doc/support/MakeLaTeXModern
eacslversion.tex: Makefile $(VERSION_FILE)
rm -f $@
printf '\\newcommand{\\eacslversion}{$(EACSL_VERSION)}' > $@
chmod a-w $@
.PHONY: clean
clean:
rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \
......@@ -73,47 +68,3 @@ transf: transf.cmo transfmain.cmo
ocamlc -o $@ $^
transfmain.cmo: transf.cmo
#################
# Generic rules #
#################
%.1: %.mp
mpost -interaction=batchmode $<
%.mps: %.1
mv $< $@
%.pp: %.tex pp
./pp -utf8 $< > $@
%.pp: %.c pp
./pp -utf8 -c $< > $@
%.tex: %.ctex pp
rm -f $@
./pp $< > $@
chmod a-w $@
%.bnf: %.tex transf
rm -f $@
./transf $< > $@
chmod a-w $@
%_modern.bnf: %.tex transf
rm -f $@
./transf -modern $< > $@
chmod a-w $@
%.ml: %.mll
ocamllex $<
%.pdf: %.tex
pdflatex $*
makeindex $*
bibtex $*
pdflatex $*
pdflatex $*
%.cmo: %.ml
ocamlc -c $<
src/plugins/e-acsl/doc/refman/changes_modern.tex
View file @ f4c58515
......@@ -124,7 +124,7 @@ in \lstinline|\\at|}
{
\section{Changes in \eacsl Implementation}
\subsection*{Version \eacslversion}
\subsection*{Version \eacslpluginversion}
\begin{itemize}
\item \changeinsection{reals}{support of rational numbers and operations}
......
src/plugins/e-acsl/doc/refman/intro_modern.tex
View file @ f4c58515
......@@ -4,7 +4,7 @@
This document is a reference manual for
\ifthenelse{\boolean{PrintImplementationRq}}%
{the \eacsl implementation provided by the \eacsl plug-in~\cite{eacsl-plugin}
(version\eacslversion) of the \framac framework~\cite{framac}.}%
(version\eacslpluginversion) of the \framac framework~\cite{framac}.}%
{E-ACSL.}
\eacsl is an acronym for ``Executable ANSI/ISO C
Specification Language''. It is an ``executable'' subset of
......
src/plugins/e-acsl/doc/refman/main.tex
View file @ f4c58515
......@@ -24,8 +24,8 @@
\usepackage{alltt}
\makeindex
\newcommand{\acslversion}{1.14\xspace}
\newcommand{\version}{\acslversion\xspace}
\newcommand{\eacsllangversion}{1.14\xspace}
\newcommand{\version}{\eacsllangversion\xspace}
\renewcommand{\textfraction}{0.01}
\renewcommand{\topfraction}{0.99}
......@@ -36,9 +36,9 @@
\hbadness=10000
\ifthenelse{\boolean{PrintImplementationRq}}%
{\coverpage{\vbox{\mbox{E-ACSL Version \version}\\[5mm]
{\coverpage{\vbox{\mbox{E-ACSL Version \eacsllangversion}\\[5mm]
\mbox{\huge{Implementation in Frama-C plug-in E-ACSL}}\\[2mm]
\mbox{\huge{version \eacslversion{}}}}}}%
\mbox{\huge{version \eacslpluginversion{}}}}}}%
{\coverpage{\vbox{\mbox{E-ACSL}\\[2mm]\vbox{\mbox{\huge{Executable ANSI/ISO C
Specification Language}}}\\[2mm]
\mbox{Version \version}}}}
......@@ -48,7 +48,7 @@
\vfill
\title{E-ACSL\\[5mm]\huge{Executable ANSI/ISO C Specification Language}}%
{Version \version{}\ifthenelse{\boolean{PrintImplementationRq}}%
{~--~Frama-C plug-in E-ACSL version \eacslversion}{}}
{~--~Frama-C plug-in E-ACSL version \eacslpluginversion}{}}
\author{Julien Signoles}
......