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

Dune appends (using coq.theory 0.2) instead of (using coq 0.2) #3624

Closed
yannl35133 opened this issue Jul 13, 2020 · 0 comments · Fixed by ocaml/opam-repository#17005
Closed

Dune appends (using coq.theory 0.2) instead of (using coq 0.2) #3624

yannl35133 opened this issue Jul 13, 2020 · 0 comments · Fixed by ocaml/opam-repository#17005
Assignees
@ejgallego
Labels
coq

Comments

@yannl35133
Copy link

When creating a new "dune repo" for Coq, if we don't mention (using coq 0.2) in dune-project (eg. not creating the file), the first dune build will append (using coq.theory 0.2) to the file, yet the following dune builds expect (using coq 0.2).

First reported by:
I ran into issue 2/3 as well: Info: appending this line to dune-project: (using coq.theory 0.1) is wrong; it needs to append (using coq 0.1) instead. I also mistakenly used filename.v instead of filename at first in the list of module; it would be nice to have examples in the doc.

Originally posted by @cpitclaudel in #2042 (comment)
@ghost ghost assigned ejgallego Jul 13, 2020
rgrinberg added a commit to rgrinberg/jbuilder that referenced this issue Jul 24, 2020
@rgrinberg
Reproduce ocaml#3624
89baefe 
This bug demonstrates dune adding an incorrect `using` line in a create
dune-project file.

Signed-off-by: Rudi Grinberg <[email protected]>
rgrinberg added a commit to rgrinberg/jbuilder that referenced this issue Jul 24, 2020
@rgrinberg
Fix ocaml#3624
9582131 
Dune should insert the name of the extension to the dune-project file.

Signed-off-by: Rudi Grinberg <[email protected]>
rgrinberg added a commit to rgrinberg/jbuilder that referenced this issue Jul 24, 2020
@rgrinberg
Fix ocaml#3624
1d6bd49 
Dune should insert the name of the extension to the dune-project file.

Signed-off-by: Rudi Grinberg <[email protected]>
rgrinberg added a commit to rgrinberg/jbuilder that referenced this issue Jul 27, 2020
@rgrinberg
Reproduce ocaml#3624
234c38e 
This bug demonstrates dune adding an incorrect `using` line in a create
dune-project file.

Signed-off-by: Rudi Grinberg <[email protected]>
rgrinberg added a commit that referenced this issue Jul 27, 2020
@rgrinberg
Merge pull request #3649 from rgrinberg/fix-3624
2f25e48 
Fix #3624
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
@Alizter Alizter added the coq label 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
3 participants
@ejgallego @Alizter @yannl35133