> On 06.10.2015, at 22:55, Jasmin Blanchette wrote:
>
> The problem is most likely caused by ebf296fe88d7. Looking at it more
> closely, one sees a proof that is (at least) quadratic in the number of
> constructors:
>
>fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distinct
> On 06.10.2015, at 22:37, Makarius wrote:
>
>> On Tue, 6 Oct 2015, Dmitriy Traytel wrote:
>>
>> So the main candidates for bad changesets are: ebf296fe88d7, 2ebdd603cd71.
>
> More results on macbroy2:
>
> 5b5656a63bd6
> Finished HOL-Proofs (0:18:14 elapsed time, 0:49:28 cpu time, factor 2.71
On Tue, 6 Oct 2015, Makarius wrote:
On Tue, 6 Oct 2015, Dmitriy Traytel wrote:
As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in
about 17 minutes.
This conforms to my expectations: HOL-Proofs is slow, but works.
I am presently on a side-branch starting from 5b5656a6
On Tue, 6 Oct 2015, Dmitriy Traytel wrote:
As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about
17 minutes.
This conforms to my expectations: HOL-Proofs is slow, but works.
I am presently on a side-branch starting from 5b5656a63bd6, and that works
as well: https://
As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about
17 minutes.
Timing = :threads=4elapsed=979.269cpu=2582.077gc=323.518factor=2.64
Dmitriy
> On 06 Oct 2015, at 21:54, Jasmin Blanchette
> wrote:
>
> Hi Makarius,
>
>> My impression is that ebf296fe88d7 (blan
Hi Makarius,
> My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out of
> resources and fail. I've made approx. 3 runs in the vicinity -- it always
> takes very long.
>
> Is that another failure to do a full "isabelle build -a" before pushing
> anything?
I did "isabelle
My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out
of resources and fail. I've made approx. 3 runs in the vicinity -- it
always takes very long.
Is that another failure to do a full "isabelle build -a" before pushing
anything?
I've actually violated this principle my
On Wed, 14 May 2014, Tobias Nipkow wrote:
This is what I did interactively: starting from Pure I loaded Proofs.thy
first and then Main.thy. Maybe this did not really switch proof terms
on?
That should do the right thing. The remaining explanation is that PIDE is
less aggressive in proof par
On 14/05/2014 16:06, Makarius wrote:
> On Wed, 14 May 2014, David Matthews wrote:
>
>> I don't know why it should be different when you run it interactively.
>
> That is just because an interactive PIDE session is quite different from a
> batch
> build session it what it does. I've tries for y
On Wed, 14 May 2014, David Matthews wrote:
I don't know why it should be different when you run it interactively.
That is just because an interactive PIDE session is quite different from a
batch build session it what it does. I've tries for years to unify that
further, but we are actually m
On 13/05/2014 17:18, Makarius wrote:
On Tue, 13 May 2014, Tobias Nipkow wrote:
I added a few lemmas to List and now the HOL-Proofs session no longer
terminates. This is what I got to see when I interrupted one run:
^Cpoly(52110,0xb0185000) malloc: *** mach_vm_map(size=8388608) failed
(error co
It seems that I have the same problem, because the 2 lemmas I added also use
metis. Playing around with system parameters does not do anything.
Tobias
On 14/05/2014 00:32, Ondřej Kunčar wrote:
> I also had a similar problem some time ago and I solved it by changing the
> proof. You can get by bis
I also had a similar problem some time ago and I solved it by changing
the proof. You can get by bisecting to the very point that makes
HOL-Proofs choke and change it. I am not sure anymore but I think in my
example I just changed metis for blast or something like this.
Ondrej
On 05/13/2014 0
On Tue, 13 May 2014, Tobias Nipkow wrote:
I added a few lemmas to List and now the HOL-Proofs session no longer
terminates. This is what I got to see when I interrupted one run:
^Cpoly(52110,0xb0185000) malloc: *** mach_vm_map(size=8388608) failed (error
code=3)
*** error: can't allocate regio
I added a few lemmas to List and now the HOL-Proofs session no longer
terminates. This is what I got to see when I interrupted one run:
^Cpoly(52110,0xb0185000) malloc: *** mach_vm_map(size=8388608) failed (error
code=3)
*** error: can't allocate region
*** set a breakpoint in malloc_error_break
>> As a first step, cf. the following changeset:
>>
>>> http://isabelle.in.tum.de/reports/Isabelle/rev/8b50286c36d3
>
> Testing this verson manually gives me 0:25:05 elapsed time total, while
> it is normally 0:16:30 on this machine with 8 cores and "build -j4 -a".
http://isabelle.in.tum.de/repo
On Mon, 22 Oct 2012, Florian Haftmann wrote:
Bijection then produced this:
The first bad revision is:
changeset: 49948:744934b818c7
user:haftmann
date:Sat Oct 20 09:12:16 2012 +0200
summary: moved quite generic material from theory Enum to more
appropriate places
I can't
On Mon, 22 Oct 2012, Florian Haftmann wrote:
HOL-Proofs has become very slow, see
http://www4.in.tum.de/~wenzelm/test/stats/mac-poly64-M8/HOL-Proofs.png
Btw. how do those graphs come into being? The still official devel
snapshot page does not link there…
It is the normal output of Admin/is
> In such cases, the general question is if making the sources "canonical"
> has any purpose. It is rather old material by Stefan Berghofer, written
> in the typical style from around 2000, and not going to be revisited in
> the foreseeable future.
It is, as part of the story Spec_Rules vs. code
On Mon, 22 Oct 2012, Florian Haftmann wrote:
I first thought it would be related to 1167c1157a5b (haftmann on
src/Pure/Proof/extraction.ML), which is not immediately easy to follow
in every detail.
It indeed isn't, but the effect is idempotent.
To my defence, reordering arguments is not very
> I first thought it would be related to 1167c1157a5b (haftmann on
> src/Pure/Proof/extraction.ML), which is not immediately easy to follow
> in every detail.
It indeed isn't, but the effect is idempotent.
To my defence, reordering arguments is not very comprehensible from a diff.
Floria
>> Bijection then produced this:
>>
>> The first bad revision is:
>> changeset: 49948:744934b818c7
>> user:haftmann
>> date:Sat Oct 20 09:12:16 2012 +0200
>> summary: moved quite generic material from theory Enum to more
>> appropriate places
>>
>>
>> I can't say for sure if t
On Sun, 21 Oct 2012, Makarius wrote:
Bijection then produced this:
The first bad revision is:
changeset: 49948:744934b818c7
user:haftmann
date:Sat Oct 20 09:12:16 2012 +0200
summary: moved quite generic material from theory Enum to more
appropriate places
I can't say f
HOL-Proofs has become very slow, see
http://www4.in.tum.de/~wenzelm/test/stats/mac-poly64-M8/HOL-Proofs.png
I first thought it would be related to 1167c1157a5b (haftmann on
src/Pure/Proof/extraction.ML), which is not immediately easy to follow in
every detail.
Bijection then produced this:
24 matches
Mail list logo
