Re: [isabelle-dev] Complete Distributive Lattice

[Viorel Preoteasa]

My changes to Complete Distributive Lattices are now integrated in the
development version of Isabelle.

I want to thank Manuel Eberl for helping with testing and pushing the
update into repository.

Viorel Preoteasa

On Fri, Mar 9, 2018 at 12:48 PM, Lawrence Paulson  wrote:

> 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> 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/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[viorel.preoteasa]

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; isabelle-dev@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.

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: isabelle-dev@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.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: isabelle-dev@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.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

Re: [isabelle-dev] Complete Distributive Lattice

[viorel.preoteasa]

It did not work in jEdit. I must have overlooked that file the first time.

Viorel

-Original Message-
From: Manuel Eberl <ebe...@in.tum.de> 
Sent: Saturday, March 10, 2018 2:01 PM
To: viorel.preote...@gmail.com; isabelle-dev@mailbroy.informatik.tu-muenchen.de
Subject: Re: [isabelle-dev] Complete Distributive Lattice

Verbose mode ("-v") can sometimes help, because you at least see what Isabelle 
is doing.

Another thing you can do is add "-o timeout=600" to your invocation of isabelle 
build. Then the build will be stopped after 600 seconds and the log file might 
help you identify what theory is causing the problem.

However, I am still a bit puzzled by the fact that, according to what you said, 
everything seems to run through in Isabelle/jEdit. That's not impossible, but 
it is somewhat unusual.

Manuel


On 10/03/18 12:46, viorel.preote...@gmail.com wrote:
> 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 file takes a certain amount of time, 
> and it does not finish, then I could pin point the problem.
> 
> Viorel

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [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-boun...@mailbroy.informatik.tu-muenchen.de> 
> On Behalf Of Manuel Eberl
> Sent: Saturday, March 10, 2018 1:26 AM
> To: isabelle-dev@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.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: isabelle-dev@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.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/isabell
>> e-dev
>>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Manuel Eberl]

Verbose mode ("-v") can sometimes help, because you at least see what
Isabelle is doing.

Another thing you can do is add "-o timeout=600" to your invocation of
isabelle build. Then the build will be stopped after 600 seconds and the
log file might help you identify what theory is causing the problem.

However, I am still a bit puzzled by the fact that, according to what
you said, everything seems to run through in Isabelle/jEdit. That's not
impossible, but it is somewhat unusual.

Manuel


On 10/03/18 12:46, viorel.preote...@gmail.com wrote:
> 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 file takes a certain amount of time, 
> and it does not finish, then I could pin point the problem.
> 
> Viorel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Manuel Eberl]

Try -d instead of -D.

The former only specifies a search path for sessions; the second one
additionally tells Isabelle to build all the sessions in that path.

However, we have some high-powered testing hardware here in Munich to
take care of these things, so we can do the testing for you, if you want.

Manuel


On 10/03/18 12:52, viorel.preote...@gmail.com wrote:
> 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
> 
> -Original Message-
> From: Makarius <makar...@sketis.net> 
> Sent: Saturday, March 10, 2018 11:29 AM
> To: viorel.preote...@gmail.com; 
> isabelle-dev@mailbroy.informatik.tu-muenchen.de
> Subject: Re: [isabelle-dev] Complete Distributive Lattice
> 
> 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.
> 
> For proposed changes in main HOL, you ultimately need to test all of Isabelle 
> + AFP. This can be quite tiresome, unless you find someone to do it for you.
> 
> The README_REPOSITORY file has more information about testing at the bottom. 
> For AFP you need to include its main session directory like
> this: "isabelle build -d .../AFP/thys -X slow".
> 
> Without "-X slow" you have hardly a chance to finish in reasonable time on 
> normal hardware, but even the "slow" group needs to be tested at some point.
> 
> 
>   Makarius
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[viorel.preoteasa]

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

-Original Message-
From: Makarius <makar...@sketis.net> 
Sent: Saturday, March 10, 2018 11:29 AM
To: viorel.preote...@gmail.com; isabelle-dev@mailbroy.informatik.tu-muenchen.de
Subject: Re: [isabelle-dev] Complete Distributive Lattice

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.

