Florian Haftmann wrote:
> > HOL-Analysis can’t be built (reproducibly) with the latest version
> > (76f2d492627e). It simply dies, no error message.
>
> I cannot reproduce this.
Neither can I; using polyml-b68438d33c69 I can build HOL-Analysis
with Isabelle-24bbc4e30e5b and manual
On 02/02/2019 15:37, Lawrence Paulson wrote:
> This worked — thanks!
>
>> On 2 Feb 2019, at 13:56, Makarius wrote:
>>
>> Can you try the following in your $ISABELLE_HOME_USER/etc/settings?
>>
>> init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202"
OK.
With Isabelle/76f2d492627e
This worked — thanks!
Larry
> On 2 Feb 2019, at 13:56, Makarius wrote:
>
> Can you try the following in your $ISABELLE_HOME_USER/etc/settings?
>
> init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202"
>
> Apparently, the last two updates on polyml-test were not as monotonic as
>
On 02/02/2019 14:56, Makarius wrote:
> On 02/02/2019 14:39, Lawrence Paulson wrote:
>> It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle
>> jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”.
>>
>> The reason I fetched in the first place was that
On 02/02/2019 14:39, Lawrence Paulson wrote:
> It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle
> jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”.
>
> The reason I fetched in the first place was that I was getting crashes in my
>
It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle
jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”.
The reason I fetched in the first place was that I was getting crashes in my
interactive sessions.
Larry
> On 2 Feb 2019, at 13:26, Florian
> HOL-Analysis can’t be built (reproducibly) with the latest version
> (76f2d492627e). It simply dies, no error message.
I cannot reproduce this.
ML_PLATFORM="x86_64_32-linux"
ML_SYSTEM="polyml-5.7.1"
ML_OPTIONS="--maxheap 9G"
Have you tried a fresh build or delete the corresponding log
HOL-Analysis can’t be built (reproducibly) with the latest version
(76f2d492627e). It simply dies, no error message.
Larry
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
