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

[coq] Add "-q" to default flags. #3931

Merged
merged 1 commit into from
Nov 25, 2020
Merged

[coq] Add "-q" to default flags. #3931

merged 1 commit into from
Nov 25, 2020

Conversation

ejgallego
Copy link
Collaborator

@ejgallego ejgallego commented Nov 9, 2020 •
edited
Loading

Fixes #3924 , and a bug where :standard was not properly set in
theory flags, as they should be inherited from the ones set in the
profile; thanks Rudi Gringerb.

@ejgallego ejgallego added the coq label Nov 9, 2020
@ejgallego ejgallego force-pushed the coq+add_q_flags branch 2 times, most recently from f9ca4a5 to 93bf215 Compare November 9, 2020 20:15
@rgrinberg
Copy link
Member

Actually this PR highlights a problem in the way we handle flags from
profile and from the theory stanza, they should form a single set I
think, however they are disjoint.

I'd try to match the OCaml behavior. Which would mean that :standard would be the env flags when expanding the theory flags.

rgrinberg
rgrinberg reviewed Nov 11, 2020
View reviewed changes
CHANGES.md Outdated Show resolved Hide resolved
@ejgallego
Copy link
Collaborator Author

I'd try to match the OCaml behavior. Which would mean that :standard would be the env flags when expanding the theory flags.

Of course, thanks; I was a bit dense writing this PR.

@ejgallego ejgallego force-pushed the coq+add_q_flags branch 4 times, most recently from 6a39bed to 52d3033 Compare November 13, 2020 20:01
@ejgallego
Copy link
Collaborator Author

@rgrinberg , this should be ready. I'll wait for you to have quick look before merge.

@rgrinberg
Copy link
Member

Looks good. I'd recommend to:

  • Add a test
  • Describe this change in the CHANGES list as well.

@ejgallego
Copy link
Collaborator Author

  • Add a test

Indeed testing would be good but I am not sure how to reliable get the flags, _build/log does contain path-dependent data.

Describe this change in the CHANGES list as well

Isn't that done? Is there some other file I should update?

@rgrinberg
Copy link
Member

The CHANGES only mention that you've added -q to the default set of flags. You didn't mention that you've changed :standard to mean all currently set flags. Previously, :standard was always empty.

@ejgallego
Copy link
Collaborator Author

The CHANGES only mention that you've added -q to the default set of flags. You didn't mention that you've changed :standard to mean all currently set flags. Previously, :standard was always empty.

Oh indeed, done thanks. Updated doc in the way.

@ejgallego ejgallego added this to the 2.8 milestone Nov 15, 2020
@rgrinberg
Copy link
Member

@ejgallego anything blocking this PR?

@ejgallego
Copy link
Collaborator Author

@rgrinberg I'm unsure how to add a test for this, otherwise it seems ready.

Indeed testing would be good but I am not sure how to reliable get the flags, _build/log does contain path-dependent data

@rgrinberg
Copy link
Member

rgrinberg commented Nov 25, 2020 •
edited
Loading

it's fine to merge this without the tests if you've checked that it works as expected

@ejgallego
[coq] Add "-q" to default flags.
307b0e4 
Fixes ocaml#3924 , and a bug where `:standard` was not properly set in
theory flags, as they should be inherited from the ones set in the
profile; thanks Rudi Gringerb.

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
@ejgallego
Copy link
Collaborator Author

Thanks @rgrinberg , will have a last look at a possible test and merge.

@ejgallego
Copy link
Collaborator Author

ejgallego commented Nov 25, 2020 •
edited
Loading

will have a last look at a possible test and merge.

Didn't find a nice way for this particular option. At some point we should strengthen the flags test suite for Coq itself, but IMHO this is good to go.

