coq.extraction does not support package field

[vzaliva]

Currently, dune extraction is always performed. The user should be able to limit its scope with the package field (like in coq.theory)

One use-case is when the project contains several packages, some of which do not require Coq. Building non-coq packages with dune build -p pkg should be possible.

[ejgallego]

Hi @vzaliva , I'm not sure I fully understand your scenario, IIANM extraction targets will only be built when depended on, either by a (library ...) stanza or by a @all or directory alias.

Can you provide some detail on your build setup and the case where extraction is run when it shouldn't?

[vzaliva]

I've created sample project demonstrating what I am trying to do: https://github.com/vzaliva/coq-dune-examlpe

Trying to build OCaml-only part fails when Coq is not installed:

$ dune build -p example-ocaml
File "coq/extracted/dune", line 1, characters 0-107:
1 | (coq.extraction
2 |  (prelude Extract)
3 |  (extracted_modules Foo CRelationClasses Datatypes)
4 |  (theories Common)
5 | )
Error: Program coqc not found in the tree or in PATH
 (context: default)
Hint: opam install coq

[Alizter]

@vzaliva But the OCaml only part of your project depends on .ml files created from extraction thus causing extraction to be done. If you don't want your extracted library to be built when building example-ocaml then don't put it in that package.

[vzaliva]

exracted library is in example-coq package. See public name. Adding (package example-coq) to it triggers:

File "coq/dune", line 15, characters 10-21:
15 |  (package example-coq)
               ^^^^^^^^^^^
Error: This library has a public_name, it already belongs to the package

[vzaliva]

OCaml-only part is bar library, which should be the only thing in example-ocaml package.

[Alizter]

In coq/dune you have example-coq.coq as the public_name for the library extracted. The prefix of the public_name will determine the package field hence your error when you added that. This means that extracted is in the package example-coq under the name example-coq.coq hence why it is being built.

[vzaliva]

@Alizter this is understood. Yet, I have no solution for how to build example-ocaml package which contains only bar OCaml library which did not depend on any Coq code.

[Alizter]

If you want to build the package example-coq but not build the extracted code, then don't put the extracted code in the package. If you just want to build the OCaml code, then instead of building the package just build the targets in the ml/ directory. You can do this with dune build ml.

There is no way to build a package "minus" a library in Dune at the moment. I don't imagine such a feature would be very useful either.

[ejgallego]

Indeed @vzaliva as of today it is not possible to build a package that contains two libraries without building the two libraries. IIUC your example-coq package contains two libraries coq and bar, so -p will try both.

So in your case you either need to introduce a new package.

There could be some other ways to achieve this:

• trying to promote the extraction results (so users don't need Coq to build the extracted code)
• trying to make the extracted library (optional )

I didn't try any of the two options. Thanks for the example by the way, it is very helpful for us to have real use cases at hand.

[Alizter]

It would be nice to make the extraction stanza have a promote mode. I am not a fan of optional.

[vzaliva]

@ejgallego I think you may misunderstand my problem. I am not trying to build example-coq package. I am trying to build example-ocaml package. This package contains only bar ML library which does not depend on Coq part. All other libraries and coq.theories are explicitly marked to belong to example-coq package (including extracted) which I am not trying to build. The command:

$ dune build -p example-ocaml
File "coq/extracted/dune", line 1, characters 0-107:
1 | (coq.extraction
2 |  (prelude Extract)
3 |  (extracted_modules Foo CRelationClasses Datatypes)
4 |  (theories Common)
5 | )
Error: Program coqc not found in the tree or in PATH
 (context: default)
Hint: opam install coq

[Alizter]

Hmm I see what you mean now. I think you are correct in that when resolving the example-ocaml package, the source files are demanded hence the extraction step.

What does --debug-dependency-path give?

[vzaliva]

Adding this flag (dune build --debug-dependency-path -p example-ocaml) does not change the output. No additional information is printed.

Another observation is that if Coq is installed, it did not actually perform extraction and compiles bar library successfully. So it looks like it checks for coqc presence but never uses it.

[Alizter]

Very strange! Thanks for the report and sorry about not understand the initial issue.

[ejgallego]

Indeed, I think I misread it too.

So after a bit of debug this seems to be due to computation of .install files again, via select_native_mode.

So even if -p is used, dune tries to compute the list of installed files for the example-coq package, and that calls coqc leading to an error.

[ejgallego]

A workaround is to add (mode vo) to both dune files in coq/extracted and coq/common

[ejgallego]

cc: #7908

Another workaround is to use (coq lang 0.6) , but that's a PITA due to the deprecation of that version.

[vzaliva]

Thanks. I will consider mode workaround after I check if it affects performance too much.

[ejgallego]

Why would it affect performance @vzaliva ?

If you need native you can use (mode native), but then you'll have to depend on coq-native opam package to build.