[isabelle-dev] Complete Distributive Lattice
viorel.preoteasa at gmail.com
viorel.preoteasa at gmail.com
Sat Mar 10 13:08:06 CET 2018
I will polish my changes, and then I will send them to you for testing. There are also some small changes needed to AFP.
From: Manuel Eberl <eberlm at in.tum.de>
Sent: Saturday, March 10, 2018 2:03 PM
To: viorel.preoteasa at gmail.com; isabelle-dev at mailbroy.informatik.tu-muenchen.de
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.
> Thank you for your help. Let me know when should I should share my repository, or if there is a better alternative.
> -----Original Message-----
> From: isabelle-dev
> <isabelle-dev-bounces at mailbroy.informatik.tu-muenchen.de> On Behalf Of
> Manuel Eberl
> Sent: Saturday, March 10, 2018 1:26 AM
> To: isabelle-dev at mailbroy.informatik.tu-muenchen.de
> 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.
> 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.
>> What is the appropriate way to test HOL-Library?
>> Viorel Preoteasa
>> -----Original Message-----
>> From: Lawrence Paulson <lp15 at cam.ac.uk>
>> Sent: Friday, March 9, 2018 12:49 PM
>> To: viorel.preoteasa at gmail.com
>> Cc: isabelle-dev at mailbroy.informatik.tu-muenchen.de
>> 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.preoteasa at gmail.com> <viorel.preoteasa at 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-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev