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 dependency to META file for Coq plugins #6167

Merged
merged 2 commits into from
Oct 11, 2022
Merged

[coq] Add dependency to META file for Coq plugins #6167

merged 2 commits into from
Oct 11, 2022

Conversation

ejgallego
Copy link
Collaborator

Traditionally, coqdep requires the source files of all involved
theories to be present in the filesystem, as to resolve logical paths
to files.

For .v files this process is easy, however for plugins, coqdep
relies on the presence of a plugin.mlpack file as a hint that a
plugin.cmxs file will be produced, so it can correctly map Declare Ml to the right .cmxs.

Starting with 8.16, coqdep can alternatively use META files to do
this mapping, but that requires META files to be present in the
build tree, at the right path pointed by OCAMLPATH.

We thus add the META files as a dependency for coqdep, which is
backwards compatible and will allow us to fix Dune to work with the
new findlib-based plugin loading method in Coq 8.16.

Unfortunately, the code in Coq upstream seems pretty broken (it seems
to produce paths that are wrong w.r.t. our META files), so this will
need fixing in Coq to fully work, but this is the Dune part, so the
rest of work belongs to Coq upstream IIANM.

@ejgallego ejgallego added the coq label Sep 28, 2022
@Alizter Alizter self-requested a review September 28, 2022 17:50
@ejgallego ejgallego mentioned this pull request Sep 28, 2022
Closed
@ejgallego ejgallego added this to the 3.5.0 milestone Sep 29, 2022
Alizter
Alizter reviewed Oct 2, 2022
View reviewed changes
CHANGES.md Outdated Show resolved Hide resolved
src/dune_rules/coq_rules.ml Outdated Show resolved Hide resolved
@Alizter Alizter self-requested a review October 2, 2022 03:21
@ejgallego ejgallego force-pushed the coq+add_meta_dep_for_plugins branch 2 times, most recently from b739d97 to eb45aad Compare October 9, 2022 20:44
@ejgallego ejgallego force-pushed the coq+add_meta_dep_for_plugins branch 5 times, most recently from 48e34b2 to c18b4f1 Compare October 9, 2022 21:28
Alizter
Alizter reviewed Oct 9, 2022
View reviewed changes
CHANGES.md Outdated Show resolved Hide resolved
@ejgallego ejgallego force-pushed the coq+add_meta_dep_for_plugins branch 2 times, most recently from 9ab842a to 204090e Compare October 9, 2022 21:45
@ejgallego ejgallego mentioned this pull request Oct 9, 2022
Merged
@ejgallego ejgallego force-pushed the coq+add_meta_dep_for_plugins branch 3 times, most recently from 2cefe23 to 3cdc4d8 Compare October 10, 2022 14:27
Alizter
Alizter reviewed Oct 10, 2022
View reviewed changes
Copy link
Collaborator

@Alizter Alizter left a comment

Choose a reason for hiding this comment

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

LGTM let's merge

christinerose
christinerose previously requested changes Oct 10, 2022
View reviewed changes
Copy link
Collaborator

@christinerose christinerose left a comment

Choose a reason for hiding this comment

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

Mostly minor formatting/grammar, but I do have a question around the formatting of Findlib, findlib, or findlib. I'd like to get a definitive answer on this so I can update the style guide.

CHANGES.md Outdated Show resolved Hide resolved
CHANGES.md Outdated Show resolved Hide resolved
CHANGES.md Outdated Show resolved Hide resolved
test/blackbox-tests/test-cases/coq/plugin-private.t/run.t Outdated Show resolved Hide resolved
@ejgallego
Copy link
Collaborator Author

Thanks a lot @christinerose , comments addressed!

@ejgallego
[coq] Add dependency to META file for Coq plugins
bc980a1 
Traditionally, `coqdep` requires the source files of all involved
theories to be present in the filesystem, as to resolve logical paths
to files.

For `.v` files this process is easy, however for plugins, `coqdep`
relies on the presence of a `plugin.mlpack` file as a hint that a
`plugin.cmxs` file will be produced, so it can correctly map `Declare
Ml` to the right `.cmxs`.

Starting with 8.16, `coqdep` can alternatively use `META` files to do
this mapping, but that requires `META` files to be present in the
build tree, at the right path pointed by `OCAMLPATH`.

We thus add the `META` files as a dependency for coqdep, which is
backwards compatible and will allow us to fix Dune to work with the
new findlib-based plugin loading method in Coq 8.16.

Unfortunately, the code in Coq upstream seems pretty broken (it seems
to produce paths that are wrong w.r.t. our `META` files), so this will
need fixing in Coq to fully work, but this is the Dune part, so the
rest of work belongs to Coq upstream IIANM.

The issue upstream is coq/coq#16571

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
@christinerose
Copy link
Collaborator

So it's Findlib then, @ejgallego? I'll update the style guide! Thanks!

@ejgallego
Copy link
Collaborator Author

So it's Findlib then, @ejgallego? I'll update the style guide! Thanks!

I chose Findlib but I'm unsure what's best. Do you have a pointer to the style guide place where this is discussed?

I will merge the PR today as the 3.5.0 release is imminent and this is important for Coq upstream, but I'm happy to fix the style of this later if needed. Thanks again!

@ejgallego ejgallego dismissed christinerose’s stale review October 11, 2022 22:41

Changes implemented, thanks!

@ejgallego ejgallego merged commit 713b5c5 into ocaml:main Oct 11, 2022
@ejgallego ejgallego deleted the coq+add_meta_dep_for_plugins branch October 11, 2022 23:07
@Alizter Alizter mentioned this pull request Oct 13, 2022
Open
@emillon emillon mentioned this pull request Oct 19, 2022
Merged
emillon added a commit to emillon/opam-repository that referenced this pull request Oct 19, 2022
@emillon
[new release] xdg, stdune, ordering, ocamlc-loc, fiber, dyn, dune, du…
2996546 
…ne-site, dune-rpc, dune-rpc-lwt, dune-private-libs, dune-glob, dune-configurator, dune-build-info, dune-action-plugin and chrome-trace (3.5.0)

CHANGES:

- macOS: Handle unknown fsevents without crashing (ocaml/dune#6217, @rgrinberg)

- Enable file watching on MacOS SDK < 10.13. (ocaml/dune#6218, @rgrinberg)

- Sandbox running cinaps actions starting from cinaps 1.1 (ocaml/dune#6176, @rgrinberg)

- Add a `runtime_deps` field in the `cinaps` stanza to specify runtime
  dependencies for running the cinaps preprocessing action (ocaml/dune#6175, @rgrinberg)

- Shadow alias module `Foo__` when building a library `Foo` (ocaml/dune#6126, @rgrinberg)

- Extend dune describe to include the root path of the workspace and the
  relative path to the build directory. (ocaml/dune#6136, @reubenrowe)

- Allow dune describe workspace to accept directories as arguments.
  The provided directories restrict the worskpace description to those
  directories. (ocaml/dune#6107, fixes ocaml/dune#3893, @esope)

- Add a terminal persistence mode that attempts to clear the terminal history.
  It is enabled by setting terminal persistence to
  `clear-on-rebuild-and-flush-history` (ocaml/dune#6065, @rgrinberg)

- Disallow generating targets in sub direcories in inferred rules. The check to
  forbid this was accidentally done only for manually specified targets (ocaml/dune#6031,
  @rgrinberg)

- Do not ignore rules marked `(promote (until-clean))` when
  `--ignore-promoted-rules` (or `-p`) is passed. (ocaml/dune#6010, fixes ocaml/dune#4401, @emillon)

- Dune no longer considers .aux files as targets during Coq compilation. This
  means that .aux files are no longer cached. (ocaml/dune#6024, fixes ocaml/dune#6004, @Alizter)

- Cinaps actions are now sandboxed by default (ocaml/dune#6062, @rgrinberg)

- Allow rules producing directory targets to be not sandboxed (ocaml/dune#6056,
  @rgrinberg)

- Introduce a `dirs` field in the `install` stanza to install entire
  directories (ocaml/dune#5097, fixes ocaml/dune#5059, @rgrinberg)

- Menhir rules are now sandboxed by default (ocaml/dune#6076, @rgrinberg)

- Allow rules producing directory targets to create symlinks (ocaml/dune#6077, fixes
  ocaml/dune#5945, @rgrinberg)

- Inline tests are now sandboxed by default (ocaml/dune#6079, @rgrinberg)

- Fix build-info version when used with flambda (ocaml/dune#6089, fixes ocaml/dune#6075, @jberdine)

- Add an `(include <file>)` term to the `include_dirs` field for adding
  directories to the include paths sourced from a file. (ocaml/dune#6058, fixes ocaml/dune#3993,
  @gridbugs)

- Support `(extra_objects ...)` field in `(executable ...)` and `(library
  ...)` stanzas (ocaml/dune#6084, fixes ocaml/dune#4129, @gridbugs)

- Fix compilation of Dune under esy on Windows (ocaml/dune#6109, fixes ocaml/dune#6098, @nojb)

- Improve error message when parsing several licenses in `(license)` (ocaml/dune#6114,
  fixes ocaml/dune#6103, @emillon)

- odoc rules now about `ODOC_SYNTAX` and will rerun accordingly (ocaml/dune#6010, fixes
  ocaml/dune#1117, @emillon)

- dune install: copy files in an atomic way (ocaml/dune#6150, @emillon)

- Add `%{coq:...}` macro for accessing data about the configuration about Coq.
  For instance `%{coq:version}` (ocaml/dune#6049, @Alizter)

- update vendored copy of cmdliner to 1.1.1. This improves the built-in
  documentation for command groups such as `dune ocaml`. (ocaml/dune#6038, @emillon,
  ocaml/dune#6169, @shonfeder)

- The test suite for Coq now requires Coq >= 8.16 due to changes in the
  plugin loading mechanism upstream (which now uses `Findlib`).

- Starting with Coq build language 0.6, theories can be built without importing
  Coq's standard library by including `(stdlib no)`.
  (ocaml/dune#6165 ocaml/dune#6164, fixes ocaml/dune#6163, @ejgallego @Alizter @LasseBlaauwbroek)

- on macOS, sign executables produced by artifact substitution (ocaml/dune#6137, ocaml/dune#6231,
  fixes ocaml/dune#5650, fixes ocaml/dune#6226, @emillon)

- Added an (aliases ...) field to the (rules ...) stanza which allows the
  specification of multiple aliases per rule (ocaml/dune#6194, @Alizter)

- The `(coq.theory ...)` stanza will now ensure that for each declared `(plugin
 ...)`, the `META` file for it is built before calling `coqdep`. This enables
 the use of the new `Findlib`-based loading method in Coq 8.16; however as of
 Coq 8.16.0, Coq itself has some bugs preventing this to work yet. (ocaml/dune#6167 ,
 workarounds ocaml/dune#5767, @ejgallego)

- Allow include statement in install stanza (ocaml/dune#6139, fixes ocaml/dune#256, @gridbugs)

- Handle CSI n K code in ANSI escape codes from commands. (ocaml/dune#6214, fixes ocaml/dune#5528,
  @emillon)

- Add a new experimental feature `mode_specific_stubs` that allows the
  specification of different flags and sources for foreign stubs depending on
  the build mode (ocaml/dune#5649, @voodoos)
@ejgallego ejgallego mentioned this pull request Sep 20, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@christinerose christinerose christinerose left review comments

@Alizter Alizter Alizter approved these changes

@rgrinberg rgrinberg rgrinberg approved these changes

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

Successfully merging this pull request may close these issues.
4 participants
@ejgallego @christinerose @rgrinberg @Alizter