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 <makar...@sketis.net>
Sent: Saturday, March 10, 2018 11:29 AM
To: viorel.preote...@gmail.com; isabelle-dev@mailbroy.informatik.tu-muenchen.de
Subject: Re: [isabelle-dev] Complete Distributive Lattice
On 09/03/18 23:54, viorel.preote...@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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
