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

adds support for loading plugins in toplevels #6082

Merged
merged 5 commits into from
Mar 7, 2023

Conversation

ivg
Copy link
Member

@ivg ivg commented Aug 17, 2022

To load a file in toplevel we should use Topdirs.dir_load (or Toploop.load_file) instead of Dynlink as the latter is not allowed in the toplevel environment. The problem, however, is that Topdirs is only available in the bytecode mode so we can't just do if !Sys.interactive then .... The trick that we are using in the BAP plugin systems is to have a hidden reference to the load function that is overridden with Topdirs's one when we are loading from a toplevel.

The proposed solution is different and relies on virtual libraries with the default library using Dynlink as the loader. To be able to use plugins from the toplevel, we need to add dune-site.toplevel to the libraries stanza.

Do you think this is user-friendly enough? Ideally, I would like to have magic, so that will pick the proper implementation without me having to specify it explicitly.

Another thing that could be improved is error reporting. Right now the toplevel load function will bark into stderr and ignore failed plugins. I can turn this into the invalid_arg exceptions, or maybe you prefer another exception instead? We capture the output and failwith it. Is it fine?

Fixes #6081 (at least the main issue).

@ivg ivg force-pushed the dune-plugins-toplevel branch 2 times, most recently from a3e0aff to 98e83b1 Compare August 17, 2022 20:27
@rgrinberg rgrinberg requested a review from bobot August 17, 2022 21:07
@ivg ivg force-pushed the dune-plugins-toplevel branch 3 times, most recently from 8067469 to c890df6 Compare August 18, 2022 14:11
ivg added a commit to ivg/bap that referenced this pull request Aug 18, 2022
Both require ocaml/dune#6082
And bap.top only works inside `baptop` but not vanila
`utop` or `ocaml`, see ocaml/dune#6081
@ivg ivg force-pushed the dune-plugins-toplevel branch from c890df6 to 14874d8 Compare August 18, 2022 21:18
ivg added a commit to ivg/bap that referenced this pull request Aug 31, 2022
Both require ocaml/dune#6082
And bap.top only works inside `baptop` but not vanila
`utop` or `ocaml`, see ocaml/dune#6081
@ivg ivg force-pushed the dune-plugins-toplevel branch from 14874d8 to f64d8ff Compare August 31, 2022 15:15
ivg added a commit to ivg/bap that referenced this pull request Aug 31, 2022
Both require ocaml/dune#6082
And bap.top only works inside `baptop` but not vanila
`utop` or `ocaml`, see ocaml/dune#6081
ivg added a commit to ivg/bap that referenced this pull request Aug 31, 2022
Both require ocaml/dune#6082
And bap.top only works inside `baptop` but not vanila
`utop` or `ocaml`, see ocaml/dune#6081
@ivg ivg force-pushed the dune-plugins-toplevel branch from f64d8ff to cd79741 Compare December 19, 2022 15:42
@ivg
Copy link
Member Author

ivg commented Dec 19, 2022

@bobot I rebased the PR, could you please take a look and give some feedback? We are blocked on this feature. We need to be able to load plugins in top-level, see BinaryAnalysisPlatform/bap#1561

Copy link
Collaborator

@bobot bobot left a comment

Choose a reason for hiding this comment

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

I didn't know this deficiency of the top-level. The solution is sound, even if it would be nice at some point in the future to not have this restriction in the top-level itself. (EDIT: https://github.com/ocaml/dune/wiki/OCamlFeatureRequest is updated with this possibility)

Still could you add some tests, please? You can extend the existing one for plugins.

@ivg ivg force-pushed the dune-plugins-toplevel branch from cd79741 to 7db3a72 Compare January 10, 2023 15:31
@richardlford
Copy link
Contributor

@ivg, @rgrinberg, @bobot: I'm helping @ivg with this PR by adding tests. So far I've just done a rebase, but will be adding tests soon.

@richardlford richardlford force-pushed the dune-plugins-toplevel branch 2 times, most recently from 9c758df to c62fce6 Compare February 22, 2023 20:03
richardlford added a commit to ivg/dune that referenced this pull request Feb 22, 2023
This is in support of PR ocaml#6082.

Signed-off-by: Richard L Ford <[email protected]>
@richardlford
Copy link
Contributor

