[isabelle-dev] Complete Distributive Lattice

[Manuel Eberl]

> 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-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.
> 
> Manuel
> 
> 
> 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
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabell
>> e-dev
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>