search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

Unicode notations by default #377

Closed JasonGross closed 10 years ago

JasonGross commented 10 years ago

I'm in favor of moving to using unicode notations primarily, and including a file/module that replaces them with ASCII notations in display. What do others think?

awodey commented 10 years ago

I prefer to keep things as simple as possible and just use ascii.

On Apr 21, 2014, at 5:43 PM, Jason Gross notifications@github.com wrote:

I'm in favor of moving to using unicode notations primarily, and including a file/module that replaces them with ASCII notations in display. What do others think?

— Reply to this email directly or view it on GitHub.

peterlefanulumsdaine commented 10 years ago

I also prefer ASCII as default, at least for the main core of the library. Using non-ASCII notations raises the tech-confidence barrier to entry: with plain ASCII, any reader can feel in principle “if I can read and understand this, then I can write this”, but with non-ASCII unicode, good mathematicians may be intimidated by uncertainty of how to input it.

I’m fine with having unicode in the more experimental library, but I’d vote for not having it as default in the core.

–p.

On Mon, Apr 21, 2014 at 8:31 PM, Steve Awodey notifications@github.comwrote:

I prefer to keep things as simple as possible and just use ascii.

On Apr 21, 2014, at 5:43 PM, Jason Gross notifications@github.com wrote:

I'm in favor of moving to using unicode notations primarily, and including a file/module that replaces them with ASCII notations in display. What do others think?

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/377#issuecomment-40992211 .

mikeshulman commented 10 years ago

I think I'm still convinced by those arguments.

spitters commented 10 years ago

After Gonthier's lecture today Cedric Villani was arguing for the opposite: To have unicode display, as a sort of compiled Latex.

Is adding unicode support so much more difficult then being able to type latex ?

On the other hand, Georges answered that unicode support is really not the biggest hurdle for formalization today.

On Tue, Apr 22, 2014 at 4:43 AM, Peter LeFanu Lumsdaine < notifications@github.com> wrote:

I also prefer ASCII as default, at least for the main core of the library. Using non-ASCII notations raises the tech-confidence barrier to entry: with plain ASCII, any reader can feel in principle “if I can read and understand this, then I can write this”, but with non-ASCII unicode, good mathematicians may be intimidated by uncertainty of how to input it.

I’m fine with having unicode in the more experimental library, but I’d vote for not having it as default in the core.

–p.

On Mon, Apr 21, 2014 at 8:31 PM, Steve Awodey notifications@github.comwrote:

I prefer to keep things as simple as possible and just use ascii.

On Apr 21, 2014, at 5:43 PM, Jason Gross notifications@github.com wrote:

I'm in favor of moving to using unicode notations primarily, and including a file/module that replaces them with ASCII notations in display. What do others think?

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/HoTT/issues/377#issuecomment-40992211> .

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/377#issuecomment-40998632 .

JasonGross commented 10 years ago

I use agda-mode to input unicode; it's very similar to LaTeX, with some abbreviations (e.g., \r is the same as \rightarrow).

JasonGross commented 10 years ago

On the other hand, Georges answered that unicode support is really not the biggest hurdle for formalization today.

What is the biggest hurdle?

mikeshulman commented 10 years ago

And for people who haven't installed Agda, Emacs has a built-in "TeX" input mode that is less powerful, but more like LaTeX.

However, as hard as it is to believe, not everyone uses Emacs.

On Tue, Apr 22, 2014 at 2:07 PM, Jason Gross notifications@github.comwrote:

I use agda-mode to input unicode; it's very similar to LaTeX, with some abbreviations (e.g., \r is the same as \rightarrow).

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/377#issuecomment-41095842 .

spitters commented 10 years ago

I use something similar: skim for KDE, we have some instructions in math-classes.

On Tue, Apr 22, 2014 at 11:07 PM, Jason Gross notifications@github.comwrote:

I use agda-mode to input unicode; it's very similar to LaTeX, with some abbreviations (e.g., \r is the same as \rightarrow).

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/377#issuecomment-41095842 .

spitters commented 10 years ago

He did not say.

On Tue, Apr 22, 2014 at 11:08 PM, Jason Gross notifications@github.comwrote:

On the other hand, Georges answered that unicode support is really not the biggest hurdle for formalization today.

What is the biggest hurdle?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/377#issuecomment-41095915 .

andrejbauer commented 10 years ago

A related issue is that the library now uses magic such as Typeclasses Opaque IsTrunc, which I think scares away a mathematician who's learned some type theory and wants to read the code. I am not sure whether there exists a cure for this sort of thing in the long run.

I am still against keeping things in ASCII, at least in the core.

By the way, does CoqIDE have support for utf-8 characters?

awodey commented 10 years ago

On Apr 23, 2014, at 5:05 AM, Andrej Bauer notifications@github.com wrote:

A related issue is that the library now uses magic such as Typeclasses Opaque IsTrunc, which I think scares away a mathematician who's learned some type theory and wants to read the code. I am not sure whether there exists a cure for this sort of thing in the long run.

I am still against keeping things in ASCII, at least in the core.

is this a typo, or are you really against keeping things in ASCII at least in the core?

By the way, does CoqIDE have support for utf-8 characters?

— Reply to this email directly or view it on GitHub.

andrejbauer commented 10 years ago

oops, it's a typo. I would like to keep ASCII.

mikeshulman commented 10 years ago

I have heard an argument that it's better to avoid typeclasses entirely (as Vladimir's library does) -- partly due to their scaring away mathematicians, but also because they introduce fragile non-local dependencies into the code. I don't know whether I'm convinced by it, but it's certainly something to consider carefully.

andrejbauer commented 10 years ago

It's too late to worry about typeclasses. They're all over the place now.

spitters commented 10 years ago

I did a quick search, I am surprised no-one has tried to make something like latex-preview for proof general/Coq.

In any case, I hear that PIDE for Coq is coming along fine. https://bitbucket.org/Carst/coq-pide

On Tue, Apr 22, 2014 at 11:10 PM, Mike Shulman notifications@github.comwrote:

And for people who haven't installed Agda, Emacs has a built-in "TeX" input mode that is less powerful, but more like LaTeX.

However, as hard as it is to believe, not everyone uses Emacs.

On Tue, Apr 22, 2014 at 2:07 PM, Jason Gross notifications@github.comwrote:

I use agda-mode to input unicode; it's very similar to LaTeX, with some abbreviations (e.g., \r is the same as \rightarrow).

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/HoTT/issues/377#issuecomment-41095842> .

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/377#issuecomment-41096126 .

andrejbauer commented 10 years ago

That's just a fork of Coq with pide subdirectory, doesn't this thing have a funky home page? Here's an arXiv paper about PIDE. Also, has anyone here tried Coqoon?

mattam82 commented 10 years ago

On 23 avr. 2014, at 11:05, Andrej Bauer notifications@github.com wrote:

A related issue is that the library now uses magic such as Typeclasses Opaque IsTrunc, which I think scares away a mathematician who's learned some type theory and wants to read the code. I am not sure whether there exists a cure for this sort of thing in the long run.

Make IsTrunc an inductive type? The issue here is one mathematicians usually do not see as reasoning up to δ-reduction happen in their head. Sadly a computer does not know when it is smart to unfold a definition or not. So it might search for things unfolding everything, when you’ve been careful to give folded versions of them. The end result is a blowup in the search space, which mathematicians can’t feel indeed, but which is a critical problem when trying to mimic their implicit thinking habits on a computer. — Matthieu

mikeshulman commented 10 years ago

It seems like we are going to keep restricting the core to ASCII for now, so let's close this issue.

spitters commented 10 years ago

This seems to be the latest update: http://pages.saclay.inria.fr/carst.tankink/files/uitp-2014.pdf I am told it will be very nice. https://bitbucket.org/Carst/coq-pide

I have not tried Coqoon, but the same question applies: Will users be able to input unicode?

On Sun, Apr 27, 2014 at 10:13 AM, Andrej Bauer notifications@github.com wrote:

That's just a fork of Coq with pide subdirectory, doesn't this thing have a funky home page? Here's an arXiv paper about PIDE http://arxiv.org/pdf/1304.6626v1.pdf. Also, has anyone here tried Coqoon http://itu.dk/research/tomeso/coqoon/?

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/377#issuecomment-41490866.