From 3de6581efd1c9eaf84a93d1e350c5e18d47441dc Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 12 Nov 2020 13:53:15 +0100
Subject: [PATCH] [doc] Remove references to FRAMAC_LIBDIR in tutorial as it is
no more needed (and source of errors).
---
doc/developer/advance.tex | 29 +++++++++----------
doc/developer/hello_world/Makefile | 1 -
doc/developer/tutorial.tex | 10 ++-----
.../hello/src/Makefile.multiple-files | 1 -
.../tutorial/hello/src/Makefile.single-file | 1 -
.../tutorial/hello/src/Makefile.test | 1 -
.../tutorial/viewcfg/src/Makefile.split | 1 -
7 files changed, 17 insertions(+), 27 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 29c9a4cd9dd..164774bce6f 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -494,12 +494,10 @@ Section~\ref{tut2:hello}). Each variable set in this example has to be set
by any plug-in.
\codeidx{Makefile.dynamic}
\codeidx{FRAMAC\_SHARE}
-\codeidx{FRAMAC\_LIBDIR}
\codeidx{PLUGIN\_CMO}
\codeidx{PLUGIN\_NAME}
\makefileinput{./tutorial/hello/generated/makefile_multiple/Makefile}
-\texttt{FRAMAC\_SHARE} must be set to the \framac share directory while
-\texttt{FRAMAC\_LIBDIR} must be set to the \framac lib directory.
+\texttt{FRAMAC\_SHARE} must be set to the \framac share directory.
\texttt{PLUGIN\_NAME} is the capitalized name of your plug-in while
\texttt{PLUGIN\_CMO} is the list of the files $.cmo$ generated from your \caml
sources.
@@ -596,18 +594,19 @@ otherwise.
\codeidx{clean-install}
\codeidx{install}
-In addition, if a plug-in wishes to install custom files to
-\texttt{FRAMAC\_LIBDIR} through the \texttt{install::} target,
-this target must depend on \texttt{clean-install}.
-Indeed, \framac's main \texttt{Makefile} removes
-all existing files in this directory before performing a fresh installation,
-in order to avoid potential interference with an obsolete (and usually
-incompatible) module from a previous installation. Adding the dependency thus
-ensures that the removal will take place before any new file has been installed
-in the directory.
-
-\begin{example} If a plug-in wants to install \texttt{external/my\_lib.cm*}
-in addition to the normal plugin files, it should use the following code:
+In addition, if a plug-in wishes to install custom files through the
+\texttt{install::} target, this target must depend on \texttt{clean-install}.
+Indeed, \framac's main \texttt{Makefile} removes all existing files in this
+directory before performing a fresh installation, in order to avoid potential
+interference with an obsolete (and usually incompatible) module from a previous
+installation. Adding the dependency thus ensures that the removal will take
+place before any new file has been installed in the directory.
+
+\begin{example} If a plug-in wants to install \texttt{external/my\_lib.cm*} in
+ addition to the normal plugin files, it should use the following code:
+ \footnote{Note that the variable \texttt{FRAMAC\_LIBDIR} is automatically set
+ by the \framac build system to the value provided by the command
+ \texttt{frama-c-config -print-libpath}.\codeidx{FRAMAC\_LIBDIR}}
\begin{makefilecode}
install:: clean-install
$(PRINT_INSTALL) "My beautiful library"
diff --git a/doc/developer/hello_world/Makefile b/doc/developer/hello_world/Makefile
index ba65abf50aa..47732363b83 100644
--- a/doc/developer/hello_world/Makefile
+++ b/doc/developer/hello_world/Makefile
@@ -18,7 +18,6 @@
# before any use of this makefile
FRAMAC_SHARE :=$(shell frama-c-config -print-share-path)
-FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
PLUGIN_NAME = Hello
PLUGIN_CMO = hello_world
include $(FRAMAC_SHARE)/Makefile.dynamic
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 41f0ab59f75..fa627601a68 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -409,7 +409,6 @@ We write a simple \texttt{./Makefile} for our
\listingname{./Makefile}
\codeidx{Makefile.dynamic}
\codeidx{FRAMAC\_SHARE}
-\codeidx{FRAMAC\_LIBDIR}
\codeidx{PLUGIN\_CMO}
\codeidx{PLUGIN\_NAME}
\makefileinput{./tutorial/hello/generated/makefile_single/Makefile}
@@ -447,9 +446,9 @@ compiled files are copied into a \texttt{top} (for {\em top-level}) subdirectory
The module can then be loaded and executed by using
\texttt{frama-c -load-module top/Hello}.
-Then run \texttt{make install} to install the plug-in (you need to
-have write access to the \texttt{\$(FRAMAC\_LIBDIR)/plugins}
-directory\codeidx{FRAMAC\_LIBDIR}).
+Then run \texttt{make install} to install the plug-in (you need to have write
+access to the \texttt{plugins} directory, located at the path given by the
+command \texttt{frama-c-config -print-libpath}).
Just launch \texttt{frama-c} (without any option): the \texttt{Hello}
plug-in is now always loaded, without the need to pass other options to
@@ -467,7 +466,6 @@ file names, in the correct \ocaml build order.
\listingname{./Makefile}
\codeidx{Makefile.dynamic}
\codeidx{FRAMAC\_SHARE}
-\codeidx{FRAMAC\_LIBDIR}
\codeidx{PLUGIN\_CMO}
\codeidx{PLUGIN\_NAME}
\makefileinput{./tutorial/hello/generated/makefile_multiple/Makefile}
@@ -517,7 +515,6 @@ subdirectory of \texttt{.tests/} where the plug-in's tests will be located:
\listingname{./Makefile}
\codeidx{Makefile.dynamic}
\codeidx{FRAMAC\_SHARE}
-\codeidx{FRAMAC\_LIBDIR}
\codeidx{PLUGIN\_CMO}
\codeidx{PLUGIN\_NAME}
\codeidx{PLUGIN\_TESTS\_DIRS}
@@ -1073,7 +1070,6 @@ configuration options.
\listingname{Makefile}
\codeidx{Makefile.dynamic}
\codeidx{FRAMAC\_SHARE}
-\codeidx{FRAMAC\_LIBDIR}
\codeidx{PLUGIN\_CMO}
\codeidx{PLUGIN\_GUI\_CMO}
\codeidx{PLUGIN\_NAME}
diff --git a/doc/developer/tutorial/hello/src/Makefile.multiple-files b/doc/developer/tutorial/hello/src/Makefile.multiple-files
index 494fc9521ce..4e97b5ed2dd 100644
--- a/doc/developer/tutorial/hello/src/Makefile.multiple-files
+++ b/doc/developer/tutorial/hello/src/Makefile.multiple-files
@@ -1,5 +1,4 @@
FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
-FRAMAC_LIBDIR := $(shell frama-c-config -print-libpath)
PLUGIN_NAME = Hello
PLUGIN_CMO = hello_options hello_print hello_run
include $(FRAMAC_SHARE)/Makefile.dynamic
diff --git a/doc/developer/tutorial/hello/src/Makefile.single-file b/doc/developer/tutorial/hello/src/Makefile.single-file
index 0f17e871c43..9b1b558bcba 100644
--- a/doc/developer/tutorial/hello/src/Makefile.single-file
+++ b/doc/developer/tutorial/hello/src/Makefile.single-file
@@ -1,5 +1,4 @@
FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
-FRAMAC_LIBDIR := $(shell frama-c-config -print-libpath)
PLUGIN_NAME = Hello
PLUGIN_CMO = hello_world
include $(FRAMAC_SHARE)/Makefile.dynamic
diff --git a/doc/developer/tutorial/hello/src/Makefile.test b/doc/developer/tutorial/hello/src/Makefile.test
index 2c292d74734..2ab6fb6a70c 100644
--- a/doc/developer/tutorial/hello/src/Makefile.test
+++ b/doc/developer/tutorial/hello/src/Makefile.test
@@ -1,5 +1,4 @@
FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
-FRAMAC_LIBDIR := $(shell frama-c-config -print-libpath)
PLUGIN_NAME = Hello
PLUGIN_CMO = hello_options hello_print hello_run
PLUGIN_TESTS_DIRS := hello
diff --git a/doc/developer/tutorial/viewcfg/src/Makefile.split b/doc/developer/tutorial/viewcfg/src/Makefile.split
index ccb89969c17..ee56b8cad49 100644
--- a/doc/developer/tutorial/viewcfg/src/Makefile.split
+++ b/doc/developer/tutorial/viewcfg/src/Makefile.split
@@ -1,5 +1,4 @@
FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
-FRAMAC_LIBDIR := $(shell frama-c-config -print-libpath)
PLUGIN_NAME = ViewCfg
PLUGIN_CMO = cfg_options cfg_core cfg_register
PLUGIN_GUI_CMO = cfg_gui
--
GitLab