Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)

[Makarius]

On 13/03/2019 21:06, Lars Hupel wrote:
>> "Unable to increase stack" is one of the various messages that tells
>> you that PolyML has run out of resources. It doesn't really tell you
>> what the problem is though. It might be an actual problem or a
>> temporary problem caused by a machine being overloaded.
> 
> This is likely connected to the recent change of platform. I will
> investigate this; maybe bumping the memory limit will resolve it.

BTW, with Poly/ML 5.8 being official, you can avoid full x86_64 for most
applications and always use the default x86_64_32.

This saves a lot of resources: I usually have ML_OPTIONS="--minheap
1500" with an open upper end -- the implicit limit is approx. 16G.

Even some entries of the slow/large groups of AFP work well with
x86_64_32, but I usually throw them into on big x86_64 pot as a special
case.

Another remaining application of full x86_64 is the huge PIDE session
forked by "isabelle dump" and related tools: it can require 64GB
(excluding slow), and I have not explored the upper end yet.


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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)

[Lars Hupel]

"Unable to increase stack" is one of the various messages that tells
you that PolyML has run out of resources. It doesn't really tell you
what the problem is though. It might be an actual problem or a
temporary problem caused by a machine being overloaded.


This is likely connected to the recent change of platform. I will 
investigate this; maybe bumping the memory limit will resolve it.


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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)

[Thomas Sewell]

"Unable to increase stack" is one of the various messages that tells you that 
PolyML has run out of resources. It doesn't really tell you what the problem is 
though. It might be an actual problem or a temporary problem caused by a 
machine being overloaded.

Cheers,
Thomas.

On 2019-03-12 12:14, Lawrence Paulson wrote:
Does anybody know what this is?

01:58:19 Running HOL-Quickcheck_Benchmark ...01:58:20 HOL-Quickcheck_Benchmark: 
theory HOL-Quickcheck_Benchmark.Needham_Schroeder_Base01:58:20 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Find_Unused_Assms_Examples01:58:23 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_Guided_Attacker_Example01:58:24 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_No_Attacker_Example01:58:24 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_Unguided_Attacker_Example02:12:01 
Warning - Unable to increase stack - interrupting thread02:12:01 *** 
Interrupt02:12:01 HOL-Quickcheck_Benchmark FAILED

Larry

> Begin forwarded message:
>
> From: Isabelle/Jenkins 
> Subject: [Isabelle-ci] Build failure in Isabelle (benchmark)
> Date: 12 March 2019 at 01:22:32 GMT
> To: 
> isabelle...@mail46.informatik.tu-muenchen.de
>
> The Isabelle build failed. See the log at: 
> https://ci.isabelle.systems/jenkins/job/isabelle-nightly-benchmark/887/
> ___
> Isabelle-ci mailing list
> isabelle...@mail46.informatik.tu-muenchen.de
> https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci

___
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] Fwd: [Isabelle-ci] Build failure in Isabelle

[Makarius]

On 09/08/16 23:51, Makarius wrote:
> On 08/08/16 14:44, Lars Hupel wrote:
>>
>> For HOL-Proofs, the relevant job is "isabelle-repo-makeall". A catalog
>> of all builds and all archived logs can be found under the following URL:
>>
>>
>> 
> 
> I did not know of this JSON API yet. In Isabelle/74604a9fc4c8 there are
> Isabelle/Scala operations to access that information. (It is an
> interesting experience to work with these untyped JSON things; reminds
> me of LISP expressions.)
> 
> I will later work out, if this is going to be a batch tool (like former
> isatest-stats) or a PIDE GUI panel. It might be actually easier to make
> proper a GUI application than a web application from it.

For now I've made a batch tool, see Isabelle/b7aab1a6cf0d. Here is an
example invocation:

  build_stats -S HOL,HOL-Proofs -s 1024x768 isabelle-repo-makeall
isabelle-nightly-benchmark

Resulting PNGs are attached (the actual result contains some HTML around
that).


Now we see that we see nothing: the repo-makeall test data looks as
messy as a climate change diagram!

