From c9dfbd1622f08966ee0e4c479cef18b8d4406ffd Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 18 Nov 2022 12:27:03 +0100
Subject: [PATCH] [devman] finish Makefile section
---
doc/developer/advance.tex | 18 ++++++++++++++++++
doc/developer/tutorial/hello/src/Makefile | 11 ++++-------
2 files changed, 22 insertions(+), 7 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 6cae8c5de9a..d4472872244 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -200,6 +200,24 @@ A minimal plugin's \verb|Makefile| can thus be the following:
\listingname{Makefile}
\makeinput{./tutorial/hello/src/Makefile}
+\texttt{Makefile.testing} introduces various targets related to \framac's
+testing infrastructure (see Section~\ref{adv:ptests}). This includes notably
+\texttt{tests} to run all the tests of the plugin, after having taken care of
+generating the corresponding \texttt{dune} files.
+
+\texttt{Makefile.installation} provides two targets, \texttt{install} and
+\texttt{uninstall}. By default, installation will occur in the current
+\texttt{opam} switch, but this can be modified by using the \texttt{PREFIX}
+variable (note that if you install your plugin in a non-default place, you will
+have to explicitly instruct \framac to load it through option
+\texttt{-load-plugin}.
+
+Other Makefiles include \texttt{Makefile.documentation}, providing the
+\texttt{doc} for generating the documentation (see Section~\ref{tut2:doc}),
+and \texttt{Makefile.headers} and \texttt{Makefile.linting} which are used
+by \framac itself to manage headers and perform various syntactic checks
+(though, of course, you can reuse them at will).
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Testing}\label{adv:ptests}\index{Test|bfit}
diff --git a/doc/developer/tutorial/hello/src/Makefile b/doc/developer/tutorial/hello/src/Makefile
index 5c30410ff80..bfdef3c8367 100644
--- a/doc/developer/tutorial/hello/src/Makefile
+++ b/doc/developer/tutorial/hello/src/Makefile
@@ -1,16 +1,13 @@
FRAMAC_SHARE:=$(shell frama-c-config -print-share-path)
-sinclude ${FRAMAC_SHARE}/Makefile.common
+## Common definitions
-##########################################################################
+include ${FRAMAC_SHARE}/Makefile.common
-# Tests
+## Tests-related targets
include ${FRAMAC_SHARE}/Makefile.testing
-##########################################################################
-
-# Install
+## Installation-related targets
include ${FRAMAC_SHARE}/Makefile.installation
-
--
GitLab