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.

Sign up for GitHub

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

Jump to bottom

feature(coq): omit -q flag during dune coq top #6848

Merged
merged 3 commits into from
Jan 24, 2023
Merged

feature(coq): omit -q flag during dune coq top #6848

merged 3 commits into from
Jan 24, 2023

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Jan 9, 2023

Signed-off-by: Ali Caglayan alizter@gmail.com

@Alizter Alizter mentioned this pull request Jan 9, 2023
Closed
@Alizter
Copy link
Collaborator Author

Alizter commented Jan 9, 2023

I'm not a big fan of having Coq's standard flags being set from within env_node.ml.

@Alizter Alizter added the coq label Jan 9, 2023
@Alizter Alizter force-pushed the ps/rr/feature_coq___omit__q_flag_during_dune_coq_top branch 2 times, most recently from 037b2c0 to fbbdfe1 Compare January 9, 2023 23:01
@Alizter Alizter marked this pull request as ready for review January 9, 2023 23:33
@Alizter Alizter linked an issue Jan 10, 2023 that may be closed by this pull request
Dune Coq top skips loading .coqrc #6847
Closed
@Alizter Alizter force-pushed the ps/rr/feature_coq___omit__q_flag_during_dune_coq_top branch from fbbdfe1 to 6131907 Compare January 10, 2023 02:56
@ejgallego
Copy link
Collaborator

ejgallego commented Jan 10, 2023 •
edited
Loading

I don't see why dune coq top should behave specially here, in fact that seems like a recipe for problems (different behavior on build and top).

If the user in that project need to omit passing -q, they can just do :standard \ -q where they need it.

But that's again a slippery slope, because dune won't realize that now .coqrc must be tracked and thus a change in .coqrc would lead to unsound builds.

@ejgallego
Copy link
Collaborator

Overall we can allow this, but it seems a misfeature to me due to users being confused about hidden stuff in .coqrc, moreover that file has the potential to affect soundness of the build.

There is an alternative which is to extend the (coq.theory ) to add some settings for interactive use, that way other projects such as coq-lsp could also access those settings.

If we merge this, then we need to fix:

  • don't ignore the :standard flags on coqtop
  • coqc should always get -q

@Alizter Alizter force-pushed the ps/rr/feature_coq___omit__q_flag_during_dune_coq_top branch from 6131907 to febe2aa Compare January 21, 2023 18:32
@Alizter
Copy link
Collaborator Author

Alizter commented Jan 21, 2023 •
edited
Loading

@ejgallego We set -q for every coq program and nothing for coqtop now. No need to mess around with \ -q. This also makes the interaction with env simpler.

Alizter
Alizter commented Jan 21, 2023
View reviewed changes
src/dune_rules/env_node.ml Outdated Show resolved Hide resolved
@ejgallego ejgallego self-assigned this Jan 21, 2023
@ejgallego
Copy link
Collaborator

Test suite is failing; pay attention in particular to the flags tests, these are actually super tricky due to the way env rules work.

@Alizter Alizter force-pushed the ps/rr/feature_coq___omit__q_flag_during_dune_coq_top branch from febe2aa to 09cd6a1 Compare January 22, 2023 15:04
ejgallego
ejgallego reviewed Jan 22, 2023
View reviewed changes
Copy link
Collaborator

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

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