This is probably a consequence of running the regular test against
itself with option -j. The nightly-benchmark does not do that for main
HOL, so it is much better. There might be also a problem from the
virtualization of the machine, meaning that the nightly-benchmark is
only clean as long as no other virtual slice is active: this needs to be
practically verified.


Note that the isatest runs were carefully crafted not to conflict with
anything else, using -j1 and threads=1,2,4,8 for meaningful
measurements. (Threads=2 is actually relatively uninteresting.)

Is it possible to let Jenkins redo the changes from the last 4 weeks
with a setup that produces good physical measurements?


Makarius

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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Makarius]

On 08/08/16 14:44, Lars Hupel wrote:
> 
> For HOL-Proofs, the relevant job is "isabelle-repo-makeall". A catalog
> of all builds and all archived logs can be found under the following URL:
> 
> 
> 

I did not know of this JSON API yet. In Isabelle/74604a9fc4c8 there are
Isabelle/Scala operations to access that information. (It is an
interesting experience to work with these untyped JSON things; reminds
me of LISP expressions.)

I will later work out, if this is going to be a batch tool (like former
isatest-stats) or a PIDE GUI panel. It might be actually easier to make
proper a GUI application than a web application from it.


Makarius

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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Lars Hupel]

> With a chart showing performance parameters (CPU time, elapsed time,
> heap size) in the past few weeks, it should be normally easy to see a
> small step or spike for HOL-Proofs or its applications.

Happy to assist with that. In a previous mail you indicated that these
parameters can be found in the log files. Luckily, Jenkins archives all
of them indefinitely.

For HOL-Proofs, the relevant job is "isabelle-repo-makeall". A catalog
of all builds and all archived logs can be found under the following URL:




This catalog also contains a timestamp (which I believe is the regular
Unix timestamp but with milliseconds instead of seconds).

The URLs where the specific log files can be found is easy to construct,
e.g.




That should contain all necessary data for plotting performance graphs.

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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Makarius]

On 08/08/16 11:14, Lars Hupel wrote:
> Dear all,
> 
> the latest build failure for the repository is spurious:
> 
> *** exception Fail raised (line 83 of "./basis/PolyMLException.sml"):
> Insufficient memory
> 
> This happened in HOL-Proofs. Makarius, it may or may not be connected to
> the recent changes you did in proof reconstruction (994d1a1105ef).

This situation illustrates what "flying blind means" concerning
continuous testing.

With a chart showing performance parameters (CPU time, elapsed time,
heap size) in the past few weeks, it should be normally easy to see a
small step or spike for HOL-Proofs or its applications.


Makarius

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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Makarius]

On 08/08/16 13:13, Manuel Eberl wrote:
> I've heard of negative thermal expansion in some materials, but I don't
> think RAM is subject to it. (scnr)
> 
> In a more serious fashion: I don't see how ambient temperature could
> affect memory usage. I've run into "insufficient memory" and stack
> overflow problems in Isabelle several times lately, usually sporadically
> and irreproducibly.

The point is that a hot CPU runs slower. Memory management in Poly/ML
works on multiple cores, and the runtime behaviour changes the
characteristics of how the heap is cleaned up and resized dynamically.


> Perhaps the times when 32 Bit Isabelle was enough for all applications
> are indeed over.

I don't think that this is the case here.


Makarius


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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Tobias Nipkow]

On 08/08/2016 13:13, Manuel Eberl wrote:

I've heard of negative thermal expansion in some materials, but I don't think
RAM is subject to it. (scnr)

In a more serious fashion: I don't see how ambient temperature could affect
memory usage. I've run into "insufficient memory" and stack overflow problems in
Isabelle several times lately, usually sporadically and irreproducibly.


On my laptop this happens fairly reliably for some time now with HOL-Proofs or 
related sessions. I played around with PolyML parameters, but to no avail.


Tobias


Perhaps the times when 32 Bit Isabelle was enough for all applications are
indeed over.


Cheers,

Manuel


On 08/08/16 13:06, Makarius wrote:

On 08/08/16 11:14, Lars Hupel wrote:

the latest build failure for the repository is spurious:

