[isabelle-dev] Proposing extensions to the Isabelle library?

Makarius makarius at sketis.net
Sun Jul 21 10:33:54 CEST 2013


On Fri, 19 Jul 2013, Alessandro Coglio wrote:

> The following command succeeds
>
> ./bin/isabelle build -c -a -d ../AFP/thys

BTW, you should never need the option -c (clean build) with isabelle build 
for regular test runs. It is only for special situations where you do 
things that are outside the session dependency management, e.g. when 
rebuilding a session with different parameters for document preparation.

In distant past (i.e. until 1 year ago) I used to be paranoid about "make 
clean && make" myself, but isabelle build is not using "make".  You can 
trust that isabelle build always does the right thing after changes of 
theory sources.  (If it does not, you should give some hints about the 
situation, so that it can be improved.)


 	Makarius



More information about the isabelle-dev mailing list