Coq part looks good to me thanks! (Tho I'm unsure why we again inline stuff that was not inlined for a reason)

About the changes in Ordered_set_lang, that's beyond my knowledge of Dune, need someone that knows that part to have a look.

@Alizter
Copy link
Collaborator Author

Alizter commented Jan 22, 2023

I inlined that function since it was only being used once and was out of the way. I can uninline it and move it closer to the call site if you prefer or just leave it alone completely.

I'm also not sure about my change to Ordered_set_lang.

@Alizter Alizter force-pushed the ps/rr/feature_coq___omit__q_flag_during_dune_coq_top branch from 09cd6a1 to 15c7b0f Compare January 22, 2023 16:30
@Alizter
Copy link
Collaborator Author

Alizter commented Jan 22, 2023

@rgrinberg Could you comment on the changes to Ordered_set_lang and perhaps suggest a better way of doing what we are doing here? I'm basically passing \ -q to an existing Ordered_set_lang.

@rgrinberg
Copy link
Member

It looks OK. It would be better to expand the ordered set language and then make the modification to it rather than dealing with the raw ast.

ejgallego
ejgallego approved these changes Jan 23, 2023
View reviewed changes
Copy link
Collaborator

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

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

Ok then!

@ejgallego
Copy link
Collaborator

@Alizter merge yourself please if you don't implement that last suggestion.

@rgrinberg
Copy link
Member

At least try to implement the suggestion first though. This diff function isn't something that is good to make public.

@Alizter Alizter force-pushed the ps/rr/feature_coq___omit__q_flag_during_dune_coq_top branch 2 times, most recently from 25919d6 to 554366e Compare January 23, 2023 23:53
@Alizter
Copy link
Collaborator Author

Alizter commented Jan 23, 2023

OK, I've implemented the more direct list scrubbing and removed the changes to Ordered_set_lang.

rgrinberg
rgrinberg approved these changes Jan 24, 2023
View reviewed changes
src/dune_rules/coq/coq_rules.ml Outdated Show resolved Hide resolved
@Alizter Alizter force-pushed the ps/rr/feature_coq___omit__q_flag_during_dune_coq_top branch 2 times, most recently from eeb4b91 to 56589da Compare January 24, 2023 06:36
@Alizter
feature(coq): omit -q flag during dune coq top
81aea6d 
<!-- ps-id: 5a03ba95-9ec7-41fd-8f3f-db31c6742042 -->

Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter Alizter force-pushed the ps/rr/feature_coq___omit__q_flag_during_dune_coq_top branch from 56589da to 81aea6d Compare January 24, 2023 06:38
@ejgallego ejgallego merged commit ce578be into ocaml:main Jan 24, 2023
@Alizter Alizter deleted the ps/rr/feature_coq___omit__q_flag_during_dune_coq_top branch January 25, 2023 01:57
emillon added a commit to emillon/opam-repository that referenced this pull request Feb 6, 2023
@emillon
[new release] xdg, stdune, ordering, ocamlc-loc, dyn, dune, dune-site…
4eab166 
…, dune-rpc, dune-rpc-lwt, dune-private-libs, dune-glob, dune-configurator, dune-build-info, dune-action-plugin and chrome-trace (3.7.0~alpha1)

CHANGES:

- Fix parsing of OCaml errors that contain code excerpts with `...` in them.
  (ocaml/dune#7008, @rgrinberg)

- Pre-emptively clear screen in watch mode (ocaml/dune#6987, fixes ocaml/dune#6884, @rgrinberg)

- Fix cross compilation configuration when a context with targets is itself a
  host of another context (ocaml/dune#6958, fixes ocaml/dune#6843, @rgrinberg)

- Fix parsing of the `<=` operator in *blang* expressions of `dune` files.
  Previously, the operator would be interpreted as `,`. (ocaml/dune#6928, @tatchi)

- Fix `--trace-file` output. Dune now emits a single *complete* event for every
  executed process. Unterminated *async* events are no longer written. (ocaml/dune#6892,
  @rgrinberg)

- Fix preprocessing with `staged_pps` (ocaml/dune#6748, fixes ocaml/dune#6644, @rgrinberg)

- Use colored output with MDX when Dune colors are enabled.
  (ocaml/dune#6462, @MisterDA)

- Make `dune describe workspace` return consistent dependencies for
  executables and for libraries. By default, compile-time dependencies
  towards PPX-rewriters are from now not taken into account (but
  runtime dependencies always are). Compile-time dependencies towards
  PPX-rewriters can be taken into account by providing the
  `--with-pps` flag. (ocaml/dune#6727, fixes ocaml/dune#6486, @esope)

- Print missing newline after `$ dune exec`. (ocaml/dune#6821, fixes ocaml/dune#6700, @rgrinberg,
  @Alizter)

- Fix binary corruption when installing or promoting in parallel (ocaml/dune#6669, fixes
  ocaml/dune#6668, @edwintorok)

- Use colored output with GCC and Clang when compiling C stubs. The
  flag `-fdiagnostics-color=always` is added to the `:standard` set of
  flags. (ocaml/dune#4083, @MisterDA)

- Fix the parsing of decimal and hexadecimal escape literals in `dune`,
  `dune-package`, and other dune s-expression based files (ocaml/dune#6710, @shym)

- Report an error if `dune init ...` would create a "dune" file in a location
  which already contains a "dune" directory (ocaml/dune#6705, @gridbugs)

- Fix the parsing of alerts. They will now show up in diagnostics correctly.
  (ocaml/dune#6678, @rginberg)

- Fix the compilation of modules generated at link time when
  `implicit_transitive_deps` is enabled (ocaml/dune#6642, @rgrinberg)

- Allow `$ dune utop` to load libraries defined in data only directories
  defined using `(subdir ..)` (ocaml/dune#6631, @rgrinberg)

- Format dune files when they are named `dune-file`. This occurs when we enable
  the alternative file names project option. (ocaml/dune#6566, @rgrinberg)

- Move `$ dune ocaml-merlin -dump-config=$dir` to `$ dune ocaml merlin
  dump-config $dir`. (ocaml/dune#6547, @rgrinberg)

- Allow compilation rules to be impacted by `(env ..)` stanzas that modify the
  environment or set binaries. (ocaml/dune#6527, @rgrinberg)

- Coq native mode is now automatically detected by Dune starting with Coq lang
  0.7. `(mode native)` has been deprecated in favour of detection from the
  configuration of Coq. (ocaml/dune#6409, @Alizter)

- Print "Leaving Directory" whenever "Entering Directory" is printed. (ocaml/dune#6149,
  fixes ocaml/dune#138, @cpitclaudel, @rgrinberg)

- Allow `$ dune ocaml dump-dot-merlin` to run in watch mode. Also this command
  shouldn't print "Entering Directory" mesages. (ocaml/dune#6497, @rgrinberg)

- `dune clean` should no longer fail under Windows due to the inability to
  remove the `.lock` file. Also, bring the implementation of the global lock
  under Windows closer to that of Unix. (ocaml/dune#6523, @nojb)

- Remove "Entering Directory" messages for `$ dune install`. (ocaml/dune#6513,
  @rgrinberg)

- Stop passing `-q` flag in `dune coq top`, which allows for `.coqrc` to be
  loaded. (ocaml/dune#6848, fixes ocaml/dune#6847, @Alizter)

- Fix missing dependencies when detecting the kind of C compiler we're using
  (ocaml/dune#6610, fixes ocaml/dune#6415, @emillon)

- Allow `(include_subdirs qualified)` for OCaml projects. (ocaml/dune#6594, fixes ocaml/dune#1084,
  @rgrinberg)

- Accurately determine merlin configuration for all sources selected with
  `copy#` and `copy_files#`. The old heuristic of looking for a module in
  parent directories is removed (ocaml/dune#6594, @rgrinberg)

- Fix inline tests with *js_of_ocaml* and whole program compilation mode
  enabled (ocaml/dune#6645, @hhugo)

- Fix *js_of_ocaml* separate compilation rules when `--enable=effects`
  ,`--enable=use-js-string` or `--toplevel` is used. (ocaml/dune#6714, ocaml/dune#6828, ocaml/dune#6920, @hhugo)

- Fix *js_of_ocaml* separate compilation in presence of linkall (ocaml/dune#6832, ocaml/dune#6916, @hhugo)

- Remove spurious build dir created when running `dune init proj ...` (ocaml/dune#6707,
  fixes ocaml/dune#5429, @gridbugs)

- Allow `--sandbox` to affect `ocamldep` invocations. Previously, they were
  wrongly marked as incompatible (ocaml/dune#6749, @rgrinberg)

- Validate the command line arguments for `$ dune ocaml top-module`. This
  command requires one positional argument (ocaml/dune#6796, fixes ocaml/dune#6793, @rgrinberg)

- Add a `dune cache size` command for displaying the size of the cache (ocaml/dune#6638,
  @Alizter)

- Add 4.14.0 MSVC to CI (ocaml/dune#6917, @jonahbeckford)

- Fix dependency cycle when installing files to the bin section with
  `glob_files` (ocaml/dune#6764, fixes ocaml/dune#6708, @gridbugs)

- Handle "Too many links" errors when using Dune cache on Windows (ocaml/dune#6993, @nojb)
@emillon emillon mentioned this pull request Feb 6, 2023
Closed
@emillon emillon mentioned this pull request Feb 17, 2023
Merged
emillon added a commit to emillon/opam-repository that referenced this pull request Feb 17, 2023
@emillon
[new release] xdg, stdune, ordering, ocamlc-loc, dyn, dune, dune-site…
c5fc79e 
…, dune-rpc, dune-rpc-lwt, dune-private-libs, dune-glob, dune-configurator, dune-build-info, dune-action-plugin and chrome-trace (3.7.0)

CHANGES:

- Allow running `$ dune exec` in watch mode (with the `-w` flag). In watch mode,
  `$ dune exec` the executed binary whenever it is recompiled. (ocaml/dune#6966,
  @gridbugs)

- `coqdep` is now called once per theory, instead of one time per Coq
  file. This should significantly speed up some builds, as `coqdep`
  startup time is often heavy (ocaml/dune#7048, @Alizter, @ejgallego)

- Add `map_workspace_root` dune-project stanza to allow disabling of
  mapping of workspace root to `/workspace_root`. (ocaml/dune#6988, fixes ocaml/dune#6929,
  @richardlford)

- Fix handling of support files generated by odoc. (ocaml/dune#6913, @jonludlam)

- Fix parsing of OCaml errors that contain code excerpts with `...` in them.
  (ocaml/dune#7008, @rgrinberg)

- Pre-emptively clear screen in watch mode (ocaml/dune#6987, fixes ocaml/dune#6884, @rgrinberg)

- Fix cross compilation configuration when a context with targets is itself a
  host of another context (ocaml/dune#6958, fixes ocaml/dune#6843, @rgrinberg)

- Fix parsing of the `<=` operator in *blang* expressions of `dune` files.
  Previously, the operator would be interpreted as `<`. (ocaml/dune#6928, @tatchi)

- Fix `--trace-file` output. Dune now emits a single *complete* event for every
  executed process. Unterminated *async* events are no longer written. (ocaml/dune#6892,
  @rgrinberg)

- Fix preprocessing with `staged_pps` (ocaml/dune#6748, fixes ocaml/dune#6644, @rgrinberg)

- Use colored output with MDX when Dune colors are enabled.
  (ocaml/dune#6462, @MisterDA)

- Make `dune describe workspace` return consistent dependencies for
  executables and for libraries. By default, compile-time dependencies
  towards PPX-rewriters are from now not taken into account (but
  runtime dependencies always are). Compile-time dependencies towards
  PPX-rewriters can be taken into account by providing the
  `--with-pps` flag. (ocaml/dune#6727, fixes ocaml/dune#6486, @esope)

- Print missing newline after `$ dune exec`. (ocaml/dune#6821, fixes ocaml/dune#6700, @rgrinberg,
  @Alizter)

- Fix binary corruption when installing or promoting in parallel (ocaml/dune#6669, fixes
  ocaml/dune#6668, @edwintorok)

- Use colored output with GCC and Clang when compiling C stubs. The
  flag `-fdiagnostics-color=always` is added to the `:standard` set of
  flags. (ocaml/dune#4083, @MisterDA)

- Fix the parsing of decimal and hexadecimal escape literals in `dune`,
  `dune-package`, and other dune s-expression based files (ocaml/dune#6710, @shym)

- Report an error if `dune init ...` would create a "dune" file in a location
  which already contains a "dune" directory (ocaml/dune#6705, @gridbugs)

- Fix the parsing of alerts. They will now show up in diagnostics correctly.
  (ocaml/dune#6678, @rginberg)

- Fix the compilation of modules generated at link time when
  `implicit_transitive_deps` is enabled (ocaml/dune#6642, @rgrinberg)

- Allow `$ dune utop` to load libraries defined in data only directories
  defined using `(subdir ..)` (ocaml/dune#6631, @rgrinberg)

- Format dune files when they are named `dune-file`. This occurs when we enable
  the alternative file names project option. (ocaml/dune#6566, @rgrinberg)

- Move `$ dune ocaml-merlin -dump-config=$dir` to `$ dune ocaml merlin
  dump-config $dir`. (ocaml/dune#6547, @rgrinberg)

- Allow compilation rules to be impacted by `(env ..)` stanzas that modify the
  environment or set binaries. (ocaml/dune#6527, @rgrinberg)

- Coq native mode is now automatically detected by Dune starting with Coq lang
  0.7. `(mode native)` has been deprecated in favour of detection from the
  configuration of Coq. (ocaml/dune#6409, @Alizter)

- Print "Leaving Directory" whenever "Entering Directory" is printed. (ocaml/dune#6419,
  fixes ocaml/dune#138, @cpitclaudel, @rgrinberg)

- Allow `$ dune ocaml dump-dot-merlin` to run in watch mode. Also this command
  shouldn't print "Entering Directory" mesages. (ocaml/dune#6497, @rgrinberg)

- `dune clean` should no longer fail under Windows due to the inability to
  remove the `.lock` file. Also, bring the implementation of the global lock
  under Windows closer to that of Unix. (ocaml/dune#6523, @nojb)

- Remove "Entering Directory" messages for `$ dune install`. (ocaml/dune#6513,
  @rgrinberg)

- Stop passing `-q` flag in `dune coq top`, which allows for `.coqrc` to be
  loaded. (ocaml/dune#6848, fixes ocaml/dune#6847, @Alizter)

- Fix missing dependencies when detecting the kind of C compiler we're using
  (ocaml/dune#6610, fixes ocaml/dune#6415, @emillon)

- Allow `(include_subdirs qualified)` for OCaml projects. (ocaml/dune#6594, fixes ocaml/dune#1084,
  @rgrinberg)

- Accurately determine merlin configuration for all sources selected with
  `copy#` and `copy_files#`. The old heuristic of looking for a module in
  parent directories is removed (ocaml/dune#6594, @rgrinberg)

- Fix inline tests with *js_of_ocaml* and whole program compilation mode
  enabled (ocaml/dune#6645, @hhugo)

- Fix *js_of_ocaml* separate compilation rules when `--enable=effects`
  ,`--enable=use-js-string` or `--toplevel` is used. (ocaml/dune#6714, ocaml/dune#6828, ocaml/dune#6920, @hhugo)

- Fix *js_of_ocaml* separate compilation in presence of linkall (ocaml/dune#6832, ocaml/dune#6916, @hhugo)

- Remove spurious build dir created when running `dune init proj ...` (ocaml/dune#6707,
  fixes ocaml/dune#5429, @gridbugs)

- Allow `--sandbox` to affect `ocamldep` invocations. Previously, they were
  wrongly marked as incompatible (ocaml/dune#6749, @rgrinberg)

- Validate the command line arguments for `$ dune ocaml top-module`. This
  command requires one positional argument (ocaml/dune#6796, fixes ocaml/dune#6793, @rgrinberg)

- Add a `dune cache size` command for displaying the size of the cache (ocaml/dune#6638,
  @Alizter)

- Fix dependency cycle when installing files to the bin section with
  `glob_files` (ocaml/dune#6764, fixes ocaml/dune#6708, @gridbugs)

- Handle "Too many links" errors when using Dune cache on Windows (ocaml/dune#6993, @nojb)

- Allow the `cinaps` stanza to set a custom alias. By default, if the alias is
  not set then the cinaps actions will be attached to both `@cinaps` and
  `@runtest` (ocaml/dune#6991, @rgrinberg)

- Add `(using ctypes 0.3)`. When used, paths in `(ctypes)` are interpreted
  relative to where the stanza is defined. (ocaml/dune#6883, fixes ocaml/dune#5325, @emillon)

- Auto-detect `dune-workspace` files as `dune` files in Emacs (ocaml/dune#7061,
  @ilankri)

- Add native support for polling mode on Windows (ocaml/dune#7010, @yams-yams, @nojb)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@rgrinberg rgrinberg rgrinberg approved these changes

@ejgallego ejgallego ejgallego approved these changes

Assignees

@ejgallego ejgallego

Labels
coq
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Dune Coq top skips loading .coqrc
3 participants
@Alizter @ejgallego @rgrinberg