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

Running "dune coq top --no-build ..." tries to take the lock #7671

Closed
rlepigre opened this issue May 3, 2023 · 5 comments · Fixed by #10547
Closed

Running "dune coq top --no-build ..." tries to take the lock #7671

rlepigre opened this issue May 3, 2023 · 5 comments · Fixed by #10547
Labels
coq

Comments

@rlepigre
Copy link
Contributor

rlepigre commented May 3, 2023

Expected Behavior

Running dune coq top --no-build ... should not fail if there is a concurrently running dune build command.

Actual Behavior

You get: Error: A running dune instance has locked the build directory.

Is there anything we can do to fix this? Or does dune coq top --no-build ... possibly need to build stuff?
@Alizter
Copy link
Collaborator

Alizter commented May 3, 2023 •
edited
Loading

@rlepigre I'll look into it. We might be running coqdep causing the build to lock.

I'll also write a cram so that we can preserve this behaviour.

@Alizter Alizter added the coq label May 3, 2023
@rlepigre
Copy link
Contributor Author

rlepigre commented May 3, 2024

@Alizter did you ever try looking into this, or did you just not get the time?

@Alizter
Copy link
Collaborator

Alizter commented May 3, 2024

@rlepigre I remember investigating but I didn't find anything conclusive. The nobuuild was set up correctly as far as I could tell, but something was causing the global lock to trigger.

@rlepigre
Copy link
Contributor Author

rlepigre commented May 3, 2024

OK cool. Now that I think about it, is it possible that this got fixed by #10446?

@Alizter
Copy link
Collaborator

Alizter commented May 3, 2024

@rlepigre I think it's unlikely, but I haven't checked. I think this issue was around before that bug was introduced.

@lzy0505 lzy0505 mentioned this issue May 17, 2024
Merged
@gridbugs gridbugs mentioned this issue Jun 5, 2024
Closed
gridbugs added a commit to gridbugs/opam-repository that referenced this issue Jun 5, 2024
@gridbugs
[new release] dune (15 packages) (3.16.0~alpha1)
0858f47 
CHANGES:

### Added

- allow libraries with the same `(name ..)` in projects as long as they don't
  conflict during resolution (via `enabled_if`). (ocaml/dune#10307, @anmonteiro,
  @jchavarri)

- `dune describe pp` now finds the exact module and the stanza it belongs to,
  instead of guessing the name of the preprocessed file. (ocaml/dune#10321, @anmonteiro)

- Print the result of `dune describe pp` with the respective dialect printer.
  (ocaml/dune#10322, @anmonteiro)

- Add new flag `--context` to `dune ocaml-merlin`, which allows to select a
  Dune context when requesting Merlin config. Add `dune describe contexts`
  subcommand. Introduce a field `generate_merlin_rules` for contexts declared
  in the workspace, that allows to optionally produce Merlin rules for other
  contexts besides the one selected for Merlin (ocaml/dune#10324, @jchavarri)

- melange: add include paths for private library `.cmj` files during JS
  emission. (ocaml/dune#10416, @anmonteiro)

- `dune ocaml-merlin`: communicate additional directives `SOURCE_ROOT`,
  `UNIT_NAME` (the actual name with wrapping) and `INDEX` with the paths to the
  index(es). (ocaml/dune#10422, @voodoos)

- Add a new alias `@ocaml-index` that uses the `ocaml-index` binary to generate
  indexes that can be read by tools such as Merlin to provide project-wide
  references search. (ocaml/dune#10422, @voodoos)

- merlin: add optional `(merlin_reader CMD)` construct to `(dialect)` stanza to
  configure a merlin reader (ocaml/dune#8567, @andreypopp)

### Changed

- melange: treat private libraries with `(package ..)` as public libraries,
  fixing an issue where `import` paths were wrongly emitted. (ocaml/dune#10415,
  @anmonteiro)

- install `.glob` files for Coq theories too (ocaml/dune#10602, @ejgallego)

### Fixed

- Don't try to document non-existent libraries in doc-new target (ocaml/dune#10319, fixes
  ocaml/dune#10056, @jonludlam)

- Make `dune-site`'s `load_all` function look for `META` files so that it
  doesn't fail on empty directories in the plugin directory (ocaml/dune#10458, fixes
  ocaml/dune#10457, @shym)

- Fix incorrect warning for libraries defined inside non-existant directories
  using `(subdir ..)` and used by executables using `dune-build-info` (ocaml/dune#10525,
  @rgrinberg)

- Don't try to take build lock when running `coq top --no-build` (ocaml/dune#10547, fixes
  ocaml/dune#7671, @lzy0505)

- Make sure to truncate dune's lock file after locking and unlocking so that
  users cannot observe incorrect pid's (ocaml/dune#10575, @rgrinberg)

- mdx: link mdx binary with `byte_complete`. This fixes `(libraries)` with
  foreign archives on Linux. (ocaml/dune#10586, fixes ocaml/dune#10582, @anmonteiro)
emillon added a commit to emillon/opam-repository that referenced this issue Jun 17, 2024
@emillon
[new release] dune (15 packages) (3.16.0)
a6069b9 
CHANGES:

### Added

- allow libraries with the same `(name ..)` in projects as long as they don't
  conflict during resolution (via `enabled_if`). (ocaml/dune#10307, @anmonteiro,
  @jchavarri)

- `dune describe pp` now finds the exact module and the stanza it belongs to,
  instead of guessing the name of the preprocessed file. (ocaml/dune#10321, @anmonteiro)

- Print the result of `dune describe pp` with the respective dialect printer.
  (ocaml/dune#10322, @anmonteiro)

- Add new flag `--context` to `dune ocaml-merlin`, which allows to select a
  Dune context when requesting Merlin config. Add `dune describe contexts`
  subcommand. Introduce a field `generate_merlin_rules` for contexts declared
  in the workspace, that allows to optionally produce Merlin rules for other
  contexts besides the one selected for Merlin (ocaml/dune#10324, @jchavarri)

- melange: add include paths for private library `.cmj` files during JS
  emission. (ocaml/dune#10416, @anmonteiro)

- `dune ocaml-merlin`: communicate additional directives `SOURCE_ROOT`,
  `UNIT_NAME` (the actual name with wrapping) and `INDEX` with the paths to the
  index(es). (ocaml/dune#10422, @voodoos)

- Add a new alias `@ocaml-index` that uses the `ocaml-index` binary to generate
  indexes that can be read by tools such as Merlin to provide project-wide
  references search. (ocaml/dune#10422, @voodoos)

- merlin: add optional `(merlin_reader CMD)` construct to `(dialect)` stanza to
  configure a merlin reader (ocaml/dune#8567, @andreypopp)

### Changed

- melange: treat private libraries with `(package ..)` as public libraries,
  fixing an issue where `import` paths were wrongly emitted. (ocaml/dune#10415,
  @anmonteiro)

- install `.glob` files for Coq theories too (ocaml/dune#10602, @ejgallego)

### Fixed

- Don't try to document non-existent libraries in doc-new target (ocaml/dune#10319, fixes
  ocaml/dune#10056, @jonludlam)

- Make `dune-site`'s `load_all` function look for `META` files so that it
  doesn't fail on empty directories in the plugin directory (ocaml/dune#10458, fixes
  ocaml/dune#10457, @shym)

- Fix incorrect warning for libraries defined inside non-existant directories
  using `(subdir ..)` and used by executables using `dune-build-info` (ocaml/dune#10525,
  @rgrinberg)

- Don't try to take build lock when running `coq top --no-build` (ocaml/dune#10547, fixes
  ocaml/dune#7671, @lzy0505)

- Make sure to truncate dune's lock file after locking and unlocking so that
  users cannot observe incorrect pid's (ocaml/dune#10575, @rgrinberg)

- mdx: link mdx binary with `byte_complete`. This fixes `(libraries)` with
  foreign archives on Linux. (ocaml/dune#10586, fixes ocaml/dune#10582, @anmonteiro)

- virtual libraries: fix an issue where linking an executable involving several
  virtual libries would cause an error. (ocaml/dune#10581, fixes ocaml/dune#10460, @rgrinberg)
@emillon emillon mentioned this issue Jun 17, 2024
Merged
avsm pushed a commit to avsm/opam-repository that referenced this issue Sep 5, 2024
@emillon @avsm
[new release] dune (15 packages) (3.16.0)
4423f45 
CHANGES:

### Added

- allow libraries with the same `(name ..)` in projects as long as they don't
  conflict during resolution (via `enabled_if`). (ocaml/dune#10307, @anmonteiro,
  @jchavarri)

- `dune describe pp` now finds the exact module and the stanza it belongs to,
  instead of guessing the name of the preprocessed file. (ocaml/dune#10321, @anmonteiro)

- Print the result of `dune describe pp` with the respective dialect printer.
  (ocaml/dune#10322, @anmonteiro)

- Add new flag `--context` to `dune ocaml-merlin`, which allows to select a
  Dune context when requesting Merlin config. Add `dune describe contexts`
  subcommand. Introduce a field `generate_merlin_rules` for contexts declared
  in the workspace, that allows to optionally produce Merlin rules for other
  contexts besides the one selected for Merlin (ocaml/dune#10324, @jchavarri)

- melange: add include paths for private library `.cmj` files during JS
  emission. (ocaml/dune#10416, @anmonteiro)

- `dune ocaml-merlin`: communicate additional directives `SOURCE_ROOT`,
  `UNIT_NAME` (the actual name with wrapping) and `INDEX` with the paths to the
  index(es). (ocaml/dune#10422, @voodoos)

- Add a new alias `@ocaml-index` that uses the `ocaml-index` binary to generate
  indexes that can be read by tools such as Merlin to provide project-wide
  references search. (ocaml/dune#10422, @voodoos)

- merlin: add optional `(merlin_reader CMD)` construct to `(dialect)` stanza to
  configure a merlin reader (ocaml/dune#8567, @andreypopp)

### Changed

- melange: treat private libraries with `(package ..)` as public libraries,
  fixing an issue where `import` paths were wrongly emitted. (ocaml/dune#10415,
  @anmonteiro)

- install `.glob` files for Coq theories too (ocaml/dune#10602, @ejgallego)

### Fixed

- Don't try to document non-existent libraries in doc-new target (ocaml/dune#10319, fixes
  ocaml/dune#10056, @jonludlam)

- Make `dune-site`'s `load_all` function look for `META` files so that it
  doesn't fail on empty directories in the plugin directory (ocaml/dune#10458, fixes
  ocaml/dune#10457, @shym)

- Fix incorrect warning for libraries defined inside non-existant directories
  using `(subdir ..)` and used by executables using `dune-build-info` (ocaml/dune#10525,
  @rgrinberg)

- Don't try to take build lock when running `coq top --no-build` (ocaml/dune#10547, fixes
  ocaml/dune#7671, @lzy0505)

- Make sure to truncate dune's lock file after locking and unlocking so that
  users cannot observe incorrect pid's (ocaml/dune#10575, @rgrinberg)

- mdx: link mdx binary with `byte_complete`. This fixes `(libraries)` with
  foreign archives on Linux. (ocaml/dune#10586, fixes ocaml/dune#10582, @anmonteiro)

- virtual libraries: fix an issue where linking an executable involving several
  virtual libries would cause an error. (ocaml/dune#10581, fixes ocaml/dune#10460, @rgrinberg)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
coq
Projects
Coq + Dune
Archived in project
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: don't take build lock for coq top --no-build lzy0505/dune
2 participants
@rlepigre @Alizter