Sergei Meshveliani (Jun 25 2021 at 19:53): Sergei Meshveliani (Jun 25 2021 at 19:53):I have a newbie question.
I am trying to understand of what is is written in the "Mathematical Components" book.
Just start to read it.
It has many fragments like this:
"In Coq, the user can also associate a name with the operation (fun n => n + 1) , in the following manner:
Definition f := fun n => n + 1.
"
The impression is that Coq is a programming language, and that the above line is a program in this language.
Is it?
Alternatively, is Coq a system + library of functions written in Gallina ?
Is the above line a program written in Gallina?
Probably, these fragments are written in the language for the Coq interactive shell
(?)
Alexander Gryzlov (Jun 25 2021 at 20:03):Technically it's a mix of Vernacular (the Definition f := and . parts) and Gallina (the fun n => n + 1). Plain Coq usually also throws Ltac (tactic metalanguage) in the mix, and there are yet another additions in different frameworks (e.g. mathcomp both adds some constructs to Gallina and defines its own tactic DSL).
Andrey Klaus (Jun 26 2021 at 11:36):Alexander's answer is good and correct (as far as I know). And when one would like to speak about specific part of system, one needs use "Galina" as a programming language "Vernacular" for special keywords (or kind of), etc. But usually, saying "Coq is a programming language" is ok and as far as I know the terms "Galina" and "Coq" and even "Vernacular" are interchangable according to some authors. So, I think your impression is right.
Théo Zimmermann (Jun 26 2021 at 13:10):Gallina is the programming language fragment of Coq. Therefore, and contrary to popular belief, the Definition f := part is also Gallina. Vernacular was the name originally given to the complete set of commands, so it includes both Gallina, Ltac and any other stuff you can put in a .v (for vernacular) file. I personally prefer to say "the Coq language" than "the Vernacular language". It's clearer what is meant for everyone.
Pierre-Marie Pédrot (Jun 26 2021 at 13:18):I've always found the insistence on separating Gallina and the vernacular very weird. It looks like concerns from the 80's that survived in the manual because nobody ever understood them.
Pierre-Marie Pédrot (Jun 26 2021 at 13:19):In no other language one separates the name of the language for the code proper, and the one for all the corresponding pragmas and whatnot.
Théo Zimmermann (Jun 26 2021 at 14:47):Note that at that point, it hasn't really survived in the manual anymore.
Enrico Tassi (Jun 26 2021 at 15:59):Well, looking at the code constr is gallina, vernac_expr is, well, the vernacular. Even for a final user there is a difference between what is a term, eg something you can pass to Check <here> and what is a toplevel statement, eg Check itself. Most non-functional languages out there distinguish between "expressions" and "statements", it is not that weird after all to have two syntactic categories, especially if they don't nest (you can't write Check in the middle of <here>)
Paolo Giarrusso (Jun 27 2021 at 01:23):If the distinction is between the syntactic categories of "expressions" and "toplevel statements", those seem perfectly good words.
Paolo Giarrusso (Jun 27 2021 at 01:29):From my perspective, having new words for existing concepts is a net negative. Having new words whose definition is not clear to experts (as witnessed above) seems even worse.
Enrico Tassi (Jun 27 2021 at 06:37):I don't understand your last remark.I was trying to pick meaningful, standard, names for gallina and vernacular, which are the ones used today but not clear even to the Devs. There is an ongoing work in improving the user manual, maybe using "toplelel statements (historically vernacular)" can clarify. My 2C
Ignat Insarov (Jun 27 2021 at 08:50):So, Gallina is the language of expressions and Vernacular is the language of statements. Right?
Enrico Tassi (Jun 27 2021 at 11:03):This is my understanding of it, at least ;-)
Ignat Insarov (Jun 27 2021 at 11:14):Then I think this answers the question of terminology. There are expressions, there are statements, and there are the corresponding languages.
Paolo Giarrusso (Jun 27 2021 at 16:48):@Enrico Tassi Sorry for the ambiguity. I do like terms and statements, and we should IMHO mark “Gallina” and “Vernacular” as historical :-) if they correspond to terms and statements like you say. And if they meant something else (I hear you but no clue myself), maybe we should retire them anyway as hopelessly confusing :-).
Ignat Insarov (Jun 27 2021 at 17:02):No no wait wait wait a sec. We found out that Gallina and Vernacular are _languages_ of expressions and statements, respectively. This is not the same as expressions and statements.
Ignat Insarov (Jun 27 2021 at 17:08):For example, saying _«a vernacular expression»_ would be wrong and saying _«a gallina expression»_ would be redundant, but saying _«I can handle Gallina pretty well, since it is not much different from other functional languages, but I find Vernacular difficult, since there are so many haphazardly made extensions to that language»_ is fine.
Christian Doczkal (Jun 27 2021 at 17:29):Wonderful, the Google dictionary explains vernacular as "the language or dialect spoken by the ordinary people in a particular country or region" and lists "formal language" as the opposite. As to the above sentence, My understanding is that "vernacular" is relative to another language. So I would instead say: "but I find the Coq vernacular difficult, ..." In a sense, it's the specific dialect of Gallina (higher-order type theory) understood by Coq. My 2ct :smile:
Paolo Giarrusso (Jun 27 2021 at 17:40):@Ignat Insarov I wasn't disagreeing with that definition, mostly suggesting that people stop uttering "Gallina" and "Vernacular" since that's bound to cause confusion.
Christian Doczkal (Jun 27 2021 at 17:42):I'm all in favor of talking about the "term language" and the "command and tactic language/syntax"
Paolo Giarrusso (Jun 27 2021 at 17:43):@Ignat Insarov However, now that you show examples, I don’t think I like "languages". Enrico had said “syntactic categories”, aka nonterminals. And just like other functional languages, the Coq language has both :-).
Théo Zimmermann (Jun 28 2021 at 08:19):Enrico Tassi said:
This is my understanding of it, at least ;-)
But I'm quite sure that your understanding is incorrect, in fact. So this reinforces the point of @Paolo Giarrusso.
Théo Zimmermann (Jun 28 2021 at 08:20):I've already taken out most uses of the two words from the reference manual, but historically, the Gallina language has been designating the specification / programming language of Coq, i.e. not just expressions but also the top-level statements.
Christian Doczkal (Jun 28 2021 at 10:47):Théo Zimmermann said:
I've already taken out most uses of the two words from the reference manual, but historically, the Gallina language has been designating the specification / programming language of Coq, i.e. not just expressions but also the top-level statements.
So what's the (historical) vernacular then, if Gallina includes the top-level statements as well?
Enrico Tassi (Jun 28 2021 at 12:47):In particular, I'm pretty sure that what I propose makes some sense, both looki ng at the codebase and at the syntax. It may not be exactly what the manual says today, but it is for sure something we can explain to a CS oriented audience, if we core Devs agree with my previous sentence. @Théo Zimmermann could you fork this stream, it is getting a bit off topic? Also CC @Jim Fehrle
Théo Zimmermann (Jun 28 2021 at 12:59):I've changed the title to better reflect the actual content of the discussion. But technically, it was the same topic from the beginning.
Théo Zimmermann (Jun 28 2021 at 13:01):@Christian Doczkal quoting my own initial answer to this topic:
Théo Zimmermann said:
Gallina is the programming language fragment of Coq. Therefore, and contrary to popular belief, the
Definition f :=part is also Gallina. Vernacular was the name originally given to the complete set of commands, so it includes both Gallina, Ltac and any other stuff you can put in a.v(for vernacular) file. I personally prefer to say "the Coq language" than "the Vernacular language". It's clearer what is meant for everyone.
I'm indeed not basing my claims on the code but on my historical understanding and what the manual used to say. Obviously, not on what it says today since as I've said before, these terms are virtually not used anymore.
Théo Zimmermann (Jun 28 2021 at 13:02):And @Enrico Tassi, if there is a proposal for a revision of the refman in your comment, then please clarify because I don't get what is problematic with the current content.
Enrico Tassi (Jun 28 2021 at 13:20):Well, if users are still asking about Gallina and Vernacular they must have read it somewhere
Enrico Tassi (Jun 28 2021 at 13:21):If they are really gone from the manual, where are they used?
Guillaume Melquiond (Jun 28 2021 at 13:23):For the record, my interpretation was the same as Enrico. Definition := is vernacular, and so is Eval cbv in. The Gallina part was only to the right of these commands.
Gaëtan Gilbert (Jun 28 2021 at 13:26):Gallina is not gone from the refman, it's mentione in ring and in the ssr chapter
Gaëtan Gilbert (Jun 28 2021 at 13:26):PS I think there are 2 meanings of gallina, as "terms" and as "whatever coqdoc --gallina produces"
Jim Fehrle (Jun 28 2021 at 18:17):Enrico Tassi said:
Well, if users are still asking about Gallina and Vernacular they must have read it somewhere
The introduction to Mathematical Components mentions Gallina and SSReflect as languages. 11 uses of "Gallina" in the document and 2 uses of "vernacular". The Coq doc uses "Gallina" in 25 places and "vernacular" in only 1 place (or 14 if you include changes.rst and history.rst). I agree these are not very useful terms; I've found the most useful distinctions are between "terms", "commands" and "tactics". I don't use the term "statements", which IIUC would correspond to "commands". The doc has indexes for commands and tactics.
I don't like referring to Gallina and SSReflect as separate languages. I think of SSReflect as feature of Coq that has certain grammar elements. They are subparts of the grammar Coq accepts and are used together.
Well, looking at the code constr is gallina, vernac_expr is, well, the vernacular.
Right idea but not quite. "term" in both the .mlg source files and in the doc corresponds to gallina. ("constr" in the mlg corresponds to "one_term" in the doc.) "vernac_expr" doesn't exist in the mlgs, the mlgs use "command" for most but not all commands.
Enrico Tassi (Jun 28 2021 at 20:45):I was talking about the name of the data types. I agree the grammar entries are the ones you mention, and their names are well chosen. Gallina is the language of terms while vernacular is the language of commands. Tactics are yet another one, tha like commands, take terms arguments. I'm sorry I did not find the time to help rework the SSR chapter.
Jim Fehrle (Jun 29 2021 at 06:13):I'd like to finish updating the syntax in the tactics chapter before getting back to the SSR chapter. In a couple months, if/when you or some other expert has time.
Last updated: Sep 26 2023 at 12:02 UTC