Skip to content

[coq] Fix composition of boot library when it has plugins, add field to allow libraries to opt out of stdlib#6165

Merged
ejgallego merged 5 commits intoocaml:mainfrom
ejgallego:coq+fix_boot_plugins
Sep 28, 2022
Merged

[coq] Fix composition of boot library when it has plugins, add field to allow libraries to opt out of stdlib#6165
ejgallego merged 5 commits intoocaml:mainfrom
ejgallego:coq+fix_boot_plugins

Conversation

@ejgallego
Copy link
Copy Markdown
Collaborator

@ejgallego ejgallego commented Sep 27, 2022

We fix a bug introduced in #5866 , which prevented the composition to work when a boot library has plugins.

The approach of #5866 is essentially reverted, there are many places (such as source_rule for coqdep) which must be handled properly for a boot library, so we add it back to the list of libraries if required.

Motivated by #6163 , we add in passing a flag to coq theories that allows to opt out of this addition, and moreover if present will instruct coqc to ignore a boot / stdlib library if present.

This was referenced Sep 27, 2022
Closed
Merged
@ejgallego ejgallego added the coq label Sep 27, 2022
@ejgallego
[coq] [test suite] Better name for compose boot no dups test.
96fd279 
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
@ejgallego
[coq] [test] Add test for missing plugins flags from boot (issue intr…
27f1c04 
…oduced in ocaml#5866)

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
LasseBlaauwbroek
LasseBlaauwbroek reviewed Sep 27, 2022
View reviewed changes
@ejgallego
Copy link
Copy Markdown
Collaborator Author

ejgallego commented Sep 27, 2022

@Alizter this seems to work pretty well on HoTT and stdlib2 , so that's good news IMHO.

@Alizter Alizter self-requested a review September 28, 2022 11:23
Alizter
Alizter reviewed Sep 28, 2022
View reviewed changes
test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/dune-workspace
@@ -0,0 +1 @@
(lang dune 3.4)
Copy link
Copy Markdown
Collaborator

@Alizter Alizter Sep 28, 2022

Choose a reason for hiding this comment

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

Don't we need (using coq 0.5) here as well? Seems like a bug.

Copy link
Copy Markdown
Collaborator Author

@ejgallego ejgallego Sep 28, 2022

Choose a reason for hiding this comment

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

I don't think so, but not expert on workspaces.

@ejgallego
[coq] Re-add boot library to list of dependencies in Coq_lib.DB
614ce7d 
Should fix a bug introduced in ocaml#5866 , the handling of boot Coq lib
really needs to be done at the top level as coqdep's `source_rule`
etc... need to be aware of it.

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
@ejgallego
[coq] Small refactor of plugin dep code.
3582ba2 
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
@ejgallego
[coq] Generate flags correctly for use_stdlib
4e6d57f 
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
@Alizter
Copy link
Copy Markdown
Collaborator

Alizter commented Sep 28, 2022

LGTM and to merge

@ejgallego ejgallego merged commit ad37847 into ocaml:main Sep 28, 2022
@ejgallego ejgallego deleted the coq+fix_boot_plugins branch September 28, 2022 17:50
@emillon emillon mentioned this pull request Oct 11, 2022
Closed
emillon added a commit to emillon/opam-repository that referenced this pull request Oct 11, 2022
@emillon
[new release] xdg, stdune, ordering, ocamlc-loc, fiber, dyn, dune, du…
3b35c07 
…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~alpha1)

CHANGES:

- 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, fixes
  ocaml/dune#5650, @emillon)

- Added an (aliases ...) field to the (rules ...) stanza which allows the
  specification of multiple aliases per rule (ocaml/dune#6194, @Alizter)
@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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Alizter Alizter Alizter approved these changes

+1 more reviewer

@LasseBlaauwbroek LasseBlaauwbroek LasseBlaauwbroek left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

coq

Projects

Coq + Dune
Archived in project

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@ejgallego @Alizter @LasseBlaauwbroek