Command line option to set the directory for Extraction "file"

[Lysxia]

(as of Coq 8.8)

Extraction "file" foo. with coqc puts the extracted file wherever the current directory is, which is typically the root of your project, and which should ideally not be thus polluted.

A possible workaround is to change the current directory, but in a Makefile you have to be careful to do it on the same line as the coqc command, and then you have to accordingly shift the -Q arguments. A command line option would be a much more obvious solution.

This sounds related to #8649 but I'm not actually familiar with those commands.

[ejgallego]

cc: #8052

[tchajed]

Until Coq has better support, what I do is create a file haskell-project/Extract.v that looks like

Cd "haskell-project/extract".
Require Import MyCoqDevelopment.
Separate Extraction foo.
Cd "../..".

Now you must run coqc haskell-project/Extract.v from the root of your project for this to work, but you're running make from that directory anyway so it's not hard to arrange that (even make -C will work, since it changes the working directory).

This file is difficult to use interactively since you have to make sure the working directory is correct. I'll typically temporarily remove the Cd directives to debug it, and then I just make sure to put the extraction directives somewhere else and import them to Extract.v so that the file rarely changes.

(Note that while I phrased everything in terms of Haskell I think the story would be pretty much identical for OCaml, modulo where exactly you should put the output code.)

[Zimmi48]

Related to #9295.

[andres-erbsen]

see also #8649 #4953

[ejgallego]

