Add general option -output-directory #17392

herbelin · 2023-03-16T21:40:35Z

Depends on, and refines #16126 (which added option Set Extraction Output Directory).

This PR adds an option -output-directory (with word directory in full to be consistent with using a full word in option Set Extraction Output Directory in #16126, and more generally with the general use of non-abbreviated words in commands) with synonym -output-dir (to be consistent with other command line options such as -native-output-dir).

This option is used by default for extraction (when Extraction Output Directory is unset), Redirect "file", and Print Universes "file" when "file" is not an absolute path.

Together with #16126, this should provide:

an indirect answer to Redirect (or Cd) should have an option/variant that computes paths relative to the directory of the .vo file #8649 which asks for a way to Redirect relatively to the repository where the .vo file is output
to remove the command Cd deprecate Cd command #16119 (or to replace it by an option Set Output Directory interactively mimicking -output-directory, though this might not be what most developers would recommend)

Closes #8649

Add support for output directory in extraction #16126 closing Command line option to set the directory for Extraction "file" #9148

Added / updated test-suite.
Added changelog.
Added / updated documentation.

Open questions:

Mentioned in dune improvements meta issue #8052 (dune) but I'm not specialist of dune.
Can it have an effect on Redirect/Extraction should validate file names to avoid (over)writing to arbitrary files #4953 (validity of filenames for Redirect/Extraction)?
Should we have also more specific options -redirect-output-directory, -extraction-output-directory?

Alizter · 2023-03-17T00:03:01Z

Do we want to make the option agnostic to extraction ?

herbelin · 2023-03-17T08:02:36Z

Do we want to make the option agnostic to extraction ?

What do you mean? Isn't it already independent of extraction per se?

Alizter · 2023-03-17T09:03:37Z

@herbelin right but the option is still named extraction output directory?

herbelin · 2023-03-17T18:55:37Z

With this PR, there are two levels of options, one on the command line -output-directory dir (for all commands with an output) and one using Set (specifically for extraction, and taking precedence over -output-directory dir if the former is already set).

Is it confusing? If yes, we may also add, say Set Redirect Output Directory. Or having only -output-directory dir but then, that would not solve the CoqIDE MacOS app problem mentioned in #14721.

Alizter · 2023-03-17T19:02:42Z

OK then I was just confused.

coqbot-app · 2023-05-01T02:17:54Z

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

coqbot-app · 2023-05-31T02:31:20Z

This PR was not rebased after 30 days despite the warning, it is now closed.

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

herbelin · 2024-02-24T07:11:57Z

I fixed in passing an issue with option -native-output-dir which was failing badly when provided with an absolute name. I added support for it, but maybe, it should be forbidden, I don't know.

Done

ejgallego · 2024-02-26T16:14:19Z

lib/flags.mli

@@ -96,3 +96,6 @@ val default_inline_level : int
 (** Global profile_ltac flag  *)
 val profile_ltac : bool ref
 val profile_ltac_cutoff : float ref
+
+(** Default output directory *)
+val output_directory : CUnix.physical_path option ref


IMO this should be in system.ml (use point), not here.

Why not. I will consider it.

ejgallego · 2024-02-26T16:18:26Z

sysinit/coqargs.ml

@@ -382,6 +384,10 @@ let parse_args ~usage ~init arglist : t * string list =
      let native_output_dir = next () in
      { oval with config = { oval.config with native_output_dir } }

+    |"-output-dir" | "-output-directory" ->
+      let dir = CUnix.canonical_dir (next ()) in


I think that messing with the directory the user provides is not a good idea. Why are you doing this?

For example, error messages won't contain the original directory, and the extra resolution may cause other issues.

IMHO this is a blocker for this PR.

The motivation is to be robust over Cd: it is more intuitive that a relative directory given on the command line is resolved relatively to the command line directory than dynamically depending on which Cds have done so far.

But the question of reporting an error is a good question. So maybe, what can be done is to keep the pair of both the relative output directory and of the directory in which the command has been launched??

ejgallego · 2024-02-26T16:19:53Z

boot/util.ml

@@ -48,7 +48,7 @@ let use_suffix prefix suffix =
  then suffix
  else Filename.concat prefix suffix

-let canonical_path_name p =
+let canonical_dir p =


Please don't do these kind of changes in unrelated PRs.

Due to the renaming extra noise, it took me much longer to review this PR, and I couldn't do as much of as precise job.

Sorry about that, I should have told that the renaming is in a separate commit.

More generally, even with the renaming, I'm not fully satisfied by the terminology used in CUnix. We should fix some naming conventions at some time.

Yes, I didn't mean in a bad way (I hope it was clear, I was just writing a bit rushed)

It is just that the change could be merged already while we discuss the minor issue with path normalization.

I agree that it'd be great to do some CUnix refactoring, I'd suggest doing a small meeting of those interested and coming up with maybe a new design?

For example, I've found many useful patterns in other OCaml projects which are all about files (like dune), we could also think of what's the right IO interface design for the lower layers of Coq, where IO is usually owned by the build system / doc manager.

SkySkimmer · 2024-02-28T13:08:40Z

@herbelin do you want to do some code changes in response to @ejgallego comments or is this ready?

ejgallego · 2024-02-28T13:47:36Z

@SkySkimmer I think maybe we should avoid the canonical_dir call, and instead respect the original path given (and preprend pwd if needed), that can be done in a new commit so the change is contained if you want.

Other than I think the PR is OK.

SkySkimmer · 2024-02-28T14:29:32Z

If someone does coqc -output-dir foo bar.v and bar.v contains

Cd "baz".
Redirect "file" Check True.

what should happen? The canonical_dir call IIUC is to make it write to $original_cwd/foo/file.out instead of $original_cwd/baz/foo/file.out.

ejgallego · 2024-02-28T15:04:33Z

The canonical_dir call IIUC is to make it write to $original_cwd/foo/file.out instead of $original_cwd/baz/foo/file.out.

The canonical_dir call is used to make the directory absolute, but it does a lot more stuff, for example will resolve hard and soft links. That second behavior is the problematic one, as user passes -output-dir foo.

If foo a symlink, then it will be resolved; that can break other stuff, as people often assume particular layouts which are not invariant under this (actually ill-defined) "path canonization".

What I propose is not to mess with output-dir argument except by preprending pwd if it is not absolute.

[Note that we must handle absolute stuff for windows paths too, etc...]

ejgallego · 2024-02-28T15:06:03Z

In the end I think the discussion just outlines that the businees of path / artifacts handling is complex (as we well known for example in Dune), an in general it is better for most of Coq to just have an interface so layers producing articats can inform the DM / build system, which is usually well-prepared to handle this kind of issues, as it has knowlegde about where files are (which coqc doesn't).

herbelin · 2024-02-28T19:25:41Z

What I propose is not to mess with output-dir argument except by preprending pwd if it is not absolute.

We could do that as well.

Can be used for example to choose the extraction output directory from the build system.

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

herbelin · 2024-02-29T11:35:56Z

I now moved the cUnix.ml things in #18732 and simply prepended the current directory when the output directory is relative.

lib/system.ml

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

SkySkimmer · 2024-03-01T13:10:17Z

@coqbot merge now

herbelin added part: tools Coqdoc, coq_makefile, etc. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: merge of dependency This PR depends on another PR being merged first. labels Mar 16, 2023

herbelin added this to the 8.18+rc1 milestone Mar 16, 2023

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 16, 2023

herbelin force-pushed the master+add-output-directory branch from 4e5c1e9 to 9eb1c17 Compare March 16, 2023 21:45

herbelin added a commit to herbelin/github-coq that referenced this pull request Mar 17, 2023

Adding change log for coq#17392

6309b5e

herbelin force-pushed the master+add-output-directory branch from 9eb1c17 to 6309b5e Compare March 17, 2023 07:34

herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 17, 2023

herbelin added a commit to herbelin/github-coq that referenced this pull request Mar 17, 2023

Adding change log for coq#17392

0b8844e

herbelin force-pushed the master+add-output-directory branch from 6309b5e to 0b8844e Compare March 17, 2023 07:36

coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Mar 17, 2023

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 17, 2023

herbelin force-pushed the master+add-output-directory branch 2 times, most recently from 8fdb07a to 0b8844e Compare March 17, 2023 19:02

herbelin mentioned this pull request Mar 17, 2023

Deprecating change directory #17403

Merged

1 task

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Mar 31, 2023

coqbot-app bot added the stale This PR will be closed unless it is rebased. label May 1, 2023

coqbot-app bot closed this May 31, 2023

coqbot-app bot removed this from the 8.18+rc1 milestone May 31, 2023

herbelin reopened this Jul 6, 2023

herbelin mentioned this pull request Jul 6, 2023

Move the documentation of Pwd and Cd to the extraction chapter. #17797

Merged

herbelin added a commit to herbelin/github-coq that referenced this pull request Feb 24, 2024

Adding change log for coq#17392

ec211db

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

herbelin force-pushed the master+add-output-directory branch from 86895f7 to ec211db Compare February 24, 2024 07:11

herbelin requested a review from a team as a code owner February 24, 2024 07:11

coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 24, 2024

ejgallego reviewed Feb 26, 2024

View reviewed changes

herbelin added 2 commits February 29, 2024 12:26

Add support for absolute native-output-dir.

5b5487a

Adding command line option "-output-directory dir".

199d030

Can be used for example to choose the extraction output directory from the build system.

herbelin added a commit to herbelin/github-coq that referenced this pull request Feb 29, 2024

Adding change log for coq#17392

28df7ec

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

herbelin force-pushed the master+add-output-directory branch from ec211db to 28df7ec Compare February 29, 2024 11:27

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Feb 29, 2024

herbelin mentioned this pull request Feb 29, 2024

Towards "cleaning" a bit cUnix.ml #18732

Draft

SkySkimmer reviewed Feb 29, 2024

View reviewed changes

lib/system.ml Outdated Show resolved Hide resolved

herbelin and others added 2 commits February 29, 2024 21:06

Extending the use of -output-directory to Redirect and Print Universes.

a4e150d

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

Adding change log for coq#17392

9295b6a

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

herbelin force-pushed the master+add-output-directory branch from 28df7ec to 9295b6a Compare February 29, 2024 20:07

SkySkimmer approved these changes Mar 1, 2024

View reviewed changes

SkySkimmer removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 1, 2024

coqbot-app bot merged commit f465e19 into coq:master Mar 1, 2024
6 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add general option -output-directory #17392

Add general option -output-directory #17392

herbelin commented Mar 16, 2023 •

edited

Alizter commented Mar 17, 2023

herbelin commented Mar 17, 2023

Alizter commented Mar 17, 2023

herbelin commented Mar 17, 2023

Alizter commented Mar 17, 2023

coqbot-app bot commented May 1, 2023

coqbot-app bot commented May 31, 2023

herbelin commented Feb 24, 2024

ejgallego Feb 26, 2024

herbelin Feb 26, 2024

ejgallego Feb 26, 2024

herbelin Feb 26, 2024 •

edited

ejgallego Feb 26, 2024

herbelin Feb 26, 2024

ejgallego Feb 26, 2024

SkySkimmer commented Feb 28, 2024

ejgallego commented Feb 28, 2024

SkySkimmer commented Feb 28, 2024

ejgallego commented Feb 28, 2024

ejgallego commented Feb 28, 2024

herbelin commented Feb 28, 2024

herbelin commented Feb 29, 2024

SkySkimmer commented Mar 1, 2024

Add general option -output-directory #17392

Add general option -output-directory #17392

Conversation

herbelin commented Mar 16, 2023 • edited

Alizter commented Mar 17, 2023

herbelin commented Mar 17, 2023

Alizter commented Mar 17, 2023

herbelin commented Mar 17, 2023

Alizter commented Mar 17, 2023

coqbot-app bot commented May 1, 2023

coqbot-app bot commented May 31, 2023

herbelin commented Feb 24, 2024

ejgallego Feb 26, 2024

Choose a reason for hiding this comment

herbelin Feb 26, 2024

Choose a reason for hiding this comment

ejgallego Feb 26, 2024

Choose a reason for hiding this comment

herbelin Feb 26, 2024 • edited

Choose a reason for hiding this comment

ejgallego Feb 26, 2024

Choose a reason for hiding this comment

herbelin Feb 26, 2024

Choose a reason for hiding this comment

ejgallego Feb 26, 2024

Choose a reason for hiding this comment

SkySkimmer commented Feb 28, 2024

ejgallego commented Feb 28, 2024

SkySkimmer commented Feb 28, 2024

ejgallego commented Feb 28, 2024

ejgallego commented Feb 28, 2024

herbelin commented Feb 28, 2024

herbelin commented Feb 29, 2024

SkySkimmer commented Mar 1, 2024

herbelin commented Mar 16, 2023 •

edited

herbelin Feb 26, 2024 •

edited