@ivg, @bobot, @rgrinberg: I have added a test of the new functionality. Please review whether you think it is adequate.

@ivg
Copy link
Member Author

ivg commented Feb 22, 2023

Looks good to me! And thanks a lot for helping with this!

@ivg ivg requested a review from bobot February 22, 2023 20:24
@richardlford
Copy link
Contributor

richardlford commented Feb 22, 2023

@ivg, @bobot, @rgrinberg: I have reproduced the failing dune build when using OCaml 4.12.1 (though on Linux, not Windows). This is the failure:

$ dune build @install
File "otherlibs/site/src/plugins/linker/toplevel/linker.ml", line 4, characters 8-25:
4 |   match Toploop.load_file ppf filename with
            ^^^^^^^^^^^^^^^^^
Error: Unbound value Toploop.load_file

I seem to remembers seeing something about changing visibility of Toploop vs. Topmain. I will investigate, but if any of you already know the solution, that will save me time. Thanks.

richardlford added a commit to ivg/dune that referenced this pull request Feb 24, 2023
This is in support of PR ocaml#6082.

Signed-off-by: Richard L Ford <[email protected]>
@richardlford richardlford force-pushed the dune-plugins-toplevel branch 2 times, most recently from 38f55e8 to 9078cac Compare March 6, 2023 14:50
@richardlford
Copy link
Contributor

@ivg, @bobot, @rgrinberg, @anmonteiro, @Alizter: Ping? I did a fresh rebase and thought I might add a little more documentation. Is there anything else that might prevent this from being merged?

@richardlford
Copy link
Contributor

@ivg, @bobot, @rgrinberg, @anmonteiro, @Alizter, @christinerose : I pushed what I think should be the last update for this PR. I documented the need to use the dune-sites.toplevel library if you are creating a toplevel with plugins. I also added a couple more tests.

@richardlford
Copy link
Contributor

The two failures both seem related to recent melange commits. I don't think they are caused by this change.

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.

Approving for convenience. There are just a few suggestions around formatting and consistency. :) Hope it helps!

doc/sites.rst Outdated Show resolved Hide resolved
test/blackbox-tests/test-cases/toplevel-plugin-fail.t Outdated Show resolved Hide resolved
test/blackbox-tests/test-cases/toplevel-plugin-fail2.t Outdated Show resolved Hide resolved
Copy link
Collaborator

@bobot bobot left a comment

Choose a reason for hiding this comment

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

The tests for dune-site are in otherlibs/site/test. It is not the first time that people miss them. Perhaps (in another MR) it should be moved to test.

@richardlford richardlford force-pushed the dune-plugins-toplevel branch from e1836d3 to 03da11a Compare March 7, 2023 15:23
@richardlford
Copy link
Contributor

@christinerose, @bobot: Thanks for the feedback and approvals. I've rebased the PR. Should I do a squash?

