coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Safe to download and compile .v from evil source ?

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Safe to download and compile .v from evil source ?
Date: Sun, 2 Feb 2020 14:44:39 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:bXXvaRUKKAEha+Em+RG1CsT7UNbV8LGtZVwlr6E/grcLSJyIuqrYYxOAt8tkgFKBZ4jH8fUM07OQ7/m8HzBdqs/b7jhCKMUKC0Zez51O3kQJO42sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx8u42Pqv9JLNfg5GmCSyYa9oLBWxsA7dqtQajZFtJ6osxRbFuHRFduRZyW91O16engv36sOs8JJ+6ShdtO8t+sBaXanmY6g0SKFTASg7PWwy+MDlrwTIQxGV5nsbXGUWkx5IDBbA4RrnQJr/sTb0u/Rk1iWCMsL4Ub47WTK576d2UxDokzsINyQ48G7MlMN9ir9QrQ+7qBx+x47UZ5yVNOZ7c6jAc94WWXZNU8BMXCFHH4iybZYAD/AZMOhFsYf9qVsAoxiwCwaiC+zgyCNHiHDt0K0m0OksCx3K0BAuEt8MtnnfsdX7NL0VUeCw1KTF0SjMYOlT2Tzg9oXIchQhofCUXb1qdcre01QkGgTfgVqNs4PlOi+a2/8RvGiA9eVgVOavh3QiqwFwvjij3NkjhZTUho8MzF3P6CZ3wJ4tKNGlVkJ2YsSoHZVMuy2AKYd6WN0uT3x0tCoi1LEKpZ62cDIUxJg72hLTceGLfoyS7h/tSuqcJypzimh/d7KlnRmy9FCtyu3iWcmw11ZHti1FksTQtnAC0BzT686HSvRk8ke6xTaAzRzT5fteLU8ojqrUMZ8hwroqmpoWsETDAjX6l1vrg6+Lbkkk++6o5Pr7Yrj+u5OQKYx5hhvwP6gygMCzH/40PhYTU2SH4ei80afs/Uz9QLVElP02lazZvYjAKssGvKG5BhNa350/5BakFTim0dAYkWMCLFJEZBKLlZbmNEzTIPzgF/ewn0yskCt3x/DBJrDuHpLNLmHanLj9ebZ99lVTxREozdFf4pJUEqsOLOjyWk/3rtzYDwU2Pxa6w+b9W51B0dYVXnvKCauEOovTt0WJ76QhObqifogQ7R/xIv1tzP7qjGcwnVZVKaCl1J4cQHujF/ViZUCYfTzhjspXQjRChRY3UOG/0A7KajVUfXvnB/thtAF+M5qvCML4fq7ogLGF23zjTJpLem9BC1aDVGz0fpmNHfwXYSOWZMpgjnoJWaXzE9ZwhyHrjxfzzv9cFsSR/yQZsZz5090sur/Yjhgz8XpxDtjb3m2QHTgtwjE4AgQu1aU6mnRTj0+Z2PEl0fdDHN1XofZITkE3OYOOl+E=

It sounds like a fun project, actually. Maybe the most pragmatic mode is to check .v files for non-misleading correspondence with the final conclusions of .vo files (rather than building a pretty-printer that just starts from the .vo file and no presentation advice).

On 2/2/20 2:34 PM,
jonikelee AT gmail.com
wrote:

On Sun, 2 Feb 2020 09:51:46 -0500
Adam Chlipala
<adamc AT csail.mit.edu>
wrote:

The clear community recommendation would be to
check .vo files, not .v files. However, that mode requires
additional code-review tools that pretty-print crucial parts of .vo
files in sufficiently readable ways (definitely not involving Ltac,
plugins, etc., and in fact with no need to display proof terms, just
"final" theorem statements and their dependencies).

If the tools you requested above existed, I might be able to see that
this is the case! So, that request gets a +1 from me.

Re: [Coq-Club] Safe to download and compile .v from evil source ?, (continued)
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Emilio Jesús Gallego Arias, 02/02/2020