[isabelle-dev] Complete Distributive Lattice

Makarius makarius at sketis.net
Sat Mar 10 10:28:36 CET 2018

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


More information about the isabelle-dev mailing list