@rgrinberg rgrinberg added this to the 3.8.0 milestone Mar 7, 2023
> (map_workspace_root false)
>
> (package
> (name top_with_plugins)
Copy link
Member

Choose a reason for hiding this comment

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

We indent dune files with a single space only.

Copy link
Contributor

Choose a reason for hiding this comment

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

We indent dune files with a single space only.

I will fix these.

@@ -0,0 +1,13 @@
open Topdirs [@@ocaml.warning "-33"]
open Toploop [@@ocaml.warning "-33"]
Copy link
Member

Choose a reason for hiding this comment

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

Why do we need these opens?

Copy link
Contributor

@richardlford richardlford Mar 7, 2023

Choose a reason for hiding this comment

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

Why do we need these opens?

Before 4.13.0, loadfile is in Topdirs. After it is in Toploop. We either need some kind of conditional compilation, or else just open both and let the compiler find it. Is there a better way?
I will add a comment explaining why the two opens.

Copy link
Member

Choose a reason for hiding this comment

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

No, this seems adequate. Could you add a comment in the source explaining this however

Copy link
Contributor

Choose a reason for hiding this comment

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

No, this seems adequate. Could you add a comment in the source explaining this however

Will do.

(library
(name dune_site_backend)
(public_name dune-site.linker)
(virtual_modules linker)
Copy link
Member

Choose a reason for hiding this comment

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

Could you leave a comment here to explain why this is virtual?

Copy link
Contributor

Choose a reason for hiding this comment

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

Could you leave a comment here to explain why this is virtual?

Will do.

ivg and others added 4 commits March 7, 2023 12:05
Uses virtual libraries to select the proper dynamic linker
facility. To load in the toplevel add `dune-site.toplevel` library as
the dependency to your toplevel.

Signed-off-by: ivg <[email protected]>
Signed-off-by: Richard L Ford <[email protected]>
1. Added documentation describing what is needed to make
a toplevel with plugins.

2. Added tests.

3. Also, handle moved load_file function.  Prior to OCaml 4.13.0, the
load_file function was in Topdirs.  Starting with OCaml 4.13.0, the
load_file function moved to Toploop. In order to find it open both
these modules, suppressing the warning for unused open, and then
reference load_file unqualified.

4. Also add change log entry.

Signed-off-by: Richard L Ford <[email protected]>
Editorial changes to doc/sites.rst,
test/blackbox-tests/test-cases/toplevel-plugin-fail.t, and
test/blackbox-tests/test-cases/toplevel-plugin-fail2.t.

Co-authored-by: Christine Rose <[email protected]>
Signed-off-by: Richard L Ford <[email protected]>
1. Add comment explaining why dune-site.linker is virtual.
2. Add comment explaining why two opens in toplevel/linker.ml.
3. Fix indentation of dune stanzas in tests.

Signed-off-by: Richard L Ford <[email protected]>
@richardlford richardlford force-pushed the dune-plugins-toplevel branch from 03da11a to c495a83 Compare March 7, 2023 18:17
@richardlford
Copy link
Contributor

@rgrinberg, I have responded to your feedback, rebased, and force-pushed. When you think it is ready, I can squash all the commits into one commit if you wish.

1. In a dune file, remove extra blank line.
2. In an ml comment, fix indentation.

Signed-off-by: Richard L Ford <[email protected]>
@richardlford
Copy link
Contributor

@rgrinberg, I have done another push to fix the formatting failure.

@rgrinberg rgrinberg merged commit 086a78c into ocaml:main Mar 7, 2023
@richardlford richardlford deleted the dune-plugins-toplevel branch March 7, 2023 19:00
@ivg
Copy link
Member Author

ivg commented Mar 8, 2023

thanks @richardlford a lot!

@richardlford
Copy link
Contributor

thanks @richardlford a lot!

@ivg, Glad to help.

emillon added a commit to emillon/opam-repository that referenced this pull request Apr 18, 2023
CHANGES:

- When a rule's action is interrupted, delete any leftover directory targets.
  This is consistent with how we treat file targets. (@rgrinberg, 7564)

- Fix plugin loading with findlib. The functionality was broken in 3.7.0.
  (ocaml/dune#7556, @anmonteiro)

- Introduce a `public_headers` field on libraries. This field is like
  `install_c_headers`, but it allows to choose the extension and choose the
  paths for the installed headers. (ocaml/dune#7512, @rgrinberg)

- Load the host context `findlib.conf` when cross-compiling (ocaml/dune#7428, fixes
  ocaml/dune#1701, @rgrinberg, @anmonteiro)

- Resolve `ppx_runtime_libraries` in the target context when cross compiling
  (ocaml/dune#7450, fixes ocaml/dune#2794, @anmonteiro)

- Use `$PKG_CONFIG`, when set, to find the `pkg-config` binary  (ocaml/dune#7469, fixes
  ocaml/dune#2572, @anmonteiro)

- Preliminary support for Coq compiled intefaces (`.vos` files) enabled via
  `(mode vos)` in `coq.theory` stanzas. This can be used in combination with
  `dune coq top` to obtain fast re-building of dependencies (with no checking
  of proofs) prior to stepping into a file. (ocaml/dune#7406, @rlepigre)

- Fix dune crashing on MacOS in watch mode whenever `$PATH` contains `$PWD`
  (ocaml/dune#7441, fixes ocaml/dune#6907, @rgrinberg)

- Fix `dune install` when cross compiling (ocaml/dune#7410, fixes ocaml/dune#6191, @anmonteiro,
  @rizo)

- Find `pps` dependencies in the host context when cross-compiling,  (ocaml/dune#7410,
  fixes ocaml/dune#4156, @anmonteiro)

- Dune in watch mode no longer builds concurrent rules in serial (ocaml/dune#7395
  @rgrinberg, @jchavarri)

- `dune coq top` now correctly respects the project root when called from a
  subdirectory. However, absolute filenames passed to `dune coq top` are no
  longer supported (due to being buggy) (ocaml/dune#7357, fixes ocaml/dune#7344, @rlepigre and
  @Alizter)

- Added a `--no-build` option to `dune coq top` for avoiding rebuilds (ocaml/dune#7380,
  fixes ocaml/dune#7355, @Alizter)

- RPC: Ignore SIGPIPE when clients suddenly disconnect (ocaml/dune#7299, ocaml/dune#7319, fixes
  ocaml/dune#6879, @rgrinberg)

- Always clean up the UI on exit. (ocaml/dune#7271, fixes ocaml/dune#7142 @rgrinberg)

- Bootstrap: remove reliance on shell. Previously, we'd use the shell to get
  the number of processors. (ocaml/dune#7274, @rgrinberg)

- Bootstrap: correctly detect the number of processors by allowing `nproc` to be
  looked up in `$PATH` (ocaml/dune#7272, @Alizter)

- Speed up file copying on macos by using `clonefile` when available
  (@rgrinberg, ocaml/dune#7210)

- Adds support for loading plugins in toplevels (ocaml/dune#6082, fixes ocaml/dune#6081,
  @ivg, @richardlford)

- Support commands that output 8-bit and 24-bit colors in the terminal (ocaml/dune#7188,
  @Alizter)

- Speed up rule generation for libraries and executables with many modules
  (ocaml/dune#7187, @jchavarri)

- Add `--watch-exclusions` to Dune build options (ocaml/dune#7216, @jonahbeckford)

- Do not re-render UI on every frame if the UI doesn't change (ocaml/dune#7186, fix
  ocaml/dune#7184, @rgrinberg)

- Make coq_db creation in scope lazy (@ejgallego, ocaml/dune#7133)

- Non-user proccesses such as version control or config checking are now run
  silently. (ocaml/dune#6994, fixes ocaml/dune#4066, @Alizter)

- Add the `--display-separate-messages` flag to separate the error messages
  produced by commands with a blank line. (ocaml/dune#6823, fixes ocaml/dune#6158, @esope)

- Accept the Ordered Set Language for the `modes` field in `library` stanzas
  (ocaml/dune#6611, @anmonteiro).

- dune install now respects --display quiet mode (ocaml/dune#7116, fixes ocaml/dune#4573, fixes
  ocaml/dune#7106, @Alizter)

- Stub shared libraries (dllXXX_stubs.so) in Dune-installed libraries could not
  be used as dependencies of libraries in the workspace (eg when compiling to
  bytecode and/or Javascript).  This is now fixed. (ocaml/dune#7151, @nojb)

- Allow the main module of a library with `(stdlib ...)` to depend on other
  libraries (ocaml/dune#7154, @anmonteiro).

- Bytecode executables built for JSOO are linked with `-noautolink` and no
  longer depend on the shared stubs of their dependent libraries (ocaml/dune#7156, @nojb)

- Added a new user action `(concurrent )` which is like `(progn )` but runs the
  actions concurrently. (ocaml/dune#6933, @Alizter)

- Allow `(stdlib ...)` to be used with `(wrapped false)` in library stanzas
  (ocaml/dune#7139, @anmonteiro).

- Allow parallel execution of inline tests partitions (ocaml/dune#7012, @hhugo)

- Support `(link_flags ...)` in `(cinaps ...)` stanza. (ocaml/dune#7423, fixes ocaml/dune#7416,
  @nojb)

- Allow `(package ...)` in any position within `(rule ...)` stanza (ocaml/dune#7445,
  @Leonidas-from-XIV)

- Always include `opam` files in the generated `.install` file. Previously, it
  would not be included whenever `(generate_opam_files true)` was set and the
  `.install` file wasn't yet generated. (ocaml/dune#7547, @rgrinberg)
emillon added a commit to emillon/opam-repository that referenced this pull request May 23, 2023
CHANGES:

- Fix string quoting in the json file written by `--trace-file` (ocaml/dune#7773,
  @rleshchinskiy)

- Read `pkg-config` arguments from the `PKG_CONFIG_ARGN` environment variable
  (ocaml/dune#1492, ocaml/dune#7734, @anmonteiro)

- Correctly set `MANPATH` in `dune exec`. Previously, we would use the `bin/`
  directory of the context. (ocaml/dune#7655, @rgrinberg)

- Allow overriding the `ocaml` binary with findlib configuration (ocaml/dune#7648,
  @rgrinberg)

- merlin: ignore instrumentation settings for preprocessing. (ocaml/dune#7606, fixes
  ocaml/dune#7465, @Alizter)

- When a rule's action is interrupted, delete any leftover directory targets.
  This is consistent with how we treat file targets. (ocaml/dune#7564, @rgrinberg)

- Fix plugin loading with findlib. The functionality was broken in 3.7.0.
  (ocaml/dune#7556, @anmonteiro)

- Introduce a `public_headers` field on libraries. This field is like
  `install_c_headers`, but it allows to choose the extension and choose the
  paths for the installed headers. (ocaml/dune#7512, @rgrinberg)

- Load the host context `findlib.conf` when cross-compiling (ocaml/dune#7428, fixes
  ocaml/dune#1701, @rgrinberg, @anmonteiro)

- Add a `coqdoc_flags` field to the `coq.theory` stanza allowing the user to
  pass extra arguments to `coqdoc`. (ocaml/dune#7676, fixes ocaml/dune#7954 @Alizter)

- Resolve `ppx_runtime_libraries` in the target context when cross compiling
  (ocaml/dune#7450, fixes ocaml/dune#2794, @anmonteiro)

- Use `$PKG_CONFIG`, when set, to find the `pkg-config` binary  (ocaml/dune#7469, fixes
  ocaml/dune#2572, @anmonteiro)

- Modules that were declared in `(modules_without_implementation)`,
  `(private_modules)` or `(virtual_modules)` but not declared in `(modules)`
  will cause Dune to emit a warning which will become an error in 3.9. (ocaml/dune#7608,
  fixes ocaml/dune#7026, @Alizter)

- Preliminary support for Coq compiled intefaces (`.vos` files) enabled via
  `(mode vos)` in `coq.theory` stanzas. This can be used in combination with
  `dune coq top` to obtain fast re-building of dependencies (with no checking
  of proofs) prior to stepping into a file. (ocaml/dune#7406, @rlepigre)

- Fix dune crashing on MacOS in watch mode whenever `$PATH` contains `$PWD`
  (ocaml/dune#7441, fixes ocaml/dune#6907, @rgrinberg)

- Fix `dune install` when cross compiling (ocaml/dune#7410, fixes ocaml/dune#6191, @anmonteiro,
  @rizo)

- Find `pps` dependencies in the host context when cross-compiling,  (ocaml/dune#7410,
  fixes ocaml/dune#4156, @anmonteiro)

- Dune in watch mode no longer builds concurrent rules in serial (ocaml/dune#7395
  @rgrinberg, @jchavarri)

- Dune can now detect Coq theories from outside the workspace. This allows for
  composition with installed theories (not necessarily installed with Dune).
  (ocaml/dune#7047, @Alizter, @ejgallego)

- `dune coq top` now correctly respects the project root when called from a
  subdirectory. However, absolute filenames passed to `dune coq top` are no
  longer supported (due to being buggy) (ocaml/dune#7357, fixes ocaml/dune#7344, @rlepigre and
  @Alizter)

- Added a `--no-build` option to `dune coq top` for avoiding rebuilds (ocaml/dune#7380,
  fixes ocaml/dune#7355, @Alizter)

- RPC: Ignore SIGPIPE when clients suddenly disconnect (ocaml/dune#7299, ocaml/dune#7319, fixes
  ocaml/dune#6879, @rgrinberg)

- Always clean up the UI on exit. (ocaml/dune#7271, fixes ocaml/dune#7142 @rgrinberg)

- Bootstrap: remove reliance on shell. Previously, we'd use the shell to get
  the number of processors. (ocaml/dune#7274, @rgrinberg)

- Bootstrap: correctly detect the number of processors by allowing `nproc` to be
  looked up in `$PATH` (ocaml/dune#7272, @Alizter)

- Speed up file copying on macos by using `clonefile` when available
  (@rgrinberg, ocaml/dune#7210)

- Adds support for loading plugins in toplevels (ocaml/dune#6082, fixes ocaml/dune#6081,
  @ivg, @richardlford)

- Support commands that output 8-bit and 24-bit colors in the terminal (ocaml/dune#7188,
  @Alizter)

- Speed up rule generation for libraries and executables with many modules
  (ocaml/dune#7187, @jchavarri)

- Add `--watch-exclusions` to Dune build options (ocaml/dune#7216, @jonahbeckford)

- Do not re-render UI on every frame if the UI doesn't change (ocaml/dune#7186, fix
  ocaml/dune#7184, @rgrinberg)

- Make coq_db creation in scope lazy (@ejgallego, ocaml/dune#7133)

- Non-user proccesses such as version control or config checking are now run
  silently. (ocaml/dune#6994, fixes ocaml/dune#4066, @Alizter)

- Add the `--display-separate-messages` flag to separate the error messages
  produced by commands with a blank line. (ocaml/dune#6823, fixes ocaml/dune#6158, @esope)

- Accept the Ordered Set Language for the `modes` field in `library` stanzas
  (ocaml/dune#6611, @anmonteiro).

- dune install now respects --display quiet mode (ocaml/dune#7116, fixes ocaml/dune#4573, fixes
  ocaml/dune#7106, @Alizter)

- Stub shared libraries (dllXXX_stubs.so) in Dune-installed libraries could not
  be used as dependencies of libraries in the workspace (eg when compiling to
  bytecode and/or Javascript).  This is now fixed. (ocaml/dune#7151, @nojb)

- Allow the main module of a library with `(stdlib ...)` to depend on other
  libraries (ocaml/dune#7154, @anmonteiro).

- Bytecode executables built for JSOO are linked with `-noautolink` and no
  longer depend on the shared stubs of their dependent libraries (ocaml/dune#7156, @nojb)

- Added a new user action `(concurrent )` which is like `(progn )` but runs the
  actions concurrently. (ocaml/dune#6933, @Alizter)

- Allow `(stdlib ...)` to be used with `(wrapped false)` in library stanzas
  (ocaml/dune#7139, @anmonteiro).

- Allow parallel execution of inline tests partitions (ocaml/dune#7012, @hhugo)

- Support `(link_flags ...)` in `(cinaps ...)` stanza. (ocaml/dune#7423, fixes ocaml/dune#7416,
  @nojb)

- Allow `(package ...)` in any position within `(rule ...)` stanza (ocaml/dune#7445,
  @Leonidas-from-XIV)

- Always include `opam` files in the generated `.install` file. Previously, it
  would not be included whenever `(generate_opam_files true)` was set and the
  `.install` file wasn't yet generated. (ocaml/dune#7547, @rgrinberg)

- Fix regression where Merlin was unable to handle filenames with uppercase
  letters under Windows. (ocaml/dune#7577, @nojb)

- On nix+macos, pass `-f` to the codesign hook to avoid errors when the binary
  is already signed (ocaml/dune#7183, fixes ocaml/dune#6265, @greedy)

- Fix bug where RPC clients built with dune-rpc-lwt would crash when closing
  their connection to the server (ocaml/dune#7581, @gridbugs)

- Introduce mdx stanza 0.4 requiring mdx >= 2.3.0 which updates the default
  list of files to include `*.mld` files (ocaml/dune#7582, @Leonidas-from-XIV)

- Fix RPC server on Windows (used for OCaml-LSP). (ocaml/dune#7666, @nojb)

- Coq language versions less 0.8 are deprecated, and will be removed
  in an upcoming Dune version. All users are required to migrate to
  `(coq lang 0.8)` which provides the right semantics for theories
  that have been globally installed, such as those coming from opam
  (@ejgallego, @Alizter)

- Bump minimum version of the dune language for the melange syntax extension
  from 3.7 to 3.8 (ocaml/dune#7665, @jchavarri)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Dune Site Plugins do not work in toplevel
6 participants