Allow use of directory names for filename lines in _CoqProject #16308

jfehrle · 2022-07-11T05:29:20Z

UPDATED 7/27: Currently coq_makefile requires listing every single file in the project. Every time you add a file to the project, you have to update _CoqProject and rerun coq_makefile. That's a waste of energy and brain cells.

This PR adds expansion of directory names, so _CoqProject will need far fewer entries and far fewer updates. Expansion is also applied to paths specified on the coq_makefile command line. (Names that start with - or that have an extension are not expanded. If a specified directory doesn't exist, it is ignored.)
For example, instead of:

core/Core.v
core/ByteDecidable.v
core/DeserializerMonad.v
core/BasicSerializers.v
core/Cheerios.v
core/Tree.v
core/Combinators.v
core/Types.v
core/Tactics.v

extraction/ExtrOcamlCheeriosFinInt.v
extraction/ExtrOcamlCheeriosBasic.v
extraction/ExtrOcamlCheeriosString.v
extraction/ExtrOcamlCheeriosNatInt.v

runtime/coq/ExtractTreeSerializerDeps.v
runtime/coq/ExtractPositiveSerializerDeps.v
runtime/coq/ExtractTreeSerializer.v
runtime/coq/ExtractPositiveSerializer.v

you could have:

core
extraction
runtime/coq

Still needs:

~~changelog~~
~~documentation~~

tools/coq_makefile.ml

gares · 2022-07-11T08:05:31Z

I wanted to support bash-style ** wildcards to recursively match subdirectories, allowing things like **/*.v. It can be done like this, but that adds a dependency on bash, which seems like something to avoid. Right?

I think this feature is nice, and ** is not really needed IMO

Alizter · 2022-07-11T12:38:50Z

I think ** would open this to be abused, but I welcome the * change.

jfehrle · 2022-07-11T19:29:13Z

What is the potential for "abuse" of **? I don't see it.

I'll update the doc once #15888 is merged.

Alizter · 2022-07-11T20:02:52Z

I mean misuse rather than abuse. Some people, for example, have git submodules in their projects. If those submodules contain .v files as well, then suddenly more .v files are being picked up by _CoqProject. This is less likely to happen with * and impossible with the current behaviour of manually specifying files.

jfehrle · 2022-07-11T20:10:02Z

OK, makes sense. I don't think about git submodules very much.

jfehrle · 2022-07-11T20:50:14Z

However, Coq ignores _CoqProject when creating the loadpath. It looks for .vo files in every subdirectory, so the submodules will appear in the loadpath under strange names based on their path in the filesystem, e.g. submodules/MySubmodule will be under the logical path Foo.submodules.MySubmodule without the logical name given in SubModule's _CoqProject (in -Q/-R).

The solution would be for Coq to look for _CoqProject files and use the -Q/-R assigned logical name. I don't know how important that use case is.

Alizter · 2022-07-11T20:57:04Z

I think Coq (coqc/coqtop) knowing about _CoqProject in general is not a very good idea for several reasons. I won't get into it here though. _CoqProject is used by (and intended for) coq_makefile, coqide and other IDEs like PG.

SkySkimmer · 2022-07-11T20:58:29Z

However, Coq ignores _CoqProject when creating the loadpath. It looks for .vo files in every subdirectory, so the submodules will appear in the loadpath under strange names based on their path in the filesystem, e.g. submodules/MySubmodule will be under the logical path Foo.submodules.MySubmodule without the logical name given in SubModule's _CoqProject (in -Q/-R).

That only happens if the submodule is in the scope of the -Q/-R, in which case that's what the _coqproject writer wanted so what's the problem?

jfehrle · 2022-07-11T21:42:52Z

That only happens if the submodule is in the scope of the -Q/-R, in which case that's what the _coqproject writer wanted so what's the problem?

You are correct.

jfehrle · 2022-07-11T23:00:03Z

You are correct.

I spoke too soon. It is a problem if the project is loaded through $COQPATH, in which case no -Q/-R info is applied.

I think Coq (coqc/coqtop) knowing about _CoqProject in general is not a very good idea for several reasons. I won't get into it here though.

There are other use cases that would work better with _CoqProject info. I'll create a new issue for a discussion fairly soon.

jfehrle · 2022-07-15T19:01:18Z

Changed to use the simpler "echo <filenames>" and changed coqdep to also expand wildcards. Also added documentation, a test and a changelog. I think ready for final review/merge. @gares, are you the appropriate reviewer?

Separate from this PR, did you ever consider having a single shared copy of CoqMakefile in the Coq installation? In the makefile, include can use a variable, so Makefile.conf should be able to include such a file. That would mean no need to generate the CoqMakefile for each package, check it in to git or update it for each release of Coq. Or are there reasons that this would be unwise?

coqbot-app · 2022-07-15T19:18:01Z

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

Alizter · 2022-07-15T19:27:52Z

@jfehrle There seem to be some extra files in your commit. The directory wildcards/t shouldn't be there for instance.

jfehrle · 2022-07-15T20:32:33Z

OK, I removed that directory. I think all the others are needed, right?

Updated.

test-suite/cram/coq-makefile/wildcards.t/run.t

Alizter · 2022-07-15T20:40:14Z

If it makes the test easier to read, you can also include _CoqProject in run.t directly. You will need to remove the existing _CoqProject and put:

  $ cat > _CoqProject << EOF
  > -R . Wildcards
  >
  > a.v
  > b?.v
  > c[1-3].v
  > x/*.v
  > EOF

at the start of your run.t.

jfehrle · 2022-07-15T21:06:34Z

If it makes the test easier to read, you can also include _CoqProject in run.t directly.

I prefer it totally static as it is, thanks.

coqbot-app · 2022-07-15T21:42:50Z

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

doc/sphinx/practical-tools/utilities.rst

gares

this PR lacks tests (no need to use cram)

doc/sphinx/practical-tools/utilities.rst

silene · 2022-07-28T06:24:55Z

doc/sphinx/practical-tools/utilities.rst

+
+In addition, you can list individual files, for example for the two script files
+`File1.v` and `SubDir/File2.v` whose logical paths are `MyProject.File1` and
+`MyProject.SubDir.File2`.  We recommend naming that directory `MyProject`, the


Who are we to tell the user how they should name their directories?

Moreover, this is a recommendation that might be painful to follow for users. For example, the current directory might well be the name of a cloned git repository (e.g., coq-foo) while the logical path is quite different (e.g., Foo). Sure, users could always rename their checkout directory to match it against the logical path, but why should they care and why do we?

Who are we to tell the user how they should name their directories?

There's nothing wrong per se in giving advice, indeed advice can often be quite helpful. Of course it has to be good advice. Users will do what they wish.

For example, the current directory might well be the name of a cloned git repository (e.g., coq-foo) while the logical path is quite different (e.g., Foo).

A good point. I had not considered that case when I wrote this section. For a single package project, the IDE gets the -R/-Q information from _CoqProject and passes it to Coq, so coq-foo is fine. But the IDE only uses a single _CoqProject, which isn't sufficient for projects that have multiple uninstalled packages, (uninstalled because e.g. you're editing multiple packages at once). Packages that you're editing should not be in the user-contrib directory, so you need to use $COQPATH to point to them. COQPATH uses the directory name as the first part of the logical name, hence the recommendation.

I have a proposal that will allow handling both your coq-foo use case and the multipackage case as well as a few others we currently don't handle. I planned to bring that up shortly after completing this PR. Whether that proposal is implemented or not, I'd love to improve this section to address your concerns. I think that would work best as a separate discussion rather than in this PR. It's really a different topic from allowing directory names in _CoqProject. Note that I'm not really adding new recommendations in this PR, but rather moving them from one spot to another. Is this a reasonable approach?

Moreover, this is a recommendation that might be painful to follow for users.

Calling this "painful" seems exaggerated. git doesn't care about the name of the directory containing a cloned git repository.

While I agree that the advice is essentially the existing one, I agree it violates the most common conventions.

It's also pretty confusing — if you have a folder containing the suggested _CoqProject, File1.v, and SubDir/File2.v, then the name of that folder is technically irrelevant in this scenario.

For a single package project, the IDE gets the -R/-Q information from _CoqProject and passes it to Coq, so coq-foo is fine.

Dashes are common in project nams, but they're illegal in logical names — you can't use -Q . my-package, because Require my-package.foo does not parse correctly.

Let's refine the recommendations very soon, but not in this PR.

silene · 2022-07-28T06:29:20Z

doc/sphinx/practical-tools/utilities.rst

-Perhaps this will be simplified in the future.  The order of the entries does not
-matter.
+using a single `-R` with `.` as the :term:`physical path` for simplicity.  You must also
+identify all the `.v` files in your package.  We recommend using directory names


I am wary of all these recommendations. That is certainly not something I would ever recommend to a user. And in fact, this is not even the common practice in the Coq ecosystem. Common practice is to have a directory theories and to have the corresponding option -R theories Logical.

silene · 2022-07-28T06:42:57Z

doc/sphinx/practical-tools/utilities.rst

@@ -163,8 +169,8 @@ Then:

 - Compile your project with :n:`make -f CoqMakefile` as needed.

-If you add new files to your project, add them to `_CoqProject` and
-re-run `coq_makefile` and `make`.
+If you add more files to your project that are not in directories listed


Is that correct? Since coq_makefile is responsible for traversing the directories, I don't understand how a new file could be located without running it again.

I mistakenly dropped the expansion of directories in the makefile, I'll re-add that.

jfehrle · 2022-07-29T23:16:30Z

I created two new tests and dropped the cram test. They run just fine locally, but they inexplicably report they're unable to find coq_makefile. I have no clue why this doesn't work; it's very similar to the other coq_makefile tests. Suggestions?

run.sh: line 6: coq_makefile: command not found
actual:
expected: a/b/g.v a/g.mlg a/g.mllib a/g.mlpack g.ml g.mli nonexistent.v
==========> FAILURE <==========
    coq-makefile/expand-directories/run.sh...Error!

run.sh: line 5: coq_makefile: command not found
actual:
expected: x/a.v b.v
==========> FAILURE <==========
    coq-makefile/expand-directories2/run.sh...Error!

test-suite/coq-makefile/expand-directories/run.sh

Alizter · 2022-07-30T11:37:45Z

I originally suggested the use of cram tests to Jim since they could be easier to work with, however for coq_makefile this hasn't worked too well due to the special environment expected by coq_makefile. I don't have enough knowledge to set that up correctly.

Blaisorblade · 2022-07-30T21:49:56Z

doc/sphinx/practical-tools/utilities.rst

+`MyProject.SubDir.File2`.  We recommend naming that directory `MyProject`, the
+same as the logical name::
+
+  -R . MyProject


Beware the new text mixes -R . MyPackage and -R . MyProject. That might be because the old text was already incorrect — it uses -R . MyPackage to configure a "logical name" MyProject, which is just wrong.

At a first look, there isn't a real distinction, so the simplest fix is to unify them.

Thanks, got it. They are all MyPackage now.

jfehrle · 2022-07-30T23:07:06Z

@gares The tests pass. If this looks good, I'll squash before the merge.

jfehrle · 2022-07-31T04:37:53Z

I think the failure in ci-fiat_parsers is unrelated. The log for that job shows a change made this afternoon. It worked in the previous run and I made no substantive code change to the PR since then:

commit fccfd0e4b85dd9958e835a6701e13673c6b7c792
Author: Jason Gross <jgross@mit.edu>
Date:   Sat Jul 30 17:40:25 2022 -0400
    Actually fix _CoqProject

JasonGross · 2022-07-31T09:36:05Z

I've restarted Fiat parsers. The commit you mention should build

jfehrle · 2022-07-31T14:51:39Z

@JasonGross fiat parsers is still failing, but probably unrelated to this PR

## Remaking _CoqProject for Coq v8.17
## 
rm -f _CoqProject
make --no-print-directory _CoqProject
( echo '-arg "-native-compiler no"'; echo '-arg "-require-import Coq.Compat.AdmitAxiom"'; (cat "_CoqProject.in" | sed s'/\.@ML4_OR_MLG@/.mlg/g' | sed 's/@META@/META.coq-fiat-parsers/g' ) ) > "_CoqProject"
make[1]: *** No rule to make target 'FORCE', needed by 'update-ml-files'.  Stop.

JasonGross · 2022-07-31T20:06:19Z

Trying another fix

jfehrle · 2022-07-31T20:55:42Z

Don't rush on my account. I think we can safely ignore the failure for this PR.

gares · 2022-07-31T21:06:10Z

doc/sphinx/practical-tools/utilities.rst

+other file types) in the current directory and its subdirectories:
+
+  -R . MyPackage
+  .


I think this little dot deserves a comment, the reader may not even see it. Could also be written ./ to make it more visible

Anyway, I'd recommend putting the sources in a (sub) directory. I don't recall any project placing source files at the root.

Ah, it was supposed to be formatted like this, which I fixed:

I'll refine the recommendations soon. FWIW the bignums package puts files at the root. Hard to expect people to know about or follow unwritten conventions.

~/.opam/__coq-platform.2022.01.0~8.15~beta1/.opam-switch/sources/coq-bignums.8.15.0$ more _CoqProject -I plugin -R . Bignums

jfehrle · 2022-07-31T21:47:01Z

Updated and squashed, please merge.

Thanks to all of you who reviewed, commented and helped me!

jfehrle · 2022-08-04T17:17:20Z

@gares Do you plan to ~~assign and~~ merge this soon? (If you're on vacation, I hope you're having a good time.) Thanks.

gares · 2022-08-04T21:55:21Z

@coqbot merge now

coqbot-app · 2022-08-04T21:55:22Z

@gares: You cannot merge this PR because:

There is no kind: label.

gares · 2022-08-05T11:12:51Z

@coqbot merge now

jfehrle added the part: coq_makefile The coq_makefile binary for generating makefiles. label Jul 11, 2022

jfehrle requested a review from a team as a code owner July 11, 2022 05:29

jfehrle force-pushed the wildcards_in_coqproject branch from 5994924 to 8504ea7 Compare July 11, 2022 05:33

gares reviewed Jul 11, 2022

View reviewed changes

tools/coq_makefile.ml Outdated Show resolved Hide resolved

gares reviewed Jul 11, 2022

View reviewed changes

tools/coq_makefile.ml Outdated Show resolved Hide resolved

jfehrle force-pushed the wildcards_in_coqproject branch 2 times, most recently from 6a91ea5 to 4362cc8 Compare July 11, 2022 08:23

jfehrle added this to the 8.17+rc1 milestone Jul 11, 2022

jfehrle force-pushed the wildcards_in_coqproject branch from 4362cc8 to 29d6875 Compare July 15, 2022 18:41

jfehrle requested review from a team as code owners July 15, 2022 18:41

Alizter reviewed Jul 15, 2022

View reviewed changes

test-suite/cram/coq-makefile/wildcards.t/run.t Outdated Show resolved Hide resolved

jfehrle force-pushed the wildcards_in_coqproject branch from 29d6875 to 98e1648 Compare July 15, 2022 21:05

gares reviewed Jul 28, 2022

View reviewed changes

doc/sphinx/practical-tools/utilities.rst Show resolved Hide resolved

gares requested changes Jul 28, 2022

View reviewed changes

silene reviewed Jul 28, 2022

View reviewed changes

jfehrle force-pushed the wildcards_in_coqproject branch 3 times, most recently from 222c1f4 to ac8af24 Compare July 29, 2022 07:40

SkySkimmer reviewed Jul 30, 2022

View reviewed changes

test-suite/coq-makefile/expand-directories/run.sh Show resolved Hide resolved

jfehrle force-pushed the wildcards_in_coqproject branch 2 times, most recently from 6e940b3 to 6e72168 Compare July 30, 2022 18:28

Blaisorblade reviewed Jul 30, 2022

View reviewed changes

jfehrle force-pushed the wildcards_in_coqproject branch from 6e72168 to 2e23c15 Compare July 30, 2022 23:07

gares approved these changes Jul 31, 2022

View reviewed changes

Expand filepaths that are directories in _CoqProject

c62c02d

jfehrle force-pushed the wildcards_in_coqproject branch from 2e23c15 to c62c02d Compare July 31, 2022 21:45

gares self-assigned this Aug 1, 2022

jfehrle added the kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. label Aug 4, 2022

coqbot-app bot merged commit 4a562a8 into coq:master Aug 5, 2022

Allow use of directory names for filename lines in _CoqProject #16308

Allow use of directory names for filename lines in _CoqProject #16308

Conversation

jfehrle commented Jul 11, 2022 • edited Loading

gares commented Jul 11, 2022

Alizter commented Jul 11, 2022

jfehrle commented Jul 11, 2022

Alizter commented Jul 11, 2022 • edited Loading

jfehrle commented Jul 11, 2022

jfehrle commented Jul 11, 2022

Alizter commented Jul 11, 2022

SkySkimmer commented Jul 11, 2022

jfehrle commented Jul 11, 2022

jfehrle commented Jul 11, 2022

jfehrle commented Jul 15, 2022

coqbot-app bot commented Jul 15, 2022

Alizter commented Jul 15, 2022 • edited Loading

jfehrle commented Jul 15, 2022 • edited Loading

Alizter commented Jul 15, 2022

jfehrle commented Jul 15, 2022 • edited Loading

coqbot-app bot commented Jul 15, 2022

gares left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jfehrle Jul 28, 2022 • edited Loading

Choose a reason for hiding this comment

jfehrle Jul 30, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jfehrle commented Jul 29, 2022

Alizter commented Jul 30, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jfehrle commented Jul 30, 2022

jfehrle commented Jul 31, 2022

JasonGross commented Jul 31, 2022

jfehrle commented Jul 31, 2022

JasonGross commented Jul 31, 2022

jfehrle commented Jul 31, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jfehrle commented Jul 31, 2022 • edited Loading

jfehrle commented Aug 4, 2022 • edited Loading

gares commented Aug 4, 2022

coqbot-app bot commented Aug 4, 2022

gares commented Aug 5, 2022

jfehrle commented Jul 11, 2022 •

edited

Loading

Alizter commented Jul 11, 2022 •

edited

Loading

Alizter commented Jul 15, 2022 •

edited

Loading

jfehrle commented Jul 15, 2022 •

edited

Loading

jfehrle commented Jul 15, 2022 •

edited

Loading

jfehrle Jul 28, 2022 •

edited

Loading

jfehrle Jul 30, 2022 •

edited

Loading

jfehrle commented Jul 31, 2022 •

edited

Loading

jfehrle commented Aug 4, 2022 •

edited

Loading