Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] survey on Coq interfaces

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] survey on Coq interfaces


chronological Thread 
  • From: Mihai ANDRIES <mihai AT andries.eu>
  • To: Aaron Stump <aaron.stump AT gmail.com>
  • Cc: coq-club AT inria.fr, Juan Pablo Hourcade <juanpablo-hourcade AT uiowa.edu>, Benjamin Berman <bnjmnbrmn AT gmail.com>
  • Subject: Re: [Coq-Club] survey on Coq interfaces
  • Date: Sun, 4 Dec 2011 19:23:37 +0100

Probably one of the main problems in CoqIDE is the naming of the intermediate variables.
Although i always name my variables to keep the code easier to reuse, i have no control (or at least i don't know how to control) the naming of the intermediate variables, which result after applying a specific tactic.

It seems that the names of variables' type influence the naming algorithm used in CoqIDE.
For instance, i wanted to change the name of a type from EvaluationArith to aeval, i made all the necessary changes in the code, and proof's execution failed because the names of intermediate variables have changed. My "apply det_ArithEval with (E:=E) (a:=e)." is no longer valid.

Mihai

On 2 December 2011 15:26, Aaron Stump <aaron.stump AT gmail.com> wrote:
Dear Coq community members,

We are writing to solicit your thoughts and experiences, via a short (1 page)
online survey, on user interfaces for Coq. We would like to use this input to
help guide our work on a new project which will apply contemporary HCI research
methods and ideas to the user interfaces of proof assistants, Coq in particular.
Two of us (Hourcade and Berman)are HCI researchers, and the other (Stump)
works on type theory. We are hoping to be able bridge the significant gap between
these communities. Your ideas on features for a new interface for Coq will
help a lot!  Responses by Friday, Dec. 9th, would be appreciated.

The survey can be found here:

https://uiowa.qualtrics.com/SE/?SID=SV_1Ukjx44UQKS57lW
 
Thanks in advance,
Aaron, Juan Pablo, and Ben

Aaron Stump
Juan Pablo Hourcade
Ben Berman
Computer Science
The University of Iowa 




Archive powered by MhonArc 2.6.16.

Top of Page