#114 Jmlc should compile used and out-of-date files

[Gary T. Leavens]

The JML compiler, jmlc, doesn't automatically compile
files that are not compiled but are used by other files
that are explicitly asked to be compiled. It would be
nice if the JML compiler acted in the same way as the
Java compiler with respect to compiling files that are
used which are out of date with respect to their class
files. This would enable the JML compiler to act as a
drop-in replacement for javac.

Richard Mitchell suggested this enhancement. It would
probably benefit new users.

[Gary T. Leavens]

Logged In: YES
user_id=633675

I would also add the following comment from another user (W.
Craig Trader) on the JML interest list:

One of the biggest problems with JMLC (either with or
without Ant) is the lack of internal dependency checking.
JMLC will always recompile a class, even if none of the
source dependencies for that class have changed. This
results in significant delays when you change one class in a
project that is composed of hundreds of classes.

[Gary T. Leavens]

Logged In: YES
user_id=633675
Originator: YES

Franco Luque also reported this problem. He wrote in response to Yoonsik Cheon's clarification:

> It looks like that Provider.java wasn't compiled with jmlc. Try
> jmlc Client.java Provider.java
> and see whether you have the same symptom; you have to list all the source
> code files as arguments to jmlc.

So that was the problem... I am using NetBeans and my "compile-single"
ant target was correctly compiling with JMLC the selected class, but
was compiling without JMLRAC all its dependencies and overwrinitg the
previously JMLC compiled versions. That was because i was not telling
JMLC where to find the already compiled classes (via the classpath).

Now its fixed, so that it does not overwrite already compiled classes,
but it still compiles without JMLRAC those dependencies that were not
previously compiled. This is on purpose, isn't it? Why?

[Gary T. Leavens]

Logged In: YES
user_id=633675
Originator: YES

Another pitfall caused by this bug is that the jtest script that we have doesn't work as one might expect. Suppose one has a class C that implements an interface I. Then executing

jtest C.java
jmlrac C

doesn't test C properly, because the interface I, where some specifications may be found, is not compiled with jmlc, but instead by javac, which does get compile I, since it is out of date.