[isabelle-dev] Complete Distributive Lattice

[Manuel Eberl]

Try -d instead of -D.

The former only specifies a search path for sessions; the second one
additionally tells Isabelle to build all the sessions in that path.

However, we have some high-powered testing hardware here in Munich to
take care of these things, so we can do the testing for you, if you want.

Manuel


On 10/03/18 12:52, viorel.preoteasa at gmail.com wrote:
> I am trying to build the afp-devel, but the process stops saying "Nothing to build"
> 
> $ ./bin/isabelle build -d ../afp-devel/thys -X slow
> ### Nothing to build
> 0:00:00 elapsed time
> 
> $ ./bin/isabelle build -c -d ../afp-devel/thys -X slow
> ### Nothing to build
> 0:00:01 elapsed time
> 
> Viorel
> 
> -----Original Message-----
> From: Makarius <makarius at sketis.net> 
> Sent: Saturday, March 10, 2018 11:29 AM
> To: viorel.preoteasa at gmail.com; isabelle-dev at mailbroy.informatik.tu-muenchen.de
> Subject: Re: [isabelle-dev] Complete Distributive Lattice
> 
> On 09/03/18 23:54, viorel.preoteasa at gmail.com wrote:
>> I am trying to test HOL-Library by using:
>>
>> ./bin/isabelle build -v HOL-Library
>>
>> But it takes very long. It has now been working for few hours, and it is still running.
>> I also tried to open all files from HOL/Library in Isabelle/jedit and 
>> they were processed quite fast, without any errors.
> 
> For proposed changes in main HOL, you ultimately need to test all of Isabelle + AFP. This can be quite tiresome, unless you find someone to do it for you.
> 
> The README_REPOSITORY file has more information about testing at the bottom. For AFP you need to include its main session directory like
> this: "isabelle build -d .../AFP/thys -X slow".
> 
> Without "-X slow" you have hardly a chance to finish in reasonable time on normal hardware, but even the "slow" group needs to be tested at some point.
> 
> 
> 	Makarius
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>