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

Johannes Kanig kanig at adacore.com
Mon Apr 4 11:59:44 CEST 2011

Hello Why3 team,

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.

There are two mechanisms that we use in our tools at AdaCore to
circumvent this limitation. The first one is to use an environment
variable, say WHY_SEARCH_PATH, which contains the relevant directories.
This pushes the maximum length quite far on many systems, but not far
enough. The second one is to pass a file to the tool, which enumerates
the directories to be searched line by line. This second solution pushes
the limit very far.

Could Why3 implement one or the other of these solutions (preferably the
second one)?

There is a third mechanism I want to tell you about, which is a variant
of the second one, but which can greatly improve efficiency, especially
when part of the project is on a slow file system (NFS etc). In GNAT,
the technique is called a mapping file, and it is a file that contains
sequences of three lines, as follows:

<unit name>
<file name without path>
<file name with full path>

This information allows the compiler to quickly find the correct source
file for a compilation unit, without having to search the entire

This third variant could also be interesting for Why3.	

This is not an urgent request, as we do not run Hi-Lite on large
projects yet, and we do not use Why3 yet, but we prefer to anticipate
our need, to give you time to choose the right solution for Why3.


Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list