Stream: Coq users

Topic: [Beginner] Differences between Coq and Gallina


view this post on Zulip 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:

  1. Is Gallina only one part of Coq? If so, what are the other parts of Coq? Tactics?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Jul 17 2022 at 11:31):

I never remember what Gallina is, because it doesn't matter.

view this post on Zulip Gaëtan Gilbert (Jul 17 2022 at 11:32):

pcuic is for polymorphic as in universe polymorphic AFAIK

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Jul 17 2022 at 11:33):

although https://arxiv.org/abs/1710.03912 says it's predicative

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jul 17 2022 at 11:39):

so the distinction between "input language" and other parts of a proof assistant can be important

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip 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...)

view this post on Zulip 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 ...

view this post on Zulip Karl Palmskog (Jul 17 2022 at 12:09):

do we really want to conflate the input language with the calculus of elaborated terms?

view this post on Zulip Karl Palmskog (Jul 17 2022 at 12:10):

I thought the distinction of input vs. elaborated stuff was useful when learning

view this post on Zulip Karl Palmskog (Jul 17 2022 at 12:11):

fine by me if you call them something like "Coq programming language" and "Coq calculus" though

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 17 2022 at 17:31):

(I see that Gaëtan made similar points above, minus "we've been over this")

view this post on Zulip Karl Palmskog (Jul 17 2022 at 17:51):

the definition that Enrico gave, "Gallina is constr [in the AST]" is quite precise

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jul 17 2022 at 17:52):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 .

view this post on Zulip Karl Palmskog (Jul 17 2022 at 19:12):

I'm sure there are quite a few special cases, but this is my mental model

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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:

  1. Gallina ~= functional PL similar to the pure subset of SML/OCaml for writing data structures and algorithms
  2. Tactics ~= an imperative language for proving properties of data structures and algorithms written in Gallina
  3. Ltac ~= macro system for writing tactics, for keeping it DRY.

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?

view this post on Zulip 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 was (almost) the same gallina as in 7.xx.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jul 18 2022 at 11:41):

Or it should be a CEP that allows (async) discussion about this with the community.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jul 18 2022 at 12:46):

also note that we still have coqdoc --gallina

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jul 18 2022 at 12:48):

(even that one does not highlight exactly the Gallina parts)

view this post on Zulip 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.

view this post on Zulip 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 :=

view this post on Zulip Karl Palmskog (Jul 18 2022 at 12:51):

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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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").

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Jul 18 2022 at 13:55):

we can probably also exclude other vernaculars — certainly Set/Unset, maybe Require, Import, modules, ...

view this post on Zulip 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".

view this post on Zulip Paolo Giarrusso (Jul 18 2022 at 13:59):

Let's set modules aside for a moment, since they were added later after the corruption...

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 18 2022 at 14:00):

despite the contradiction that @Théo Zimmermann observes, this _is_ interesting.

view this post on Zulip Paolo Giarrusso (Jul 18 2022 at 14:00):

_if_ we distinguish "Gallina vernacular" and "other vernacular", everything else makes _more_ sense.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Jul 18 2022 at 14:03):

@Pierre Castéran can you maybe help enlighten us further?

view this post on Zulip 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: ?

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 18 2022 at 15:44):

(whose refman I linked above and was the ancestor to coqdoc --gallina)

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 !)

view this post on Zulip 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."

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jul 20 2022 at 11:23):

sure, so you'd need both a "mini-Vernac" and a "mini-Gallina"

view this post on Zulip 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).

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC