[isabelle-dev] Non-responding Isabelle/jEdit and Monitor panel

Hi, I observed (in at least a99125aa964f) that when Isabelle/jEdit has been running for some time (about 2 to 4 hours perhaps), the GUI starts to "hang": every 3-4 seconds, the GUI does not respond to inputs for about half a second. I realized that this is apparently related to the Monitor

Re: [isabelle-dev] the function "real"

Okay, I look at the AFP entries. I assume Affine_Arithmetic is just slow, but I can ask Fabian tomorrow if this is unusual. - Johannes Am Mittwoch, den 11.11.2015, 17:19 + schrieb Lawrence Paulson: > It would be great if you could help. I have just committed some > corrections to a number

Re: [isabelle-dev] the function "real"

It would be great if you could help. I have just committed some corrections to a number of AFP theories, including that one I think. Affine_Arithmetic comes with some examples that run extremely slowly; I’m not sure whether there is a problem or whether it is always like that. If you want to

Re: [isabelle-dev] the function "real"

Hi Larry, this is a huge change and after I adapted Markov_Models I see that it simplifies some proofs. If you want I can adapt all AFP entries for which I'm the maintainer, or which are related to Probability theory: Density_Compiler Integration Lower_Semicontinuous Markov_Models

Re: [isabelle-dev] the function "real"

I’m glad to have your support. It’s just possible that I might ask your help in getting some things working in the AFP. Larry > On 10 Nov 2015, at 17:53, Manuel Eberl wrote: > > This is very nice to hear. ‘real’ has plagued me for some time now and I am > glad to see it

[isabelle-dev] Proposal to use hierarchical heaps with Poly/ML

Hi all, Isabelle currently saves fully self-contained heaps. This is wasteful since a low-level session like HOL will be duplicated in every heap that depends on it. For a long time, Poly/ML has supported hierarchical heaps (PolyML.SaveState.saveChild). As I understand it, this feature was not

Re: [isabelle-dev] the function "real"

It looks like the setup for blast changed, in the following entries is a non-terminating blast call. They do not seam to be related to the change at all: Graph_Theory ShortestPath Rank_Nullity_Theorem Echelon_Form Gauss_Jordan Interestingly in Jordan_Normal_Form QR_Decomposition a