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:
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).
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
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), (continued)
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Jonathan Leivent, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Lucian M. Patcas, 03/04/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/04/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/04/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Bas Spitters, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Kyle Stemen, 03/04/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Kyle Stemen, 03/04/2016
Archive powered by MHonArc 2.6.18.