abella_dep

abella_dep reads a collection of Abella developments and writes a Makefile that records the dependencies between them. Running make with that Makefile recompiles only the .thm files whose sources or dependencies have changed, and the generated rules work with parallel make -j.

Synopsis

abella_dep [OPTION]... [SOURCE]...

Each SOURCE is a .thm file or a directory. A directory is processed only with -r.

$ abella_dep a.thm d/b.thm c/*.thm
$ abella_dep -r examples

Options

Option	Meaning
-a CMD, --abella=CMD	Use CMD in the generated rules.
-c, --clobber	Allow overwriting an existing output file.
-o FILE, --output=FILE	Write the Makefile to FILE; - is stdout.
-r	Process directories recursively.
--help[=FMT]	Show help in a given format.

The FMT of --help is one of auto, pager, groff, or plain.

-a overrides the ABELLA environment variable. When neither is given, abella_dep looks for an executable named abella, abella.exe, or abella.bc in the directory containing abella_dep.

If -o names an existing file, abella_dep refuses to overwrite it unless -c is given. Output to standard output is never considered a clobber.

Generated Makefile

The output begins with a comment identifying the generator and the time of generation. It then declares the generic rule:

# DO NOT EDIT! This file was autogenerated by abella_dep.
# Generated on: 2026-11-07 20:28:12Z
.PHONY: all
%.thc: %.thm
	abella --non-recursive --output=${<:%.thm=%.out} $<

For each development, it adds the compiled target to all and lists its dependencies:

all: examples/lambda-calculus/type-uniq/type-uniq.thc
examples/lambda-calculus/type-uniq/type-uniq.thc: \
  examples/lambda-calculus/type-uniq/type-uniq.sig \
  examples/lambda-calculus/type-uniq/type-uniq.mod

The dependencies are:

• the .sig and .mod files of the specification, including everything they pull in through accum_sig and accumulate;
• the .thc files of developments loaded with Import.

The rule runs Abella with --non-recursive, because the Makefile itself handles the ordering. It writes normal output to file.out and the compiled development to file.thc.

Input rules

A regular file must end in .thm; anything else is an error unless it is inside a directory being processed recursively. A directory argument requires -r; without it, abella_dep reports an error.

Circular dependencies between developments are detected and reported.

Examples

Generate a Makefile for a few explicit files:

$ abella_dep a.thm d/b.thm c/*.thm > Makefile
$ make -j

Generate and overwrite a named Makefile:

$ abella_dep -c -o build.mk -r examples
$ make -f build.mk -j

Use a specific Abella executable:

$ abella_dep -a /usr/local/bin/abella -o Makefile -r examples

Related tools

• abella runs the proofs.
• abella_doc generates HTML pages from the same sources.