Re: [isabelle-dev] Complete Distributive Lattice

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

Re: [isabelle-dev] Complete Distributive Lattice

I will polish my changes, and then I will send them to you for testing. There are also some small changes needed to AFP. Viorel -Original Message- From: Manuel Eberl Sent: Saturday, March 10, 2018 2:03 PM To: viorel.preote...@gmail.com;

Re: [isabelle-dev] Complete Distributive Lattice

I managed to identify this problem. It was one file that did not finish. I made a new session and added the Library files little by little until I found the once causing problems. When you build a session, is it possible to find out what file(s) cause problems? If I would know that a certain

Re: [isabelle-dev] Complete Distributive Lattice

Verbose mode ("-v") can sometimes help, because you at least see what Isabelle is doing. Another thing you can do is add "-o timeout=600" to your invocation of isabelle build. Then the build will be stopped after 600 seconds and the log file might help you identify what theory is causing the

Re: [isabelle-dev] Complete Distributive Lattice

> The test did not finish, although I left it overnight. There is something > wrong. I don't know how to identify the problem since the jedit interface > seems to work, all files are completely processed. > > I can share may changes with you. I can use "hg serve", unless you know of a > better

Re: [isabelle-dev] Complete Distributive Lattice

It did not work in jEdit. I must have overlooked that file the first time. Viorel -Original Message- From: Manuel Eberl Sent: Saturday, March 10, 2018 2:01 PM To: viorel.preote...@gmail.com; isabelle-dev@mailbroy.informatik.tu-muenchen.de Subject: Re: [isabelle-dev]

Re: [isabelle-dev] Complete Distributive Lattice

Hi, The test did not finish, although I left it overnight. There is something wrong. I don't know how to identify the problem since the jedit interface seems to work, all files are completely processed. I can share may changes with you. I can use "hg serve", unless you know of a better

Re: [isabelle-dev] Complete Distributive Lattice

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

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