Re: [isabelle-dev] NEWS: sightly more parallel checking
On 05/06/18 14:54, Fabian Immler wrote: > >> What kind of theory is this? Many commands? Long-running / >> non-terminating commands? > In this particular case, it was a relatively short theory (300 lines) with no > long-running or non-terminating commands. I inserted and removed some > diagnostic commands (code_thms, export_code foo in SML), but those were not > present anymore when I observed this 4-second-consolidation-loop. The consolidation operates on the whole theory graph, even if relatively little has actually happened. For a large session this might be expensive. I have now changed this in Isabelle/2fd3a6d6ba2e, and tested it with HOL-Library, HOL-Analysis, HOL-Probability, even with updates of the State panel in between. So far it looks good to me. Please keep me updated if there are remaining problems. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: sightly more parallel checking
> Am 05.06.2018 um 14:47 schrieb Makarius : > > On 05/06/18 14:45, Fabian Immler wrote: >> >> The only way to stop this apparently is to invalidate something in the beginning of the (currently open) theory. >>> >>> It should be possible to achieve this effect by removing the concluding >>> 'end' command. >> Just now I was in the middle of a theory (without any 'end' command), where >> every (are they supposed to happen periodically?) "consolidation" took about >> 4 seconds. >> >> It seems like something is accumulating somewhere when editing the document, >> because after invalidating the beginning of the theory and going back to the >> same place as before, the "consolidation" was not noticeable any more. > > What kind of theory is this? Many commands? Long-running / > non-terminating commands? In this particular case, it was a relatively short theory (300 lines) with no long-running or non-terminating commands. I inserted and removed some diagnostic commands (code_thms, export_code foo in SML), but those were not present anymore when I observed this 4-second-consolidation-loop. Fabian smime.p7s Description: S/MIME cryptographic signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: sightly more parallel checking
On 05/06/18 14:45, Fabian Immler wrote: > > >>> The only way to stop this apparently is to invalidate something in the >>> beginning of the (currently open) theory. >> >> It should be possible to achieve this effect by removing the concluding >> 'end' command. > Just now I was in the middle of a theory (without any 'end' command), where > every (are they supposed to happen periodically?) "consolidation" took about > 4 seconds. > > It seems like something is accumulating somewhere when editing the document, > because after invalidating the beginning of the theory and going back to the > same place as before, the "consolidation" was not noticeable any more. What kind of theory is this? Many commands? Long-running / non-terminating commands? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: sightly more parallel checking
> Am 05.06.2018 um 13:39 schrieb Makarius : > > On 04/06/18 20:17, Fabian Immler wrote: >> >> This "something in the background" appears to happen on a regular basis: >> every 2-3 seconds, the poly process consumes 200%CPU for about a second. >> poly should be idle (or used to be in such a situation) because (as far >> as I can tell) nothing else (e.g., sledgehammer, find theorems) seems to >> be active. > > This is probably due to the implicit "consolidation" of finished > theories, which I have made a bit more official as PIDE document edit > (see Isabelle/09ac56914b29). That is important, because of the final > "presentation", e.g. for generated LaTeX. > > In Isabelle/38272f9481c2, I have also changed the delay from 1s to 2.5s > -- you can make this 10s or more until I figure out a way to reduce the > impact of it. Thanks, this really seems to be the "consolidation": I can see the effect of chainging editor_consolidate_delay. >> The only way to stop this apparently is to invalidate something in the >> beginning of the (currently open) theory. > > It should be possible to achieve this effect by removing the concluding > 'end' command. Just now I was in the middle of a theory (without any 'end' command), where every (are they supposed to happen periodically?) "consolidation" took about 4 seconds. It seems like something is accumulating somewhere when editing the document, because after invalidating the beginning of the theory and going back to the same place as before, the "consolidation" was not noticeable any more. Fabian smime.p7s Description: S/MIME cryptographic signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: sightly more parallel checking
On 04/06/18 20:17, Fabian Immler wrote: > > This "something in the background" appears to happen on a regular basis: > every 2-3 seconds, the poly process consumes 200%CPU for about a second. > poly should be idle (or used to be in such a situation) because (as far > as I can tell) nothing else (e.g., sledgehammer, find theorems) seems to > be active. This is probably due to the implicit "consolidation" of finished theories, which I have made a bit more official as PIDE document edit (see Isabelle/09ac56914b29). That is important, because of the final "presentation", e.g. for generated LaTeX. In Isabelle/38272f9481c2, I have also changed the delay from 1s to 2.5s -- you can make this 10s or more until I figure out a way to reduce the impact of it. > The only way to stop this apparently is to invalidate something in the > beginning of the (currently open) theory. It should be possible to achieve this effect by removing the concluding 'end' command. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: sightly more parallel checking
*** Isabelle/jEdit Prover IDE *** * Slightly more parallel checking, notably for high priority print functions (e.g. State output). This refers to Isabelle/b00b40dc41af -- with various fine points in the organization of PIDE execution forks, not just the preceeding cd387c55e085. As we are heading towards the release, it is important to keep an eye on the system, that everything works smoothly. I will try not to touch more such delicate points of PIDE document processing. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