After a bit of thinking (maybe not enough) , I think that the best choice of action here is to actually remove Cd (and also redirect, but that's unrelated), and then migrate extraction to use the output directory of the .vo file.

There is no sane way Coq could understand enough context as for Cd not to create a lot of problems. Removing Cd also opens a path to actually improving the behavior of the extraction object output directory; package willing to maintain compat with both semantics should always call extraction from the current dir.

Not to talk about the semantics of Cd with respect to language servers.

That being said, having an option to set the output dir is also compatible with the above plan; but I am a bit wary of option creep; ideally the option would be shared for extraction objects and .vo s.

[ejgallego]

The deprecation plan for Cd could go as follows; emit a warning, and point to the Cd documentation where the changes are explained. This will be a bit painful for users as coq_makefile doesn't support extraction AFAICT; so we are talking about adapting a few custom build rules.

[Zimmi48]

What about instead, in 8.12:

• change the behavior of extraction (extract to the directory where the extract command is located) and of Cd (no-op, and warns that it is a no-op and deprecated) ;
• provide a (deprecated) compatibility option to restore the previous behavior that is set in the 8.11 compatibility file.

The compatibility option will ensure that users have time to migrate, while the transformation of Cd into a no-op will make it possible to write code that is compatible with Coq < & >= 8.12 (without resorting to the compatibility option).

[tchajed]

I don't like this proposal because it forces me to use the Coq source tree as the Haskell source tree (I believe all of this applies equally to OCaml), and places even more auto-generated files in that tree. If Coq supported a separate output directory (which would clean up the source tree), then that directory would have both build outputs and be a Haskell source tree.

My layout looks like this:

proj/
- src/
  - foo.v
  - foo.vo
  - lib/
    - bar.v
    - bar.vo
- proj-client/
  - stack.yaml
  - Extraction.v
  - extract/
    - foo.hs
    - lib/
      - bar.hs
  - src/
    - Main.hs

This places all the auto-generated Haskell files in their own extract directory,
separate from the Coq source tree, and with the right module structure. It also makes the Coq project pretty isolated from the extraction. The only hack I need for this is that Extraction.v does Cd "proj-client/exract", does not work in interactive mode, and extraction does start in src/ and output files in proj-client/. The lack of interactive mode is fine because it only imports one module and runs Separate Extraction.

I think the solution I'd like best would be to use paths relative to the source file. It doesn't have to be Cd, but I'd like to keep extracted source code separate from Coq build outputs.

[JasonGross]

@tchajed what do you mean by "and extraction does start in src/ and output files in proj-client/"? Do you mean that some of your files other than Extract.v contain extraction?

How painful would it be if you needed to put Extract.v inside proj-client/extract, rather than inside proj-client?

(Also, I thought Coq does now support separate output directories, since dune?)

[JasonGross]

@tchajed I think extraction build outputs are sort-of like assembly .s files emitted by gcc, or other build intermediates, which are generally placed in the build outputs directory. Do you view them differently?

[tchajed]

@tchajed what do you mean by "and extraction does start in src/ and output files in proj-client/"? Do you mean that some of your files other than Extract.v contain extraction?

No, I just meant that extraction means that the Haskell project has to know about the Coq project, which makes it complicated. However, the Coq project is perfectly ordinary. You can probably ignore this point - at some point clearly we need a unified build system that connects Coq to haskell-stack, and that gets messy because it happens by using make to compose the Coq build system with stack. In OCaml the situation could be better, where everything is managed by dune.

In practice I do need a file with the extraction setup on the Coq side, so maybe I should just put Extract.v there. I adopted this convention once I had a project with multiple independent Haskell projects.

[tchajed]

@tchajed I think extraction build outputs are sort-of like assembly .s files emitted by gcc, or other build intermediates, which are generally placed in the build outputs directory. Do you view them differently?

This is a good point. The biggest difference is that I actually use the extracted files - I open them in an editor, they're processed by Haskell's language server, and I need to search them occasionally.

I think the concrete thing I'm not sure how to do is that I'll need the Haskell stack project to include a source directory outside of the root to grab the Coq build directory, whether that's an output directory proj/build or proj/src. I don't even know if this is possible, or how well it works (eg, will my editor understand it and support go-to-definition).

[Zimmi48]

In OCaml the situation could be better, where everything is managed by dune.

That's precisely what we are trying to improve (see ocaml/dune#3299).

I thought Coq does now support separate output directories, since dune?

The way it works (for Coq and also for OCaml) is that Dune copies the source files in _build/default and builds everything in there. Thus, the build is hygienic without having to change Coq to support outputting the resulting file in another directory.

I'm not sure I've understood from this discussion if your use case could be covered by simply moving the file containing the extraction commands to the Haskell part of your project @tchajed?

Regarding the build workflow, you could use Dune (next version) to build the Coq project up to Haskell extraction, use (mode promote) or (mode (promote until-clean)) to get the generated Haskell files in your Haskell source tree, and use Stack to build the Haskell project, possibly wrapping the whole thing in a small Makefile.

[tchajed]

Yeah, I think my setup actually already works as long as I keep the output adjacent to the Coq file, except that Extraction.v has to be alongside the auto-generated code.

It’s still annoying that this will require changes to my Haskell extraction and doesn’t improve the situation for me (except for the perceived security concern of using Cd). For example, I still use post-processing to insert additional imports needed for Extract Constant commands (eg, Data.ByteString).

[JasonGross]

For example, I still use post-processing to insert additional imports needed for Extract Constant commands (eg, Data.ByteString).

I thought there was an issue about this, but I couldn't find it, so I made #11956

It’s still annoying that this will require changes to my Haskell extraction and doesn’t improve the situation for me (except for the perceived security concern of using Cd)

It will actually improve the user-experience a little bit: you will no longer have to modify the file to get it to compile interactively. (Admittedly, this is not very interesting for tiny files with just Extraction commands in them.) And, indeed, it's unfortunate that the user experience around extraction is so often so hacky.

[JasonGross]

@Zimmi48

• change the behavior of extraction (extract to the directory where the extract command is located)

I think extracted files should go in the build outputs directory, though, not the .v file directory.

What about the following, in 8.12?

• when coqc starts, set the cwd (which is used for extraction and redirect) to the directory into which the .vo file will be output, unless -compat 8.11 is passed on the command-line (is there still a way to condition things on that?)
• make Cd a deprecated no-op with an option to restore the previous behavior (which will be set in the 8.11 compat file)

[Zimmi48]

I think extracted files should go in the build outputs directory, though, not the .v file directory.

Yes, but currently this is the same and there is no way to configure it, is there?

See also:

I thought Coq does now support separate output directories, since dune?

The way it works (for Coq and also for OCaml) is that Dune copies the source files in _build/default and builds everything in there. Thus, the build is hygienic without having to change Coq to support outputting the resulting file in another directory.

[Zimmi48]

@JasonGross Is there much difference between our two proposals? I feel like the only difference is whether the behavior of Extraction is controlled directly by -compat 8.11 or by the compatibility option (that is activated anyway by -compat 8.11).

[JasonGross]

I think the difference is that my proposal also affects Redirect. The reason that my proposal doesn't have an option and just a command line flag is that there is a bit of a question of what to do with Set Compat. Cd foo. Unset Compat. Extraction. Set Compat. Extraction.

However, on second look, I think your proposal might be simpler, and I'm fine with it (but let's also have it apply to Redirect and the like).

[ejgallego]

Useful discussion thanks; I'll try to address this next week; I'll introduce an abstraction for controlling the generation of object files in general so it should be easy to tweak it.

[Alizter]

I've made a PR allowing you to configure the output directory of extraction. This "kind of" lets you have a command line option for it also: #16126