*** exception Fail raised (line 83 of "./basis/PolyMLException.sml"):
Insufficient memory

This happened in HOL-Proofs.

I have tried Isabelle/1e7c5bbea36d once again with

  ML_PLATFORM="x86-linux"
  ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.6-1/x86-linux"
  ML_SYSTEM="polyml-5.6"
  ML_OPTIONS="-H 1000 --gcthreads 2"

The result is:

Finished HOL-Proofs (0:17:18 elapsed time, 0:33:38 cpu time, factor 1.94)


Is the test hardware in an air-conditioned server room? Otherwise we
might be actually testing the surrounding temperature or some other
environmental effects.



Makarius, it may or may not be connected to
the recent changes you did in proof reconstruction (994d1a1105ef).

This is merely for printing, which normally does not happen at all.


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Manuel Eberl]

I've heard of negative thermal expansion in some materials, but I don't 
think RAM is subject to it. (scnr)


In a more serious fashion: I don't see how ambient temperature could 
affect memory usage. I've run into "insufficient memory" and stack 
overflow problems in Isabelle several times lately, usually sporadically 
and irreproducibly.


Perhaps the times when 32 Bit Isabelle was enough for all applications 
are indeed over.



Cheers,

Manuel


On 08/08/16 13:06, Makarius wrote:

On 08/08/16 11:14, Lars Hupel wrote:

the latest build failure for the repository is spurious:

*** exception Fail raised (line 83 of "./basis/PolyMLException.sml"):
Insufficient memory

This happened in HOL-Proofs.

I have tried Isabelle/1e7c5bbea36d once again with

   ML_PLATFORM="x86-linux"
   ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.6-1/x86-linux"
   ML_SYSTEM="polyml-5.6"
   ML_OPTIONS="-H 1000 --gcthreads 2"

The result is:

Finished HOL-Proofs (0:17:18 elapsed time, 0:33:38 cpu time, factor 1.94)


Is the test hardware in an air-conditioned server room? Otherwise we
might be actually testing the surrounding temperature or some other
environmental effects.



Makarius, it may or may not be connected to
the recent changes you did in proof reconstruction (994d1a1105ef).

This is merely for printing, which normally does not happen at all.


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] Fwd: [Isabelle-ci] Build failure in Isabelle

[Makarius]

On 08/08/16 11:14, Lars Hupel wrote:
> the latest build failure for the repository is spurious:
> 
> *** exception Fail raised (line 83 of "./basis/PolyMLException.sml"):
> Insufficient memory
> 
> This happened in HOL-Proofs.

I have tried Isabelle/1e7c5bbea36d once again with

  ML_PLATFORM="x86-linux"
  ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.6-1/x86-linux"
  ML_SYSTEM="polyml-5.6"
  ML_OPTIONS="-H 1000 --gcthreads 2"

The result is:

Finished HOL-Proofs (0:17:18 elapsed time, 0:33:38 cpu time, factor 1.94)


Is the test hardware in an air-conditioned server room? Otherwise we
might be actually testing the surrounding temperature or some other
environmental effects.


> Makarius, it may or may not be connected to
> the recent changes you did in proof reconstruction (994d1a1105ef).

This is merely for printing, which normally does not happen at all.


Makarius

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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Manuel Eberl]

Sure, I can do that later today.

By the way, "isabelle build -o document=pdf HOL-Multivariate_Analysis" 
builds the session with document processing enabled. If it fails, it 
tells you both the location of the document directory (with all the 
generated LaTeX files) and the build log.


In my experience, the build log is often too long for me to find the 
errors in it, so I usually just go to the document directory, run 
"pdflatex root.tex" and see where it gets stuck.


Cheers,

Manuel



On 16/06/16 00:13, Lawrence Paulson wrote:

Many thanks for getting to the bottom of these problems!

All of these texts were copied from HOL Light. I can fix them sometime 
tomorrow, or feel free to do it yourself if you prefer.

--lcp


On 15 Jun 2016, at 21:17, Manuel Eberl  wrote:

