Hi, I'm confused about the differences between Coq the theorem prover and Gallina the programming language.

Questions:

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

Previous related discussion(s):

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.

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)

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

pcuic is for polymorphic as in universe polymorphic AFAIK

I think it's more accurate to say: Gallina doesn't matter to the foundations of Coq and its kernel

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

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

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

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

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

the distinction between some part of the input language and some other part is not really important

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

and the tactic code and Gallina code is typically written with quite different goals in mind, e.g., on maintainability

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

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 :-)

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

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...)

Also, pcuic is doomed to obsolete. I see no S for sprop, and when we will have sort polymorphism ...

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

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

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

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.

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?

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?

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?

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.

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

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.

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

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

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.

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

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

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

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.

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.

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.

@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?

I think that's correct, but others who have actually worked more at OCaml level will know better

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

sounds like a Coq document _might_ have type `vernac_expr`

, but I am not confident I’m parsing that link.

I think it's better to think of it [the Coq document] as a **list** of `vernac_expr`

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 `.`

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

Indeed, there is a control box (for fail, time,....), but a document is morally a list of vernac expr.

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.

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?

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:

- Gallina ~= functional PL similar to the pure subset of SML/OCaml for writing data structures and algorithms
- Tactics ~= an imperative language for proving properties of data structures and algorithms written in Gallina
- 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?

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.

the syntax of dependent product in V7 was without the forall keyword, see eg https://github.com/coq/coq/commit/9a6e3fe764dc2543dfa94de20fe5eec42d6be705#diff-e33da29506e770f8309cc0e4140c077bfb7a438b4950d86a423e0bfbfd6fa54fL95-R95

also match was written `Cases x of branches end`

, see eg Peano.v in that commit

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.

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.

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.

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.

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.

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:

- language of all surface Coq commands
- surface specification language ("enriched lambda calculus") usable as part of some Coq commands
- elaborated term language
- foundational calculus ("CIC" as Théo suggests is fine by me)

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.

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

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.

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

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.

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.

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).

And I used to be in the "most core devs" category, because I too thought that Gallina was the language of terms.

also note that we still have coqdoc --gallina

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

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

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.

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)

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.

I think there is a part of core dev that considers defining Gallina irrelevant/unnecessary, regardless of how it is defined

this is how I read Gaëtan's comments above (and I think PMP said something similar earlier)

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`

).

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.

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).

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).

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.

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`

"

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.

(And it was already self-contradictory, since beyond this section "The Vernacular" inside the "Gallina" chapter, there was also another chapter called "Vernacular commands").

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?

we can probably also exclude other vernaculars — certainly `Set/Unset`

, maybe `Require`

, `Import`

, modules, ...

Modules: not clear if you consider Gallina as being "the (purely functional) programming language subset of Coq".

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

Coq 8.9's manual also has > This grammar describes The Vernacular which is the language of commands of Gallina.

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

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

"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

https://coq.github.io/doc/v8.9/refman/proof-engine/vernacular-commands.html has everything else, which it makes sense to set aside.

(no, I'm not defending the terminology, but trying to recover what distinguish might have been there)

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

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: ?

in Coq V5, there is a man page that defines Gallina rather unambiguously, and this is pretty much "the output of coqdoc --gallina"

here is the contents of that file, for reference: https://gist.github.com/ppedrot/a68529fc3ed73b0392064ce707280e02

Gallina doesn't give any result in Coq 4.X, so I believe it was introduced in Coq 5.X

The V5 manual is already ambiguous though, it already calls Gallina "the specification language" but contradicts itself in only a few lines

IIUC this whole Gallina stuff only made sense in a primitive world where Coq files were much simpler as they are now.

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.

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

there are not that many mentions (essentially 5 paragraphs) and they're are self-contradicting, so good luck

the source code doesn't mention gallina except for the tool of the same name

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

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.

(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.)

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.

@Benjamin Pierce is registered though, so maybe he will react to this discussion after this explicit mention.

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.

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 `.v`

files into this declarative vernacular.

(to be improved !)

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`

."

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!

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.

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

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?

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

I'm taking the "specification language" to go beyond terms; you can't write specs without `Definition`

and `Inductive`

.

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.

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

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).

I don't remember if it was mentioned but we also have

```
Print Grammar vernac.
(* Entry gallina is
some stuff *)
```

Last updated: Sep 26 2023 at 11:01 UTC