Re: [isabelle-dev] Towards the next release
On Fri, 30 Nov 2012, Lawrence Paulson wrote: Doubtless some student enjoys tinkering with video formats and could make a five-minute video that simply answers the question, how do I get started? What are the main interaction modes? And maybe touches on some of the more advanced features. I had pointed to this before, but it still fun to watch: http://www.youtube.com/user/bauerandrej He is using a different proof assistant, but the classic Proof General 3.7.1.1. So this guy actually has an Isabelle distribution around as well. The last official version of the 3.x branch was 3.7.1, and I made this "temporary lifetime extension" for the Isabelle distribution in desparation when the Emacs platform was moving forward, but PG 4.x was still not to be seen to catch up. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
I don't think you need to do this personally. Doubtless some student enjoys tinkering with video formats and could make a five-minute video that simply answers the question, how do I get started? What are the main interaction modes? And maybe touches on some of the more advanced features. Larry On 30 Nov 2012, at 15:27, Makarius wrote: > On Fri, 30 Nov 2012, Lawrence Paulson wrote: > >> I imagine that some sort of short tutorial video or slideshow (analogous to >> the one I made a number of years ago) might be better than any amount of >> written documentation. > > I've recently started experimenting with video recording, which works quite > well e.g. on Ubuntu 12.04 with one of the many open-source applications for > that. > > After spending some hours on it, I tried to present the results on a web page > and failed miserably. Web "standards" don't really exist. One might > interpret the "5" in HTML5 as "5 years from now" or "need 5 different formats > for your video". Most people seem to delegate the problem to Youtube. > > I am only a beginner in the film production business. So maybe some experts > on it can say more. > > Once the technical side-conditions are worked out, one needs to have a good > "script" to explain how to produce nice proof documents (not scripts). > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
On Fri, 30 Nov 2012, Lawrence Paulson wrote: I think we should still include hints on how to use PG but without the same level of support as in the past. Obviously, if a clamour arose for a bundled PG version, we could deal with that at the time. Whatever happens, it needs to be clear reasonably early before the actual release, and afterwards we cannot change it until the next release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
On Fri, 30 Nov 2012, Lawrence Paulson wrote: I imagine that some sort of short tutorial video or slideshow (analogous to the one I made a number of years ago) might be better than any amount of written documentation. I've recently started experimenting with video recording, which works quite well e.g. on Ubuntu 12.04 with one of the many open-source applications for that. After spending some hours on it, I tried to present the results on a web page and failed miserably. Web "standards" don't really exist. One might interpret the "5" in HTML5 as "5 years from now" or "need 5 different formats for your video". Most people seem to delegate the problem to Youtube. I am only a beginner in the film production business. So maybe some experts on it can say more. Once the technical side-conditions are worked out, one needs to have a good "script" to explain how to produce nice proof documents (not scripts). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
It actually makes sense to put every effort into making the jEdit version as good as possible, especially for beginners. It might be worth investigating what issues cause them the most problems; I imagine that some sort of short tutorial video or slideshow (analogous to the one I made a number of years ago) might be better than any amount of written documentation. I think we should still include hints on how to use PG but without the same level of support as in the past. Obviously, if a clamour arose for a bundled PG version, we could deal with that at the time. Larry On 29 Nov 2012, at 17:22, Makarius wrote: > Generally, it touches the question if Proof General should be bundled at all. > I started that a long time ago to approximate an out-of-the-box experience > for Isabelle, but never succeeded in the last consequence. Right now there > are PG 3.7.1.1, 4.0, 4.1 being activly used, so which one to chose? (I would > have taken the latest stable version.) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
