Alfa has a simple plug-in interface, allowing Haskell programmers to write plug-in modules that extends Alfa's core functionality in various ways.

The intention is that it should be possible develop and distribute plug-ins separately from Alfa, but for the time being, plug-in modules have to be hardwired into Alfa. (This is because current Haskell implementations do not support dynamic code loading.)

Alfa currently comes with a small number of plug-ins:

translates formal proofs (i.e., definitions and expressions in Alfa) to natural language. At present, there is support for English, French and Swedish, but more languages can be added by the user. (It is called GF because it is implemented using the Grammatical Framework, GF.)
use Alfa as an alternate user interface to the GF.
generate equality relations for data types.
generate natural deduction style proofs for propositional logic formulas.
a simple test of the plug-in interface. Allows plain text files to be opened in Alfa. Counts how many times a file has been saved and reopened.
Most of these are in an experimental and/or undocumented state...

Activating plug-in modules

When starting Alfa, no plug-ins are activated by default. By supplying the flag -plugins,
alfa - -plugins
all plug-ins are activated. You can selectively activate some plug-ins by supplying a colon-separated list after the -plugins flag, e.g.,
alfa - -plugins GF:Pesca
alfa - -plugins Derive

Alfa announces the activation of a plug-in in the terminal window when Alfa is started. Plug-ins usually also announce their presence in the info display, at the bottom of Alfa's window, when the entire document is selected:

[Plugins awake window dump]

Using plug-ins

Exactly how to use a plug-in depends on the plug-in, of course. In general, users interact with plug-ins through extra commands that appear in the menus. The commands can provide Additionally, plug-ins can