coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Domain-specific visual representations of structures for proofs

From: Jim Fehrle <jim.fehrle AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Domain-specific visual representations of structures for proofs
Date: Mon, 15 Nov 2021 12:34:33 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f42.google.com
Ironport-hdrordr: A9a23:Rs+tBK18OUACfxuI7NA/CQqjBMckLtp133Aq2lEZdPU7SKClfqyV8cjzqyWbtN95YhhJ8uxoU5PufZqzz/RI3bU=
Ironport-phdr: A9a23:PEp6MBHYqCwqxJGSwF9uhp1Gf8lMhN3EVzX9CrIZgr5DOp6u447ldBSGo6k31BmYBM6GtLptsKn/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uys55HfeQFFiCeybb5yLhi9sBncuNQRjYZ+MKg61wHHomFPe+RYxGNoIUyckhPh7cqu/5Bt7jpdtes5+8FPTav1caI4TadFDDs9KGA6+NfrtRjYQgSR4HYXT3gbnQBJAwjB6xH6Q4vxvy7nvedzxCWWIcv7Rq0vVD+886lkVgPniCYfNz447m7XjNBwjLlGqx6lvhBz3pLYbJ2QOPd4Y6jTf84VRXBZU8leWSxOAIOyYYUMAeQcI+hXs5LwqEESoRakHwSgGP/jxz1Oi3Tr3aM6yeMhEQTe0QIkHtIOtWnfotXrO6cSS+C1yLfHxijEYvNU2Df97ZLEch4/rvGMR7JwddTexFIgFwPAlFqQqIjlMymJ2eQKtmiW9uxtXv+ghGA7sQ9+uCSvxtsyhYnTgIIY0kzJ+CZnzYsxKtC1SUp2bNy4HJZOuS+XM5d6T98mTm10uSs3xLwLtIClcSQWzJkqwxzSZvOJfYWV7RzuSficLSt+iXl4e7y/nw6//Va8xuD4TMW501ZHojBYntTNt30BzRPe5taBR/Bg5EmuwyyP2BrW6uxcIUA7i67bK5k5z741jJUTsEDDEjb3mEXxkaOab0sk9+e25+j9bbXmoZicN4Bwig7gKKghhsu/AeEgPggPWWiU5/i82aX98UHlRLhGlP47n6nDvJzHJMkWp7S1DgBL3oo77hawFTam0NAWnXkdK1JFfQqKj4roO1HLOvz4A+mwg1S2kDdv2f/LJbLhApDXIXjClLftZ6py60lZyAYr19BQ+4pUCq0dIPL0QkL+qNvYDgYgPwOox+bnFc5y25gFWWOPB6+ZKLndvUWJ5uIpOemMZZUatCzzK/g/tLbSiioSnkZVVq2019NDY3ehW/9iPk+xYHz2g95HH31c7SQkS+m/qlyHGRBeZ2y2Uupo5DA+ToyrDZ3HS6iihbWA2GGwGZgANTMOMUyFDXq9L9bMYPwLci/HZ5Y5ylTsupCuToYg0VelswqoktKPz8LR8ywc8JPkjZ17u7eVmhY1+jh5Sc+a1jPVJ4mRtmwNTj4ymqt4pB4lomo=

One thought, by analogy: When I work on a large program, perhaps on a bug, I often wish that my dev tools would let me identify what files, functions and data structures are relevant to what I'm doing and highlight those items in source code buffers and info panels listing those items. Also (if my dev tools supported them) in more graphic forms such a representation of a call graph. If a proof-visualization tool shows a complex overall graphic, it would likely be helpful to identify the relevant parts for various subparts of the proof.

[Coq-Club] Domain-specific visual representations of structures for proofs, Talia Ringer, 11/14/2021
- Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Timothy Carstens, 11/14/2021
- Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Eduardo Ochs, 11/14/2021
- Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Ralf Jung, 11/14/2021
  - Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Cyrus Omar, 11/14/2021
    - Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Lawrence Dunn, 11/15/2021
- Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Clément Pit-Claudel, 11/15/2021
  - Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Jim Fehrle, 11/15/2021