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:13, Florian Haftmann wrote:
> * The module naming schema gets more sophisticated: default, name or
> prefix. The key point is that this naming schema is again
> target-language specific.
Just abstractly, a reform should strive for unification and
simplification whenever
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
>> Maybe the »checking« should just be a variant of the regular export.
>>
>> Hence the modification could be quite conservative:
>>
>> export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME )
>> ( file … | ( prefix … ) ( checked ) )
>>
>> where »file« denotes a relative root
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
