Discussion:
Lean Theorem Prover
(too old to reply)
Saulo Araujo
2016-02-25 00:17:07 UTC
Permalink
Hi,

I recently discovered the Lean Theorem Prover (
https://leanprover.github.io/about/). I did some toy experiments with it
and and, at least in this first contact, it seemed similar to Coq. I am
curious about how the Coq community sees Lean. Does it see Lean as
"competitor" of Coq? Is it possible for Coq to bridge the gap betweem
interactive and automated theorem proving like Lean aims to do?

Saulo
Jonathan Leivent
2016-02-25 02:21:56 UTC
Permalink
Post by Saulo Araujo
Hi,
I recently discovered the Lean Theorem Prover (
https://leanprover.github.io/about/). I did some toy experiments with it
and and, at least in this first contact, it seemed similar to Coq.
It looks eerily similar to Coq. The syntax and semantics both seem very
similar. One of the minor semantic differences I saw in a quick
walk-through is that Lean's Prop universe has built-in irrelevance,
while Coq's Prop can get irrelevance via an additional axiom. Even the
tactic names are similar.

It almost looks like Lean is a project to rebuild Coq that doesn't have
to pay homage to backward compatibility. I'll bet there are some Coq
developers that would be quite envious of that position. Although, it is
written in C++ instead of OCaml, so maybe their envy would turn to
schadenfreude. ;-)
Post by Saulo Araujo
I am
curious about how the Coq community sees Lean. Does it see Lean as
"competitor" of Coq? Is it possible for Coq to bridge the gap betweem
interactive and automated theorem proving like Lean aims to do?
Saulo
I think many Coq users are also familiar with, perhaps even regular
users of, alternative dependent-typed proof assistants, such as Agda,
Idris, F*, Matita, NuPrl, ATS2, etc. I doubt many would see these as
"competitors". More like kin.

As for this "bridge the gap between interactive and automated theorem
proving" - I'm not sure what the author(s) meant by this. Do they mean
that Lean supports connections to various SMT solvers? Do they mean it
has a powerful proof search capability? Version 8.5 of Coq has
considerably more proof search capability than did version 8.4, by
virtue of its enhanced support for backtracking. If that is what is
meant by this "bridging the gap", then Coq perhaps qualifies.

-- Jonathan
Soegtrop, Michael
2016-02-25 08:37:06 UTC
Permalink
Dear Saulo,

since they are looking into automation, I wonder if they plan to use Z3 for some of its backend work. The manual doesn't mention Z3 ...

Otherwise the choice between Lean and Coq looks like the choice between F# and OCaml.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenc
Benjamin Pierce
2016-02-25 13:21:31 UTC
Permalink
According to Leo's talk at the recent CPP workshop, lean does not use Z3 itself, to avoid awkward encodings of type theory in FOL. However, he says that almost all of the techniques used in Z3 can be adapted fairly readily to type theory, so most of Z3 will be in some sense built in.

- B
Post by Soegtrop, Michael
Dear Saulo,
since they are looking into automation, I wonder if they plan to use Z3 for some of its backend work. The manual doesn't mention Z3 ...
Otherwise the choice between Lean and Coq looks like the choice between F# and OCaml.
Best regards,
Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
Soegtrop, Michael
2016-02-25 13:39:04 UTC
Permalink
Dear Benjamin,
Post by Benjamin Pierce
According to Leo's talk at the recent CPP workshop, lean does not use Z3 itself, to avoid awkward encodings of type theory in FOL.
However, he says that almost all of the techniques used in Z3 can be adapted fairly readily to type theory, so most of Z3 will be in some sense built in.
thanks for the information! So I guess some of the people working on Z3 also work on Lean. This is an interesting development. I wonder what this means for the future of directly Z3 based verification tools like Dafny.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
Freek Wiedijk
2016-02-25 11:01:05 UTC
Permalink
Hi Jonathan,
Post by Jonathan Leivent
It looks eerily similar to Coq.
I also is quite different from Coq in some respects.

It is implemented in C++, not in ML. It has proof
irrelevance, function extensionality, classical logic, even
a choice operator as part of the standard setup (exactly
which of those are hardwired in, and which ones are just
conventionally available in the library, I don't know.)
It has been explicitly designed to be useful for HoTT (how
that can be true in conjunction with the previous sentence, I
don't know :-)) The type theory is simpler: they don't have
"match" in the foundations, but instead work with recursors,
and they don't have universe cumulativity.

Jeremy Avigad is one of the people behind Lean. He comes
from an Isabelle background. I can imagine Lean will feel
more familiar to Isabelle people than Coq does.

Freek
Théo Zimmermann
2016-02-25 11:45:32 UTC
Permalink
Hi Freek,

Lean has two modes: one standard and one "HoTT". The standard one has proof
irrelevance built-in, indeed, but the HoTT one has not, of course. Leonardo
de Moura claims that Lean would make it possible to add new modes, if a new
logic became of much interest for experimentation.

As for bridging the gap between automated theorem proving and interactive
theorem proving, this is a long term goal. Leonardo de Moura comes from the
world of automated theorem proving so has probably some interesting plans
on how to do so.

On how it compares to Agda and Coq, I would add that by default you write
your proofs as terms, but these terms look more natural, by the use of
keywords such as take and assume instead of fun; and have. There is also a
tactic mode which you can easily switch to (similar to Coq's new tactic in
term capability).

Théo
Post by Freek Wiedijk
Hi Jonathan,
Post by Jonathan Leivent
It looks eerily similar to Coq.
I also is quite different from Coq in some respects.
It is implemented in C++, not in ML. It has proof
irrelevance, function extensionality, classical logic, even
a choice operator as part of the standard setup (exactly
which of those are hardwired in, and which ones are just
conventionally available in the library, I don't know.)
It has been explicitly designed to be useful for HoTT (how
that can be true in conjunction with the previous sentence, I
don't know :-)) The type theory is simpler: they don't have
"match" in the foundations, but instead work with recursors,
and they don't have universe cumulativity.
Jeremy Avigad is one of the people behind Lean. He comes
from an Isabelle background. I can imagine Lean will feel
more familiar to Isabelle people than Coq does.
Freek
Bas Spitters
2016-02-25 13:54:53 UTC
Permalink
Yes, Jeremy's Isabelle background can be seen too. The proofs are,
arguably, more readable than Coq proofs.

The lean tutorial gives a good overview of the system.
Post by Freek Wiedijk
Hi Jonathan,
Post by Jonathan Leivent
It looks eerily similar to Coq.
I also is quite different from Coq in some respects.
It is implemented in C++, not in ML. It has proof
irrelevance, function extensionality, classical logic, even
a choice operator as part of the standard setup (exactly
which of those are hardwired in, and which ones are just
conventionally available in the library, I don't know.)
It has been explicitly designed to be useful for HoTT (how
that can be true in conjunction with the previous sentence, I
don't know :-)) The type theory is simpler: they don't have
"match" in the foundations, but instead work with recursors,
and they don't have universe cumulativity.
Jeremy Avigad is one of the people behind Lean. He comes
from an Isabelle background. I can imagine Lean will feel
more familiar to Isabelle people than Coq does.
Freek
roux cody
2016-02-25 15:29:38 UTC
Permalink
I'm only loosely associated with Lean, so I won't presume to speak for the
motivations of all involved.

I think part of the motivation from the Z3 side was that for many
applications, using tactic like hints was becoming a reality, which
naturally leads to considering a full-fledged interactive theorem prover
with powerful proof strategies. In addition, it's terrifyingly easy to make
subtle soundness mistakes in SMT solvers. Backing one into an ITP from the
start forces you to be honest.

Leo considered several languages for implementation, including Ocaml. While
I'm certain his familiarity with C++ played a big part in the final
decision, he has very justified reasons for choosing it. He claims that
it's extremely hard to get excellent performance without breaking the nice
abstractions built by such languages (memory management, data structure
layout etc.), and I have to say, Lean is blindingly fast when
type-checking. A lot of things become easy when working with such a
mainstream language, like writing FFI bindings and using compiler
frameworks.

As a social stepping stone, there is a type-checker for the kernel
implemented entirely in Haskell, which is well-maintained at the moment I
believe: https://github.com/leanprover/tc. It's pretty neat. The C++ code
is also cleaner than I thought possible. Perhaps surprisingly, the C++
kernel is only about as large as the one in Coq I believe (though this
might just be explained by it's relative youth).

The theoretical differences between Coq and Lean have been pretty well
summarized. I think the practical differences are probably more important
in the long run. The striking features are the web interface, the full
concurrent type checking, and the excellent emacs-mode, which type-checks
as you write and auto-completes in the eclipse style. The standard library
is shaping to be very generic (based on type classes), and while smaller,
is looking more like the MathComp library than the Coq standard library, so
there is really an opportunity for a do-over here.

I believe Coq either has or is in the process of acquiring these features
though, so it's still hard to say which are the real distinguishing things
(though the Agda-style unicode bindings are just so fun!).

Jonathan sums it up the best I think. Lean is another point in the design
space of dependent type based ITPs, with a lot of opportunities for trying
out things that are impossible in Coq because of backward compatibility or
just size and complexity.

Best,
Cody


This email has been sent from a virus-free computer protected by Avast.
www.avast.com <https://www.avast.com/sig-email>
<#DDB4FAA8-2DD7-40BB-A1B8-4E2AA1F9FDF2>
Post by Bas Spitters
Yes, Jeremy's Isabelle background can be seen too. The proofs are,
arguably, more readable than Coq proofs.
The lean tutorial gives a good overview of the system.
Post by Freek Wiedijk
Hi Jonathan,
Post by Jonathan Leivent
It looks eerily similar to Coq.
I also is quite different from Coq in some respects.
It is implemented in C++, not in ML. It has proof
irrelevance, function extensionality, classical logic, even
a choice operator as part of the standard setup (exactly
which of those are hardwired in, and which ones are just
conventionally available in the library, I don't know.)
It has been explicitly designed to be useful for HoTT (how
that can be true in conjunction with the previous sentence, I
don't know :-)) The type theory is simpler: they don't have
"match" in the foundations, but instead work with recursors,
and they don't have universe cumulativity.
Jeremy Avigad is one of the people behind Lean. He comes
from an Isabelle background. I can imagine Lean will feel
more familiar to Isabelle people than Coq does.
Freek
Clément Pit--Claudel
2016-02-25 15:47:50 UTC
Permalink
Post by roux cody
and auto-completes in the eclipse style
We're working on this :)

Is there anything in lean-mode that is not described in https://leanprover.github.io/presentations/20150123_lean-mode/lean-mode.pdf ? Most of what's in there seems to already be available for Coq.

Clément.
Clément Pit--Claudel
2016-02-25 15:48:08 UTC
Permalink
Post by roux cody
(though the Agda-style unicode bindings are just so fun!).
What do you mean?
Jonathan Leivent
2016-02-25 16:22:57 UTC
Permalink
Is there a way in Lean for users to define new tactics, as with Ltac?

Is there any extraction capability?

As for building-in proof irrelevance (while having a separate HoTT mode)
that might not bother anyone but me: I (ab)use proof *relevance* in Coq
as a way to get really good erasability.

-- Jonathan
John Wiegley
2016-02-25 22:31:40 UTC
Permalink
The type theory is simpler: they don't have "match" in the foundations, but
instead work with recursors
I wonder if runs into the same issues that Coq did. See "Meta-theory à la
Carte", section "The Problem of Church Encodings and Induction",
http://people.csail.mit.edu/bendy/MTC/.
--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2
Daniel Schepler
2016-02-25 22:39:45 UTC
Permalink
Post by Saulo Araujo
Hi,
I recently discovered the Lean Theorem Prover
(https://leanprover.github.io/about/). I did some toy experiments with it
and and, at least in this first contact, it seemed similar to Coq. I am
curious about how the Coq community sees Lean. Does it see Lean as
"competitor" of Coq? Is it possible for Coq to bridge the gap betweem
interactive and automated theorem proving like Lean aims to do?
One thing I did notice in my quick browse through the tutorial: its
standard library includes a typeclass for decision procedures for
propositions (though I'd call it Decision instead of decidable as Lean
does, as the last suggests the proposition (P \/ ~P) rather than
something with extractable information). It also includes a notation
for defining a proof by inferring a decision procedure and then
running it.

This is something I've thought of proposing as an addition to the Coq
standard library at various times - and I might even have mentioned
some elements of my thinking in some previous messages to the list.
So, the basic outline would be something like:

Class Decision (P:Prop) : Set :=
decide : {P} + {~P}.

Arguments decide P [Decision].

Instance true_dec : Decision True := left _ I.
Instance and_dec {P Q:Prop}
`{!Decision P} `{!Decision Q} : Decision (P /\ Q) := ...
...
Instance bounded_nat_dec {P : nat -> Prop}
`{!forall m:nat, Decision (P m)}
(n : nat) : Decision (forall m:nat, m < n -> P m) :=
fix ...
Instance Forall_dec {A:Type} {P : A -> Type}
`{!forall x:A, Decision (P x)}
(l : list A) : Decision (Forall P l) :=
fix ...
...

Ltac decide := (* untested *)
match goal with
|- ?P =>
let dec := hnf (decide P) in
match dec with
| left _ ?pf => exact pf
| right _ _ => error 2 "statement is false"
| _ => error 2 "could not evaluate decision procedure"
end
end.
Notation decision_pf := ltac:(decide).

Example my_max (m n:nat) : nat :=
if decide (m <= n) then n else m.

Maybe it could also include some framework for enumerating all
elements of finite types, which would be useful for things like
Definition bor_assoc (x y z:bool) :
bor x (bor y z) = bor (bor x y) z := decision_pf.
--
Daniel Schepler
Abhishek Anand
2016-02-25 22:46:05 UTC
Permalink
MathClasses <https://github.com/math-classes/math-classes> has something
similar, which I like a lot:

http://www.cs.cornell.edu/~aa755/ROSCoq/coqdoc/MathClasses.misc.decision.html



-- Abhishek
http://www.cs.cornell.edu/~aa755/
Post by Daniel Schepler
Post by Saulo Araujo
Hi,
I recently discovered the Lean Theorem Prover
(https://leanprover.github.io/about/). I did some toy experiments with
it
Post by Saulo Araujo
and and, at least in this first contact, it seemed similar to Coq. I am
curious about how the Coq community sees Lean. Does it see Lean as
"competitor" of Coq? Is it possible for Coq to bridge the gap betweem
interactive and automated theorem proving like Lean aims to do?
One thing I did notice in my quick browse through the tutorial: its
standard library includes a typeclass for decision procedures for
propositions (though I'd call it Decision instead of decidable as Lean
does, as the last suggests the proposition (P \/ ~P) rather than
something with extractable information). It also includes a notation
for defining a proof by inferring a decision procedure and then
running it.
This is something I've thought of proposing as an addition to the Coq
standard library at various times - and I might even have mentioned
some elements of my thinking in some previous messages to the list.
Class Decision (P:Prop) : Set :=
decide : {P} + {~P}.
Arguments decide P [Decision].
Instance true_dec : Decision True := left _ I.
Instance and_dec {P Q:Prop}
`{!Decision P} `{!Decision Q} : Decision (P /\ Q) := ...
...
Instance bounded_nat_dec {P : nat -> Prop}
`{!forall m:nat, Decision (P m)}
(n : nat) : Decision (forall m:nat, m < n -> P m) :=
fix ...
Instance Forall_dec {A:Type} {P : A -> Type}
`{!forall x:A, Decision (P x)}
(l : list A) : Decision (Forall P l) :=
fix ...
...
Ltac decide := (* untested *)
match goal with
|- ?P =>
let dec := hnf (decide P) in
match dec with
| left _ ?pf => exact pf
| right _ _ => error 2 "statement is false"
| _ => error 2 "could not evaluate decision procedure"
end
end.
Notation decision_pf := ltac:(decide).
Example my_max (m n:nat) : nat :=
if decide (m <= n) then n else m.
Maybe it could also include some framework for enumerating all
elements of finite types, which would be useful for things like
bor x (bor y z) = bor (bor x y) z := decision_pf.
--
Daniel Schepler
Daniel Schepler
2016-02-25 23:01:12 UTC
Permalink
On Thu, Feb 25, 2016 at 2:46 PM, Abhishek Anand
Post by Abhishek Anand
http://www.cs.cornell.edu/~aa755/ROSCoq/coqdoc/MathClasses.misc.decision.html
OK, there's a lot of stuff otherwise in MathClasses that I wish would
make its way into the standard library, too. I just hadn't noticed
that one - though it does seem like it could still use more extension
along the lines I was thinking. (For example, I see and_dec and
or_dec there, but no impl_dec.)
--
Daniel Schepler
roux cody
2016-02-26 03:18:54 UTC
Permalink
I hope someone with more expertise will weigh in here, since I am a bit out
of my depth. Still I'll try to answer some of the questions with the caveat
that I'm not really an expert.
Post by roux cody
(though the Agda-style unicode bindings are just so fun!).
What do you mean?

I just mean I like the agda-style input which replaces \forall by the
unicode ∀ seamlessly. It's possible that this is supported in coq as well I
guess (I'm a little behind the times).
Post by roux cody
Is there anything in lean-mode that is not described in
https://leanprover.github.io/presentations/20150123_lean-mode/lean-mode.pdf
?

You'd really have to ask Soonho directly.
Post by roux cody
Is there a way in Lean for users to define new tactics, as with Ltac?
Not really at the moment. This is a definite drawback (though Isabelle
users don't seem so gung-ho about this). You can sort of pretend with the
Lua bindings, I think.
Post by roux cody
Is there any extraction capability?
It's in the works.
Post by roux cody
As for building-in proof irrelevance (while having a separate HoTT mode)
that might not bother anyone but me: I (ab)use proof *relevance* in Coq as
a way to get really good erasability.

I'm confused about this. Could you elaborate? Proof-irrelevance and proof
erasure seem to go rather well together, in my mind.
Post by roux cody
I wonder if runs into the same issues that Coq did. See "Meta-theory à la
Carte", section "The Problem of Church Encodings and Induction",
http://people.csail.mit.edu/bendy/MTC/
<http://people.csail.mit.edu/bendy/MTC/>.

Unless I misunderstand, the problem there seems to concern church encodings
in pure CoC (as opposed to CIC), so not much to do with how inductives are
implemented.


Best,
Cody





This email has been sent from a virus-free computer protected by Avast.
www.avast.com
<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail>
<#DDB4FAA8-2DD7-40BB-A1B8-4E2AA1F9FDF2>
Post by roux cody
On Thu, Feb 25, 2016 at 2:46 PM, Abhishek Anand
http://www.cs.cornell.edu/~aa755/ROSCoq/coqdoc/MathClasses.misc.decision.html
OK, there's a lot of stuff otherwise in MathClasses that I wish would
make its way into the standard library, too. I just hadn't noticed
that one - though it does seem like it could still use more extension
along the lines I was thinking. (For example, I see and_dec and
or_dec there, but no impl_dec.)
--
Daniel Schepler
Jonathan Leivent
2016-02-26 03:47:48 UTC
Permalink
Post by roux cody
...
Post by Jonathan Leivent
As for building-in proof irrelevance (while having a separate HoTT mode)
that might not bother anyone but me: I (ab)use proof *relevance* in Coq as
a way to get really good erasability.
I'm confused about this. Could you elaborate? Proof-irrelevance and proof
erasure seem to go rather well together, in my mind.
Coq's standard erasures of Prop, type-like things, and the ability to do
Extraction Implicit don't erase everything that could be erased. For
example, they don't erase non-Prop data (in Set) that is passed around
and used only "uninformatively" - meaning only by Props. Consider, for
example, the height of a binary tree used in invariants in dependent
types defining the tree and its functions, but which one doesn't want to
be a field of the extracted binary tree or args in the extracted
functions. So, I do this:

Inductive Erasable(A : Set) : Prop :=
erasable: A -> Erasable A.

Arguments erasable [A] _.
...
Axiom Erasable_inj : forall {A : Set}{a b : A}, erasable a= erasable b
-> a=b.

Adding this erasable injectivity axiom makes proofs relevant. However,
it gives me the ability to pass around and use (in Props) all manner of
things wrapped in the erasable constructor that Coq will then end up
erasing at extraction time. This trick works great, especially when one
is embedding many complex invariants into dependent types. But I still
wish I didn't have to use it.

If you're interested in how nicely erased the extracted results are, you
can take a look at my github projects:

https://github.com/jonleivent/mindless-coding (stale, slightly bit-rotted)
https://github.com/jonleivent/mindless-coding-phase2 (up-to-date for Coq
8.5)

The best comparison would be in mindless-coding-phase2, between files
wavl.v and its extraction wavl.ml - or, if you'd prefer the
non-proof-mode version: wavl-noninter.v and wavl-noninter.ml.

-- Jonathan
Arnaud Spiwack
2016-02-26 06:23:59 UTC
Permalink
Post by roux cody
I just mean I like the agda-style input which replaces \forall by the
unicode ∀ seamlessly. It's possible that this is supported in coq as well I
guess (I'm a little behind the times).
That's just built-in in emacs. There are even several ways to do that (the
old-school quail, and the newish company-math at least).
Clément Pit--Claudel
2016-02-26 14:20:04 UTC
Permalink
I just mean I like the agda-style input which replaces \forall by the unicode ∀ seamlessly. It's possible that this is supported in coq as well I guess (I'm a little behind the times).
That's just built-in in emacs. There are even several ways to do that (the old-school quail, and the newish company-math at least).
Indeed; with plain Emacs, just typing `M-x set-input-method RET TeX RET` will give you the Agda-style input that you mentionned.
Alternatively (if you use it), company-coq loads company-math, so typing \rightarr will offer \rightarrow, and RET will complete it to →.

Should we make this the default input method in PG?

Clément.
Benjamin C. Pierce
2016-02-26 14:34:09 UTC
Permalink
Since we’re talking about unicode, I’d like to get people’s advice


At some point, I’d really like to convert Software Foundations to unicode, as this would avoid a lot of hassles with notation, awkward hacks in HTML generation, etc. But I’ve been nervous about making the switch so far for two reasons:
I wonder whether beginning users will find the available input methods confusing or off-putting, and
(more significantly) I wonder whether the world has stabilized to the point where the major Coq IDEs will “just work” with unicode in their default configurations on all platforms.
What do people think? Should I just take the plunge? Or is it not time yet?

- Benjamin
Post by Clément Pit--Claudel
I just mean I like the agda-style input which replaces \forall by the unicode ∀ seamlessly. It's possible that this is supported in coq as well I guess (I'm a little behind the times).
That's just built-in in emacs. There are even several ways to do that (the old-school quail, and the newish company-math at least).
Indeed; with plain Emacs, just typing `M-x set-input-method RET TeX RET` will give you the Agda-style input that you mentionned.
Alternatively (if you use it), company-coq loads company-math, so typing \rightarr will offer \rightarrow, and RET will complete it to →.
Should we make this the default input method in PG?
Clément.
Soegtrop, Michael
2016-02-26 17:32:24 UTC
Permalink
Dear Benjamin,
At some point, I’d really like to convert Software Foundations to Unicode, as this would avoid a lot of hassles with notation, awkward hacks in HTML generation, etc.
a few reasons for switching to Unicode:


1.) Using Unicode notations in the HTML version but ASCII in the IDE is as confusing as finding the shortcuts for the right symbols

2.) Most people read more than they write, so it makes sense to optimize for readability – and the Unicode symbols are more readable

3.) The shortcuts for the Unicode symbols can be mentioned in IDE menus at a prominent place

Regarding your portability concerns:


· On Windows non-Unicode is dead. The last non Unicode Version was Windows ME (Millennium Edition) which I don’t think is used any more. Even its successor Windows XP is out of maintenance since a while and XP does support Unicode (always – there are no XP systems which don’t support it). Here is a link to OS usage statistics: https://en.wikipedia.org/wiki/Usage_share_of_operating_systems.

· I did a quick search on google for Unicode issues with Linux/Debian/Ubuntu/Fedora/Mint. The first 20 articles I found where all 2009 or older. So I think issues are solved since then, since google doesn’t tend to prefer old articles.

· I would think Mac with its DTP background was pretty much always Unicode.

Best regards,

Michael

From: coq-club-***@inria.fr [mailto:coq-club-***@inria.fr] On Behalf Of Benjamin C. Pierce
Sent: Friday, February 26, 2016 3:34 PM
To: coq-***@inria.fr
Subject: Re: [Coq-Club] Lean Theorem Prover

Since we’re talking about unicode, I’d like to get people’s advice


At some point, I’d really like to convert Software Foundations to unicode, as this would avoid a lot of hassles with notation, awkward hacks in HTML generation, etc. But I’ve been nervous about making the switch so far for two reasons:

1. I wonder whether beginning users will find the available input methods confusing or off-putting, and
2. (more significantly) I wonder whether the world has stabilized to the point where the major Coq IDEs will “just work” with unicode in their default configurations on all platforms.
What do people think? Should I just take the plunge? Or is it not time yet?

- Benjamin


On Feb 26, 2016, at 9:20 AM, Clément Pit--Claudel <***@gmail.com<mailto:***@gmail.com>> wrote:

On 02/26/2016 01:23 AM, Arnaud Spiwack wrote:

I just mean I like the agda-style input which replaces \forall by the unicode ∀ seamlessly. It's possible that this is supported in coq as well I guess (I'm a little behind the times).

That's just built-in in emacs. There are even several ways to do that (the old-school quail, and the newish company-math at least).

Indeed; with plain Emacs, just typing `M-x set-input-method RET TeX RET` will give you the Agda-style input that you mentionned.
Alternatively (if you use it), company-coq loads company-math, so typing \rightarr will offer \rightarrow, and RET will complete it to →.

Should we make this the default input method in PG?

Clément.

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
Clément Pit--Claudel
2016-02-26 18:14:29 UTC
Permalink
Hi Benjamin and Michael,

I like the idea of moving to Unicode symbols, and I think it's quite feasible. There are a few issues, though; not so much with encoding, but with font support:

* There is currently no free monospace font with good Unicode coverage. If pixel-perfect indentation is a concern (and I see most people using Coq with a fixed-width font), then Unicode will cause some grief. I've done some work on this (https://github.com/cpitclaudel/monospacifier), but it isn't perfect.

* On Debian derivatives, the only commonly installed fonts that include a wide range of symbols are TeX fonts, and there's a bug in their metrics which causes Emacs and other metrics-respecting applications to display them with huge line gaps (see https://github.com/cpitclaudel/company-coq/issues/15, https://github.com/cpitclaudel/company-coq/issues/31, and https://emacs.stackexchange.com/questions/251/line-height-with-unicode-characters for more info). This was fixed in Emacs 25 (https://lists.gnu.org/archive/html/bug-gnu-emacs/2015-05/msg00696.html), but it's not released yet.

* Many users don't have the right fonts installed, so some symbols will show up as ᅵ or as a white box.

This is nothing that can't be solved with a bit of setup time, though. And Unicode everywhere seems to work for Agda, so it could probably work for us too.

Cheers,
Clément.
Post by Soegtrop, Michael
Dear Benjamin,
At some point, I’d really like to convert Software Foundations to Unicode, as this would avoid a lot of hassles with notation, awkward hacks in HTML generation, etc.
1.) Using Unicode notations in the HTML version but ASCII in the IDE is as confusing as finding the shortcuts for the right symbols
2.) Most people read more than they write, so it makes sense to optimize for readability – and the Unicode symbols are more readable
3.) The shortcuts for the Unicode symbols can be mentioned in IDE menus at a prominent place
· On Windows non-Unicode is dead. The last non Unicode Version was Windows ME (Millennium Edition) which I don’t think is used any more. Even its successor Windows XP is out of maintenance since a while and XP does support Unicode (always – there are no XP systems which don’t support it). Here is a link to OS usage statistics: https://en.wikipedia.org/wiki/Usage_share_of_operating_systems.
· I did a quick search on google for Unicode issues with Linux/Debian/Ubuntu/Fedora/Mint. The first 20 articles I found where all 2009 or older. So I think issues are solved since then, since google doesn’t tend to prefer old articles.
· I would think Mac with its DTP background was pretty much always Unicode.
Best regards,
Michael
*Sent:* Friday, February 26, 2016 3:34 PM
*Subject:* Re: [Coq-Club] Lean Theorem Prover
Since we’re talking about unicode, I’d like to get people’s advice

1. I wonder whether beginning users will find the available input methods confusing or off-putting, and
2. (more significantly) I wonder whether the world has stabilized to the point where the major Coq IDEs will “just work” with unicode in their default configurations on all platforms.
What do people think? Should I just take the plunge? Or is it not time yet?
- Benjamin
I just mean I like the agda-style input which replaces \forall by the unicode ∀ seamlessly. It's possible that this is supported in coq as well I guess (I'm a little behind the times).
That's just built-in in emacs. There are even several ways to do that (the old-school quail, and the newish company-math at least).
Indeed; with plain Emacs, just typing `M-x set-input-method RET TeX RET` will give you the Agda-style input that you mentionned.
Alternatively (if you use it), company-coq loads company-math, so typing \rightarr will offer \rightarrow, and RET will complete it to →.
Should we make this the default input method in PG?
Clément.
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
Makarius
2016-02-26 18:16:54 UTC
Permalink
Post by Soegtrop, Michael
1.) Using Unicode notations in the HTML version but ASCII in the IDE is
as confusing as finding the shortcuts for the right symbols
2.) Most people read more than they write, so it makes sense to optimize
for readability – and the Unicode symbols are more readable
3.) The shortcuts for the Unicode symbols can be mentioned in IDE menus
at a prominent place
I fully agree that high-end proof assistants should support proper
mathematical symbols without the user having to think about it. I disagree
that such a blissful situation can be equated with "Unicode". Unicode is a
rather big standard with many sub-standards, and it requires years and
decades to make it really work for a particular task.

About 8 years ago, I set out to make mathematical symbols "just work" for
the forthcoming Prover IDE of Isabelle -- uniformly on all platforms. It
required several years to get there, and every year I learned new aspects
of Unicode that I could not imagine before. In the current release of
Isabelle2016 (February 2016) this is mostly routine, and we have again
eliminated a lot of old ASCII replacement syntax. Interestingly, that
release also parts with official Unicode in various ways, e.g. see "more
arrow symbols" announced here
http://isabelle.in.tum.de/dist/Isabelle2016/doc/NEWS.html

Hopefully you see there arrows of length 3 and 4, taken from a server-side
font that is also used in the IDE. Length 1 and 2 are defined by the
Unicode standard and are in their usual place. Note that in standard
Unicode fonts, length 2 arrows can already be a problem, and lead to
disappointing white or black boxes.
Post by Soegtrop, Michael
· On Windows non-Unicode is dead. The last non Unicode Version was
Windows ME (Millennium Edition) which I don’t think is used any more.
Even its successor Windows XP is out of maintenance since a while and XP
does support Unicode (always – there are no XP systems which don’t
https://en.wikipedia.org/wiki/Usage_share_of_operating_systems.
· I did a quick search on google for Unicode issues with
Linux/Debian/Ubuntu/Fedora/Mint. The first 20 articles I found where all
2009 or older. So I think issues are solved since then, since google
doesn’t tend to prefer old articles.
· I would think Mac with its DTP background was pretty much always
Unicode.
All these platforms pretend to support Unicode for some decades, but it is
still possible to get into problems. It is not something that just works
by default and can be counted on.

With some care, it is possible to turn Unicode into some use. I recommend
to read the relevant documentation:
http://isabelle.in.tum.de/dist/Isabelle2016/doc/jedit.pdf
http://isabelle.in.tum.de/dist/Isabelle2016/doc/system.pdf
http://isabelle.in.tum.de/dist/Isabelle2016/doc/isar-ref.pdf
and search for "Isabelle symbols". The phrase "Unicode" is hardly ever
used, because it is of little relevance.


I have pointed this out to various Coq people more than once, and this is
just an opportunity to make a broadcast.


Makarius
Clément Pit--Claudel
2016-02-26 21:00:21 UTC
Permalink
Post by Makarius
About 8 years ago, I set out to make mathematical symbols "just work"
for the forthcoming Prover IDE of Isabelle -- uniformly on all
platforms. It required several years to get there, and every year I
learned new aspects of Unicode that I could not imagine before. In
the current release of Isabelle2016 (February 2016) this is mostly
routine, and we have again eliminated a lot of old ASCII replacement
syntax. Interestingly, that release also parts with official Unicode
in various ways, e.g. see "more arrow symbols" announced here
http://isabelle.in.tum.de/dist/Isabelle2016/doc/NEWS.html.
I don't think this implies departing from Unicode, except to the extent that you're introducing new glyphs. There are simple ways do this while remaining compliant (see http://www.unicode.org/faq/private_use.html). This page says

Private-use characters are code points whose interpretation is not
specified by a character encoding standard and whose use and
interpretation may be determined by private agreement among
cooperating users. Private-use characters are sometimes also referred
to as user-defined characters (UDC) or vendor-defined characters
(VDC).
Post by Makarius
Hopefully you see there arrows of length 3 and 4, taken from a
server-side font that is also used in the IDE.
There seems to be a bug in that page. The sources include:
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
and further down:
Support for more arrow symbols, with rendering in LaTeX and Isabelle fonts: ⇚ ⇛ ‎ ‏ ⇠ ⇢.

If the intent is that these should display as long arrows, then charset=utf-8 is incorrect. Instead of using previously unassigned codes for extra arrows, it seems that Isabelle decided instead to recycle existing UTF-8 codes for "(LEFT/RIGHT)WARDS (DOUBLE/TRIPLE) DASH ARROW", thus creating a new coding system (diverging slightly from UTF-8). Is that right? This means that Isabelle sources will look funny if viewed in a git diff, on GitHub, in emails, and in any other places that do not use Isabelle's custom font. Switching to that font as the system default, on the other hand, will break dashed arrows in every other program.
Post by Makarius
Note that in standard Unicode fonts, length 2 arrows can already be a
problem
I don't think this is a Unicode issue. It has to do with whether the user has installed a font containing long arrows ( ⟶ and ⟵ ). Such fonts are getting more common, but indeed they aren't available everywhere yet. Installing a good font is an easy way to solve this issue, and this can happen when Isabelle is installed (it already happens for Isabelle's own font).
Post by Makarius
and lead to disappointing white or black boxes.
That problem still exists in Isabelle 2016; see Loading Image.... In fact, it seems that Isabelle's configuration of jEdit ignores other installed fonts, even though they contain the right characters. This is visible both when using symbols that Isabelle's font do not include, and when writing in non-English scripts, such as east Asian scripts; these characters are shown as squares in jEdit, but they display properly in my web browser and in most other applications on my system.

Cheers,
Clément.
Makarius
2016-02-26 22:53:34 UTC
Permalink
Post by Clément Pit--Claudel
Interestingly, that release also parts with official Unicode in various
ways, e.g. see "more arrow symbols" announced here
http://isabelle.in.tum.de/dist/Isabelle2016/doc/NEWS.html.
I don't think this implies departing from Unicode, except to the extent
that you're introducing new glyphs. There are simple ways do this while
remaining compliant (see http://www.unicode.org/faq/private_use.html).
Hopefully you see there arrows of length 3 and 4, taken from a
server-side font that is also used in the IDE.
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
Support for more arrow symbols, with rendering in LaTeX and Isabelle fonts: ⇚ ⇛ ‎ ‏ ⇠ ⇢.
If the intent is that these should display as long arrows, then
charset=utf-8 is incorrect. Instead of using previously unassigned codes
for extra arrows, it seems that Isabelle decided instead to recycle
existing UTF-8 codes for "(LEFT/RIGHT)WARDS (DOUBLE/TRIPLE) DASH ARROW",
thus creating a new coding system (diverging slightly from UTF-8).
This is why I said we are more and more departing from official Unicode --
and were actually never really using it. The task is not to comply with a
monster standard, but to support mathematical symbols in formal texts
(including sub/superscripts and bold face).

The rendering of ‎ ‏ ⇠ ⇢ (officially arrows with 3/4 dashes) as arrows
of length 3/4 is just one of many workarounds to make something useful out
of the situation. As long as the Isabelle font is used, it is shown as
intended. Outside of this context (i.e. copied into some email or onto
Stackoverflow) it still makes some sense, if the system font happens to
provide these standard glyphs. It should be clear to users that a text
terminal or mail reader is not as accurate as the Prover IDE itself (or
its LaTeX-based document preparation system).
Post by Clément Pit--Claudel
Is that right? This means that Isabelle sources will look funny if
viewed in a git diff, on GitHub
Isabelle users Mercurial, not git. But the question is the same: sources
are stored without Unicode encoding in clear text, e.g. see
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016/NEWS

For the Prover IDE, this representation counts as "encoding", which is
defined as part of the jEdit plugin. In principle it could be also done
for the JVM. Thus Isabelle symbols look like normal Unicode strings to JVM
applications, but they need to be handled with care.
Post by Clément Pit--Claudel
in emails, and in any other places that do not use Isabelle's custom
font. Switching to that font as the system default, on the other hand,
will break dashed arrows in every other program.
The principle is this: authentic sources are stored as plain text with
explicit symbol names. Thus the repertoire of symbols is easily
extensible and decodable by archeologists who find our proof repositories
in distant future.


Mails and adhoc views in editors or browsers are less authentic, using
Unicode only as a poor-man's rendering tool.

Such rendering can go badly wrong, if official Unicode standards are
observed, e.g. in the change of left-to-right versus right-to-left
characters. See the bottom of
http://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Hebrew.html -- I made
this example quite enthusiastically, when Unicode was first supported in
some version of XEmacs, before Emacs 22 started to support Unicode. Only
much later, I discovered that Emacs was rendering that wrongly: In the
final lemma, the "He" and the "135" need to be swapped across the equation
sign. This gives mathematical nonsense, but is correct Unicode text
rendering. (I should probably explain this explicitly in the example.)

There are more such traps hidden in Unicode, e.g. "Combining Characters".
This means you can never be quite sure what the equality on character
strings really is.


The conclusion is that Isabelle does not support official Unicode, but
uses it as approximative tool to render its infinite collection of named
symbols. That should be understood as a flat version of LaTeX math, with
visual representation in the editor.


Makarius
Clément Pit--Claudel
2016-02-27 00:23:34 UTC
Permalink
Post by Makarius
This is why I said we are more and more departing from official
Unicode -- and were actually never really using it. The task is not
to comply with a monster standard, but to support mathematical
symbols in formal texts (including sub/superscripts and bold face).
Aren't subscripts and superscripts a markup issue? They seem to have little to do with Unicode.
Post by Makarius
For the Prover IDE, this representation counts as "encoding", which
is defined as part of the jEdit plugin. In principle it could be also
done for the JVM. Thus Isabelle symbols look like normal Unicode
strings to JVM applications, but they need to be handled with care.
Thanks for the clarification. Is this approach superior to just using a smarter display layer, like Emacs does with prettify-symbols-mode or Proof General's unicode-tokens (which supported HOL and Isar a while ago)? It seems that the core Isabelle is essentially ASCII only, but the IDE comes with a rendering engine that uses a translation to and from a non-ASCII string to display pretty math into a basic text box. Is this better than using a smarter text box (one that would be aware of Isabelle's markup)?
Post by Makarius
The principle is this: authentic sources are stored as plain text
with explicit symbol names. Thus the repertoire of symbols is easily
extensible and decodable by archeologists who find our proof
repositories in distant future.
I see; thanks. Most Coq developments seem to follow this principle too, using plain text only. It's easy then to set up one's editor to display plain text documents with pretty symbols (Proof General does it optionally with unicode-tokens; company-coq does it by default). If I understand correctly, though, Prof. Pierce doesn't seem fully satisfied with this solution.
Post by Makarius
There are more such traps hidden in Unicode, e.g. "Combining
Characters". This means you can never be quite sure what the equality
on character strings really is.
Unicode defines various level of language-awareness in string comparisons, all under the headline of collation (http://www.unicode.org/collation/). Is this relevant to that issue?

Clément.
Makarius
2016-02-27 16:25:26 UTC
Permalink
This post might be inappropriate. Click to display it.
Enrico Tassi
2016-02-27 16:54:28 UTC
Permalink
Post by Makarius
This is again in conflict with "minimize assumptions about available
technology".
I recall the Matita guys trying to provide smarter text boxes for OCaml GTK
(based on MathML). Did this ever reach the big masses of users on all
platforms?
Sadly no. Also GTK+ cannot really be considered cross platform :-/
Recent version of Matita output plain utf8 text.

Ciao
--
Enrico Tassi
Clément Pit--Claudel
2016-02-26 20:53:12 UTC
Permalink
Post by Makarius
About 8 years ago, I set out to make mathematical symbols "just work"
for the forthcoming Prover IDE of Isabelle -- uniformly on all
platforms. It required several years to get there, and every year I
learned new aspects of Unicode that I could not imagine before. In
the current release of Isabelle2016 (February 2016) this is mostly
routine, and we have again eliminated a lot of old ASCII replacement
syntax. Interestingly, that release also parts with official Unicode
in various ways, e.g. see "more arrow symbols" announced here
http://isabelle.in.tum.de/dist/Isabelle2016/doc/NEWS.html.
I don't think this implies departing from Unicode, except to the extent that you're introducing new glyphs. There are simple ways do this while remaining compliant (see http://www.unicode.org/faq/private_use.html). This page says

Private-use characters are code points whose interpretation is not
specified by a character encoding standard and whose use and
interpretation may be determined by private agreement among
cooperating users. Private-use characters are sometimes also referred
to as user-defined characters (UDC) or vendor-defined characters
(VDC).
Post by Makarius
Hopefully you see there arrows of length 3 and 4, taken from a
server-side font that is also used in the IDE.
There seems to be a bug in that page. Looking at its sources, I see:
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
and further down:
Support for more arrow symbols, with rendering in LaTeX and Isabelle fonts: ⇚ ⇛ ⤎ ⤏ ⇠ ⇢.

If the intent is that these should display as long arrows, then charset=utf-8 is incorrect. Instead of using previously unassigned codes for extra arrows, it seems that Isabelle decided instead to recycle existing UTF-8 codes for "(LEFT/RIGHT)WARDS (DOUBLE/TRIPLE) DASH ARROW", thus creating a new coding system (diverging slightly from UTF-8). Is that right? This means that Isabelle sources will look funny if viewed in a git diff, on GitHub, in emails, and in any other places that do not use Isabelle's custom font. Switching to that font as the system default, on the other hand, will break dashed arrows in every other program.
Post by Makarius
Note that in standard Unicode fonts, length 2 arrows can already be a
problem
I don't think this is a Unicode issue. It has to do with whether the user has installed a font containing long arrows ( ⟶ and ⟵ ). Such fonts are getting more common, but indeed they aren't available everywhere yet. Installing a good font is an easy way to solve this issue, and this can happen when Isabelle is installed (it already happens for Isabelle's own font).
Post by Makarius
and lead to disappointing white or black boxes.
That problem still exists in Isabelle 2016; see https://i.imgur.com/KoibYJu.png. In fact, it seems that Isabelle's configuration of jEdit ignores other installed fonts, even though they contain the right characters. This is visible both when using symbols that Isabelle's font do not include, and when writing in non-English scripts, such as east Asian scripts; these characters are shown as squares in jEdit, but they display properly in my web browser and in most other applications on my system.

Cheers,
Clément.
Soegtrop, Michael
2016-02-29 09:52:40 UTC
Permalink
Dear Makarius,
Post by Makarius
I fully agree that high-end proof assistants should support proper
mathematical symbols without the user having to think about it. I disagree
that such a blissful situation can be equated with "Unicode". Unicode is a
rather big standard with many sub-standards, and it requires years and
decades to make it really work for a particular task.
I see that I was a bit simple minded here. I have quite some experience with supporting languages like Japanese or Russian in my SW, but I see that supporting math is a completely different story. I guess it boils down to the fact that OSes don't have a language package for "math" as they have for e.g. Japanese. Maybe this is what we should try to achieve long term. E.g. not only math fonts but a SW independent math IME (the thing in an OS which converts what you type to Unicode characters). Coming back to the subject of this thread: there is some hope.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsge
Daniel Schepler
2016-02-26 22:58:08 UTC
Permalink
On Fri, Feb 26, 2016 at 6:34 AM, Benjamin C. Pierce
Post by Benjamin C. Pierce
(more significantly) I wonder whether the world has stabilized to the point
where the major Coq IDEs will “just work” with unicode in their default
configurations on all platforms.
As just one data point - on Debian GNU/Linux, the GTK-based CoqIDE
just works with unicode. As for inputting unicode characters, it took
a bit more effort - but the instructions at
https://coq.inria.fr/cocorico/TeXInputMethodForUnicodeNotations under
"In CoqIDE (using UIM on POSIX systems)" were all I needed to get that
working.
--
Daniel
Saulo Araujo
2016-02-26 23:52:42 UTC
Permalink
Hi,

IÂŽd like to thank everybody who took some time to share his impressions
about Lean. The thread has changed a little bit and now we are talking
about Unicode, but that's ok :

Saulo
Post by Daniel Schepler
On Fri, Feb 26, 2016 at 6:34 AM, Benjamin C. Pierce
Post by Benjamin C. Pierce
(more significantly) I wonder whether the world has stabilized to the
point
Post by Benjamin C. Pierce
where the major Coq IDEs will “just work” with unicode in their default
configurations on all platforms.
As just one data point - on Debian GNU/Linux, the GTK-based CoqIDE
just works with unicode. As for inputting unicode characters, it took
a bit more effort - but the instructions at
https://coq.inria.fr/cocorico/TeXInputMethodForUnicodeNotations under
"In CoqIDE (using UIM on POSIX systems)" were all I needed to get that
working.
--
Daniel
Saulo Araujo
2016-02-27 00:05:07 UTC
Permalink
Oops, an important character was missing in the previous email: What I
meant was "but that's ok :)"

Saulo
Post by Saulo Araujo
Hi,
IÂŽd like to thank everybody who took some time to share his impressions
about Lean. The thread has changed a little bit and now we are talking
Saulo
Post by Daniel Schepler
On Fri, Feb 26, 2016 at 6:34 AM, Benjamin C. Pierce
Post by Benjamin C. Pierce
(more significantly) I wonder whether the world has stabilized to the
point
Post by Benjamin C. Pierce
where the major Coq IDEs will “just work” with unicode in their default
configurations on all platforms.
As just one data point - on Debian GNU/Linux, the GTK-based CoqIDE
just works with unicode. As for inputting unicode characters, it took
a bit more effort - but the instructions at
https://coq.inria.fr/cocorico/TeXInputMethodForUnicodeNotations under
"In CoqIDE (using UIM on POSIX systems)" were all I needed to get that
working.
--
Daniel
Clément Pit--Claudel
2016-03-01 07:41:00 UTC
Permalink
Hi Benjamin and Michael,
Post by Soegtrop, Michael
1. I wonder whether beginning users will find the available input methods confusing or off-putting
1.) Using Unicode notations in the HTML version but ASCII in the IDE is as confusing as finding the shortcuts for the right symbols [...]
3.) The shortcuts for the Unicode symbols can be mentioned in IDE menus at a prominent place
As an experiment, I've added input and prettification hints to company-coq. When the point is on a prettified symbol (such as ‘fun’ being displayed as ‘λ’, or ‘nat’ being displayed as ‘ℕ’), company-coq now shows a message similar to these:

‘λ’ is a prettified version of ‘fun’.
‘ℕ’ is a prettified version of ‘nat’.

On the other hand, when the point is on a Unicode symbol, such as ‘∪’ or ‘⊕’, company-coq now shows a message similar to these:

To input ‘∪’, type ‘\cup RET’.
To input ‘⊕’, type ‘\oplus RET’.

There are screenshots at https://github.com/cpitclaudel/company-coq/#misc-extensions-of-proof-general

As always, comments and suggestions are very welcome! Let me know what you think.

Cheers,
Clément.
Soegtrop, Michael
2016-03-01 08:07:47 UTC
Permalink
Dear Clément,
Post by Clément Pit--Claudel
As always, comments and suggestions are very welcome! Let me know what you think.
I admit I am a CoqIDE user. Maybe it is time to revisit emacs. I used it a lot during my university time, but not much since then.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen
Enrico Tassi
2016-03-01 09:25:53 UTC
Permalink
Post by Soegtrop, Michael
Dear Clément,
Post by Clément Pit--Claudel
As always, comments and suggestions are very welcome! Let me know what you think.
I admit I am a CoqIDE user. Maybe it is time to revisit emacs. I used
it a lot during my university time, but not much since then.
As far as I know, today only CoqIDE and Coqoon support the asynchronous
evaluation of proofs.

I hope I'll manage to get Pierre and Clement in the same room during the
forthcoming "developers workshop"... and "fix" this.

If a brave one really wants to add to CoqIDE handy utf8 input mode, I'd
suggest copying the one we had in Matita:
https://github.com/gares/matita/blob/master/matita/matitaScript.ml#L358
https://github.com/gares/matita/blob/master/matita/matitaScript.ml#L436
https://github.com/gares/matita/blob/master/matita/predefined_virtuals.ml
It was quite pleasant to use.

Best,
--
Enrico Tassi
Pierre-Marie Pédrot
2016-03-01 09:50:44 UTC
Permalink
Post by Enrico Tassi
If a brave one really wants to add to CoqIDE handy utf8 input mode, I'd
Notwithstanding this whole discussion, I'm not sure this is the rôle of
the editor to implement a nice input method. KISS! Plus GTK-sourceview
2.x is a really crappy editor, and interfering with what the user types
is often buggy.

I am a proud user of CoqIDE and ibus + latextables and I'm pretty much
happy about it. Maybe we should provide an even better method for proof
writing in ibus?

PMP
Soegtrop, Michael
2016-03-01 11:05:28 UTC
Permalink
Dear Pierre-Marie,
Notwithstanding this whole discussion, I'm not sure this is the rôle of the
editor to implement a nice input method. KISS! Plus GTK-sourceview 2.x is a
really crappy editor, and interfering with what the user types is often buggy.
I agree that we should go for what Microsoft calls an IME (https://en.wikipedia.org/wiki/Input_method) for typing math symbols. It would make more sense to type the same way when writing an email or a document as when typing in Coq. Not sure, though, if IMEs can be nested, e.g. if a Japanese IME can be used in combination with a math IME. Does this work on Linux?

If I understand you right, something like this exists for Linux. Could you give a few more pointers?

The Lean project gives me some hope that we will have something like this for Windows as well. If we agree on this is the way to go, I could try to use some contacts to push this within MS. I might also be able to come up with a prototype. I think there is some open source SW which can be tweaked to behave like a configurable IME.

Not sure what to do on Mac, though. Does it come with a configurable IME like Linux?

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
Matej Kosik
2016-03-01 11:32:30 UTC
Permalink
Post by Soegtrop, Michael
Dear Pierre-Marie,
Notwithstanding this whole discussion, I'm not sure this is the rôle of the
editor to implement a nice input method. KISS! Plus GTK-sourceview 2.x is a
really crappy editor, and interfering with what the user types is often buggy.
I agree that we should go for what Microsoft calls an IME (https://en.wikipedia.org/wiki/Input_method) for typing math symbols. It would make more sense to type the same way when writing an email or a document as when typing in Coq. Not sure, though, if IMEs can be nested, e.g. if a Japanese IME can be used in combination with a math IME. Does this work on Linux?
If I understand you right, something like this exists for Linux. Could you give a few more pointers?
This weekend, I've tried XIM (The X Input Method).
I guess that is the oldest input method for X.

Here are my notes what I needed to do to get what I needed.

https://github.com/matej-kosik/coq/tree/v8.5__Show_Tree__BLANK__propositional_logic__1#configuring-xim-the-x-input-method

Then I was able to type the UNICODE glyphs I needed
(in coqtop running in my X terminal
in CoqIDE
in Emacs
and just about anywhere where I bothered to test ... ⊤ ⊥ ¬ ∧ ∨ → ↔ ℙ)

There are much more fancier alternatives but this one (XIM) worked for me well.
Soegtrop, Michael
2016-03-01 11:56:47 UTC
Permalink
Dear Matje,
Post by Matej Kosik
https://github.com/matej-
kosik/coq/tree/v8.5__Show_Tree__BLANK__propositional_logic__1#config
uring-xim-the-x-input-method
Nice. I try to achieve something similar for Windows. Give me a week ...

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munic
Vincent Laporte
2016-03-01 12:11:08 UTC
Permalink
Hi,

Here is a software that provides a “compose key” for MS-Windows:

https://github.com/samhocevar/wincompose

Cheers,
--
Vincent.
Soegtrop, Michael
2016-03-01 12:23:06 UTC
Permalink
Dear Vincent,
Post by Vincent Laporte
https://github.com/samhocevar/wincompose
An interesting feature of this is that it seems to use the same file format as Xcompose for X.
The one thing I am not sure about is if one should use an IME (something that is recognized by Windows as an IME) or some post processor like this. Since I don't think IMEs can be stackes, I guess such a postprocessor is more deseriable for those languages which require an IME.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 18692
Soegtrop, Michael
2016-03-02 09:03:11 UTC
Permalink
Dear Coq Team & Users,
Post by Vincent Laporte
https://github.com/samhocevar/wincompose
I had a look at WinCompose as Math IME as suggested by Vincent Laporte (test machine is Win7 64). It works well with CoqIDE and any other SW I tested and it reuses the Linux Xcompose file. The license of wincompose as well as of the used Xcompose file is a permissive open source license. It doesn't require complicated installation (just unzip and run the exe).

So how about bundling this with CoqIDE for Windows and using Xcompose on Linux (and I guess also Mac).
One change I would do in Wincompose is that it checks if it is already started and exits immediately if so. Then CoqIDE could just spawn WinCompose to make sure it is loaded.

Some important sequences are as follows:

Compose A A for "forall"
Compose E E for "exists"
Compose - > for "arrow right"
Compose < - for "arrow left"
Compose <-> for "arrow double

The Compose key (by default right alt) is pressed and released - not hold.
For forall the A is upper case, so it has to be pressed with shift.
One little down side is that some sequences have a common header like <- and <->. So the <- symbol appears only after one presses a character which doesn't lead to known sequence, like space.
Not sure if it would be more convenient to require that the Compose key is kept held down to avoid this.

Of cause it would be possible to add additional sequences like

Compose forall for "forall"
Compose exists for "exists"
Compose implies for "arrow right"

The following abbreviations are also still free:

Compose fa for "forall"
Compose ex for exists
Compose imp for implies

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen
Soegtrop, Michael
2016-03-02 16:24:04 UTC
Permalink
Dear Coq Team and Users,
Post by Soegtrop, Michael
So how about bundling this with CoqIDE for Windows and using Xcompose on
Linux (and I guess also Mac).
I have to revoke my assessment that that it would be a good idea to use WinCompose for the input of Unicode characters on Windows for e.g. CoqIDE. The license is permissive, but not what lawyers want to have in a SW IP list (you will know what I mean when you read the license).

What do others think? Should the input of math Unicode characters be part of the IDE or part of the OS or some IME like SW?

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Regist
Pierre-Marie Pédrot
2016-03-02 16:32:50 UTC
Permalink
Post by Soegtrop, Michael
I have to revoke my assessment that that it would be a good idea to
use WinCompose for the input of Unicode characters on Windows for
e.g. CoqIDE. The license is permissive, but not what lawyers want to
have in a SW IP list (you will know what I mean when you read the
license).
What? WTFPL is a respectable free software license! It's accepted by
both Debian and the FSF, what are you asking for?

I mean, Coq is already named Coq thanks to the great and immortal French
people, why do you think it would be worse in any respect?

Moreover, I, as a Frenchman, particularly appreciate Sam Hocevar's trait
Post by Soegtrop, Michael
Isn’t this license basically public domain?
There is no such thing as “putting a work in the public domain”, you
America-centered, Commonwealth-biased individual. Public domain
varies with the jurisdictions, and it is in some places debatable
whether someone who has not been dead for the last seventy years is
entitled to put his own work in the public domain.
PMP
Soegtrop, Michael
2016-03-02 17:06:33 UTC
Permalink
Dear Pierre-Marie,
Isn’t this license basically public domain?
Public domain is something which doesn't have any license or copyright conditions at all - WTFPL is still a license and implies it is not PD. But this is lawyer fine print and essentially you are right. Nevertheless it might have some negative implications. I don't know what your rules are, but if we publish SW we make sure we name all the licenses of all the pieces of SW involved. In case you have similar rules, it would mean you have to name the WTFPL in the overall license of Coq. Then it might be that others, namely industrial users of Coq, don't like this. One of our lawyers just told me that WTFPL is pretty much a no go, just because she doesn't want to discuss it with other lawyers. So if I want to use Coq, and Coq would bundle this, I would end up explaining a group of corporate lawyers why I need this anyway, although it has this strangely named license in it.

Of cause the WTFPL would also allow to relicense it say under LGPL like Coq. So INRIA could do this and publish all under LGPL. But then some corporate users will likely find out (there are automated tools for this) and wonder why INRIA changes the license and maybe start bothering you with questions around this.

To make it short: industrial users take open source serious and including WTFPL stuff is somehow not compatible with this. I guess lawyers just feel a bit teased by the lack of respect for their profession expressed by WTFPL.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgeri
Ralf Jung
2016-03-02 17:49:50 UTC
Permalink
Hi,
Post by Soegtrop, Michael
Of cause the WTFPL would also allow to relicense it say under LGPL
like Coq. So INRIA could do this and publish all under LGPL. But then
some corporate users will likely find out (there are automated tools
for this) and wonder why INRIA changes the license and maybe start
bothering you with questions around this.
This is pretty normal practice, albeit it often happens implicitly --
whenever someone is distributing, e.g., a GPL-ed application with a
BSD-licensed library, they are effectively re-licensing the library
under GPL to make it compatible with the application.

Kind regards,
Ralf
Clément Pit--Claudel
2016-03-02 17:51:32 UTC
Permalink
Post by Soegtrop, Michael
Of cause the WTFPL would also allow to relicense it say under LGPL
like Coq. So INRIA could do this and publish all under LGPL. But then
some corporate users will likely find out (there are automated tools
for this) and wonder why INRIA changes the license and maybe start
bothering you with questions around this.
Feel free to use this MIT licensed fork: https://github.com/cpitclaudel/wincompose

Clément.
Enrico Tassi
2016-03-02 18:10:46 UTC
Permalink
Post by Soegtrop, Michael
Of cause the WTFPL would also allow to relicense it say under LGPL
like Coq. So INRIA could do this and publish all under LGPL. But then
some corporate users will likely find out (there are automated tools
for this) and wonder why INRIA changes the license and maybe start
bothering you with questions around this.
Would it make any difference if the software was relicensed by its
author, instead of Inria?

Best
--
Enrico Tassi
Soegtrop, Michael
2016-03-02 22:23:00 UTC
Permalink
Dear Enrico,
Would it make any difference if the software was relicensed by its author, instead of Inria?
I guess so. I sent him an email explaining the situation. Let's see what happens.

The MIT branch created by Clément might work or might not work. We use tools which compares SW we use or deliver with essentially all SW on the internet, so the issue with the WTFPL would likely still show up in case we would in some future create a Coq based toolchain. The issue is not really a legal issue, but it would force us to put some obscenity in SW ancestry documentation, and this is simply a no go in an international company.

Best regards,

Michael

-----Original Message-----
From: coq-club-***@inria.fr [mailto:coq-club-***@inria.fr] On Behalf Of Enrico Tassi
Sent: Wednesday, March 2, 2016 7:11 PM
To: coq-***@inria.fr
Subject: Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)
Of cause the WTFPL would also allow to relicense it say under LGPL
like Coq. So INRIA could do this and publish all under LGPL. But then
some corporate users will likely find out (there are automated tools
for this) and wonder why INRIA changes the license and maybe start
bothering you with questions around this.
Would it make any difference if the software was relicensed by its author, instead of Inria?

Best
--
Enrico Tassi
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
Pierre-Marie Pédrot
2016-03-02 22:47:39 UTC
Permalink
This post might be inappropriate. Click to display it.
Gabriel Scherer
2016-03-03 13:17:33 UTC
Permalink
Pierre-Marie, I think the worry is valid, and that sending an email to the
author when there are licensing troubles is the right process to follow,
independently of the author's sense of humor.

On Wed, Mar 2, 2016 at 5:47 PM, Pierre-Marie Pédrot <
Post by Pierre-Marie Pédrot
Post by Soegtrop, Michael
I guess so. I sent him an email explaining the situation. Let's see what happens.
You're seriously trying to make Sam Hocevar relicense a software he
wrote because of the name of the license? Do you know that apart from
being the designer of the WTFPL, he's also the developer of the famous
libcaca, one of the author of the famous http://cyclim.se/ site, as well
as a fan of that sort of stuff: http://sam.zoy.org/porn/ (do not worry,
that's SFW).
I would personally feel a bit ashamed to know that people ask him to do
this for the benefit of the Coq software...
« Gérard, reviens, ils sont devenus fous ! »
PMP
Enrico Tassi
2016-03-03 14:34:58 UTC
Permalink
Post by Pierre-Marie Pédrot
I would personally feel a bit ashamed to know that people ask him to do
this for the benefit of the Coq software...
I know and esteem Sam, as any Debian developer of my generation does,
and believe me, he is far from being a fool, despite his peculiar sense
of humor.

This is why I asked if a relicensing coming from him would help.
I think I could have some grip on this topic, given we share a common
background on free software. Also, his (to my taste) hilarious license
was designed as a pun to GPL-vs-BSD zealots, not to annoy companies.

Ciao
--
Enrico Tassi
Soegtrop, Michael
2016-03-03 15:59:20 UTC
Permalink
Dear Enrico,
Post by Enrico Tassi
This is why I asked if a relicensing coming from him would help.
I think I could have some grip on this topic, given we share a common
background on free software. Also, his (to my taste) hilarious license was
designed as a pun to GPL-vs-BSD zealots, not to annoy companies.
If I would know Sam personally, I would definitely try to make him aware of the issues.

Btw.: do you think that keeping Unicode input outside of CoqIDE is the right way to go?

One interesting point is that I had a discussions with a SW engineer on this topic today and he really doesn't like special notations for things like forall or exists. He believes that many SW engineers might be repelled by such notations, because they are not used to it. I argued that doing math to a certain extent uses the visual capabilities of the brain and that this requires a notation which can be visually processed, but I don't think I could convince him. Maybe there are people who a more audio/language centric and others who are more visual centric and that this influences which notations you prefer.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
Clément Pit--Claudel
2016-03-03 16:42:44 UTC
Permalink
Post by Soegtrop, Michael
One interesting point is that I had a discussions with a SW engineer
on this topic today and he really doesn't like special notations for
things like forall or exists. He believes that many SW engineers
might be repelled by such notations, because they are not used to it.
I argued that doing math to a certain extent uses the visual
capabilities of the brain and that this requires a notation which can
be visually processed, but I don't think I could convince him. Maybe
there are people who a more audio/language centric and others who are
more visual centric and that this influences which notations you
prefer.
I think prettification offers an interesting middle ground (see an example at https://github.com/cpitclaudel/company-coq/#prettification-of-operators-types-and-subscripts; these two screenshots show the same Emacs buffer, with and without the prettification layer). This should allow both kinds of SW engineers to work on the same files.

Clément.
Jonathan Leivent
2016-03-03 17:28:28 UTC
Permalink
Post by Clément Pit--Claudel
Post by Soegtrop, Michael
One interesting point is that I had a discussions with a SW engineer
on this topic today and he really doesn't like special notations for
things like forall or exists. He believes that many SW engineers
might be repelled by such notations, because they are not used to it.
I argued that doing math to a certain extent uses the visual
capabilities of the brain and that this requires a notation which can
be visually processed, but I don't think I could convince him. Maybe
there are people who a more audio/language centric and others who are
more visual centric and that this influences which notations you
prefer.
I think prettification offers an interesting middle ground (see an example at https://github.com/cpitclaudel/company-coq/#prettification-of-operators-types-and-subscripts; these two screenshots show the same Emacs buffer, with and without the prettification layer). This should allow both kinds of SW engineers to work on the same files.
Clément.
I'll put in a plug for Clémen's work, as well. I am a SW engineer
trying to come to terms with this issue, and the prettification
mechanism offered by Company Coq is a very good compromise. However, it
ties those who want the prettification to the Emacs/PG/Company-Coq
toolset. Not that there's anything wrong with that.

As to Michael's comment: I'm not sure it is audio/language centric vs.
visual centric, but perhaps an explanation doesn't really matter. What
matters is that many SW engineers will see such symbol usage as an
impediment.

-- Jonathan
Lucian M. Patcas
2016-03-04 04:59:21 UTC
Permalink
Hi Clément,

I've been playing with company-coq for a few days and have a few questions:

1. Is it possible to disable subscripting? I have many identifiers of the
form c_n, where c is a string and n a number that I don't want to be
displayed as a subscript.
2. Can comments be prettified?
3. Is it possible to generate prettified coqdoc documents?
4. I don't want Prop, bool etc to be prettified. What file do I have to
edit to remove this behaviour?

Thank you,
Lucian
Post by Clément Pit--Claudel
I think prettification offers an interesting middle ground (see an example
at
https://github.com/cpitclaudel/company-coq/#prettification-of-operators-types-and-subscripts;
these two screenshots show the same Emacs buffer, with and without the
prettification layer). This should allow both kinds of SW engineers to work
on the same files.
Clément.
Clément Pit--Claudel
2016-03-04 06:18:28 UTC
Permalink
Post by Lucian M. Patcas
Hi Clément,
Hi Lucian,
Post by Lucian M. Patcas
1. Is it possible to disable subscripting? I have many identifiers of
the form c_n, where c is a string and n a number that I don't want to
be displayed as a subscript.
Sure; `M-x company-coq-toggle-feature RET smart-subscripts RET` will disable them temporarily. To make that change permanent, use `M-x customize-variable RET company-coq-disabled-features RET`
Post by Lucian M. Patcas
2. Can comments be prettified?
They are in Emacs 25, which is currently in pretest. In 24, the prettification code isn't flexible enough.
Post by Lucian M. Patcas
3. Is it possible to generate prettified coqdoc documents?
Do you mean prettifying symbols inside of code blocks in comments ([
])? If so, yes, but only in Emacs 25.
Or did you have something else in mind?
Post by Lucian M. Patcas
4. I don't want Prop, bool etc to be prettified. What file do I have
to edit to remove this behaviour?
No need to edit a file :) It should be enough to customize the variable `company-coq-prettify-symbols-alist`.

Cheers,
Clément.
Post by Lucian M. Patcas
I think prettification offers an interesting middle ground (see an
example at
https://github.com/cpitclaudel/company-coq/#prettification-of-operators-types-and-subscripts;
these two screenshots show the same Emacs buffer, with and without
the prettification layer). This should allow both kinds of SW
engineers to work on the same files.
Clément.
Clément Pit--Claudel
2016-03-05 23:26:47 UTC
Permalink
Post by Lucian M. Patcas
3. Is it possible to generate prettified coqdoc documents?
Extending prettifications to the output of coqdoc would be nice. I don't know much about CoqDoc, but I'd be happy to talk to someone who does. Here's an example of what exporting a prettified Emacs buffer to Emacs looks like:

http://web.mit.edu/cpitcla/www/html-export/FMapAVL.v.html

One of the tricky aspects is prettifying HTML content without breaking copy-paste; that is, it should be possible to copy Coq code from a prettified page. The page above works fine with Firefox and Chrome; I don't know about Safari and IE.

Clément.
Soegtrop, Michael
2016-03-04 07:45:18 UTC
Permalink
Dear Clément,
Post by Clément Pit--Claudel
I think prettification offers an interesting middle ground (see an example at
https://github.com/cpitclaudel/company-coq/#prettification-of-operators-
types-and-subscripts; these two screenshots show the same Emacs buffer,
with and without the prettification layer). This should allow both kinds of SW
engineers to work on the same files.
Yes indeed. Looking into the fact that some people for whatever reason don't like fancy notations, it is likely the best option to keep the files in ASCII and just display and edit them on the fly in fancy notation.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
Soegtrop, Michael
2016-03-09 11:07:41 UTC
Permalink
Dear Enrico,
Post by Enrico Tassi
This is why I asked if a relicensing coming from him would help.
I think I could have some grip on this topic, given we share a common
background on free software. Also, his (to my taste) hilarious license was
designed as a pun to GPL-vs-BSD zealots, not to annoy companies.
I asked one of our open source licensing experts, which license would be closest to Sam's WTFPL.

He said the closest "accepted" license is the creative commons CC0 license, which was designed to be as close to "Public Domain" as permissible in the various jurisdictions. One nice feature of the CC licenses is that they publish a summary version and a longer version, but the long version is still fairly short.

https://creativecommons.org/publicdomain/zero/1.0/
https://creativecommons.org/publicdomain/zero/1.0/legalcode

So CC0 might be what Sam wants.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
Pierre Courtieu
2016-03-11 15:22:41 UTC
Permalink
Hi,

Concerning prettification there is one problem that is difficult to solve:
indentation. Look for example at the following code that is indented for
non-prettified display:

forall x y, x +
y.

This will not look good if prettified:

∀ x y, x +
y.

And conversely a good indentation in prettified mode would not look good in
non prettified.

In pg+company-coq indentation is done according to the current mode
(prettified or not), but user opening the file with the other mode will
have ugly indentation.

P.
Gabriel Scherer
2016-03-11 15:27:00 UTC
Permalink
Since this thread in in the outside-the-box-thinking category, people
may be interested by Elastic Tabstops that solve this indentation
problem:
http://nickgravgaard.com/elastic-tabstops/

On Fri, Mar 11, 2016 at 10:22 AM, Pierre Courtieu
Post by Pierre Courtieu
Hi,
indentation. Look for example at the following code that is indented for
forall x y, x +
y.
∀ x y, x +
y.
And conversely a good indentation in prettified mode would not look good in
non prettified.
In pg+company-coq indentation is done according to the current mode
(prettified or not), but user opening the file with the other mode will have
ugly indentation.
P.
Clément Pit--Claudel
2016-03-11 15:45:23 UTC
Permalink
Hi Gabriel,

Indeed, it's a cool trick; I wonder if something similar could exist for cases like

[ H: False |- _ ] => congruence
[ H: True /\ False |- _ ] => destruct H

being rendered as

[ H: ⊥ ⊢ _ ] ⇒ congruence
[ H: ⊀ ∧ ⊥ ⊢ _ ] ⇒ destruct H

Clément.
Post by Gabriel Scherer
Since this thread in in the outside-the-box-thinking category, people
may be interested by Elastic Tabstops that solve this indentation
http://nickgravgaard.com/elastic-tabstops/
On Fri, Mar 11, 2016 at 10:22 AM, Pierre Courtieu
Post by Pierre Courtieu
Hi,
indentation. Look for example at the following code that is indented for
forall x y, x +
y.
∀ x y, x +
y.
And conversely a good indentation in prettified mode would not look good in
non prettified.
In pg+company-coq indentation is done according to the current mode
(prettified or not), but user opening the file with the other mode will have
ugly indentation.
P.
Clément Pit--Claudel
2016-03-11 15:39:56 UTC
Permalink
Post by Pierre Courtieu
Hi,
forall x y, x +
y.
∀ x y, x +
y.
And conversely a good indentation in prettified mode would not look good in non prettified.
That's definitely an issue. It tends to be less of a problem in practice than I expected, though; maybe because I tend to align things as

forall x y,
x + y.

instead of the style above.

Another, related issue is uncommon characters not being available in your monospace font, and thus breaking alignment (ever so slightly). It makes block editing a pain. My attempt at fixing that is at https://github.com/cpitclaudel/monospacifier.

Clément.
Clément Pit--Claudel
2016-03-11 15:41:03 UTC
Permalink
Post by Pierre Courtieu
Hi,
forall x y, x +
y.
∀ x y, x +
y.
And conversely a good indentation in prettified mode would not look good in non prettified.
That's definitely an issue. It tends to be less of a problem in practice than I expected, though; maybe because I tend to align things as

forall x y,
x + y.

instead of the style above. We can also teach Emacs to ignore prettifications for indentation purposes.

Another, related issue is uncommon characters not being available in your monospace font, and thus breaking alignment (ever so slightly). It makes block editing a pain. My attempt at fixing that is at https://github.com/cpitclaudel/monospacifier.

Clément.
Jonathan Leivent
2016-03-11 15:42:08 UTC
Permalink
Post by Pierre Courtieu
Hi,
indentation. Look for example at the following code that is indented for
forall x y, x +
y.
∀ x y, x +
y.
And conversely a good indentation in prettified mode would not look good in
non prettified.
In pg+company-coq indentation is done according to the current mode
(prettified or not), but user opening the file with the other mode will
have ugly indentation.
P.
A similar issue occurs with splitting lines to prevent wrapping. A line
with many prettified (hence shortened) symbols can be split much later
when prettified than it would need to when not to keep from wrapping.

Consider also prettification vs. Set Printing Width. Currently,
Company-Coq has an automatic Set Printing Width mode (the default, I
believe) that tracks the buffer width. However, it can't accommodate
its own prettifications - unless it somehow takes over the line
splitting chore from Coq.

I only noticed this when using Company-Coq to fold true and false to
script/bold t and f, hence having many prettifications in the same
term. This enhances readability of terms where the bool constants occur
often. But when printed, the often severe shortening of the resulting
lines makes for uneven output due to the splits occurring too soon.

-- Jonathan
Soegtrop, Michael
2016-03-03 15:13:24 UTC
Permalink
Dear Pierre-Marie,
because of the name of the license? Do you know that apart from being the
designer of the WTFPL, he's also the developer of the famous libcaca, one of
the author of the famous http://cyclim.se/ site, as well as a fan of that sort of
stuff: http://sam.zoy.org/porn/ (do not worry, that's SFW).
yes I am aware of this and I hesitated a bit before I sent the email. I did it anyway because all of the people I know who are a punk outside are very sensible inside and I am not sure if he is aware of the consequences of the F in WTFPL. In the end I think people write open source SW so that it is used (at least this is my motivation). It is fun to create something like the WTFPL but if this has the consequence that your SW is then not used as much, and more importantly the SW of others who copy the WTFPL, I would ask myself if the fun is worth it.
I would personally feel a bit ashamed to know that people ask him to do this
for the benefit of the Coq software...
Would you accept my apologizes if I promise to pay for a beer/wine/scotch/... for you and Sam when you meet him?

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
Pierre-Marie Pédrot
2016-03-02 09:50:02 UTC
Permalink
Post by Soegtrop, Michael
If I understand you right, something like this exists for Linux.
Could you give a few more pointers?
Yep. The engine I use is ibus:

https://en.wikipedia.org/wiki/Intelligent_Input_Bus

and the particular IME is latex-table, which was originally designed for
chinese but allows actually to use any input table based on a user-given
description file (you need to recompile it if you want to change it though).

https://github.com/acevery/ibus-table

https://github.com/acevery/ibus-table/blob/master/tables/additional/latex.txt

I have installed it through Debian, with the ibus-table-latex package.

PMP
Bas Spitters
2016-03-02 10:00:18 UTC
Permalink
This is what we've been using:
https://github.com/c-corn/corn/blob/master/tools/coq.mim

On Wed, Mar 2, 2016 at 10:50 AM, Pierre-Marie Pédrot
Post by Pierre-Marie Pédrot
Post by Soegtrop, Michael
If I understand you right, something like this exists for Linux.
Could you give a few more pointers?
https://en.wikipedia.org/wiki/Intelligent_Input_Bus
and the particular IME is latex-table, which was originally designed for
chinese but allows actually to use any input table based on a user-given
description file (you need to recompile it if you want to change it though).
https://github.com/acevery/ibus-table
https://github.com/acevery/ibus-table/blob/master/tables/additional/latex.txt
I have installed it through Debian, with the ibus-table-latex package.
PMP
Kyle Stemen
2016-03-04 08:10:18 UTC
Permalink
On Wed, Mar 2, 2016 at 1:50 AM, Pierre-Marie Pédrot
pierre-marie.pedrot-at-inria.fr |coq-club/Example Allow| <
Post by Pierre-Marie Pédrot
https://en.wikipedia.org/wiki/Intelligent_Input_Bus
and the particular IME is latex-table, which was originally designed for
chinese but allows actually to use any input table based on a user-given
description file (you need to recompile it if you want to change it though).
https://github.com/acevery/ibus-table
https://github.com/acevery/ibus-table/blob/master/tables/additional/latex..txt
Thanks for pointing out this input method. I tried it and I like it.

I'm running Fedora and there was one little trick to the installation
process. It appears that in later versions of ibus table, the latex table
is no longer bundled by default; it was separated out into a different
package and repository. See issue 1026:
https://groups.google.com/forum/#!topic/ibus-devel/GZ3YABGkUpI

More specifically to install it on Fedora I had to:
1. Install the ibus-table-code package
2. Log out and log in
3. Go to the Region & Language page in the settings dialog.
4. Expand the other category in the add input source dialog.
5. Select Other (LaTeX).
Post by Pierre-Marie Pédrot
I have installed it through Debian, with the ibus-table-latex package.
PMP
Kyle Stemen
2016-03-04 08:10:18 UTC
Permalink
On Wed, Mar 2, 2016 at 1:50 AM, Pierre-Marie Pédrot
pierre-marie.pedrot-at-inria.fr |coq-club/Example Allow| <
Post by Pierre-Marie Pédrot
https://en.wikipedia.org/wiki/Intelligent_Input_Bus
and the particular IME is latex-table, which was originally designed for
chinese but allows actually to use any input table based on a user-given
description file (you need to recompile it if you want to change it though).
https://github.com/acevery/ibus-table
https://github.com/acevery/ibus-table/blob/master/tables/additional/latex.txt
Thanks for pointing out this input method. I tried it and I like it.

I'm running Fedora and there was one little trick to the installation
process. It appears that in later versions of ibus table, the latex table
is no longer bundled by default; it was separated out into a different
package and repository. See issue 1026:
https://groups.google.com/forum/#!topic/ibus-devel/GZ3YABGkUpI

More specifically to install it on Fedora I had to:
1. Install the ibus-table-code package
2. Log out and log in
3. Go to the Region & Language page in the settings dialog.
4. Expand the other category in the add input source dialog.
5. Select Other (LaTeX).
Post by Pierre-Marie Pédrot
I have installed it through Debian, with the ibus-table-latex package.
PMP
Clément Pit--Claudel
2016-03-02 18:37:31 UTC
Permalink
Post by Enrico Tassi
If a brave one really wants to add to CoqIDE handy utf8 input mode, I'd
Notwithstanding this whole discussion, I'm not sure this is the rÃŽle of
the editor to implement a nice input method. KISS! Plus GTK-sourceview
2.x is a really crappy editor, and interfering with what the user types
is often buggy.
Indeed, I use IBus for east-asian scripts and it works nicely there. I haven't used it to input symbols, but it's a cool idea!

Quick sampling from Github gives the following tokens as a few examples of Unicode being used in Proof Scripts:

Γ Π Ί Κ φ ← → ↩ ↟ ⇓ ∅ ∈ ∉ ∖ ∧ √ ∩ ∪ ≅ ≡ ≢ ≀ ≥ ≫ ≌ ⊂ ⊄ ⊆ ⊈ ⊑ ⊗ ⊣ ⊀ ⊥ ⋃ ⋅ ■ □ ▷ ● ◯ ★ ✓ ⟹ ⟩ ⟶ ⟟

Is there a way for me (from Emacs) to query IBus, so I can help users input these characters? Otherwise, does IBus have a good story about discoverability?

Clément
Saulo Araujo
2016-03-07 18:33:30 UTC
Permalink
Maybe the popularization of fonts like https://github.com/i-tu/Hasklig and
https://github.com/tonsky/FiraCode help in this matter. By the way, Visual
Studio Code (an open source code centric IDE developed by Microsoft) has
just added support to these fonts (more details in the section Ligatures
for VS Code of https://code.visualstudio.com/Updates).

Best regards,
Saulo

On Mon, Mar 7, 2016 at 3:06 PM, Emilio Jesús Gallego Arias <
Post by Benjamin C. Pierce
I wonder whether beginning users will find the available input methods
confusing or off-putting, and (more significantly)
I wonder whether the world has stabilized to the point where the major
Coq IDEs will “just work” with unicode in their default configurations
on all platforms.
Regarding these questions, in jsCoq (and thus in courses using it)
+ Assume Coq users know LaTeX: unicode input is done by typing latex
commands, as in emacs.
Whether this is off putting to students, we don't know, but we assume
to know a bit of TeX cannot harm too much.
[Adding a toolbar with symbols would be pretty easy]
+ No pretty-fication: thus no confusion between \leq and ≀ .
+ We believe Unicode should work seamlessly in all supported platforms
(thanks to webfonts).
We'd be very interested to hear whether some use cases are not covered
by these constrains.
Best regards,
Emilio
Clément Pit--Claudel
2016-03-07 20:53:14 UTC
Permalink
Post by Saulo Araujo
Maybe the popularization of fonts like
https://github.com/i-tu/Hasklig and
https://github.com/tonsky/FiraCode help in this matter. By the way,
Visual Studio Code (an open source code centric IDE developed by
Microsoft) has just added support to these fonts (more details in the
section Ligatures for VS Code of
https://code.visualstudio.com/Updates).
Note that this is a special case of prettification: instead of mapping character sequences to common unicode characters, you map them to private codepoints where an alternate representation of the corresponding character is stored.

For example, instead of mapping ‘->’ to ‘→’, you map it to an alternate character (0x110059 in the case of Fira Mono) which also looks like an arrow, but has the right width.
Dominic Mulligan
2016-02-26 08:30:55 UTC
Permalink
Post by roux cody
Not really at the moment. This is a definite drawback (though Isabelle
users don't seem so gung-ho about this). You can sort of pretend with the
Lua bindings, I think.
The last couple of versions of Isabelle have an embedded proof method DSL
called Eisbach, inspired by LTac:

http://ssrg.nicta.com.au/publications/nictaabstracts/7847.pdf
Post by roux cody
Post by Jonathan Leivent
Is there any extraction capability?
It's in the works.
Post by Jonathan Leivent
As for building-in proof irrelevance (while having a separate HoTT mode)
that might not bother anyone but me: I (ab)use proof *relevance* in Coq as
a way to get really good erasability.
I'm confused about this. Could you elaborate? Proof-irrelevance and proof
erasure seem to go rather well together, in my mind.
Post by Jonathan Leivent
I wonder if runs into the same issues that Coq did. See "Meta-theory à la
Carte", section "The Problem of Church Encodings and Induction",
http://people.csail.mit.edu/bendy/MTC/
<http://people.csail.mit.edu/bendy/MTC/>.
Unless I misunderstand, the problem there seems to concern church
encodings in pure CoC (as opposed to CIC), so not much to do with how
inductives are implemented.
Best,
Cody
This email has been sent from a virus-free computer protected by Avast.
www.avast.com
<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail>
<#-1522109089_DDB4FAA8-2DD7-40BB-A1B8-4E2AA1F9FDF2>
Post by Jonathan Leivent
On Thu, Feb 25, 2016 at 2:46 PM, Abhishek Anand
http://www.cs.cornell.edu/~aa755/ROSCoq/coqdoc/MathClasses.misc.decision.html
OK, there's a lot of stuff otherwise in MathClasses that I wish would
make its way into the standard library, too. I just hadn't noticed
that one - though it does seem like it could still use more extension
along the lines I was thinking. (For example, I see and_dec and
or_dec there, but no impl_dec.)
--
Daniel Schepler
Bas Spitters
2016-02-26 10:10:43 UTC
Permalink
The use of type classes in lean was somewhat influenced by mathclasses.
(I was at CMU last winter when they were developing this.)

Lean has found a nice way to efficiently implement type classes and
features of canonical structures, but without actually needing to
implement the latter. Jeremy Avigad has worked with in the
math-components team for a year, so he's well aware of the way ssr
does these things.

Their type class implementation also provides some mechanisms for
extending and renaming structures.
It seems light weight, but the repackaging that is done behind the
scenes looks really helpful and natural.
https://leanprover.github.io/tutorial/ (Chapter Structures.)
Post by Daniel Schepler
On Thu, Feb 25, 2016 at 2:46 PM, Abhishek Anand
Post by Abhishek Anand
http://www.cs.cornell.edu/~aa755/ROSCoq/coqdoc/MathClasses.misc.decision.html
OK, there's a lot of stuff otherwise in MathClasses that I wish would
make its way into the standard library, too. I just hadn't noticed
that one - though it does seem like it could still use more extension
along the lines I was thinking. (For example, I see and_dec and
or_dec there, but no impl_dec.)
--
Daniel Schepler
Loading...