Re: [isabelle] 2016-1-RC4 Responsiveness



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.


	Makarius





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