From b0de1d74676e69a9aac6b72aa32c86be611d0622 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 17 Nov 2022 11:25:50 +0100
Subject: [PATCH] [devman] Capitalized filename is not mandatory anymore
---
doc/developer/tutorial.tex | 32 ++++++++-----------
.../hello/src/Makefile.multiple-files | 26 ---------------
.../tutorial/hello/src/Makefile.single-file | 26 ---------------
.../tutorial/hello/src/{Hello.ml => hello.ml} | 0
.../hello/v1-simple/{Hello.ml => hello.ml} | 0
.../hello/v2-register/{Hello.ml => hello.ml} | 0
.../hello/v3-log/{Hello.ml => hello.ml} | 0
.../hello/v4-options/{Hello.ml => hello.ml} | 0
.../hello/v5-multiple/{Hello.ml => hello.ml} | 0
.../v6-test-with-bug/{Hello.ml => hello.ml} | 0
.../hello/v7-doc/{Hello.ml => hello.ml} | 0
11 files changed, 13 insertions(+), 71 deletions(-)
delete mode 100644 doc/developer/tutorial/hello/src/Makefile.multiple-files
delete mode 100644 doc/developer/tutorial/hello/src/Makefile.single-file
rename doc/developer/tutorial/hello/src/{Hello.ml => hello.ml} (100%)
rename doc/developer/tutorial/hello/v1-simple/{Hello.ml => hello.ml} (100%)
rename doc/developer/tutorial/hello/v2-register/{Hello.ml => hello.ml} (100%)
rename doc/developer/tutorial/hello/v3-log/{Hello.ml => hello.ml} (100%)
rename doc/developer/tutorial/hello/v4-options/{Hello.ml => hello.ml} (100%)
rename doc/developer/tutorial/hello/v5-multiple/{Hello.ml => hello.ml} (100%)
rename doc/developer/tutorial/hello/v6-test-with-bug/{Hello.ml => hello.ml} (100%)
rename doc/developer/tutorial/hello/v7-doc/{Hello.ml => hello.ml} (100%)
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index c8aa6dd2ba4..f1765764717 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -186,7 +186,7 @@ minimally of the following files:
\begin{itemize}
\item a \texttt{dune-project} file that describes the project;
\item a \texttt{dune} file that describes the build of the project;
- \item a \texttt{<My\_plugin>.ml} file that defines the API of the plugin
+ \item a \texttt{<my\_plugin>.ml} file that defines the API of the plugin
(which can be empty).
\end{itemize}
@@ -198,7 +198,7 @@ For example, for the Hello plugin:
\listingname{./dune}
\duneinput{./tutorial/hello/v1-simple/dune}
-\texttt{Hello.ml} is just an empty file.
+\texttt{hello.ml} is just an empty file.
Then the plugin can be built using the following command:
@@ -225,10 +225,10 @@ Note a few details about the naming conventions:
\texttt{frama-c-<my-plugin>}
\item in the \texttt{dune} file, the name of:
\begin{itemize}
- \item the library is \texttt{My\_plugin} (it is a module name);
+ \item the library is \texttt{my\_plugin};
\item the public name of the library is \texttt{frama-c-<my-plugin>.core}
(dune project name core);
- \item the name of the plugin is \texttt{my-plugin};
+ \item the name of the plugin is \texttt{<my-plugin>};
\item the plugin must at least include the library
\texttt{frama-c-<my-plugin>.core}.
\end{itemize}
@@ -402,26 +402,20 @@ These new options also appear in the inline help for the hello plug-in:
\subsection{About the plug-in build process}
As mentioned before, each plug-in needs a module declaring its public API.
-In our examples, this was file \verb|Hello.ml|, which was left empty.
+In our examples, this was file \verb|hello.ml|, which was left empty.
To make it more explicit to future users of our plug-in, it is customary to
add a comment such as the following:
-\listingname{./Hello.ml}
-\ocamlinput{./tutorial/hello/v5-multiple/Hello.ml}
-
-\begin{important}
- Note the unusual capitalization of the filename \texttt{Hello.ml}, which
- must correspond to the name of the plug-in specified in the Dune file
- (the \texttt{name} part inside \texttt{library}).
-\end{important}
+\listingname{./hello.ml}
+\ocamlinput{./tutorial/hello/v5-multiple/hello.ml}
Note that, to avoid issues, the name of each compilation unit
(here \texttt{hello\_world}) must be different from the plug-in name set in
-the \texttt{dune} file (here \texttt{Hello}), from any other plug-in names
+the \texttt{dune} file (here \texttt{hello}), from any other plug-in names
(\eg \texttt{eva}, \texttt{wp}, etc.) and from any other \framac kernel
\caml files (\eg \texttt{plugin}).
-The module name chosen by a plug-in (here \texttt{Hello}) is used by Dune to
+The module name chosen by a plug-in (here \texttt{hello}) is used by Dune to
{\em pack} that plug-in; any functions declared in it become part of the
plug-in's public API. They become accessible to other plug-ins and need to be
maintained by the plug-in developer. Leaving it empty avoids exposing
@@ -432,7 +426,7 @@ packed module. It can be installed along with the other \framac plug-ins using
\verb|dune install|.
You can then just launch \texttt{frama-c} (without any options), and the
-\texttt{Hello} plug-in will be automatically loaded. Check it with the command
+\texttt{hello} plug-in will be automatically loaded. Check it with the command
\verb|frama-c -hello-help|.
You can uninstall it by running \verb|dune uninstall|.
@@ -735,11 +729,11 @@ This relies on \odoc and requires the plug-in to be documented following the
We show here how the Hello plug-in could be slightly documented and use
\odoc features such as @-tags and cross references. First, we modify the
-\texttt{Hello.ml} file to export all inner modules, otherwise \odoc will not
+\texttt{hello.ml} file to export all inner modules, otherwise \odoc will not
generate documentation for them:
-\listingname{./Hello.ml}
-\ocamlinput{./tutorial/hello/v7-doc/Hello.ml}
+\listingname{./hello.ml}
+\ocamlinput{./tutorial/hello/v7-doc/hello.ml}
Then, we add some documentation tags to our modules:
diff --git a/doc/developer/tutorial/hello/src/Makefile.multiple-files b/doc/developer/tutorial/hello/src/Makefile.multiple-files
deleted file mode 100644
index 0a63c0353f0..00000000000
--- a/doc/developer/tutorial/hello/src/Makefile.multiple-files
+++ /dev/null
@@ -1,26 +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
-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
deleted file mode 100644
index b99d50a1dce..00000000000
--- a/doc/developer/tutorial/hello/src/Makefile.single-file
+++ /dev/null
@@ -1,26 +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_world
-include $(FRAMAC_SHARE)/Makefile.dynamic
diff --git a/doc/developer/tutorial/hello/src/Hello.ml b/doc/developer/tutorial/hello/src/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/src/Hello.ml
rename to doc/developer/tutorial/hello/src/hello.ml
diff --git a/doc/developer/tutorial/hello/v1-simple/Hello.ml b/doc/developer/tutorial/hello/v1-simple/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v1-simple/Hello.ml
rename to doc/developer/tutorial/hello/v1-simple/hello.ml
diff --git a/doc/developer/tutorial/hello/v2-register/Hello.ml b/doc/developer/tutorial/hello/v2-register/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v2-register/Hello.ml
rename to doc/developer/tutorial/hello/v2-register/hello.ml
diff --git a/doc/developer/tutorial/hello/v3-log/Hello.ml b/doc/developer/tutorial/hello/v3-log/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v3-log/Hello.ml
rename to doc/developer/tutorial/hello/v3-log/hello.ml
diff --git a/doc/developer/tutorial/hello/v4-options/Hello.ml b/doc/developer/tutorial/hello/v4-options/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v4-options/Hello.ml
rename to doc/developer/tutorial/hello/v4-options/hello.ml
diff --git a/doc/developer/tutorial/hello/v5-multiple/Hello.ml b/doc/developer/tutorial/hello/v5-multiple/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v5-multiple/Hello.ml
rename to doc/developer/tutorial/hello/v5-multiple/hello.ml
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/Hello.ml b/doc/developer/tutorial/hello/v6-test-with-bug/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v6-test-with-bug/Hello.ml
rename to doc/developer/tutorial/hello/v6-test-with-bug/hello.ml
diff --git a/doc/developer/tutorial/hello/v7-doc/Hello.ml b/doc/developer/tutorial/hello/v7-doc/hello.ml
similarity index 100%
rename from doc/developer/tutorial/hello/v7-doc/Hello.ml
rename to doc/developer/tutorial/hello/v7-doc/hello.ml
--
GitLab