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 <ebe...@in.tum.de> Sent: Saturday, March 10, 2018 2:03 PM To: viorel.preote...@gmail.com; firstname.lastname@example.org Subject: 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 method. The main changes are to HOL, and I updated HOL-Library for > these changes. hg serve is possible. You can also fork the repository on Bitbucket. The "normal" approach is to just create a Mercurial patch file with "hg export" or "hg diff" and email it to the other person. Manuel > > Thank you for your help. Let me know when should I should share my > repository, or if there is a better alternative. > > Viorel > > -----Original Message----- > From: isabelle-dev > <isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de> On Behalf Of > Manuel Eberl > Sent: Saturday, March 10, 2018 1:26 AM > To: email@example.com > Subject: Re: [isabelle-dev] Complete Distributive Lattice > > That /is/ the proper way to test it. > > On my machine, HOL-Library takes 6 minutes of CPU time. If it takes > significantly more than that on yours, there's something wrong. If it takes > hours and still isn't done, there's something very wrong. > > Are you sure the files are processed fully and without non-terminating steps > in Isabelle/jEdit? > > If you share your version of HOL-Library with me, I'll happily take a look at > it. > > Manuel > > > 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. >> >> What is the appropriate way to test HOL-Library? >> >> Viorel Preoteasa >> >> -----Original Message----- >> From: Lawrence Paulson <l...@cam.ac.uk> >> Sent: Friday, March 9, 2018 12:49 PM >> To: viorel.preote...@gmail.com >> Cc: firstname.lastname@example.org >> Subject: Re: [isabelle-dev] Complete Distributive Lattice >> >> I don’t think it’s a problem that your more general theorems require the >> Axiom of Choice, and Hilbert_Choice.thy is not too large already (far from >> it). >> >> Larry Paulson >> >> >> >>> On 8 Mar 2018, at 21:35, <viorel.preote...@gmail.com> >>> <viorel.preote...@gmail.com> wrote: >>> >>> I have a question about how to organize these changes. The problem >>> is that most of the results for the more general lattice >>> (instantiations to set, fun) require Hilbert_Choice which is not available >>> in Complete_Lattice. Now I have added all results about complete >>> distributive lattices that need Hilbert Choice in Hilbert_Choice.thy. Is >>> this acceptable? >>> >> >> >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel >> l >> e-dev >> > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabell > e-dev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev