> 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-boun...@mailbroy.informatik.tu-muenchen.de>
> On Behalf Of Manuel Eberl
> Sent: Saturday, March 10, 2018 1:26 AM
> To: firstname.lastname@example.org
> 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
> 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: email@example.com
>> 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
>> 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-dev mailing list
isabelle-dev mailing list