Loading a library that was extracted from Coq

Learning
1

The coq-buchberger package is a formally verified implementation of Buchberger’s algorithm in Coq which can be extracted to OCaml code. I want to use this extracted OCaml code in an OCaml project. How should I do that?

There is an opam package for coq-buchberger in the coq-released repository, but as far as I can tell this only installs the Coq files; it doesn’t extract the OCaml code and place it anywhere that I can load from an OCaml project. Specifically, I installed this opam package, but the extracted file sin_num.ml is not visible anywhere in the opam directory, and I can’t load any libraries called coq-buchberger, coq_buchberger, buchberger, or sin_num from a dune file.

I can clone the coq-buchberger repository as a subdirectory of my dune project, and (as I recently learned) this will automatically cause dune to build it, which includes extracting the OCaml code. However, the extracted sin_num.ml file ends up in _build/default/buchberger/src/, which doesn’t seem to be a place from which my code can load it. The dune documentation for coq.extraction says

The extracted sources can then be used in executable or library stanzas as any other sources.

but I can’t figure out how to do this from my project. I tried adding buchberger, sin_num, or buchberger.sin_num to my libraries stanza, but nothing works. I also tried adding a public_name to the coq.extraction stanza in the buchberger repository (although I’d prefer not to have to modify that submodule), but apparently coq.extraction doesn’t support that.

The only thing I’ve tried that works is to symlink _build/default/buchberger/src/sin_num.ml into my source directory, which is obviously not ideal.

2

Judging by the documentation, coq.extraction extracts source files, not libraries.

This means it is up to you to assemble these source files into a library or to include them directly into your final executable.

You can use copy rules (eg (copy#)) to copy the extracted sources to the directory where you want to use them, and then define a (library) or (executable) stanza that refers to it, as you would do with any other source file.

Cheers,
Nicolas

3

Thanks! What is the best way to do that with copy#? I have come up with

(rule
  (target sin_num.ml)
  (deps %{project_root}/_build/%{context_name}/buchberger/src/sin_num.ml)
  (action
    (copy# %{deps} %{target})))

which seems to work. Is this the best practice? It seems a bit odd to hardcode the directory _build but I can’t find a variable that would replace it.

4

In general, the directory in which a Dune files is evaluated is the directory containing the Dune file, but translated inside the build tree (ie inside _build/%{context_name}) so normally one is able to write relative paths to reach your target directory, without ever mentioning _build (nor the context name) explicitly. In fact, I don’t see how it works as written in your post.

Typically one could use:

(copy_files# <relative path to sln_num.ml>)

to achieve what you need.

Cheers,
Nicolas

5

Ah, I see. I was assuming I wanted the files to be copied to my source directory, rather than to its doppelganger inside the build tree.

(copy_files# ../buchberger/src/sin_num.ml)

works.

6

Note that you do not even need to clone the whole repository as a subdirectory. You can keep it as a regular dependency. You just need to have a Coq file containing the following three lines:

From Buchberger Require Import LexiOrder BuchRed.
From Coq Require Import Extraction.
Extraction "sin_num.ml" redbuch splus smult sscal spO sp1 sgen orderc_dec degc total_orderc_dec.