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

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

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 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

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

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. What

[isabelle-dev] Complete Distributive Lattice

I am working on the generalization of the complete distributive lattices. Changing the axioms from sup x (Inf Y) = … to the more general form: Sup (Inf ` A) = … I have done these changes already for the previous release candidate, and I just need to integrate them into the