For proposed changes in main HOL, you ultimately need to test all of Isabelle + 
AFP. This can be quite tiresome, unless you find someone to do it for you.

The README_REPOSITORY file has more information about testing at the bottom. 
For AFP you need to include its main session directory like
this: "isabelle build -d .../AFP/thys -X slow".

Without "-X slow" you have hardly a chance to finish in reasonable time on 
normal hardware, but even the "slow" group needs to be tested at some point.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[viorel.preoteasa]

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 file takes a certain amount of time, 
and it does not finish, then I could pin point the problem.

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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[viorel.preoteasa]

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-boun...@mailbroy.informatik.tu-muenchen.de> On 
Behalf Of Manuel Eberl
Sent: Saturday, March 10, 2018 1:26 AM
To: isabelle-dev@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.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: isabelle-dev@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.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/isabell
> e-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Makarius]

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.

For proposed changes in main HOL, you ultimately need to test all of
Isabelle + AFP. This can be quite tiresome, unless you find someone to
do it for you.

The README_REPOSITORY file has more information about testing at the
bottom. For AFP you need to include its main session directory like
this: "isabelle build -d .../AFP/thys -X slow".

Without "-X slow" you have hardly a chance to finish in reasonable time
on normal hardware, but even the "slow" group needs to be tested at some
point.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Manuel Eberl]

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: isabelle-dev@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.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/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[viorel.preoteasa]

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: isabelle-dev@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.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/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Lawrence Paulson]

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,  
>  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/isabelle-dev

[isabelle-dev] Complete Distributive Lattice

[viorel.preoteasa]

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 current repository version.

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?

 

Best regards,

 

Viorel Preoteasa

 

 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Viorel Preoteasa]

OK, I understand, what is the time frame for going back to normal? I did 
spent some time on this and I would like to see it finished.


As I mentioned earlier, I added finite lattices to simplify the proofs
in Enum.thy that finite_n are distributive complete lattices. However,
searching for dependencies on complete_distrib_lattice, I found a very 
similar class of finite lattices in Library. How should this be handled?


Viorel

On 8/28/2017 5:26 PM, Lawrence Paulson wrote:
For sure. The work is very welcome, but too drastic to undertake at this 
precise moment.

Larry

On 28 Aug 2017, at 13:08, Makarius > wrote:


Nothing of this is relevant for the Isabelle2017 release. When the "RC"
versions show up, it is time to finish and not to start new things.



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Makarius]

On 28/08/17 20:26, Viorel Preoteasa wrote:
> OK, I understand, what is the time frame for going back to normal?

This is hard to say, since official Isabelle2017-RC1 is not even there
yet, but it is planned for Sun 03-Sep-2017.

The final lift off will probably take 6 weeks from Isabelle2017-RC1, but
it also depends a lot on the participation of users testing the RC chain.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Lawrence Paulson]

For sure. The work is very welcome, but too drastic to undertake at this 
precise moment.
Larry

> On 28 Aug 2017, at 13:08, Makarius  wrote:
> 
> Nothing of this is relevant for the Isabelle2017 release. When the "RC"
> versions show up, it is time to finish and not to start new things.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Makarius]

On 27/08/17 16:59, Viorel Preoteasa wrote:
> I managed to integrate the new complete distributive lattice into HOL
> library.
> 
> The changes are these:
> 
> Timing HOL (2 threads, 266.231s elapsed time, 487.094s cpu time, 43.344s
> GC time, factor 1.83)
> Finished HOL (0:04:26 elapsed time)
> 
> Finished at Sun Aug 27 17:41:30 GMT+3 2017
> 0:04:37 elapsed time
> 
> But I don't now how to go from here to have these changes into Isabelle.

Someone who understands Isabelle library maintenance needs to pick it up
and apply it in the proper way. This usually takes quite some time, and
exposes many unexpected problems. Main HOL is not easily changed on the
spot.


> There is also AFP.

This usually takes 2-3 more rounds of exploration.


Nothing of this is relevant for the Isabelle2017 release. When the "RC"
versions show up, it is time to finish and not to start new things.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev