Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Install the .v files of Coq theories along with their .vo files #3384

Merged
merged 2 commits into from Apr 17, 2020

Conversation

lthms
Copy link
Contributor

@lthms lthms commented Apr 17, 2020

With this patch, we mimic the behavior of coq_makefile, which is to
install not only the .vo files of a Coq theories (produced by coqc)
but also the .v file. This is useful for Coq-related tools such a
Proof General, which use them to implement “goto definition”-like
feature.

Fixes issue #3383

@lthms lthms requested a review from ejgallego as a code owner Apr 17, 2020
@ejgallego ejgallego added the coq label Apr 17, 2020
@@ -409,16 +409,20 @@ let install_rules ~sctx ~dir s =
in
Dir_contents.coq dir_contents
|> Coq_sources.library ~name
|> List.map ~f:(fun (vfile : Coq_module.t) ->
|> List.concat_map ~f:(fun (vfile : Coq_module.t) ->
let to_path f = Path.reach ~from:(Path.build dir) (Path.build f) in
Copy link
Collaborator

@ejgallego ejgallego Apr 17, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems to me that this function could be useful also for OCaml once it gets qualified subdir support?

Should we move it to Path @rgrinberg ?

Copy link
Member

@rgrinberg rgrinberg Apr 17, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For now, let's keep it here. In fact, we are trying to avoid adding dune specific stuff to Path and make it a more general purpose module.

Copy link
Collaborator

@ejgallego ejgallego Apr 17, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, I was thinking that'd be a general function tho, "relocate" ? My main gripe is that the current implementation doesn't seem very efficient, but not a big deal indeed.

Copy link
Collaborator

@ejgallego ejgallego left a comment

Great thanks; please add an entry in the CHANGES file, you will also have to update the test-suite, it can be done using make test-coq then make promote once you have reviewed the changes.

@ejgallego
Copy link
Collaborator

@ejgallego ejgallego commented Apr 17, 2020

See related issue #3383

This should really be "fixes #3383" right?

@ejgallego
Copy link
Collaborator

@ejgallego ejgallego commented Apr 17, 2020

we mimic the behavior of coq_makefile, which is to
install not only the .vo files of a Coq theories (produced by coqc)
but also the .v file.

We also mimic what Dune does for OCaml so indeed that's more uniform within Dune itself. I didn't look at how the rules are in the OCaml land but they should be pretty straightforward.

@lthms
Copy link
Contributor Author

@lthms lthms commented Apr 17, 2020

Wrt. the test-suite, it looks like rather adding a new case, I shall probably update the one which failed in the CI, right?

@ejgallego
Copy link
Collaborator

@ejgallego ejgallego commented Apr 17, 2020

Wrt. the test-suite, it looks like rather adding a new case, I shall probably update the one which failed in the CI, right?

Yes, in this case updating the existing ones should do the trick as your change applies to all public Coq theories, see my comment above on how to do it.

Signed-off-by: Thomas Letan <lthms@soap.coffee>
@lthms lthms force-pushed the install-v-files branch 2 times, most recently from 6ea8f5c to fea9485 Compare Apr 17, 2020
@lthms
Copy link
Contributor Author

@lthms lthms commented Apr 17, 2020

It seems to me that this function could be useful also for OCaml once it gets qualified subdir support?

Should we move it to Path @rgrinberg ?

I can definitely do that, indeed.

We also mimic what Dune does for OCaml […]

I reworded the patch description according to your feedback.

Great thanks; please add an entry in the CHANGES file, you will also have to update the test-suite, it can be done using make test-coq then make promote once you have reviewed the changes.

I did what you asked (I actually had to add a missing EOF to make the test-suite pass). AFAICT, make promote did nothing to the source tree. What is it suppose to do?

Anyway, I have updated the PR accordingly.

@lthms lthms changed the title Install the .v file of Coq theories along with their .vo files Install the .v files of Coq theories along with their .vo files Apr 17, 2020
@rgrinberg
Copy link
Member

@rgrinberg rgrinberg commented Apr 17, 2020

Looks good to me. Did you run $ make fmt?

With this patch, we mimic the behavior of coq_makefile and of dune
itself with OCaml libraries, which is to install not only “interface
file” (the .vo files of a Coq theories in our cases) but also the
source files (.v file). This is useful for Coq-related tools such a
Proof General, which use them to implement “goto definition”-like
feature.

This fixes ocaml#3383

Signed-off-by: Thomas Letan <lthms@soap.coffee>
@lthms
Copy link
Contributor Author

@lthms lthms commented Apr 17, 2020

I just did!

@ejgallego
Copy link
Collaborator

@ejgallego ejgallego commented Apr 17, 2020

Thanks, it looks good to me! Will merge soon so it can reach 2.5.1.

@lthms
Copy link
Contributor Author

@lthms lthms commented Apr 17, 2020

I’m happy to read that. (: It is fortunate that Travis is also happy with my PR, as all is green!

@ejgallego ejgallego merged commit 4c57ab8 into ocaml:master Apr 17, 2020
3 checks passed
rgrinberg added a commit to rgrinberg/opam-repository that referenced this issue Apr 17, 2020
…lugin, dune-private-libs and dune-glob (2.5.1)

CHANGES:

- [coq] Fix install .v files for Coq theories (ocaml/dune#3384, @lthms)

- [coq] Fix install path for theory names with level greater than 1 (ocaml/dune#3358,
  @ejgallego)

- Fix a bug introduced in 2.0.0 where the [locks] field in rules with no targets
  had no effect. (@aalekseyev, report by @CraigFe)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
Status: Done
Development

Successfully merging this pull request may close these issues.

None yet

3 participants