Skip to content

feature(coq): support :standard in coq.pp (modules) field#6229

Merged
Alizter merged 2 commits intoocaml:mainfrom
Alizter:ps/rr/feature_coq___support__standard_in_coq_pp__modules__field
Nov 6, 2022
Merged

feature(coq): support :standard in coq.pp (modules) field#6229
Alizter merged 2 commits intoocaml:mainfrom
Alizter:ps/rr/feature_coq___support__standard_in_coq_pp__modules__field

Conversation

@Alizter
Copy link
Copy Markdown
Collaborator

@Alizter Alizter commented Oct 14, 2022

@Alizter Alizter mentioned this pull request Oct 14, 2022
3 tasks
@ejgallego ejgallego self-assigned this Oct 14, 2022
@ejgallego ejgallego added the coq label Oct 14, 2022
@Alizter Alizter force-pushed the ps/rr/feature_coq___support__standard_in_coq_pp__modules__field branch 2 times, most recently from ff37692 to dcaf9e6 Compare October 14, 2022 01:22
@Alizter Alizter force-pushed the ps/rr/feature_coq___support__standard_in_coq_pp__modules__field branch 3 times, most recently from be252ee to 7c1066d Compare October 24, 2022 18:52
@Alizter Alizter requested a review from ejgallego October 24, 2022 18:52
@Alizter Alizter force-pushed the ps/rr/feature_coq___support__standard_in_coq_pp__modules__field branch from 7c1066d to 0900529 Compare October 25, 2022 14:54
@Alizter Alizter force-pushed the ps/rr/feature_coq___support__standard_in_coq_pp__modules__field branch 8 times, most recently from 8b1fd66 to c8f60f8 Compare October 29, 2022 17:49
@Alizter Alizter force-pushed the ps/rr/feature_coq___support__standard_in_coq_pp__modules__field branch from c8f60f8 to 2271770 Compare November 6, 2022 09:17
Signed-off-by: Ali Caglayan <alizter@gmail.com>

ps-id: 31c9fa4a-36ff-4ffe-81b2-3d957c09b17a
@Alizter Alizter force-pushed the ps/rr/feature_coq___support__standard_in_coq_pp__modules__field branch from 2271770 to ef094dc Compare November 6, 2022 13:36
@Alizter Alizter requested a review from rgrinberg November 6, 2022 15:45
@ejgallego
Copy link
Copy Markdown
Collaborator

Contrary to what the PR description says, this PR doesn't guard the change on the 0.7 Coq build language; but IMHO that's not a big deal.

@Alizter
Copy link
Copy Markdown
Collaborator Author

Alizter commented Nov 6, 2022

@ejgallego I don't think it would be easy to guard the :standard clause and probably not worth it since mlg use is so little. The PR description was really referencing the fact that when I was bumping to 0.7 I had a merge conflict so this needed to wait.

@Alizter Alizter merged commit b7d519d into ocaml:main Nov 6, 2022
@Alizter Alizter deleted the ps/rr/feature_coq___support__standard_in_coq_pp__modules__field branch November 6, 2022 19:11
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

Labels

Projects

Archived in project

Development

Successfully merging this pull request may close these issues.

coq.pp :standard?

4 participants