Hi Makarius, Thank you for the pointers.
I did not publish my reasons for still using Proof General because in such cases my reasons are typically not very useful. But I'll give it a try: Proof General is a silent proof partner who gives me a lot of space. By contrast, Isabelle/jEdit seems like a corridor full of smart people who keep offering to help me. I prefer to do proofs with my office door closed. Andrei On Thursday, May 15, 2014 11:13 PM, Makarius <makar...@sketis.net> wrote: On Thu, 15 May 2014, Andrei Popescu wrote: > Concerning HyperCTL: I will fix this by Tuesday at 8:00 AM. (Sorry for > delaying this. > > I was extremely busy the last weeks, and did not get a chance to pull > out the development version and fix In Isabelle/01637dd1260c + AFP/12b00c2f46bf we are back to normal, which means that HyperCTL is still not terminating. So I have added this: changeset: 4462:12b00c2f46bf tag: tip user: wenzelm date: Thu May 15 23:04:42 2014 +0200 files: thys/HyperCTL/ROOT description: tighter timeout, to avoid burning test cycles with this non-terminating entry; Once you are finished with it, you need to reset the timeout to something reasonable: 600 is a common default. Here is also the relevant part of isabelle/README_REPOSITORY: cd isabelle hg pull -u ./bin/isabelle components -a ./bin/isabelle jedit -l HOL Isabelle/jEdit is particularly useful for such maintenance tasks. If you are still using Proof General, you should indeed be ashamed that you did not publish your list of remaining reasons for that. (That thread is still open.) Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