There is one instance in Extension.thy where you wrote "real ^ n" in a subsection heading 
about Urysohn's lemma. That causes an error when interpreted as LaTeX code. I suggest replacing it 
with "Euclidean space", which is more apt in Isabelle anyway, I should think.

There are two more instances in Brouwer_Fixpoint.thy where you wrote something like 
"R^n" in text, causing the same error.

Cheers,

Manuel



On 15/06/16 18:19, Lawrence Paulson wrote:
No idea what’s going on here. I did commit a lot of stuff but it works on my 
machine. I added a theory, but the addition was committed and I have no 
untracked files. If anybody can figure out what’s going on I'd be grateful. I 
see it is a document preparation failure, presumably that isn’t being checked 
locally for some reason?

Larry


Begin forwarded message:

From: Isabelle/Jenkins 
Subject: [Isabelle-ci] Build failure in Isabelle
Date: 15 June 2016 at 17:14:27 BST
To: isabelle...@mail46.informatik.tu-muenchen.de

The Isabelle build failed. See the log at: 
https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/249/



___
Isabelle-ci mailing list
isabelle...@mail46.informatik.tu-muenchen.de
https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci




___
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



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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Lawrence Paulson]

Many thanks for getting to the bottom of these problems!

All of these texts were copied from HOL Light. I can fix them sometime 
tomorrow, or feel free to do it yourself if you prefer.

--lcp

> On 15 Jun 2016, at 21:17, Manuel Eberl  wrote:
> 
> There is one instance in Extension.thy where you wrote "real ^ n" in a 
> subsection heading about Urysohn's lemma. That causes an error when 
> interpreted as LaTeX code. I suggest replacing it with "Euclidean space", 
> which is more apt in Isabelle anyway, I should think.
> 
> There are two more instances in Brouwer_Fixpoint.thy where you wrote 
> something like "R^n" in text, causing the same error.
> 
> Cheers,
> 
> Manuel
> 
> 
>> On 15/06/16 18:19, Lawrence Paulson wrote:
>> No idea what’s going on here. I did commit a lot of stuff but it works on my 
>> machine. I added a theory, but the addition was committed and I have no 
>> untracked files. If anybody can figure out what’s going on I'd be grateful. 
>> I see it is a document preparation failure, presumably that isn’t being 
>> checked locally for some reason?
>> 
>> Larry
>> 
>>> Begin forwarded message:
>>> 
>>> From: Isabelle/Jenkins 
>>> Subject: [Isabelle-ci] Build failure in Isabelle
>>> Date: 15 June 2016 at 17:14:27 BST
>>> To: isabelle...@mail46.informatik.tu-muenchen.de
>>> 
>>> The Isabelle build failed. See the log at: 
>>> https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/249/
>>> 
>>> 
 ___
 Isabelle-ci mailing list
 isabelle...@mail46.informatik.tu-muenchen.de
 https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci
>>> 
>>> 
>>> 
>>> ___
>>> 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

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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Manuel Eberl]

There is one instance in Extension.thy where you wrote "real ^ n" in a 
subsection heading about Urysohn's lemma. That causes an error when 
interpreted as LaTeX code. I suggest replacing it with "Euclidean 
space", which is more apt in Isabelle anyway, I should think.


There are two more instances in Brouwer_Fixpoint.thy where you wrote 
something like "R^n" in text, causing the same error.


Cheers,

Manuel


On 15/06/16 18:19, Lawrence Paulson wrote:

No idea what’s going on here. I did commit a lot of stuff but it works on my 
machine. I added a theory, but the addition was committed and I have no 
untracked files. If anybody can figure out what’s going on I'd be grateful. I 
see it is a document preparation failure, presumably that isn’t being checked 
locally for some reason?

Larry


Begin forwarded message:

From: Isabelle/Jenkins 
Subject: [Isabelle-ci] Build failure in Isabelle
Date: 15 June 2016 at 17:14:27 BST
To: isabelle...@mail46.informatik.tu-muenchen.de

The Isabelle build failed. See the log at: 
https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/249/



___
Isabelle-ci mailing list
isabelle...@mail46.informatik.tu-muenchen.de
https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci




___
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