[isabelle-dev] isabelle.in.tum.de web server encoding
Dear Apache experts, some days ago I noticed the famous French problem http://www.apprendre-en-ligne.net/bloginfo/index.php/2009/01/21/151-martine-ecrit-en-utf-8 on the TUM web server. This affects names in http://isabelle.in.tum.de/website-Isabelle2013-RC2/dist/Isabelle2013-RC2/CONTRIBUTORS for example. Right now I don't see it, maybe because it is due to a different web client configuration on my side. In principle, the local config-tum repository should tell about the situation, but I am unsure where is the right spot to tell Apache using UTF-8 encoding by default. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle.in.tum.de web server encoding
Just as a further data point: when visiting http://isabelle.in.tum.de/website-Isabelle2013-RC2/dist/Isabelle2013-RC2/CONTRIBUTORS using firefox (on Linux) where the default encoding on the client side is Western ISO-8859-1 then some symbols are strange. If I explicitly set the encoding to Unicode UTF-8, everything seems fine. cheers chris On 02/06/2013 09:20 PM, Makarius wrote: Dear Apache experts, some days ago I noticed the famous French problem http://www.apprendre-en-ligne.net/bloginfo/index.php/2009/01/21/151-martine-ecrit-en-utf-8 on the TUM web server. This affects names in http://isabelle.in.tum.de/website-Isabelle2013-RC2/dist/Isabelle2013-RC2/CONTRIBUTORS for example. Right now I don't see it, maybe because it is due to a different web client configuration on my side. In principle, the local config-tum repository should tell about the situation, but I am unsure where is the right spot to tell Apache using UTF-8 encoding by default. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problem with let-simproc
I'd forgotten I'd ever reported this to you. My problems with let_simproc run a little deeper anyway, and I've moved to a different approach in the meanwhile. Sorry if I've left you labouring on my behalf. Yours, Thomas. On 07/02/13 02:38, Johannes Hölzl wrote: Am Mittwoch, den 06.02.2013, 12:25 +0100 schrieb Makarius: On Tue, 5 Feb 2013, Johannes Hölzl wrote: there is a bugproblem with the let-simproc, resulting in a non terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of isabelle-release): theory Scratch imports Complex_Main begin lemma (let x = Collect P in R x x ∧ (Ball s P)) = X using [[simp_trace]] apply simp The attached hg-bundle changes this behaviour to a terminating simproc. (The bundle can be applied to a repo containing #58e2d0cd81ae by hg pull let_simp_betaeta.bundle) It currently runs in the testboard: http://isabelle.in.tum.de/testboard/Isabelle/rev/31f3b7c70a2c @Makarius: Is it possible to include this patch in Isabelle2013, when the testboard run is green? Testboard does not test very much, compared to what has been tested manually and semi-automatically in the past 2 weeks for the release. AFP would also have to be covered. Anyway, this behaviour of let_simproc seems to have been there from its beginning, or at least back until Isabelle2011 (what is what I have tried). Nobody has noticed a problem in several years, so this change is for the next release, unless there are really strong reasons to revisit it now. Makarius Thomas reported the problem to me. For me it is okay to fix it after Isabelle2013. @Thomas: Is it important for you to fix it in Isabelle2013? I hope the workaround with adding Let_def to the simplifier should work fine. Then I will add it just to the development version of Isabelle. - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
