Commit ccc25c81 authored by Virgile Prevosto's avatar Virgile Prevosto

Merge branch 'feature/michele/remove-framac-libdir-doc-dev' into 'master'

[doc] Remove references to FRAMAC_LIBDIR from developer tutorial

See merge request frama-c/frama-c!2944
parents 460e1534 3de6581e
......@@ -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"
......
......@@ -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
......@@ -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}
......
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
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
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
......
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
......
Markdown is supported
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