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

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

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

"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

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

"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

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

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: >> >> >>

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

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: > > >

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

> 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

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

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

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

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 >

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

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

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

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

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

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

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

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

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

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

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

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