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

[wish] setting coq.theory.flags from a profile #3486

Closed
gares opened this issue May 13, 2020 · 3 comments · Fixed by #3547 or ocaml/opam-repository#17005
Closed

[wish] setting coq.theory.flags from a profile #3486

gares opened this issue May 13, 2020 · 3 comments · Fixed by #3547 or ocaml/opam-repository#17005
Assignees
@ejgallego
Labels
coq

Comments

@gares
Copy link
Contributor

gares commented May 13, 2020

It seems flags to coqc can only be set from a coq.theory stanza, while it would be nice to set them from profiles as well (as one can do for the options for ocamlc).

Cc @ejgallego
@ejgallego ejgallego added the coq label May 13, 2020
@ejgallego ejgallego mentioned this issue May 13, 2020
Open
8 tasks
@ejgallego ejgallego self-assigned this May 13, 2020
@gares
Copy link
Contributor Author

gares commented Jun 2, 2020

Any news on this front?

@gares
Copy link
Contributor Author

gares commented Jun 8, 2020

In the plan discussed a few CoqWG ago this feature seemed to be needed in order to use profiles for the different compilation chains Coq provides (vos, vio). According to @ejgallego this is also trivial to implement. Can someone take care of this, or alternatively point me to the right file/API?

@ejgallego
Copy link
Collaborator

This should be easy to do, grab the flags from the super_context when building the coq-specific context in coq_rules.

Note tho that as discussed in the Coq Call, if your use case involves flags that modify the build rules, just modifying the flags in the profile won't be enough. I think vos/vio do fall into this set.

Maybe #3526 could help depending on what its final form w.r.t. build rules is.

This was referenced Jun 11, 2020
Closed
Merged
rgrinberg added a commit to rgrinberg/opam-repository that referenced this issue Aug 14, 2020
@rgrinberg
[new release] dune-build-info, dune, dune-configurator, dune-action-p…
545d8e0 
…lugin, dune-private-libs and dune-glob (2.7.0)

CHANGES:

