Que signifie V dans l'extension de fichier Coq?

Question

Est .v pour la vérification? validation? vamanos? Pourquoi ne pas utiliser une extension .coq?

Answer 1

Il y a deux langues en Coq:

1. Gallina, la langue à long terme, et
2. une langue d'administration appelée Vernacular,

en particulier:

Cette chapitre décrit Gallina, le langage de spécification de Coq. Il permet de développer des théories mathématiques et des preuves de spécifications de programmes. Les théories sont construites à partir d'axiomes, d'hypothèses, de paramètres, de lemmes, de théorèmes et de définitions de constantes, de fonctions, de prédicats et d'ensembles. La syntaxe des objets logiques impliqués dans les théories est décrite dans la section 1.2. Le langage des commandes, appelé The Vernacular est décrit dans la section 1.3.

Les extensions de fichiers correspondants sont:

1. .g pour les fichiers Gallina, qui result from .v files après avoir enlevé les preuves (voir aussi this message)
2. .v pour les fichiers vernaculaires.

Answer 2

Dans le reference manual, ils l'appellent un "fichier vernacular".