Jiahong Lee (Jul 17 2022 at 10:59): Jiahong Lee (Jul 17 2022 at 10:59):Hi, I'm confused about the differences between Coq the theorem prover and Gallina the programming language.
Questions:
Previous related discussion(s):
Karl Palmskog (Jul 17 2022 at 11:30):The top-level input language of Coq is called the Vernacular. Gallina is a strict subset of the Vernacular that is used to input for example, functions and inductive types.
Karl Palmskog (Jul 17 2022 at 11:31):At "compilation" time, (some of) the Vernacular is elaborated into the abstract syntax of the foundational calculus of Coq, sometimes called pCUIC (parameterized polymorphic ... Calculus of Inductive Constructions)
Gaëtan Gilbert (Jul 17 2022 at 11:31):I never remember what Gallina is, because it doesn't matter.
Gaëtan Gilbert (Jul 17 2022 at 11:32):pcuic is for polymorphic as in universe polymorphic AFAIK
Karl Palmskog (Jul 17 2022 at 11:33):I think it's more accurate to say: Gallina doesn't matter to the foundations of Coq and its kernel
Gaëtan Gilbert (Jul 17 2022 at 11:33):although https://arxiv.org/abs/1710.03912 says it's predicative
Gaëtan Gilbert (Jul 17 2022 at 11:33):Karl Palmskog said:
I think it's more accurate to say: Gallina doesn't matter to the foundations of Coq and its kernel
I mean the distinction between gallina and whatever doesn't matter
Karl Palmskog (Jul 17 2022 at 11:34):anyway, I think this is a good overview of the relation between the top-level language and the kernel/checker: http://math.andrej.com/asset/data/the-dawn-of-formalized-mathematics.pdf#page=23
Karl Palmskog (Jul 17 2022 at 11:38):someone could come up with a new specfication language [covering most of Gallina does] and add it as a plugin, no? Or compile a subset of Vernacular into Lean
Karl Palmskog (Jul 17 2022 at 11:39):so the distinction between "input language" and other parts of a proof assistant can be important
Gaëtan Gilbert (Jul 17 2022 at 11:40):the distinction between some part of the input language and some other part is not really important
Karl Palmskog (Jul 17 2022 at 11:44):due to the way tactic languages are integrated as plugins, it's quite easy to identify in the abstract syntax where tactics occur, and just ignore in analysis tools where you don't care about tactics
Karl Palmskog (Jul 17 2022 at 11:46):and the tactic code and Gallina code is typically written with quite different goals in mind, e.g., on maintainability
Karl Palmskog (Jul 17 2022 at 11:47):but sure, from a Coq dev viewpoint, I can see it's not a big deal if some big syntax tree has Ltac in it or not
Enrico Tassi (Jul 17 2022 at 11:49):Today Gallina is the core calculus, while the rest is vernacular. Eg inductives are in gallina, type classes are not, nor notations or coercions.
IIRC Gallina was intended to be the non kernel stuff, which was called the calculus of inductive constructions, but the manual was so badly written that everybody understood the converse and it did stick. At least I seem to recall a chat with a core dev of the generation prior to mine along these lines :-)
Gaëtan Gilbert (Jul 17 2022 at 11:55):Today Gallina is the core calculus, while the rest is vernacular. Eg inductives are in gallina, type classes are not, nor notations or coercions.
Isn't it the term language? ie match foo with bla => bli end is gallina, Definition foo := 0. isn't
this whole discussion is why I think we should stop using the name Gallina, it just confuses beginners and provides no value to experts
Enrico Tassi (Jul 17 2022 at 12:06):Yes, it is constr. But I like a name for it which is not pcuic which is impossible to remember (I had to copy it from above, my guess was pucic...)
Enrico Tassi (Jul 17 2022 at 12:08):Also, pcuic is doomed to obsolete. I see no S for sprop, and when we will have sort polymorphism ...
Karl Palmskog (Jul 17 2022 at 12:09):do we really want to conflate the input language with the calculus of elaborated terms?
Karl Palmskog (Jul 17 2022 at 12:10):I thought the distinction of input vs. elaborated stuff was useful when learning
Karl Palmskog (Jul 17 2022 at 12:11):fine by me if you call them something like "Coq programming language" and "Coq calculus" though
Jiahong Lee (Jul 17 2022 at 13:49):Didn't expect such a discussion. To add more context: I'm trying to understand Coq from a programmer's point of view (my background), and double checking whether it's correct to say/blog something like:
"Coq is a proof assistant. To master Coq, you're going to master Gallina the programming language, which is similar to how you write programs in mainstream functional PL, e.g. Scheme, OCaml, and Haskell. Also, you can write proofs in Gallina to verify properties of your programs!"
Before this, I thought Gallina is the entire UI part to Coq kernel, such that everything in a .v file can be classified as written in Gallina. From the discussion above, it seems like the reality is more nuance than that.
Jiahong Lee (Jul 17 2022 at 13:51):I heard about Gallina from:
In the first part of the course, we'll use Coq's (French for 'rooster') functional programming language Gallina (Spanish for 'hen') to write programs. In the second part of the course, we'll use Coq's unnamed tactic language to learn to write proofs.
Source: https://cs.pomona.edu/classes/cs54/book/Intro.html
The first half of this chapter introduces the most essential elements of Coq's native functional programming language, called Gallina. The second half introduces some basic tactics that can be used to prove properties of Gallina programs.
Source: https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html (The goto book for beginners)
(And maybe some other resources from the Internet.)
Throughout the book, it seems that I can do everything in Gallina. Then I wonder why is Coq the proof assistant not called "Gallina the proof assistant". Or the other way round, why is Gallina not called "Coq the programming language". From its name, seems like Gallina is one part of "Coq". So, what are the other components of Coq?
Jiahong Lee (Jul 17 2022 at 13:52):Karl Palmskog said:
anyway, I think this is a good overview of the relation between the top-level language and the kernel/checker: http://math.andrej.com/asset/data/the-dawn-of-formalized-mathematics.pdf#page=23
From page 23, seems like Coq has similar architecture as GNU/Linux operating system. So, the Coq kernel is similar to Linux kernel, the core formalism Gallina defines the APIs to the kernel (like Linux APIs), then vernacular is like the application space built on top of Gallina?
Jiahong Lee (Jul 17 2022 at 13:53):Gaëtan Gilbert said:
the distinction between some part of the input language and some other part is not really important
The reason I care about whether it's called "Gallina" is that it helps putting things into scope. If I can clearly define "Gallina the programming language", I can make sure that I have fully covered all aspects of it. Or that I can then decide to cover "Gallina the programming language" by parts. In my mind, I thought "Gallina" is like the C programming language, and the Coq kernel/type checker as something like the assembly language...
How would you introduce Coq to a beginner if not introduce it by parts or in layers?
Karl Palmskog (Jul 17 2022 at 13:59):a proof assistant like Coq is different from a regular statically typed programming language not least in that type checking and compilation is (pretty much) the same thing. So in contrast to, say, Java, where you don't have to know the JVM to understand a Java program, you essentially have to know both the surface programming language (Vernacular) and the foundations of Coq (pCUIC) in the end.
Karl Palmskog (Jul 17 2022 at 14:02):with that said, you can get quite a long way in simply using regular functional programming language theory and idioms, e.g., you can use a slogan like: Coq is about (inductive) datatypes and (total) functions, like a pure subset of a language like SML or OCaml
Karl Palmskog (Jul 17 2022 at 14:08):Jiahong Lee said:
From page 23, seems like Coq has similar architecture as GNU/Linux operating system. So, the Coq kernel is similar to Linux kernel, the core formalism Gallina defines the APIs to the kernel (like Linux APIs), then vernacular is like the application space built on top of Gallina?
It's possible to view the Coq checker in this way (as a monolithic OS kernel), but in practice all the layers above it are quite tightly integrated, so there is no ecosystem of "Coq distributions" that build only on top of the kernel. Instead, people build on top of Coq's whole stack, including Gallina.
Karl Palmskog (Jul 17 2022 at 14:09):I think the trend is definitely towards people using parts of Coq as a substrate to build other tools, though, and they may throw out things they don't want, like the tactic language or (the mechanism for defining) inductive types
Karl Palmskog (Jul 17 2022 at 14:27):Fig 2 here has an illustration of some of Coq's layers, and how the representations change going from Gallina and downwards: https://arxiv.org/pdf/2004.07761.pdf#page=5
Paolo Giarrusso (Jul 17 2022 at 17:29):Last time the discussion came up on this Zulip, the result was that: "Gallina" does not appear in the manual any more, nobody is sure what Gallina is exactly, including Coq core developers, and there are more standard and precise words for the relevant distinctions. For instance, many languages distinguish terms and top-level definitions.
Paolo Giarrusso (Jul 17 2022 at 17:31):(I see that Gaëtan made similar points above, minus "we've been over this")
Karl Palmskog (Jul 17 2022 at 17:51):the definition that Enrico gave, "Gallina is constr [in the AST]" is quite precise
Gaëtan Gilbert (Jul 17 2022 at 17:51):there's a few mentions in the manual
./doc/sphinx/addendum/ring.rst:67:ring expression in the Gallina language. For example, consider this expression
./doc/sphinx/addendum/ring.rst:439:in Gallina, Coq's language of terms, rather than |Ltac| or OCaml. From the
./doc/sphinx/using/tools/coqdoc.rst:409: :-g, --gallina: Do not print proofs.
./doc/sphinx/language/coq-library.rst:1087:The primitive operators are specified with respect to their Gallina
./doc/sphinx/changes.rst:80: represented by a regular coercion (a Gallina function)
./doc/sphinx/changes.rst:2192: Gallina-based standard library. The package Coq now depends on both
./doc/sphinx/changes.rst:4986: ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints
./doc/sphinx/changes.rst:6005:- Tools: removed the ``gallina`` utility and the homebrewed ``Emacs`` mode.
./doc/sphinx/changes.rst:6193:- Removed the `gallina` utility (extracts specification from Coq vernacular files).
./doc/sphinx/changes.rst:6848:Gallina
./doc/sphinx/changes.rst:10742:Gallina
./doc/sphinx/language/extensions/arguments-command.rst:35: control over the elaboration process (i.e. the translation of Gallina language
./doc/sphinx/README.rst:332: Use this for Gallina and Ltac snippets::
./doc/sphinx/proofs/writing-proofs/proof-mode.rst:979: Displays a template of the Gallina :token:`match<term_match>`
./doc/sphinx/proof-engine/ssreflect-proof-language.rst:179:Gallina extensions
./doc/sphinx/proof-engine/ssreflect-proof-language.rst:183:subset of Gallina, Coq’s logical specification language. This subset
./doc/sphinx/proof-engine/ssreflect-proof-language.rst:187:to Gallina, for pattern assignment, pattern testing, and polymorphism;
./doc/sphinx/proof-engine/ssreflect-proof-language.rst:188:these mitigate minor but annoying discrepancies between Gallina and
./doc/sphinx/proof-engine/ssreflect-proof-language.rst:240:Gallina expression :n:`match @term with @pattern => @term end`.
./doc/sphinx/proof-engine/ssreflect-proof-language.rst:297:setting of Gallina, which lacks a ``Match_Failure`` exception.
./doc/sphinx/proof-engine/ssreflect-proof-language.rst:300:for the primitive Gallina expression
./doc/sphinx/proof-engine/ssreflect-proof-language.rst:358:Unlike ML, polymorphism in core Gallina is explicit: the type
./doc/sphinx/proof-engine/ssreflect-proof-language.rst:1019:goal because the Gallina terms that control their action (e.g., the
This here explains constr vs. Vernac at least: https://github.com/ejgallego/coq-serapi/blob/v8.16/FAQ.md#how-many-asts-does-coq-have
Paolo Giarrusso (Jul 17 2022 at 18:50):Correction: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Gallina.20and.20Vernacular.20definitions/near/244114411 has @Théo Zimmermann said he took out most uses of Gallina, I misremembered that point.
Paolo Giarrusso (Jul 17 2022 at 18:53):I've also used Gallina for terms, but Théo pointed out that wasn't the original intention, and that's why back then we concluded the term was unlikely to become unambiguous.
Paolo Giarrusso (Jul 17 2022 at 18:55):Whether Gallina is before or after elaboration did not come up back then, and I'm not sure which is supposed to be the answer.
Paolo Giarrusso (Jul 17 2022 at 19:04):@Karl Palmskog can I ask some clarifications?
Coq's core parsing AST is called vernac_expr. [...] The top-level parsing type for terms is constr_expr.
Let me rephrase to double-check: parsing outputs an AST of type vernac_expr; in particular, parsing “terms” (as defined by a specific non-terminal in the grammar) outputs ASTs of type constr_expr. And those appear as nodes in vernac_expr ASTs. How much of that is correct?
Karl Palmskog (Jul 17 2022 at 19:05):I think that's correct, but others who have actually worked more at OCaml level will know better
Karl Palmskog (Jul 17 2022 at 19:06):I personally think of vernac_expr as a kind of container of all the weird stuff that shows up after parsing, like Ltac mixed with terms, and terms mixed with Ltac
Paolo Giarrusso (Jul 17 2022 at 19:08):sounds like a Coq document _might_ have type vernac_expr, but I am not confident I’m parsing that link.
Karl Palmskog (Jul 17 2022 at 19:09):I think it's better to think of it [the Coq document] as a list of vernac_expr
Karl Palmskog (Jul 17 2022 at 19:10):this reflects that we typically communicate with Coq using sentences, and sentences are the granularity of additions, retractions, etc., and vernac_expr will be result of parsing something that ends in .
Karl Palmskog (Jul 17 2022 at 19:12):I'm sure there are quite a few special cases, but this is my mental model
Enrico Tassi (Jul 17 2022 at 20:55):Indeed, there is a control box (for fail, time,....), but a document is morally a list of vernac expr.
Enrico Tassi (Jul 17 2022 at 20:58):Anyway, I believe having a name for the term language once fully elaborated, ie as understood by the kernel, is important. The one used in the code, constr, is a bit cryptic, not to talk about pcuic. Gallina is OK to me.
Karl Palmskog (Jul 17 2022 at 21:12):seemingly, what people perceive that they actually meet, fall in love with, or hate with a passion, is the surface syntax. I suspect that many people think a language is its surface syntax. I don't mind calling the elaborated terms Gallina, but do we then just call the whole of the surface syntax "Vernacular" and nothing else?
Jiahong Lee (Jul 18 2022 at 02:56):To chime in a little bit more to discuss about "Gallina" from a beginner's perspective, the current pedagogical approach appeals to people with programming background:
Later, it is shown that Gallina and tactics are connected by proof objects. Thus revealing to learners that they are two faces of the same thing under the hood.
From the discussion above, all of them (Gallina + tactics + Ltac) should be called "Vernacular the language", hence the .v file. So if the name "Gallina" is confusing, what would you replace it with? Or how do you think this pedagogical approach can be improved?
Pierre Castéran (Jul 18 2022 at 05:11):The term "gallina" was introduced In "old" versions of the reference manual.
https://coq.github.io/doc/v8.9/refman/language/gallina-specification-language.html
I didn't find this paragraph in the current version. Note that the terms "gallina" still occurs in https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#gallina-extensions and as an option of coqdoc.
Just a remark about "surface syntax". With Coq 8.0, the surface syntax changed dramatically, but I think it is
(almost) the same gallina as in 7.xx.
Gaëtan Gilbert (Jul 18 2022 at 05:14):the syntax of dependent product in V7 was without the forall keyword, see eg https://github.com/coq/coq/commit/9a6e3fe764dc2543dfa94de20fe5eec42d6be705#diff-e33da29506e770f8309cc0e4140c077bfb7a438b4950d86a423e0bfbfd6fa54fL95-R95
Gaëtan Gilbert (Jul 18 2022 at 05:16):also match was written Cases x of branches end, see eg Peano.v in that commit
Pierre Castéran (Jul 18 2022 at 06:33):IMO, V7's syntax surface was closer to lambda-calculus notations, and V8's to the "usual" mathematical statements (hence more readable by many users). Abstractly, they are very close, which allowed @Hugo Herbelin to write a translator which successfully adapted to V8 the standard library, many contribs, and the Coq'Art examples.
Théo Zimmermann (Jul 18 2022 at 08:46):Until a recent restructuring of the refman, it indeed had a "Gallina specification language" chapter and an "Extensions of Gallina" chapter. But the first one already contained things that go beyond the core language and the second didn't clarify whether these extensions should be considered part of the Gallina language. The new version has instead a first part called "Specification language" divided into a first chapter called "Core language", which is assimilated to the "Calculus of Inductive Constructions" which is what the kernel understands and a second part called "Language extensions" which are the things that get elaborated.
Théo Zimmermann (Jul 18 2022 at 08:47):IMHO since core devs themselves cannot be trusted on what is the definition of Gallina (since they cannot agree on a single definition), this should be left to the writers of documentation (such as tutorials) to decide whether this term and the Vernacular term are important and how to use them.
Théo Zimmermann (Jul 18 2022 at 08:49):And FTR, my opinion on using pCuIC instead of CIC to describe the language that the kernel understands is that this should be limited to theory papers, but when talking about the Coq implementation, we should keep using CIC because it is bound to continue to evolve and we cannot change the name of the core language every time.
Enrico Tassi (Jul 18 2022 at 11:09):I don't think leaving the term undefined is ok for the community, it only increase confusion. We should meet, agree, and write it down.
Karl Palmskog (Jul 18 2022 at 11:16):the distinction between surface-level Vernacular (that also includes commands without any effect) and the surface-level specification language is very useful. But "Vernacular" without qualification can be ambiguous. Ideally, I'd like canonical and precise terminology for:
Théo Zimmermann (Jul 18 2022 at 11:40):Enrico Tassi said:
I don't think leaving the term undefined is ok for the community, it only increase confusion. We should meet, agree, and write it down.
Fine, but the decision should not be left to core devs. If a discussion is to be had, it should include the main stakeholders, i.e. the documentation writers.
Théo Zimmermann (Jul 18 2022 at 11:41):Or it should be a CEP that allows (async) discussion about this with the community.
Pierre-Marie Pédrot (Jul 18 2022 at 11:50):As a core developer, I'm always confused about the Gallina vs whatever discussion, so I can't even fathom how it must feel for beginners.
Karl Palmskog (Jul 18 2022 at 11:52):given that we now recommend the Platform to install Coq, arguably a new definition of Gallina and related concepts needs to take into account how commands like Equations should be considered
Guillaume Melquiond (Jul 18 2022 at 12:10):As far as I am concerned, Gallina is the name of the surface syntax for the enriched lambda-calculus used by Coq. Equations does not have much of an impact on it, i.e., what is on the right of the innermost := is Gallina. Having a proper name to characterize this grammar of terms is a good thing and I am a bit sad to see it disappear.
Théo Zimmermann (Jul 18 2022 at 12:43):But this is not what it was called in the refman! Gallina was used in the refman to designate the left side of := as well.
Théo Zimmermann (Jul 18 2022 at 12:45):In other words, the name Gallina represents a different concept for most core devs vs the rest of the world (including the refman before I became one of its maintainers).
Théo Zimmermann (Jul 18 2022 at 12:45):And I used to be in the "most core devs" category, because I too thought that Gallina was the language of terms.
Gaëtan Gilbert (Jul 18 2022 at 12:46):also note that we still have coqdoc --gallina
Karl Palmskog (Jul 18 2022 at 12:47):I always thought of Gallina like Guillaume defines it. But I stared at the abstract OCaml syntax for a long time in SerAPI, etc. To get people to understand what part of syntax is what, we probably need more figures like this one I linked before: https://arxiv.org/pdf/2004.07761.pdf#page=5
Karl Palmskog (Jul 18 2022 at 12:48):(even that one does not highlight exactly the Gallina parts)
Guillaume Melquiond (Jul 18 2022 at 12:48):Théo Zimmermann said:
But this is not what it was called in the refman! Gallina was used in the refman to designate the left side of
:=as well.
We seem to be talking about something different. I am talking about the left-hand side of := in Equations, which as far as I know has never been part of the reference manual.
Karl Palmskog (Jul 18 2022 at 12:49):I think what Théo is saying is that this applies to Definition and so on, the refman considered this to be Gallina:
Definition my_def :=
in reality, if we had Definition my_def := 1., only the 1 should be classified as Gallina (if we accept the extended-lambda-calc def)
Guillaume Melquiond (Jul 18 2022 at 12:52):So, who are those developers who think that Gallina is something else than the language of terms? Because unless I glanced too fast over this thread, it seems there is a consensus, at least here.
Karl Palmskog (Jul 18 2022 at 12:52):I think there is a part of core dev that considers defining Gallina irrelevant/unnecessary, regardless of how it is defined
Karl Palmskog (Jul 18 2022 at 12:54):this is how I read Gaëtan's comments above (and I think PMP said something similar earlier)
Enrico Tassi (Jul 18 2022 at 13:00):Note that, even for users, the language of terms they input in not exactly the one the kernel understands. I mean match x with S (S y)) => .. is part of the language we all use, but is elaborate to a more basic one. To me this is still Gallina (and is not constr).
Guillaume Melquiond (Jul 18 2022 at 13:05):I agree. That is why I talked about the surface language. By the way, I just looked at Equations' documentation and it uses convoluted expressions like "Coq's regular term parser" and "Coq's term syntax". This strengthens my opinion that we should have a proper name for those.
Théo Zimmermann (Jul 18 2022 at 13:10):I am one (possibly the only one) core dev that opposes to using the term Gallina to designate something different from what it was originally meant to be (and documented as such in the refman) even if I'm also the one that took most of its uses out of the refman (in part because it was ambiguous since most of the core devs had another definition). But the tutorials that were quoted above are more consistent with the original Gallina definition (i.e., the programming language subset of Coq).
Théo Zimmermann (Jul 18 2022 at 13:11):What I said before was just that I initially thought it meant what most core devs still seem to think it means (according to those who have expressed themselves above).
Karl Palmskog (Jul 18 2022 at 13:18):Coq'Art said in 2004:
The language that is used to describe terms, types,[non-tactic] proofs, and programs is called Gallina
And claimed this was precisely defined in the manual at that point.
This was at least my source of slogans for Gallina.
Pierre Castéran (Jul 18 2022 at 13:27):Yes, In V8.9 this information was in https://coq.github.io/doc/v8.9/refman/language/gallina-specification-language.html . The cited paragraph said also:
" The language of commands, called The Vernacular is described in Section The Vernacular. "
Another definition of Gallina could be "the language output by coqdoc --gallina"
Théo Zimmermann (Jul 18 2022 at 13:32):The weirdest thing (if we replace this quote in context) was that Vernacular was considered to be a subset of Gallina, which is definitely far off from what everyone today actually considers to be Vernacular.
Théo Zimmermann (Jul 18 2022 at 13:33):(And it was already self-contradictory, since beyond this section "The Vernacular" inside the "Gallina" chapter, there was also another chapter called "Vernacular commands").
Paolo Giarrusso (Jul 18 2022 at 13:50):I agree it'd be nice if we could codify how to use Gallina going forward — if a useful consensus between textbooks can be found. I guess the "extended lambda calculus" is clearly in, and Ltac is clearly out. What about top-level definitions and inductives?
Paolo Giarrusso (Jul 18 2022 at 13:55):we can probably also exclude other vernaculars — certainly Set/Unset, maybe Require, Import, modules, ...
Théo Zimmermann (Jul 18 2022 at 13:57):Modules: not clear if you consider Gallina as being "the (purely functional) programming language subset of Coq".
Paolo Giarrusso (Jul 18 2022 at 13:59):Let's set modules aside for a moment, since they were added later after the corruption...
Paolo Giarrusso (Jul 18 2022 at 13:59):Coq 8.9's manual also has > This grammar describes The Vernacular which is the language of commands of Gallina.
Paolo Giarrusso (Jul 18 2022 at 14:00):despite the contradiction that @Théo Zimmermann observes, this _is_ interesting.
Paolo Giarrusso (Jul 18 2022 at 14:00):_if_ we distinguish "Gallina vernacular" and "other vernacular", everything else makes _more_ sense.
Paolo Giarrusso (Jul 18 2022 at 14:02):"Gallina vernacular" (https://coq.github.io/doc/v8.9/refman/language/gallina-specification-language.html#the-vernacular) has top-level definitions and inductives — which could belong in a "grown-up" lambda calculus
Paolo Giarrusso (Jul 18 2022 at 14:02):https://coq.github.io/doc/v8.9/refman/proof-engine/vernacular-commands.html has everything else, which it makes sense to set aside.
Paolo Giarrusso (Jul 18 2022 at 14:03):(no, I'm not defending the terminology, but trying to recover what distinguish might have been there)
Paolo Giarrusso (Jul 18 2022 at 14:03):@Pierre Castéran can you maybe help enlighten us further?
Pierre Castéran (Jul 18 2022 at 14:14):Maybe the confusion comes from the diversity of the notion of "vernacular commands", which includes "Definition" as well as "Check". The "specification language" could (should ?) include only the first kind (as does coqtop -g?).
In short, I would associate with gallina every vernacular command which defines/extends the current context :thinking: ?
Pierre-Marie Pédrot (Jul 18 2022 at 15:14):in Coq V5, there is a man page that defines Gallina rather unambiguously, and this is pretty much "the output of coqdoc --gallina"
Pierre-Marie Pédrot (Jul 18 2022 at 15:15):here is the contents of that file, for reference: https://gist.github.com/ppedrot/a68529fc3ed73b0392064ce707280e02
Pierre-Marie Pédrot (Jul 18 2022 at 15:17):Gallina doesn't give any result in Coq 4.X, so I believe it was introduced in Coq 5.X
Pierre-Marie Pédrot (Jul 18 2022 at 15:22):The V5 manual is already ambiguous though, it already calls Gallina "the specification language" but contradicts itself in only a few lines
Pierre-Marie Pédrot (Jul 18 2022 at 15:25):IIUC this whole Gallina stuff only made sense in a primitive world where Coq files were much simpler as they are now.
Pierre Castéran (Jul 18 2022 at 15:40):I agree that this discussion is more important for tutorials, books, introductions to Coq (where it's useful to start with simplified descriptions) than reference manuals.
Pierre-Marie Pédrot (Jul 18 2022 at 15:42):if you want to do a bit of archaeology, here are the relevant Coq 5.X documentation files that mention the "gallina" name: https://gist.github.com/ppedrot/2c77536a7fe70416624e9b63c0e3d54c
Pierre-Marie Pédrot (Jul 18 2022 at 15:43):there are not that many mentions (essentially 5 paragraphs) and they're are self-contradicting, so good luck
Pierre-Marie Pédrot (Jul 18 2022 at 15:43):the source code doesn't mention gallina except for the tool of the same name
Pierre-Marie Pédrot (Jul 18 2022 at 15:44):(whose refman I linked above and was the ancestor to coqdoc --gallina)
Pierre-Marie Pédrot (Jul 18 2022 at 15:46):judging from the evolution from Coq 4.X I'm starting to guess that vernacular and gallina once meant the same thing, or more precisely that "gallina" was introduced in Coq 5.X as a fancy name for what used to be called "the vernacular mathematical language" in Coq 4.X.
Pierre-Marie Pédrot (Jul 18 2022 at 15:49):(OT, but I can't help noting that some of these documentation files are outright frightening. In the getting started section one can read "We assume here that the potential user has installed Coq on his workstation, that he calls Coq from a standard teletype-like shell window and that he does not use any special interface such as Emacs or Centaur." Boy, the 90's were rough.)
Paolo Giarrusso (Jul 18 2022 at 19:52):BTW, I agree another forum would help, we’d definitely want to tag all the TAPL authors, but e.g. I never see Benjamin Pierce here.
Théo Zimmermann (Jul 19 2022 at 07:55):@Benjamin Pierce is registered though, so maybe he will react to this discussion after this explicit mention.
Benjamin Pierce (Jul 19 2022 at 16:58):Thanks for looping me in!
Here's what Software Foundations says about "Gallina":
(** The functional style of programming is founded on simple, everyday mathematical intuition: If a procedure or method has no side effects, then (ignoring efficiency) all we need to understand about it is how it maps inputs to outputs -- that is, we can think of it as just a concrete method for computing a mathematical function. This is one sense of the word "functional" in "functional programming." The direct connection between programs and simple mathematical objects supports both formal correctness proofs and sound informal reasoning about program behavior. The other sense in which functional programming is "functional" is that it emphasizes the use of functions as _first-class_ values -- i.e., values that can be passed as arguments to other functions, returned as results, included in data structures, etc. The recognition that functions can be treated as data gives rise to a host of useful and powerful programming idioms. Other common features of functional languages include _algebraic data types_ and _pattern matching_, which make it easy to construct and manipulate rich data structures, and _polymorphic type systems_ supporting abstraction and code reuse. Coq offers all of these features. The first half of this chapter introduces the most essential elements of Coq's native functional programming language, called _Gallina_. The second half introduces some basic _tactics_ that can be used to prove properties of Gallina programs. *)
The only other place it's mentioned is this:
(** Wait -- did we just write an infinite loop in Coq?!?! Sort of. While evaluation in Coq's term language, Gallina, is guaranteed to terminate, _tactic_ evaluation is not. This does not affect Coq's logical consistency, however, since the job of [repeat] and other tactics is to guide Coq in constructing proofs; if the construction process diverges (i.e., it does not terminate), this simply means that we have failed to construct a proof at all, not that we have constructed a bad proof. *)
Based on the above discussion, this seems not entirely accurate but also not entirely misleading. :-)
If experts prefer an alternate phrasing (or entirely replacing the word Gallina with something else, or...), I'd be happy to oblige.
Pierre Castéran (Jul 20 2022 at 06:41):What about a quite fuzzy definition (in some informal part of Coq's documentation) ?
"Gallina" is a Latin nickname for a declarative part of the Coq Vernacular. This part contains the terms of CIC, as well as commands which determine the context in which these terms take place. This is also a default option of the coqdoc documentation tool, which translates .vfiles into this declarative vernacular.
(to be improved !)
Guillaume Melquiond (Jul 20 2022 at 07:43):Naming this specific language feels quite useless for me. Except for one single option of coqdoc, nobody would ever have an use for the Gallina word. It feels bad to make it so meaningless. I would prefer the following definition: "Gallina is a Latin nickname for the surface language of the CIC lambda-terms manipulated by the Coq system. By an abusive extension of this definition, it has historically also encompassed a few vernacular commands that are responsible for adding such lambda-terms to the global environment, e.g., Definition and Inductive."
Théo Zimmermann (Jul 20 2022 at 08:17):Making this into the official definition sounds OK to me. But about your "nobody would ever have an use for the Gallina word" answer to Pierre's suggestion, what do you say to the OP that wrote this example quote from a hypothetical blog post?
Coq is a proof assistant. To master Coq, you're going to master Gallina the programming language, which is similar to how you write programs in mainstream functional PL, e.g. Scheme, OCaml, and Haskell. Also, you can write proofs in Gallina to verify properties of your programs!
Guillaume Melquiond (Jul 20 2022 at 09:28):I would answer that, while Gallina is indeed usable to verify (prove) properties, it is often more productive to use a tactic/strategy language instead.
Karl Palmskog (Jul 20 2022 at 10:34):I think it would be good to rename the --gallina option to coqdoc, just say for example that -g removes proof scripts and that's it
Paolo Giarrusso (Jul 20 2022 at 11:16):Would the historical meaning of "Gallina = specification language" be still relevant? I guess the problem is that "what extends the context" is not a fixed set of commands and includes e.g. Equations. Does coqdoc -g have sensible behavior on such new commands?
Karl Palmskog (Jul 20 2022 at 11:19):you mean if it's relevant if we define Gallina as the surface-level term language? In that case, why wouldn't it be? In a typical workflow, all the types (specs) and some function terms would be written in the surface term language, and then proofs would be written in Ltac(2). The Vernacular fluff like Class/Definition is arguably just a way to point the terms in the right direction
Paolo Giarrusso (Jul 20 2022 at 11:21):I'm taking the "specification language" to go beyond terms; you can't write specs without Definition and Inductive.
Paolo Giarrusso (Jul 20 2022 at 11:22):More precisely, if you trimmed away everything possible (say for a POPL paper), you'd still need one way to add inductives, and one (primitive) way to add top-level constants.
Karl Palmskog (Jul 20 2022 at 11:23):sure, so you'd need both a "mini-Vernac" and a "mini-Gallina"
Hugo Herbelin (Aug 31 2022 at 14:43):An extra comment (but w/o having reading the whole discussion, so maybe redundant). I was told by Gérard that he introduced the term Gallina with the idea of formally specifying a specification language independent of Coq, that papers, or other tools could use. So, this is something which would have typically ranged from 1.a specifying the concrete syntax of (a given subset of) (a given version of) CIC, 2.a specifying a whole specification language (including notations, properties of arguments, coercions, canonical structures, ...), 1.b specifying the CIC typing rules, 2.b specifying also the elaboration (notations, unification, ...), but at least for sure excluding tactics or queries.
This is the objective that the chapters named Gallina (1.a) and Gallina extensions (2.a) reflected.
If we accept that such a formal definition of Gallina would come with a version number, and with a level of elaboration, defining the basic elaboration-free level 1.a (former chapter Gallina) and 1.b (chapters conversion and typing rules) would be doable and doing so would even help us to clarify a few logical features whose definition can be found only in the ocaml code.
Specifying levels that include elaboration (notations, unification, ... as well as the commands controlling elaboration) so that it presents a nice well-understood picture is more like a long-term research work (but certainly a very useful one).
In any case, if we need a definition right now, I would say it is the informal 2.a language, while 1.a is the core Gallina (even if nowadays too primitive to be realistically used without a minimum of elaboration).
Gaëtan Gilbert (Aug 31 2022 at 14:50):I don't remember if it was mentioned but we also have
Print Grammar vernac.
(* Entry gallina is
some stuff *)
Last updated: Oct 13 2024 at 01:02 UTC