Email Gateway (Aug 19 2022 at 10:33): Email Gateway (Aug 19 2022 at 10:33):From: Makarius <makarius@sketis.net>
On Fri, 15 Mar 2013, Christian Sternagel wrote:
The main choices I see are plain ASCII (which would not be very
convenient, since this usually means that you manually have to change
your snippet from using Unicode tokens to plain ASCII before publishing
it; or something like 'isabelle unsymbolize' could be used... but it
would have to cover all "standard" symbols) or some variant of Unicode
(which works for me on Linux with firefox, but e.g. not on Android with
chrome).
(I am still lagging behind with this thread ...)
The ASCII-fallback approach is basically what we did around 1995, when the
mathematical symbols were working only in exceptional situations.
I am not a fan of Unicode at all, but I have been trying hard for many
years to make it somehow work as front-end display mechanism, hoping that
we can give up ASCII alternatives and "unsymbolize" eventually. I even
composed the IsabelleText font for that, although it has required a few
more years than anticipatated to become usable. (The STIX project did not
reach a usable result in the double time.)
There should be some ways to convince hosting software like the one of
Stackoverflow / Stackexchange to go beyond ASCII.
Another question: if one only sees funny symbols instead of the "real
thing" does this also mean that copy'n'paste won't work in general, or
is this independent from what is visible?
Copy-paste works more often than having things visible. The former is
about encodings, which normally work unless the web server is configured
in a bad way. The latter is about fonts, which often do not work.
HTML5 also allows to specify server-side fonts for local display. So one
could in principle force IsabelleText on the user even on the Web, but
this is still a very theoretic possibility.
Makarius
Email Gateway (Aug 19 2022 at 10:44):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
despite my initial skepticism, I found stackoverflow a convenient place
for asking and answering Isabelle questions. (And to my great surprise I
already had an account for several years that just lay dormant ;).
With this e-mail, I intend two things:
1) Encourage people to have a look at stackoverflow (others already
indicated how one can subscribe, e.g., to a news feed for the isabelle
posts).
2) Ask if anybody would be interested in developing isabelle syntax
highlighting for stackoverflow ;)
See also
http://meta.stackoverflow.com/questions/171601/how-to-add-syntax-highlighting-for-new-language
in case you are interested.
cheers
chris
Email Gateway (Aug 19 2022 at 10:45):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Is there a certain encoding to be used, or are posters entering
information with a non-standard encoding? I've tried "Western
(ISO-8859-1)" and "Unicode (UTF-8)" in Chrome, but it doesn't make a
difference. I see boxes with a question mark in this question, and in
lots of other questions:
http://stackoverflow.com/questions/15332271/drop-a-variable-in-a-goal-in-apply-style
Are there additional tags to see the comments and answers for this tag?
http://stackoverflow.com/questions/tagged/isabelle
I can subscribe to a feed for a particular question, which is not what I
want to do.
What I'm doing is subscribing to the feed for many of the people who are
showing up, with a tag like this:
http://stackoverflow.com/users/476803/chris
Doing that is pretty ridiculous because it requires that I see
everything they do on the site. But polling and scanning questions to
try and find new information would be more ridiculous. Nothing much is
ever perfect.
More imperfection.
Rather than implement LaTeX on stackoverflow as it's done on other
sites, certain people tell you how to properly think about the matter.
http://meta.stackoverflow.com/questions/4152/adding-support-for-math-notation
http://meta.stackoverflow.com/questions/30559/latex-in-stack-overflow
http://meta.stackoverflow.com/questions/4152/adding-support-for-math-notation#comment253822_60023
http://blog.stackoverflow.com/2011/04/stack-exchange-partners-with-mathjax/
If I had an account, I might have answered this question that I saw:
PS. Is it possible to get the nice symbols from Isabelle here too?
I was ready to answer, "Of course, just use LaTeX". But then I did some
searches. I didn't find anything more current that what I linked to above.
Subject wise, Isabelle is closer to what's on math.stackexchange.com,
which has LaTeX.
714 questions: http://stackoverflow.com/questions/tagged/graph-theory
1920 questions: http://math.stackexchange.com/questions/tagged/graph-theory
25 questions: http://stackoverflow.com/questions/tagged/type-theory
15 questions: http://math.stackexchange.com/questions/tagged/type-theory
504 questions: http://stackoverflow.com/questions/tagged/combinatorics
4263 questions: http://math.stackexchange.com/questions/tagged/combinatorics
1984 questions: http://stackoverflow.com/questions/tagged/logic
1877 questions: http://math.stackexchange.com/questions/tagged/logic
0 questions:
25 questions:
http://math.stackexchange.com/questions/tagged/logic+axiom-of-choice
0 questions:
105 questions: http://math.stackexchange.com/questions/tagged/proof-theory
People can disregard all this. Perception is the limiting factor,
culture determines perception, and the police on the different sites
enforce the culture.
Regards,
GB
Email Gateway (Aug 19 2022 at 10:45):From: Makarius <makarius@sketis.net>
On Wed, 13 Mar 2013, Gottfried Barrow wrote:
Subject wise, Isabelle is closer to what's on math.stackexchange.com,
which has LaTeX.
I've already spent some time looking around several sites, just see my
profile at SE. For the majority of technical questions around Isabelle,
stackoverflow tag "isabelle" looks like the right place.
On "Computer Science" and "Theoretical Computer Science" there are some
more conceptual topics covered under "proof-assistants", for example.
Someone made a "coq" tag there, but I found it odd and did not imitate it.
I find it more difficult to get into http://math.stackexchange.com,
although its "logic" tag is a starting point.
What is also interesting is the "interdisciplinary" and "multi-cultural"
aspect of SE: e.g. someone asking under "isabelle" and "scala" will make
Scala people aware of what can be done with Isabelle, which they did not
know before. (This has already happened in the past few days.)
I also hope to see more people learning from the different provers, not
just "my prover is best and the only thing I need to know".
People can disregard all this. Perception is the limiting factor,
culture determines perception, and the police on the different sites
enforce the culture.
I am unsure what you mean by police. So far I found myself received
rather well, e.g. I've earned several +2 points for brushing up some if
the tag wikis.
The maintenance men at stackoverflow never sleep, though. When you start
editing wildly, a certain automated review system becomes alert, and 5
experienced stack-exchangers will vote thumbs up or thumbs down for your
proposal. That way you can also loose points.
There is also a special review system for contributions by fresh users.
Makarius
Email Gateway (Aug 19 2022 at 10:45):From: Joachim Breitner <breitner@kit.edu>
Hi,
It is probably not a question of encoding; The correct encoding
(text/html; charset=utf-8) is transferred in the HTTP header, and things
look good here. Maybe your are missing some fonts, of have some
font-overwrite in place?
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 10:45):From: Makarius <makarius@sketis.net>
At first I thought "it just works", quite unusually for unicode. Now I
also see problems here on Mac OS X Mountain Lion / Firefox, and some other
SE user has observed problems with my unicode copy-past as well,
potentially on Windows.
So we are back at field one, where we've been 20 years ago: "Unicode is
comming, really, believe me, it is there right now to solve all our math
typesetting problems". Luckily the prover does not depend on Unicode at
all.
Nonetheless, I shall continue with the copy-pasting from Isabelle/jEdit
for the time being. These snippets are not fully authentic source anyway.
Makarius
Email Gateway (Aug 19 2022 at 10:46):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Joachim,
That's probably the case, so I at least know where the problem is.
But I'm using Windows 7, and so at this stage of the game, if fonts
across operating systems aren't standardized enough to prevent this kind
of thing, then I don't care to set my system up to be bullet proof,
because all that does is allow me to have the impression that others are
seeing what I see.
Eventually, if possible and I'm thinking right, then I try and adapt to
others, rather than expect others to be just like me.
There is ASCII, LaTeX, images, THY files, and PDF files (where even PDFs
can have font dependency problems). Those are what I can depend on.
Nothing else. So I'm trying to come up with practical ways to use those
to ask questions, and say what I want to say.
Here's another person complaining about the same problem:
If you look at the question that's asked, you see that LaTeX is that
sites solution to the problem of dealing with non-ASCII characters.
http://math.stackexchange.com/posts/323029/edit
LaTeX can be a pain, but at least it's consistent and dependable. So
it's annoying when the admins on stackoveflow tell us that "programmers"
don't need LaTeX. If they don't want to implement it, they're the boss,
but attempts at brainwashing to deflect criticism are to be frowned upon.
Thanks,
GB
Email Gateway (Aug 19 2022 at 10:46):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 3/13/2013 9:53 AM, Makarius wrote:
On Wed, 13 Mar 2013, Gottfried Barrow wrote:
Subject wise, Isabelle is closer to what's on math.stackexchange.com,
which has LaTeX.I've already spent some time looking around several sites, just see my
profile at SE. For the majority of technical questions around
Isabelle, stackoverflow tag "isabelle" looks like the right place.
I suppose so. "Isabelle" has been vetted and accepted, which counts for
a lot:
On "Computer Science" and "Theoretical Computer Science" there are
some more conceptual topics covered under "proof-assistants", for
example. Someone made a "coq" tag there, but I found it odd and did
not imitate it.I find it more difficult to get into http://math.stackexchange.com,
although its "logic" tag is a starting point.
Yea, so I guess it wouldn't be a good host. Some of the buzz words are
the same, but the foundation and emphasis is different. They would be
lacking on making contributions to the programming side of things, which
is probably why I would partly feel more at home there.
But it represents what a good balance can be. It's diverse but not so
diverse and large that going to the main page is near useless, and they
tolerate questions from beginner to advanced. These sites are about
community, and a single tag isn't a community. Also, there can't be any
real cohesion for a group if the questions are spread out over four or
five sites, and it takes more energy to keep track of all that than I
want to put into it.
People can disregard all this. Perception is the limiting factor,
culture determines perception, and the police on the different sites
enforce the culture.I am unsure what you mean by police. So far I found myself received
rather well, e.g. I've earned several +2 points for brushing up some
if the tag wikis.
The police are the majority of people who assert themselves. The police
who act as tyrants are the admins and the in-crowd who vote to close
questions which they're not qualified to vote on, and do so to protect
their domain. When I see that happen, I become more interested in
fighting the establishment.
I'm in no hurry to get an account to fight the man. Fighting the man is
generally a losing proposition.
Regards,
GB
Email Gateway (Aug 19 2022 at 10:46):From: Gergely Buday <gbuday@gmail.com>
Gottfried Barrow wrote:
An example of this:
http://discuss.area51.stackexchange.com/questions/9385/computational-logic
Sorry if this is getting off-topic but I wanted to share this
experience with Isabelle users who are interested in Stack Exchange.
Email Gateway (Aug 19 2022 at 10:46):From: Makarius <makarius@sketis.net>
I still don't see the problem, and tend to agree with Gilles who pointed
out that there are sufficiently many SE sites to cover the topic. Why all
this fragmentation, and every tiny fringe group on its own site?
Makarius
Email Gateway (Aug 19 2022 at 10:46):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
How so?
Email Gateway (Aug 19 2022 at 10:46):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I agree with your feeling in the large. I too much see how that applies,
I've seen it too many times (the last hard time was just today on an
Ubuntu forum where I opened some topics to promote some interoperable
standards in software). The crowd effects is as much present in the
software domain as it is with many more popular and non‑technical issues
(every one know an example at least). I don't know if that applies as much
in the logic and mathematics world though (I have no experience with these
communities).
Well, to get back to StackOverflow precisely, I have an account there, I
ask and answer question, a bit from time to time, I had no bad experiences
there personally so far, but I could already witness some cases where
people posting relevant questions could see their questions closed for
obscure reasons, at least, no other reasons than negative votes from
people who did not see anything relevant in the question.
Email Gateway (Aug 19 2022 at 10:47):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
Just some general remarks on the format of theory-snippets on
stackoverflow (and in principle also all other possible occurrences). In
my opinion it should be:
I think that already excludes LaTeX, or not? (Besides, creating a
snippet using LaTeX is much more cumbersome than just copy'n'paste from
your current theory.)
The main choices I see are plain ASCII (which would not be very
convenient, since this usually means that you manually have to change
your snippet from using Unicode tokens to plain ASCII before publishing
it; or something like 'isabelle unsymbolize' could be used... but it
would have to cover all "standard" symbols) or some variant of Unicode
(which works for me on Linux with firefox, but e.g. not on Android with
chrome).
Another question: if one only sees funny symbols instead of the "real
thing" does this also mean that copy'n'paste won't work in general, or
is this independent from what is visible?
cheers
chris
Email Gateway (Aug 19 2022 at 10:47):From: "Jens-D. Doll" <jd@cococo.de>
Please have a little patience; a new, really fast version of
Elbe http://cococo.de/Elbeis on the way,
including unicode Isabelle assistance and a lot more.
Jens
Email Gateway (Aug 19 2022 at 10:47):From: Makarius <makarius@sketis.net>
Seen again this recent thread
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-March/msg00011.html
which also points to some explanations here
http://www4.in.tum.de/~wenzelm/papers/isabelle-doc.pdf
Makarius
Last updated: Apr 26 2024 at 04:17 UTC