[Why3-club] Why3 Feature request: alternative to -L for many directories

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Mon Apr 4 16:33:44 CEST 2011

Hello Johannes,

> We at AdaCore came across another feature that we would very probably
> need when applying Hi-Lite to very large projects whose source files are
> distributed over a large number of directories. We want to tell why3
> where to search for Why files to include, which is basically the
> functionality of the -L switch. But if there are many directories,
> giving all of them to why3 using -L will hit the limit of the command
> line length on many platforms.
> Could Why3 implement one or the other of these solutions (preferably the
> second one)?

Why3 already provides you with these two solutions:

- the configuration file ~/.why.conf (or any configuration file 
specified on Why3's command line) may contain a list of loadpath 
directories, which are given with syntax

	loadpath = "/foo/bar/gee"
	loadpath = "/toto/titi/tata"

in section "main".

- when set, the environment variable WHY3LOADPATH (containing 
colon-separated directories) is taken into account, overriding the 
setting in ~/.why.conf

Andrei & Jean-Christophe

More information about the Why3-club mailing list