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)

From: Enrico Tassi <enrico.tassi AT inria.fr>
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: Tue, 1 Mar 2016 10:25:53 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:uqfcyBCU8gQy/yUAluHFUyQJP3N1i/DPJgcQr6AfoPdwSP74rsbcNUDSrc9gkEXOFd2CrakU1KyI4uu5AjZIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niKbsqtaKOF8ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5Jf2MMkxFPSzTM9wr7FsP8tDH7ve07xCCBJszeTLYuWD3k4b09G0ygszsOKzNsqDKfscd3lq8O+B8=

On Tue, Mar 01, 2016 at 08:07:47AM +0000, Soegtrop, Michael wrote:
> Dear Clément,
>
> > 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

[Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/01/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/01/2016
  - Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Enrico Tassi, 03/01/2016
    - Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Pierre-Marie Pédrot, 03/01/2016
      - RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/01/2016
        
        Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Matej Kosik, 03/01/2016
        
        RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/01/2016
        
        Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Vincent Laporte, 03/01/2016
        RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/01/2016
        
        RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/02/2016
        RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/02/2016
        Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Pierre-Marie Pédrot, 03/02/2016
        RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/02/2016