From fd04f42def2a2f2bfda59df0dae99700abb998cf Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Thu, 17 Nov 2022 18:48:11 +0100 Subject: [PATCH] [devman] start documenting remaining Makefiles --- doc/developer/advance.tex | 13 ++++----- doc/developer/tutorial/hello/src/Makefile | 16 +++++++++++ .../tutorial/hello/src/Makefile.test | 27 ------------------- doc/frama-c-book.cls | 8 ++++++ 4 files changed, 29 insertions(+), 35 deletions(-) create mode 100644 doc/developer/tutorial/hello/src/Makefile delete mode 100644 doc/developer/tutorial/hello/src/Makefile.test diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex index 1dc23e29441..49e246def29 100644 --- a/doc/developer/advance.tex +++ b/doc/developer/advance.tex @@ -192,16 +192,13 @@ Note that \verb|camlp5| is not among the dependencies declared in Since the adoption of Dune, \framac's \texttt{Makefile}s were largely simplified. They are still used for some tasks, partially due to conciseness (\verb|make| is shorter than \verb|dune build|), partially because some tasks -are better suited for them. +are better suited for them. Some standards targets are defined in various +Makefiles that are installed in \framac's shared directory. -Plug-in developers usually just need to copy and paste the existing Makefile -template and rename the opam file name (\verb|frama-c-<plugin>.opam|). +A minimal plugin's \verb|Makefile| can thus be the following: -This Makefile reuses code from other Makefiles, distributed in Frama-C's -{\em share} directory, such as \verb|Makefile.testing|, -\verb|Makefile.installation|, etc. Their names indicate the kinds of features -they provide. Many are shortcuts for specific dune targets, but they also -provide linting and copyright headers-related features. +\listingname{Makefile} +\makeinput{./tutorial/hello/src/Makefile} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/doc/developer/tutorial/hello/src/Makefile b/doc/developer/tutorial/hello/src/Makefile new file mode 100644 index 00000000000..61d832e1315 --- /dev/null +++ b/doc/developer/tutorial/hello/src/Makefile @@ -0,0 +1,16 @@ +FRAMAC_SHARE:=$(shell frama-c -print-share-path) + +sinclude ${FRAMAC_SHARE}/Makefile.common + +########################################################################## + +# Tests + +include ${FRAMAC_SHARE}/Makefile.testing + +########################################################################## + +# Install + +include ${FRAMAC_SHARE}/Makefile.installation + diff --git a/doc/developer/tutorial/hello/src/Makefile.test b/doc/developer/tutorial/hello/src/Makefile.test deleted file mode 100644 index 7ff38b3f00b..00000000000 --- a/doc/developer/tutorial/hello/src/Makefile.test +++ /dev/null @@ -1,27 +0,0 @@ -########################################################################## -# # -# 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). # -# # -########################################################################## - -FRAMAC_SHARE := $(shell frama-c-config -print-share-path) -PLUGIN_NAME = Hello -PLUGIN_CMO = hello_options hello_print hello_run -PLUGIN_TESTS_DIRS := hello -include $(FRAMAC_SHARE)/Makefile.dynamic diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls index cb6f16df585..532f4dbfe19 100644 --- a/doc/frama-c-book.cls +++ b/doc/frama-c-book.cls @@ -391,10 +391,18 @@ literate=% basicstyle=\lp@inline,% } +\lstdefinestyle{make-basic}{% + language=Makefile,% + style=framac-code-style,% + basicstyle=\lp@inline,% +} + \newcommand{\ocamlinput}[2][]{\lstinputlisting[style=ocaml-basic,#1]{#2}} \lstnewenvironment{ocamlcode}[1][]{\lstset{style=ocaml-basic,#1}}{} \newcommand{\duneinput}[2][]{\lstinputlisting[style=dune-basic,#1]{#2}} \lstnewenvironment{dunecode}[1][]{\lstset{style=dune-basic,#1}}{} +\newcommand{\makeinput}[2][]{\lstinputlisting[style=make-basic,#1]{#2}} +\lstnewenvironment{makecode}[1][]{\lstset{style=make-basic,#1}}{} % -------------------------------------------------------------------------- \lstdefinelanguage{Why}{% morekeywords={ -- GitLab