coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Suggestions for Proof General?

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Suggestions for Proof General?
Date: Wed, 15 Jun 2016 19:34:56 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f175.google.com
Ironport-phdr: 9a23:yvvSfBXswO/A3CU9LB1B0e1C0UzV8LGtZVwlr6E/grcLSJyIuqrYZheOt8tkgFKBZ4jH8fUM07OQ6PCxHzxfqszd+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8yVM1oD3mb1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDsB1OChTF5ReyeprwrCb8qqIp2i6cPM77Sb05cTun5qZvDhTvjXFUZHYC7GjLh5ko3+pgqxW7qkknzg==

On 06/15/2016 06:39 PM, Pierre Courtieu wrote:

Supporting Ltac debug mode would be good.
P.

Does anyone use that? I find it unhelpful. Although, the UI has something to do with that. If Ltac had a more gdb-style debug mode, with real breakpoints & watchpoints, inspection of env bindings, stack view, source-level display, debug entry on break, and a richer command set, then supporting that would be great.

-- Jonathan

[Coq-Club] Suggestions for Proof General?, Paul A. Steckler, 06/15/2016
- Re: [Coq-Club] Suggestions for Proof General?, Jonathan Leivent, 06/15/2016
  - Re: [Coq-Club] Suggestions for Proof General?, Clément Pit--Claudel, 06/15/2016
  - Re: [Coq-Club] Suggestions for Proof General?, Enrico Tassi, 06/17/2016
    - Re: [Coq-Club] Suggestions for Proof General?, Jonathan Leivent, 06/17/2016
- Re: [Coq-Club] Suggestions for Proof General?, Clément Pit--Claudel, 06/15/2016
  - Re: [Coq-Club] Suggestions for Proof General?, Pierre Courtieu, 06/16/2016
    - Re: [Coq-Club] Suggestions for Proof General?, Jonathan Leivent, 06/16/2016
      - Re: [Coq-Club] Suggestions for Proof General?, Clément Pit--Claudel, 06/16/2016
      - Re: [Coq-Club] Suggestions for Proof General?, Pierre Courtieu, 06/16/2016
  - Re: [Coq-Club] Suggestions for Proof General?, Gabriel Scherer, 06/16/2016
    - Re: [Coq-Club] Suggestions for Proof General?, Clément Pit--Claudel, 06/16/2016
      - Re: [Coq-Club] Suggestions for Proof General?, James Wilcox, 06/16/2016
        
        Re: [Coq-Club] Suggestions for Proof General?, Nico, 06/17/2016
        
        Re: [Coq-Club] Suggestions for Proof General?, Alan Schmitt, 06/17/2016
        
        Re: [Coq-Club] Suggestions for Proof General?, Jason Gross, 06/17/2016
    - Re: [Coq-Club] Suggestions for Proof General?, Emilio Jesús Gallego Arias, 06/17/2016
      - Re: [Coq-Club] Suggestions for Proof General?, Clément Pit--Claudel, 06/17/2016