[isabelle-dev] Complete Distributive Lattice

[viorel.preoteasa at gmail.com]

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 method. The main changes are to HOL, and I updated HOL-Library for these changes.

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