Re: [isabelle] 2016-1-RC4 Responsiveness



On 03/12/16 13:11, Makarius wrote:
> On 01/12/16 15:57, Peter Lammich wrote:
>>
>> I just had to restart the IDE two times before I found a non-
>> terminating "meson"-method in my theory ... As soon as this method was
>> reached, the prover instantly got unresponsive, and did not recover
>> within a few minutes.
> 
> In order to do anything, I need a tangible problem report, i.e.
> reproducible situation of such non-terminating "meson" invocation.
> 
> Without that there is just speculation: e.g. "potentially useful"
> warning messages emitted by some ML tools and underlying operations. I
> see a few such warnings in the sources src/HOL/Tools/Meson/ and its
> underlying src/Tools/misc_legacy.ML, but it is unclear if these are
> relevant.

The warning in Misc_Legacy.METAHYPS is about schematic variables. Meson
is the main user of METAHYPS, and you are the main user of schematic
variables. So there is some chance that this is significant.

I have now removed that "potentially useful output" in
https://bitbucket.org/isabelle_project/isabelle-release/commits/8b187a7a9776


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.