Re: [isabelle-dev] Fwd: status (AFP)
Thanks. I've set the JinjaThreads test to run every day now, at least until the release. In Munich, we now also use our number cruncher lxbroy10 to run the large (non-frequently tested) AFP sessions within the new testing infrastructure. This should give us some more light on failures of these AFP theories in the future. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards release
We have had this problem before with Isabelle2011. PG 4.x has a certain idea about using glyphs from existing Unicode fonts, with a preference for STIXGeneral as fall-back option As you'd expect, this is all highly configurable at PG level (see lib/unicode-tokens.el and isar/isar-unicode-tokens.el), I just set picked some reasonable default fonts and Unicode points which worked well when I wrote the code 3 years ago. I welcome improvements from anyone. By default all symbols are taken from a single Unicode font, which seems simplest and most sensible with the advent of STIX. There are mechanisms to try to choose fallback symbol renderings automatically, which can be taken glyphs or sequences of glyphs from other fonts (see isar-symbols-tokens-fallbacks). But the automation is tricky because the functions to determine whether a glyph is blank or not are not reliable. Mac users should be aware that there are issues with the underlying font support on the native Mac port of Emacs, although a couple of these have been fixed recently they haven't made it into a released version yet. http://proofgeneral.inf.ed.ac.uk/trac/ticket/338 http://proofgeneral.inf.ed.ac.uk/trac/ticket/409 I think the worst problem is broken super/sub scripts. I've checked that this *is* fixed now in the current nightly builds at http://emacsformacosx.com/builds, but it's probably not a good idea to bundle one of those with the release, 8-(. - David -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Testboard reset: Old Testboard changesets are removed
Hello all, Lars and I have taken over the maintenance of the reports and testboard from Alex yesterday. Today, due to some storage issues, we did not learn early enough about, the testboard repository changed into an inconsistent state. I reset the testboard repository to start with a clean clone from the development repository and now everything should work again. If anyone is eager to restore the old testboard's changesets, we are happy for any assistance, otherwise we will discard them within the next week, if no one objects. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard reset: Old Testboard changesets are removed
Hi Lukas, I reset the testboard repository to start with a clean clone from the development repository and now everything should work again. If anyone is eager to restore the old testboard's changesets, we are happy for any assistance, otherwise we will discard them within the next week, if no one objects. I've had the same issue (for the same reason :-) ) once or twice before. Usually, running hg verify on the repository will tell you the first corrupted revision (usually the one you were pulling when running out of space/quota), and you can then clone everything else, which gets you back where you started. While it may be a good idea to clean up testboard once in a while (I am not sure how well hg scales to thousands of heads), we should try to archive the changesets somewhere. Otherwise it will be impossible to read old threads on the list, which sometimes refer to them. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
