Email Gateway (Aug 18 2022 at 18:53): Email Gateway (Aug 18 2022 at 18:53):From: Makarius <makarius@sketis.net>
OK, that's one of the documented features in Isabelle2011-1, and will
hopefully disappear in the next release.
Makarius
Email Gateway (Aug 18 2022 at 18:53):From: Thomas Genet <Thomas.Genet@irisa.fr>
Great!
Thanks...
Thomas
Email Gateway (Aug 18 2022 at 18:54):From: René Neumann <rene.neumann@in.tum.de>
Hi Thomas,
this might be the very same problem that occurred to me on Gentoo: You
need to patch emacs (I don't know whether this is a bug in PG or in
Emacs). Please see http://proofgeneral.inf.ed.ac.uk/trac/ticket/409
Email Gateway (Aug 18 2022 at 18:54):From: Thomas Genet <Thomas.Genet@irisa.fr>
Dear René,
sorry for the delay...
Thanks for the pointer!
Hopefully, the fix we finally found did not require to patch emacs :-)
I think the problem we had was simpler than the one you pointed out.
Thanks anyway...
I hope that everything is ok at TUM...
Best regards,
Thomas
Email Gateway (Aug 18 2022 at 18:57):From: Thomas Genet <Thomas.Genet@irisa.fr>
Dear all,
we start a course on Isabelle here in Rennes but we have font problems
on the desktop computer we use for practical courses.
We use gentoo linux distrib on classroom's computers and its emacs
installation does not seem to behave well with Xsymbols. When the
Xsymbols mode is activated, depending on the font selected, logic
symbols are either partially or badly displayed.
For instance, no difference is made between symbols for "==>" and "=>"
(or "-->" and "->") which is quite embarassing.
Do anybody have an idea on how to fix this?
Thanks in advance,
Thomas
Email Gateway (Aug 18 2022 at 18:59):From: Makarius <makarius@sketis.net>
The official download instructions provide some laconic hints on this
http://isabelle.in.tum.de/download.html
Success depends on a version of Emacs and local fonts. With GNU Emacs 23
and STIXGeneral font it often works. What does Gentoo provide here?
The hint about Isabelle/jEdit in the same place might be also relevant for
you. While the new Prover IDE still lacks a few things, it is already
usable for many things, especially introductory courses. It avoids most
of the well-known installation problems, coming with fonts and everything
out of the box.
Makarius
Email Gateway (Aug 18 2022 at 19:00):From: Thomas Genet <Thomas.Genet@irisa.fr>
Dear all,
thanks for the answer.
It seems that the basic installation of emacs on Gentoo is not abble to
deal with anti-aliased fonts... and I guess that STIXGeneral is one.
I'll try to fix this out.
Thanks also for the jEdit proposition. I already consider using jEdit
but I am afraid that Isabelle/jEdit (even if it has made huge
progresses) is still not stable enough for my courses.
Thanks again,
Thomas
Email Gateway (Aug 18 2022 at 19:01):From: Makarius <makarius@sketis.net>
Do you have any concrete issues? The Isabelle2011-1 version is now beyond
the "experimental" stage of Isabelle2011, and I have documented all known
limitations in the README that shows up in the Prover Session panel.
This means such issues are official "features" by definition :-)
Anything beyond that should be reported, to get addressed at some point.
Otherwise we need to stay with the Emacs indefinitely.
Makarius
Email Gateway (Aug 18 2022 at 19:02):From: Thomas Genet <Thomas.Genet@irisa.fr>
Dear Makarius,
I heavily use nitpick/quickcheck and sledgehammer commands for my
practical courses and
(in my observation) jEdit get stuck more frequently than emacs with
those commands.
Best regards,
Thomas
Last updated: Apr 27 2024 at 01:05 UTC