Writing a Latex document embedding Coq code

Using Coq
1

Hello everyone,

Apologies if this question has been asked before - I couldn’t find a recent, similar thread.

I’m planning to write a large document in LaTeX that will include snippets of Coq code. This code depends on some Coq libraries, and I’ll need to evaluate it. Some of the code will depend on code from other Latex files.

Is there something similar to how Agda handles literate programming (Agda Literate Programming) but for Coq?

I came across Alectryon, but I’m not sure if it’s suitable for my needs. Has anyone used it with LaTeX documents?

Thank you a lot.
Best

2

Hi @turkoiz ,

I am not very familiar with how Agda handles literate programming, it would be maybe helpful if you could state a list of requirements that you need.

The coq-lsp Coq IDE and fcc compiler are designed to support literate programming, as of today, we only support markdown files, but it would be extremely easy to add LaTeX support if you would need it.

In this mode, Markdown (or LaTeX) files, are recognized by Coq, and you can edit them interactively.

3

There are a few examples of using Alectryon with LaTeX. My thesis is one (written mostly in reST by compiled using LaTeX, scroll to page 17 for example); the hydras book is another (written directly in LaTeX and using Alectryon for goals display).

There are a few more examples listed in the Alectryon README, including some using Beamer.

There is also a frontend for using Alectryon directly from a LaTeX document in a branch.

1 Like
4

Thank you for your responses and the links.

Regarding Literate Agda, I was thinking about the possibility of being able to write and evaluate code in a LaTeX file. For example, being able to have code blocks like this:

\begin{code}
    Inductive Forall : list A -> Prop :=
      | Forall_nil : Forall nil
      | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l).
\end{code}

And having a mode that would allow it to be evaluated using the company-coq commands.

5

The Alectryon branch that I pointed to will let you typecheck and record the output of such code, but ProofGeneral won’t let you evaluate it.

My preferred approach for this is to convert (“tangle”) the markup file to a source file. Alectryon supports doing this for reST and Markdown (and there’s an alectryon-mode for Emacs that binds a key to switch quickly between both), but not for LaTeX. It wouldn’t be too hard to add support for tangling LaTeX, I think: the tangling and weaving code is fairly generic.

Some background on this weaving/tangling stuff

6

@turkoiz , in the upcoming coq-lsp release, you can name your file foo.v.tex, and you can work with code blocks of the form \begin{coq} ... \end{coq}

This is also similar for Markdown, some kind of json formats, etc… coq-lsp doesn’t care about the format used, it is modular in that sense.

Note that has a different purpose than Alectryon: coq-lsp will just understand the literate document and allow you to develop in real time, but tools like Alectryon or some other systems are still required to render the document.

The coq-lsp should provide significant advantages over SerAPI, so I think at some point indeed Alectryon will use it, I guess you already use some form of LSP to talk to Lean @cpitclaudel ?

7

I use LSP for Dafny in the next branch of Alectryon and for Lean3; for Lean4 we have a SerAPI-like thing.

Basically I need to be able to segment the document into sentences + a structured way to retrieve goals (both were missing from the Lean3 LSP, and it was quite painful). Is there a way to do that with the current Coq LSP?

1 Like
8

Yup, I think the current API should serve you well, except that the segmentation is done according the Coq parser / lexer, which is often not what you want, but SerAPI had the same problem.

See coq-lsp/etc/doc/PROTOCOL.md at main · ejgallego/coq-lsp · GitHub

You actually can work in a few ways using coq-lsp / Flèche tho:

  • you can use LSP, and just send the document, do a getDocument request, and then issue goals request as you want, this is overkill tho if you want a batch processing
  • you can also use fcc with the goalsdump plugin, this way, you get all the sentences plus their goals in a single shot, .json file
  • there are many other goodies available, for example you can query the table of contents, and in 0.2.0 jump to definiton should be working project-wise, etc…
9

I have been careful to try to stay close to Lean’s LSP implementation (Isabelle’s is too far), but so far goals and getDocument are propietary.

10

Also note that we don’t take advantage of some very nice LSP stuff in 3.17 because no client does support it properly, for example pull diagnostics with progress, etc…

But if Alectryon would be such a client, there would be no problem. The underlying engine is very flexible.

There is also some design space in terms of how to integrate a tool like Alectryon in the workflow, in particular I think there are two approaches:

  • Alectryon can drive the checking, as it does not, and call Flèche for any info it needs. This has the main disadvantage that Alectryon needs to understand how files are related to each other, and maybe implement some incremental support
  • Fleche can drive the checking of the theory and call Alectryon to process a file when the file is ready. This is the model current Flèche plugins use: wait for an event (for example a proof is open) and call your tool in that case. For example Flèche could call Alectryon to process a .rst file in some way, etc…

Both approaches provide different tradeoffs, but in principle, they are feasible technically.

11

This is a very general question and I’m not sure if it’s a question for coq-lsp, Alectryon or some other tool, but would there be a way to translate the syntax tree of a Coq term into LaTeX or some other markup language in a recursive way, something like (letting [[ - ]] denote the translation function)

[[sum A B (fun C => D)]] = \sum_{ [[C]] = [[A]] }^{ [[ B ]] } [[D]]

and

[[mult A B]] = {[[A]] \cdot [[B]]}

so that

[[sum 0 10 (fun x => mult x x)]]

might get translated into

\sum_{x = 0}^{10} x \cdot x

or similarly

[[hom C x y]] = \operatorname{Hom}_{[[C]]}([[x]],[[y]])

This is really what I’d like to see in an ideal world from a literate programming tool, this is how I envision actually writing syntax translations.

It is maybe possible to do this by just translating sum and hom to LaTeX macros, but my experience with macros in general is that they are fiddly and the user has to avoid variable capture. Also I am more of a surface user of LaTeX and digging into the details of macros seems like it could be dreadful.

@cpitclaudel thoughts?