Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)


Chronological Thread 
  • From: "Kyle Stemen" <ncyms8r3x2 AT snkmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)
  • Date: Fri, 4 Mar 2016 00:10:18 -0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ncyms8r3x2 AT snkmail.com; spf=Pass smtp.mailfrom=ncyms8r3x2 AT snkmail.com; spf=None smtp.helo=postmaster AT sneak2.sneakemail.com
  • Ironport-phdr: 9a23:bthnExEJX02lpx54MtRF251GYnF86YWxBRYc798ds5kLTJ75oc2wAkXT6L1XgUPTWs2DsrQf27WQ7P2rADVRqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0pMCYOlwZzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IZ57nZLw1RqB0CzEvMmZ9pJG69EqLcQza7XwFF24SjxBgAg7f7Ri8UI2inDH9s783+zieMIXNUb0xVDLop/NtQw7tk3cdbC5j2HrRicl5jaYdqxWk8U8si7XIaZ2YYaItNpjWeskXEDYQUw==

On Wed, Mar 2, 2016 at 1:50 AM, Pierre-Marie Pédrot pierre-marie.pedrot-at-inria.fr |coq-club/Example Allow| <rosh2tjoat AT sneakemail.com> wrote:
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


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).
 


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

PMP





Archive powered by MHonArc 2.6.18.

Top of Page