> For the complete documentation index, see [llms.txt](https://b-method.gitbook.io/training-resources-for-atelier-b/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://b-method.gitbook.io/training-resources-for-atelier-b/guides-and-tutorials/extending-atelier-b.md).

# Extending Atelier B

Atelier B 4 allows running “external tools” from within the GUI. Several kinds of external tools can be integrated:

* **project external tools**. Those tools are running on a project, and appears in the “Project” menu of the GUI. For instance, they can be used to provide metrics on a project
* **component**. Those tools are running on a component, and appears in the “Component” menu of the GUI. They are launched on the selected component(s)
* **po**. Those tools are running on a selected proof obligation in the interactive prover
* **goal**. Those tools are running on the current goal of the interactive prover

Integrating an external tool is done by writing a “*.etool*” xml file.&#x20;

This file describes the type of tool, as well as the command that will be started. This file should be located in the “*extensions*” subdirectory of the Atelier B installation, and is loaded when the Atelier B GUI start.&#x20;

For each “etool” file, a corresponding menu entry is created within the “Project” or “Component” menu of the GUI.&#x20;

When the menu is clicked, the tool is launched, and the corresponding task appears in the “Tasks” window of Atelier B. Double-clicking on the task displays a windows showing the output of the tool.  The complete syntax of the “*.etool*” files is first described. Then some examples are presented.
