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.

Sign up for GitHub

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

Jump to bottom

[coq] Add .aux & .glob files as targets #3721

Merged
merged 4 commits into from
Aug 25, 2020
Merged

[coq] Add .aux & .glob files as targets #3721

merged 4 commits into from
Aug 25, 2020

Conversation

rgrinberg
Copy link
Member

Fix #3437

@gares @ejgallego should .aux files be installed as well?

@rgrinberg rgrinberg requested a review from ejgallego as a code owner August 18, 2020 20:55
@rgrinberg rgrinberg mentioned this pull request Aug 18, 2020
Closed
@rgrinberg rgrinberg added this to the 2.8 milestone Aug 19, 2020
@gares
Copy link
Contributor

gares commented Aug 19, 2020

No they should not.

In particular, Coq records in there some info that can improve user experience when compiling the same files again, which is not something you are supposed to do with v/vo files that are installed system wise.

@rgrinberg
Copy link
Member Author

Thanks. In that case, this PR is ready.

@rgrinberg rgrinberg changed the title [coq] Add .aux files as targets [coq] Add .aux & .glob files as targets Aug 21, 2020
@rgrinberg
Copy link
Member Author

I've amended the PR to include .glob files as targets.

@gares I assume these should not be installed either.

@yannl35133 should fix #3693

@rgrinberg rgrinberg force-pushed the coq-aux branch 2 times, most recently from 0799ffa to e0b5678 Compare August 21, 2020 23:08
@gares
Copy link
Contributor

gares commented Aug 22, 2020

Glob files are used to generate html hyperlinks by coqdoc, which I guess you run as part of the build, so no need to install them.

@ejgallego
Copy link
Collaborator

This is OK I think, thanks @rgrinberg ; I left .aux files out on purpose as they are indeed more of an ide thing.

I was planning to add .glob files once we do support cqqdoc; rules are pretty easy so it should be a matter of spending some minutes. I think .glob files should be installed for Coq to generate proper hyperlinks to installed libs, but I'm not sure.

Install rules for them can be anyways be added on the coqdoc PR.

A bit of a tricky point for this files is that there are some options that do indeed suppress / alter them. So indeed the set of output targets depends on the flags; my plan for that was to introduce a Coq_flags module that could provide information about compilation outputs.

This PR will break dune for example when coqc is used with -noglob or -dump-glob file ; I guess both options are mostly obsolete, for example -dump-glob was mostly used to implement more hygienic builds.

I'm a bit wary of adding support for .aux files tho, in the sense that it could be the case that they are not generated anymore in future Coq versions, so I dunno.

@rgrinberg
Copy link
Member Author

A bit of a tricky point for this files is that there are some options that do indeed suppress / alter them. So indeed the set of output targets depends on the flags; my plan for that was to introduce a Coq_flags module that could provide information about compilation outputs.

Makes sense. Although we also have a plan in dune for binaries to announce their targets dynamically. It's not without its own disadvantages, but at least it would allow us to keep all this information on one side.

I'm a bit wary of adding support for .aux files tho, in the sense that it could be the case that they are not generated anymore in future Coq versions, so I dunno.

This can probably be handled by dune getting the version of Coq. We do the same for OCaml for some flags, and it's a useful feature for other coq users I bet.

@rgrinberg
Copy link
Member Author

@ejgallego is this PR ok to go? Your comment suggests approval but you haven't approved it through github.

ejgallego
ejgallego approved these changes Aug 25, 2020
View reviewed changes
Copy link
Collaborator

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

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

LGTM, sorry for the lack of explicit approval.

@rgrinberg
Follow dune's convention of [t] comes first
81fd617 
Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
@rgrinberg
[coq] Add .aux files as targets
5cf12d6 
Fix ocaml#3437

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
@rgrinberg
Add .glob files as coqc targets as well
02ad41a 
Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
@rgrinberg
Clean up coq obj handling
fb9e7fa 
All the obj related functions are basically the same. One function +
enum is enough to handle everything.

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
@rgrinberg rgrinberg merged commit ee9bf53 into ocaml:master Aug 25, 2020
rgrinberg added a commit to rgrinberg/opam-repository that referenced this pull request Sep 3, 2020
@rgrinberg
[new release] dune-build-info, dune, dune-configurator, dune-action-p…
f714744 
…lugin, dune-private-libs and dune-glob (2.7.1)

CHANGES:

- configurator: More flexible probing of `#define`. We allow duplicate values in
  the object file, as long as they are the same after parsing. (ocaml/dune#3739, fixes
  ocaml/dune#3736, @rgrinberg)

- Record instrumentation backends in dune-package files. This makes it possible
  to use instrumentation backends defined in installed libraries (eg via OPAM).
  (ocaml/dune#3735, @nojb)

- Add missing `.aux` & `.glob` targets to coq rules (ocaml/dune#3721, fixes ocaml/dune#3437,
  @rgrinberg)

- Fix `dune-package` installation when META templates are present (ocaml/dune#3743, fixes
  ocaml/dune#3746, @rgrinberg)

- Resolve symlinks before running `$ git diff` (ocaml/dune#3750, fixes ocaml/dune#3740, @rgrinberg)

- Cram tests: when checking that all test directories contain a `run.t` file,
  skip empty directories. These can be left around by git. (ocaml/dune#3753, @emillon)
@rgrinberg rgrinberg mentioned this pull request Sep 3, 2020
Merged
rgrinberg added a commit to rgrinberg/opam-repository that referenced this pull request Sep 5, 2020
@rgrinberg
[new release] dune-build-info, dune, dune-configurator, dune-action-p…
8250214 
…lugin, dune-private-libs and dune-glob (2.7.1)

CHANGES:

- configurator: More flexible probing of `#define`. We allow duplicate values in
  the object file, as long as they are the same after parsing. (ocaml/dune#3739, fixes
  ocaml/dune#3736, @rgrinberg)

- Record instrumentation backends in dune-package files. This makes it possible
  to use instrumentation backends defined in installed libraries (eg via OPAM).
  (ocaml/dune#3735, @nojb)

- Add missing `.aux` & `.glob` targets to coq rules (ocaml/dune#3721, fixes ocaml/dune#3437,
  @rgrinberg)

- Fix `dune-package` installation when META templates are present (ocaml/dune#3743, fixes
  ocaml/dune#3746, @rgrinberg)

- Resolve symlinks before running `$ git diff` (ocaml/dune#3750, fixes ocaml/dune#3740, @rgrinberg)

- Cram tests: when checking that all test directories contain a `run.t` file,
  skip empty directories. These can be left around by git. (ocaml/dune#3753, @emillon)
@Alizter Alizter added the coq label Jun 6, 2022
@Alizter Alizter mentioned this pull request May 30, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ejgallego ejgallego ejgallego approved these changes

Assignees
No one assigned
Labels
coq
Projects
Coq + Dune
Archived in project
Milestone
2.8
Development

Successfully merging this pull request may close these issues.

aux files set-up as read-only
4 participants
@rgrinberg @gares @ejgallego @Alizter