Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
95df9e20
Commit
95df9e20
authored
2 years ago
by
Andre Maroneze
Browse files
Options
Downloads
Patches
Plain Diff
[Doc] devman: improvements after review
parent
ddd56a68
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
doc/developer/tutorial.tex
+18
-16
18 additions, 16 deletions
doc/developer/tutorial.tex
with
18 additions
and
16 deletions
doc/developer/tutorial.tex
+
18
−
16
View file @
95df9e20
...
@@ -20,24 +20,25 @@ with \framac and other plug-ins to implement analyzers of \C programs.
...
@@ -20,24 +20,25 @@ with \framac and other plug-ins to implement analyzers of \C programs.
\section
{
Development Environment
}
\label
{
tut2:environment
}
\section
{
Development Environment
}
\label
{
tut2:environment
}
The
\framac
team currently recommends using
It is easy to develop a plug-in for
\framac
with any IDE, as long as it
VS~Code
\footnote
{
\url
{
https://code.visualstudio.com
}}
as IDE.
supports the OCaml language. This includes (but is not limited to)
It offers extensions (automatically suggested when you open an OCaml source
Emacs or Vim with the Merlin
\footnote
{
\url
{
https://ocaml.github.io/merlin
}}
file) which provide type checking, syntax highlighting, and code navigation
tool, or VS~Code with the
{
\em
OCaml platform
}
extension.
features.
The last is probably the easiest to setup for a beginner in OCaml.
The
\framac
team currently uses the
\texttt
{
ocp-indent
}
opam package
for code indentation. Consider installing it if you want to ensure your
Most modern IDEs support (directly or indirectly, via Merlin)
code follows the same conventions.
OCaml-LSP
\footnote
{
\url
{
https://github.com/ocaml/ocaml-lsp
}}
,
Other IDEs often used for OCaml development include Vim and Emacs. For them,
Merlin
\footnote
{
\url
{
https://ocaml.github.io/merlin
}}
(code navigation, typing
and auto-completion tool) is currently the main editor service.
It is used by OCaml-LSP
\footnote
{
\url
{
https://github.com/ocaml/ocaml-lsp
}}
,
which is an implementation of LSP (
{
\em
Language Server Protocol
}
for OCaml.
which is an implementation of LSP (
{
\em
Language Server Protocol
}
for OCaml.
Concerning code formatting, the
\framac
team currently uses the
\texttt
{
ocp-indent
}
opam package for code indentation.
Consider installing it if you want to ensure your code follows the same
conventions.
Overall, it is
\textbf
{
strongly
}
suggested to use an OCaml-aware IDE and take
Overall, it is
\textbf
{
strongly
}
suggested to use an OCaml-aware IDE and take
the time to set it up. Plug-ins use several different parts of the
\framac
API,
the time to set it up. Plug-ins use several different parts of the
\framac
API,
and a properly setup IDE greatly improves productivity.
and a properly setup IDE greatly improves productivity, offering features such
as auto-completion, type checking, syntax highlighting, and code navigation.
\section
{
What Does a Plug-in Look Like?
}
\label
{
tut2:architecture
}
\section
{
What Does a Plug-in Look Like?
}
\label
{
tut2:architecture
}
\index
{
Plug-in!Architecture
}
\index
{
Architecture!Plug-in
}
\index
{
Plug-in!Architecture
}
\index
{
Architecture!Plug-in
}
...
@@ -206,6 +207,7 @@ Then the plugin can be built using the following command:
...
@@ -206,6 +207,7 @@ Then the plugin can be built using the following command:
If Dune is installed, this should compile the project successfully.
If Dune is installed, this should compile the project successfully.
Note that Dune emits messages
{
\em
during
}
compilation, but erases them
Note that Dune emits messages
{
\em
during
}
compilation, but erases them
afterwards. In case of success, there will be no visible output at the end.
afterwards. In case of success, there will be no visible output at the end.
Note that this behavior can be configured with Dune's option
\verb
|
--display
|
.
\begin{important}
\begin{important}
Dune always looks for
\texttt
{
dune-project
}
files in the parent directories,
Dune always looks for
\texttt
{
dune-project
}
files in the parent directories,
...
@@ -649,8 +651,8 @@ The new oracle should be committed to source control, for future testing.
...
@@ -649,8 +651,8 @@ The new oracle should be committed to source control, for future testing.
earlier will not only compile your plug-in, but also run its tests.
earlier will not only compile your plug-in, but also run its tests.
Therefore, if you want to simply compile it, you will have to run
Therefore, if you want to simply compile it, you will have to run
\verb
|
dune build @install
|
instead. Despite the name, the command will
\verb
|
dune build @install
|
instead. Despite the name, the command will
{
\em
not
}
install your plug-in
(that is performed by
{
\em
not
}
install your plug-in
, it will only build and collect all
\verb
|
dune
install
|
)
.
files necessary for its
install
ation
.
\end{important}
\end{important}
Now, let's introduce an error. Assume the plug-in has been modified as follows:
Now, let's introduce an error. Assume the plug-in has been modified as follows:
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment