[coq] Add dependency to META file for Coq plugins#6167
Merged
ejgallego merged 2 commits intoocaml:mainfrom Oct 11, 2022
Merged
Conversation
14f44ff to
1bb1e2e
Compare
Alizter
reviewed
Oct 2, 2022
Alizter
approved these changes
Oct 6, 2022
rgrinberg
approved these changes
Oct 7, 2022
b739d97 to
eb45aad
Compare
48e34b2 to
c18b4f1
Compare
Alizter
reviewed
Oct 9, 2022
9ab842a to
204090e
Compare
Alizter
approved these changes
Oct 9, 2022
204090e to
041c5c8
Compare
2cefe23 to
3cdc4d8
Compare
christinerose
previously requested changes
Oct 10, 2022
Contributor
christinerose
left a comment
There was a problem hiding this comment.
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.
Collaborator
Author
|
Thanks a lot @christinerose , comments addressed! |
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 rocq-prover/rocq#16571 Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
3cdc4d8 to
bc980a1
Compare
Contributor
|
So it's |
Collaborator
Author
I chose 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! |
Changes implemented, thanks!
emillon
added a commit
to emillon/opam-repository
that referenced
this pull request
Oct 19, 2022
…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)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Traditionally,
coqdeprequires the source files of all involvedtheories to be present in the filesystem, as to resolve logical paths
to files.
For
.vfiles this process is easy, however for plugins,coqdeprelies on the presence of a
plugin.mlpackfile as a hint that aplugin.cmxsfile will be produced, so it can correctly mapDeclare Mlto the right.cmxs.Starting with 8.16,
coqdepcan alternatively useMETAfiles to dothis mapping, but that requires
METAfiles to be present in thebuild tree, at the right path pointed by
OCAMLPATH.We thus add the
METAfiles as a dependency for coqdep, which isbackwards 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
METAfiles), so this willneed fixing in Coq to fully work, but this is the Dune part, so the
rest of work belongs to Coq upstream IIANM.