- Write intermediate files in a `.mdx` folder for each `mdx` stanza
  to prevent the corresponding actions to be executed as part of the `@all`
  alias (ocaml/dune#3659, @NathanReb)

- Read Coq flags from `env` (ocaml/dune#3547 , fixes ocaml/dune#3486, @gares)

- Allow bisect_ppx to be enabled/disabled via dune-workspace. (ocaml/dune#3404,
  @stephanieyou)

- Formatting of dune files is now done in the executing dune process instead of
  in a separate process. (ocaml/dune#3536, @nojb)

- Add a `--debug-artifact-substution` flag to help debug problem with
  version not being captured by `dune-build-info` (ocaml/dune#3589,
  @jeremiedimino)

- Allow the use of the `context_name` variable in the `enabled_if` fields of
  executable(s) and install stanzas. (ocaml/dune#3568, fixes ocaml/dune#3566, @voodoos)

- Fix compatibility with OCaml 4.12.0 when compiling empty archives; no .a file
  is generated. (ocaml/dune#3576, @dra27)

- `$ dune utop` no longer tries to load optional libraries that are unavailable
  (ocaml/dune#3612, fixes ocaml/dune#3188, @anuragsoni)

- Fix dune-build-info on 4.10.0+flambda (ocaml/dune#3599, @emillon, @jeremiedimino).

- Allow multiple libraries with `inline_tests` to be defined in the same
  directory (ocaml/dune#3621, @rgrinberg)

- Run exit hooks in jsoo separate compilation mode (ocaml/dune#3626, fixes ocaml/dune#3622,
  @rgrinberg)

- Add (alias ...), (mode ...) fields to (copy_fields ...) stanza (ocaml/dune#3631, @nojb)

- (copy_files ...) now supports copying files from outside the workspace using
  absolute file names (ocaml/dune#3639, @nojb)

- Dune does not use `ocamlc` as an intermediary to call C compiler anymore.
  Configuration flags `ocamlc_cflags` and `ocamlc_cppflags` are always prepended
  to the compiler arguments. (ocaml/dune#3565, fixes ocaml/dune#3346, @voodoos)

- Revert the build optimization in ocaml/dune#2268. This optimization slows down building
  individual executables when they're part of an `executables` stanza group
  (ocaml/dune#3644, @rgrinberg)

- Use `{dev}` rather than `{pinned}` in the generated `.opam` file. (ocaml/dune#3647,
  @kit-ty-kate)

- Insert correct extension name when editing `dune-project` files. Previously,
  dune would just insert the stanza name. (ocaml/dune#3649, fixes ocaml/dune#3624, @rgrinberg)

- Fix crash when evaluating an `mdx` stanza that depends on unavailable
  packages. (ocaml/dune#3650, @craigfe)

- Fix typo in `cache-check-probablity` field in dune config files. This field
  now requires 2.7 as it wasn't usable before this version. (ocaml/dune#3652, @edwintorok)

- Add `"odoc" {with-doc}` to the dependencies in the generated `.opam` files.
  (ocaml/dune#3667, @kit-ty-kate)

- Do not allow user actions to capture dune's stdin (ocaml/dune#3677, fixes ocaml/dune#3672,
  @rgrinberg)

- `(subdir ...)` stanzas can now appear in dune files used via `(include ...)`.
  (ocaml/dune#3676, @nojb)
@rgrinberg rgrinberg mentioned this issue Aug 14, 2020
Merged
rgrinberg added a commit to rgrinberg/opam-repository that referenced this issue Aug 14, 2020
@rgrinberg
[new release] dune-build-info, dune, dune-configurator, dune-action-p…
fd24ec4 
…lugin, dune-private-libs and dune-glob (2.7.0)

CHANGES:

- Write intermediate files in a `.mdx` folder for each `mdx` stanza
  to prevent the corresponding actions to be executed as part of the `@all`
  alias (ocaml/dune#3659, @NathanReb)

- Read Coq flags from `env` (ocaml/dune#3547 , fixes ocaml/dune#3486, @gares)

- Add instrumentation framework to toggle instrumentation by `bisect_ppx`,
  `landmarks`, etc, via dune-workspace and/or the command-line. (ocaml/dune#3404, ocaml/dune#3526
  @stephanieyou, @nojb)

- Formatting of dune files is now done in the executing dune process instead of
  in a separate process. (ocaml/dune#3536, @nojb)

- Add a `--debug-artifact-substution` flag to help debug problem with
  version not being captured by `dune-build-info` (ocaml/dune#3589,
  @jeremiedimino)

- Allow the use of the `context_name` variable in the `enabled_if` fields of
  executable(s) and install stanzas. (ocaml/dune#3568, fixes ocaml/dune#3566, @voodoos)

- Fix compatibility with OCaml 4.12.0 when compiling empty archives; no .a file
  is generated. (ocaml/dune#3576, @dra27)

- `$ dune utop` no longer tries to load optional libraries that are unavailable
  (ocaml/dune#3612, fixes ocaml/dune#3188, @anuragsoni)

- Fix dune-build-info on 4.10.0+flambda (ocaml/dune#3599, @emillon, @jeremiedimino).

- Allow multiple libraries with `inline_tests` to be defined in the same
  directory (ocaml/dune#3621, @rgrinberg)

- Run exit hooks in jsoo separate compilation mode (ocaml/dune#3626, fixes ocaml/dune#3622,
  @rgrinberg)

- Add (alias ...), (mode ...) fields to (copy_fields ...) stanza (ocaml/dune#3631, @nojb)

- (copy_files ...) now supports copying files from outside the workspace using
  absolute file names (ocaml/dune#3639, @nojb)

- Dune does not use `ocamlc` as an intermediary to call C compiler anymore.
  Configuration flags `ocamlc_cflags` and `ocamlc_cppflags` are always prepended
  to the compiler arguments. (ocaml/dune#3565, fixes ocaml/dune#3346, @voodoos)

- Revert the build optimization in ocaml/dune#2268. This optimization slows down building
  individual executables when they're part of an `executables` stanza group
  (ocaml/dune#3644, @rgrinberg)

- Use `{dev}` rather than `{pinned}` in the generated `.opam` file. (ocaml/dune#3647,
  @kit-ty-kate)

- Insert correct extension name when editing `dune-project` files. Previously,
  dune would just insert the stanza name. (ocaml/dune#3649, fixes ocaml/dune#3624, @rgrinberg)

- Fix crash when evaluating an `mdx` stanza that depends on unavailable
  packages. (ocaml/dune#3650, @craigfe)

- Fix typo in `cache-check-probablity` field in dune config files. This field
  now requires 2.7 as it wasn't usable before this version. (ocaml/dune#3652, @edwintorok)

- Add `"odoc" {with-doc}` to the dependencies in the generated `.opam` files.
  (ocaml/dune#3667, @kit-ty-kate)

- Do not allow user actions to capture dune's stdin (ocaml/dune#3677, fixes ocaml/dune#3672,
  @rgrinberg)

- `(subdir ...)` stanzas can now appear in dune files used via `(include ...)`.
  (ocaml/dune#3676, @nojb)
@Alizter Alizter moved this to Todo in Coq + Dune Jun 6, 2022
@Alizter Alizter moved this from Todo to Done in Coq + Dune Jun 6, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ejgallego ejgallego

Labels
coq
Projects
Coq + Dune
Archived in project
Milestone
No milestone
2 participants
@gares @ejgallego