@rgrinberg rgrinberg merged commit d336ddd into ocaml:master Nov 25, 2020
@ejgallego ejgallego deleted the coq+add_q_flags branch November 25, 2020 23:37
@LasseBlaauwbroek LasseBlaauwbroek mentioned this pull request Dec 16, 2020
Closed
@rgrinberg rgrinberg mentioned this pull request Jan 13, 2021
Merged
rgrinberg added a commit to rgrinberg/opam-repository that referenced this pull request Jan 13, 2021
@rgrinberg
[new release] dune-build-info, dune, dune-configurator, dune-site, du…
dbe0014 
…ne-action-plugin, dune-private-libs and dune-glob (2.8.0)

CHANGES:

- `dune rules` accepts aliases and other non-path rules (ocaml/dune#4063, @mrmr1993)

- Action `(diff reference test_result)` now accept `reference` to be absent and
  in that case consider that the reference is empty. Then running `dune promote`
  will create the reference file. (ocaml/dune#3795, @bobot)

- Ignore special files (BLK, CHR, FIFO, SOCKET), (ocaml/dune#3570, fixes ocaml/dune#3124, ocaml/dune#3546,
  @ejgallego)

- Experimental: Simplify loading of additional files (data or code) at runtime
  in programs by introducing specific installation sites. In particular it allow
  to define plugins to be installed in these sites. (ocaml/dune#3104, ocaml/dune#3794, fixes ocaml/dune#1185,
  @bobot)

- Move all temporary files created by dune to run actions to a single directory
  and make sure that actions executed by dune also use this directory by setting
  `TMPDIR` (or `TEMP` on Windows). (ocaml/dune#3691, fixes ocaml/dune#3422, @rgrinberg)

- Fix bootstrap script with custom configuration. (ocaml/dune#3757, fixes ocaml/dune#3774, @marsam)

- Add the `executable` field to `inline_tests` to customize the compilation
  flags of the test runner executable (ocaml/dune#3747, fixes ocaml/dune#3679, @lubegasimon)

- Add `(enabled_if ...)` to `(copy_files ...)` (ocaml/dune#3756, @nojb)

- Make sure Dune cleans up the status line before exiting (ocaml/dune#3767,
  fixes ocaml/dune#3737, @alan-j-hu)

- Add `{gitlab,bitbucket}` as options for defining project sources with `source`
  stanza `(source (<host> user/repo))` in the `dune-project` file.  (ocaml/dune#3813,
  @rgrinberg)

- Fix generation of `META` and `dune-package` files when some targets (byte,
  native, dynlink) are disabled. Previously, dune would generate all archives
  for regardless of settings. (ocaml/dune#3829, ocaml/dune#4041, @rgrinberg)

- Do not run ocamldep to for single module executables & libraries. The
  dependency graph for such artifacts is trivial (ocaml/dune#3847, @rgrinberg)

- Fix cram tests inside vendored directories not being interpreted correctly.
  (ocaml/dune#3860, fixes ocaml/dune#3843, @rgrinberg)

- Add `package` field to private libraries. This allows such libraries to be
  installed and to be usable by other public libraries in the same project
  (ocaml/dune#3655, fixes ocaml/dune#1017, @rgrinberg)

- Fix the `%{make}` variable on Windows by only checking for a `gmake` binary
  on UNIX-like systems as a unrelated `gmake` binary might exist on Windows.
  (ocaml/dune#3853, @kit-ty-kate)

- Fix `$ dune install` modifying the build directory. This made the build
  directory unusable when `$ sudo dune install` modified permissions. (fix
  ocaml/dune#3857, @rgrinberg)

- Fix handling of aliases given on the command line (using the `@` and `@@`
  syntax) so as to correctly handle relative paths. (ocaml/dune#3874, fixes ocaml/dune#3850, @nojb)

- Allow link time code generation to be used in preprocessing executable. This
  makes it possible to use the build info module inside the preprocessor.
  (ocaml/dune#3848, fix ocaml/dune#3848, @rgrinberg)

- Correctly call `git ls-tree` so unicode files are not quoted, this fixes
  problems with `dune subst` in the presence of unicode files. Fixes ocaml/dune#3219
  (ocaml/dune#3879, @ejgallego)

- `dune subst` now accepts common command-line arguments such as
  `--debug-backtraces` (ocaml/dune#3878, @ejgallego)

- `dune describe` now also includes information about executables in addition to
  that of libraries. (ocaml/dune#3892, ocaml/dune#3895, @nojb)

- instrumentation backends can now receive arguments via `(instrumentation
  (backend <name> <args>))`. (ocaml/dune#3906, ocaml/dune#3932, @nojb)

- Tweak auto-formatting of `dune` files to improve readability. (ocaml/dune#3928, @nojb)

- Add a switch argument to opam when context is not default. (ocaml/dune#3951, @tmattio)

- Avoid pager when running `$ git diff` (ocaml/dune#3912, @AltGr)

- Add `(root_module ..)` field to libraries & executables. This makes it
  possible to use library dependencies shadowed by local modules (ocaml/dune#3825,
  @rgrinberg)

- Allow `(formatting ...)` field in `(env ...)` stanza to set per-directory
  formatting specification. (ocaml/dune#3942, @nojb)

- [coq] In `coq.theory`, `:standard` for the `flags` field now uses the
  flags set in `env` profile flags (ocaml/dune#3931 , @ejgallego @rgrinberg)

- [coq] Add `-q` flag to `:standard` `coqc` flags , fixes ocaml/dune#3924, (ocaml/dune#3931 , @ejgallego)

- Add support for Coq's native compute compilation mode (@ejgallego, ocaml/dune#3210)

- Add a `SUFFIX` directive in `.merlin` files for each dialect with no
  preprocessing, to let merlin know of additional file extensions (ocaml/dune#3977,
  @vouillon)

- Stop promoting `.merlin` files. Write per-stanza Merlin configurations in
  binary form. Add a new subcommand `dune ocaml-merlin` that Merlin can use to
  query the configuration files. The `allow_approximate_merlin` option is now
  useless and deprecated. Dune now conflicts with `merlin < 3.4.0` and
  `ocaml-lsp-server < 1.3.0` (ocaml/dune#3554, @voodoos)

- Configurator: fix a bug introduced in 2.6.0 where the configurator V1 API
  doesn't work at all when used outside of dune. (ocaml/dune#4046, @aalekseyev)

- Fix `libexec` and `libexec-private` variables. In cross-compilation settings,
  they now point to the file in the host context. (ocaml/dune#4058, fixes ocaml/dune#4057,
  @TheLortex)

- When running `$ dune subst`, use project metadata as a fallback when package
  metadata is missing. We also generate a warning when `(name ..)` is missing in
  `dune-project` files to avoid failures in production builds.

- Remove support for passing `-nodynlink` for executables. It was bypassed in
  most cases and not correct in other cases in particular on arm32.
  (ocaml/dune#4085, fixes ocaml/dune#4069, fixes ocaml/dune#2527, @emillon)

- Generate archive rules compatible with 4.12. Dune longer attempt to generate
  an archive file if it's unnecessary (ocaml/dune#3973, fixes ocaml/dune#3766, @rgrinberg)

- Fix generated Merlin configurations when multiple preprocessors are defined
  for different modules in the same folder. (ocaml/dune#4092, fixes ocaml/dune#2596, ocaml/dune#1212 and
  ocaml/dune#3409, @voodoos)

- Add the option `use_standard_c_and_cxx_flags` to `dune-project` that 1.
  disables the unconditional use of the `ocamlc_cflags` and `ocamlc_cppflags`
  from `ocamlc -config` in C compiler calls, these flags will be present in the
  `:standard` set instead; and 2. enables the detection of the C compiler family
  and populates the `:standard` set of flags with common default values when
  building CXX stubs. (ocaml/dune#3875, ocaml/dune#3802, fix ocaml/dune#3718 and ocaml/dune#3528, @voodoos)
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

@emillon emillon Awaiting requested review from emillon

@nojb nojb Awaiting requested review from nojb

Assignees
No one assigned
Labels
coq
Projects
Coq + Dune
Archived in project
Milestone
2.8
Development

Successfully merging this pull request may close these issues.

[Coq] Use the flag -q by default
2 participants
@ejgallego @rgrinberg