fix(coq): fix coqtop args being passed incorrectly #6369
Merged
Conversation
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
8e982e6 to
cc977e7
Compare
Please do that in a separate PR or commit as it makes reviewing the code changes very hard. |
cc977e7 to
baa7b24
Compare
|
@ejgallego The diff should be cleaner now. |
baa7b24 to
8c05b50
Compare
|
@ejgallego ping |
ejgallego
approved these changes
Nov 10, 2022
|
This deserves an entry in |
db4316a to
b2b78c7
Compare
Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: 81125bb0-a001-4b22-9484-a6ee1cc37b58 Signed-off-by: Ali Caglayan <alizter@gmail.com>
b2b78c7 to
a0ab39a
Compare
ejgallego
reviewed
Nov 11, 2022
| @@ -52,6 +52,8 @@ Unreleased | |||
| - Allow `:standard` in the `(modules)` field of the `coq.pp` stanza (#6229, | |||
| fixes #2414, @Alizter) | |||
|
|
|||
| - Fix passing of native flags to dune coq top (#6369, fixes #6366, @Alizter) | |||
There was a problem hiding this comment.
Not only native, but user flags too (that was actually the bug IIRC)
emillon
added a commit
to emillon/opam-repository
that referenced
this pull request
Nov 14, 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.6.0) CHANGES: - Forbid multiple instances of dune running concurrently in the same workspace. (ocaml/dune#6360, fixes ocaml/dune#236, @rgrinberg) - Allow promoting into source directories specified by `subdir` (ocaml/dune#6404, fixes ocaml/dune#3502, @rgrinberg) - Make dune describe workspace return the correct root path (ocaml/dune#6380, fixes ocaml/dune#6379, @esope) - Introduce a `$ dune ocaml top-module` subcommand to load modules directly without sealing them behind the signature. (ocaml/dune#5940, @rgrinberg) - [ctypes] do not mangle user written names in the ctypes stanza (ocaml/dune#6374, fixes ocaml/dune#5561, @rgrinberg) - Support `CLICOLOR` and `CLICOLOR_FORCE` to enable/disable/force ANSI colors. (ocaml/dune#6340, fixes ocaml/dune#6323, @MisterDA). - Forbid private libraries with `(package ..)` set from depending on private libraries that don't belong to a package (ocaml/dune#6385, fixes ocaml/dune#6153, @rgrinberg) - Allow `Byte_complete` binaries to be installable (ocaml/dune#4873, @AltGr, @rgrinberg) - Revive `$ dune external-lib-deps` under `$ dune describe external-lib-deps`. (ocaml/dune#6045, @moyodiallo) - Fix running inline tests in bytecode mode (ocaml/dune#5622, fixes ocaml/dune#5515, @dariusf) - [ctypes] always re-run `pkg-config` because we aren't tracking its external dependencies (ocaml/dune#6052, @rgrinberg) - [ctypes] remove dependency on configurator in the generated rules (ocaml/dune#6052, @rgrinberg) - Build progress status now shows number of failed jobs (ocaml/dune#6242, @Alizter) - Allow absolute build directories to find public executables. For example, those specified with `(deps %{bin:...})` (ocaml/dune#6326, @anmonteiro) - Create a fake socket file `_build/.rpc/dune` on windows to allow rpc clients to connect using the build directory. (ocaml/dune#6329, @rgrinberg) - Prevent crash if absolute paths are used in the install stanza and in recursive globs. These cases now result in a user error. (ocaml/dune#6331, @gridbugs) - Add `(glob_files <glob>)` and `(glob_files_rec <glob>)` terms to the `files` field of the `install` stanza (ocaml/dune#6250, closes ocaml/dune#6018, @gridbugs) - Allow `:standard` in the `(modules)` field of the `coq.pp` stanza (ocaml/dune#6229, fixes ocaml/dune#2414, @Alizter) - Fix passing of flags to dune coq top (ocaml/dune#6369, fixes ocaml/dune#6366, @Alizter) - Extend the promotion CLI to a `dune promotion` group: `dune promote` is moved to `dune promotion apply` (the former still works) and the new `dune promotion diff` command can be used to just display the promotion without applying it. (ocaml/dune#6160, fixes ocaml/dune#5368, @emillon)
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.
fixes #6366
More refactoring of coqtop will have to come at a later date, this at least makes the flags match up correctly.