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 coq top: add --no-build option to avoid building dependencies #7380

Merged
merged 1 commit into from
Apr 3, 2023
Merged

dune coq top: add --no-build option to avoid building dependencies #7380

merged 1 commit into from
Apr 3, 2023

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Mar 22, 2023 •
edited
Loading

We add a --no-build option to dune coq top that allows avoiding the building of dependencies.

  • changelog
  • doc

@Alizter Alizter added the coq label Mar 22, 2023
@Alizter Alizter mentioned this pull request Mar 22, 2023
Closed
@Alizter Alizter linked an issue Mar 22, 2023 that may be closed by this pull request
Option to make "dune coq top" more permissive #7355
Closed
@rlepigre
Copy link
Contributor

I'm getting the following error after trying this out:

Internal error, please report upstream including the contents of _build/log.
Description:
  ("Command.Expert.expand: Dyn encountred", {})
Raised at Stdune__code_error.raise in file
  "otherlibs/stdune/src/code_error.ml", line 11, characters 30-62
Called from Stdlib__List.rev_map.rmap_f in file "list.ml" (inlined), line
  103, characters 22-25
Called from Stdlib__List.rev_map in file "list.ml", line 105, characters 2-13
Called from Stdune__list.map in file "otherlibs/stdune/src/list.ml"
  (inlined), line 5, characters 19-33
Called from Dune_rules__command.Expert.expand in file
  "src/dune_rules/command.ml", line 155, characters 26-56
Called from Main__coqtop.term.(fun) in file "bin/coq/coqtop.ml", line 122,
  characters 18-64
Called from Fiber__scheduler.exec in file "otherlibs/fiber/src/scheduler.ml",
  line 73, characters 8-11

My test was run in a complicated project involving plugins.

@Alizter
Copy link
Collaborator Author

Alizter commented Mar 23, 2023

@rlepigre OK thanks, I was half expecting that. I will see what I can do about it.

@Alizter Alizter force-pushed the ps/branch/dune_coq_top__add___no_build_option_to_avoid_building_dependencies branch from b3fb03a to 29b62d9 Compare March 28, 2023 10:56
@Alizter
Copy link
Collaborator Author

Alizter commented Mar 28, 2023

@rlepigre I added a way for dynamic arguments to be expanded. See if this now works.

@rlepigre
Copy link
Contributor

Thanks @Alizter!

Testing in the same project as before, the internal error is gone, but even with --no-build all .vo files seem to be rebuilt (and there are additionally some errors due to .cmxs files not being found for plugins).

@Alizter
Copy link
Collaborator Author

Alizter commented Mar 28, 2023 •
edited
Loading

@rlepigre OK, looks like I am running too much now. I will try to tweak it so that it is I between. Not easy to do but I will have a go soon. I tried running it because otherwise we wouldn't get the plugin flags but looks like that didn't work anyway.

@Alizter Alizter force-pushed the ps/branch/dune_coq_top__add___no_build_option_to_avoid_building_dependencies branch from 29b62d9 to 4e90d64 Compare March 29, 2023 17:22
@Alizter
Copy link
Collaborator Author

Alizter commented Mar 29, 2023

OK I think I have a much simpler way to do it. Can you give it a go @rlepigre? This should avoid any rebuilding (coqdep included).

@ejgallego ejgallego self-assigned this Mar 29, 2023
@ejgallego
Copy link
Collaborator

Current version looks good to me, I think it should work. Happy to merge once test a doc are added.

@rlepigre
Copy link
Contributor

Seems to work perfectly! Thanks @Alizter.

@Alizter Alizter force-pushed the ps/branch/dune_coq_top__add___no_build_option_to_avoid_building_dependencies branch from 4e90d64 to 8c7e62e Compare March 29, 2023 21:15
@Alizter Alizter marked this pull request as ready for review March 29, 2023 21:16
rlepigre
rlepigre reviewed Mar 29, 2023
View reviewed changes
CHANGES.md Outdated Show resolved Hide resolved
@Alizter Alizter force-pushed the ps/branch/dune_coq_top__add___no_build_option_to_avoid_building_dependencies branch 2 times, most recently from ad10732 to e956951 Compare March 29, 2023 21:18
@rlepigre
Copy link
Contributor

rlepigre commented Apr 3, 2023

Is this not ready now @Alizter?

@Alizter
Copy link
Collaborator Author

Alizter commented Apr 3, 2023

@rlepigre yes it is, I'll try to get @ejgallego to give it a look and merge.

@ejgallego
Copy link
Collaborator

Shouldn't we document this in the rst files too? Otherwise looks good to me.

@Alizter Alizter force-pushed the ps/branch/dune_coq_top__add___no_build_option_to_avoid_building_dependencies branch from e956951 to ecf6bf3 Compare April 3, 2023 19:44
@Alizter
Copy link
Collaborator Author

Alizter commented Apr 3, 2023

@ejgallego I didn't initially want to advertise this specialist feature in the documentation so I didn't include it. Now I've changed my mind and included it.

@ejgallego ejgallego merged commit 7bed96d into ocaml:main Apr 3, 2023
@ejgallego
Copy link
Collaborator

ejgallego commented Apr 3, 2023 •
edited
Loading

Thanks @Alizter !

Indeed it seems to me that this is something often discussed by users so it makes sense to advertise it I think.

In particular as we are now using dune coq top with two purposes: to obtain the flags for a file, and to build its deps.

@Alizter Alizter deleted the ps/branch/dune_coq_top__add___no_build_option_to_avoid_building_dependencies branch April 3, 2023 22:04
@emillon emillon mentioned this pull request Apr 18, 2023
Closed
emillon added a commit to emillon/opam-repository that referenced this pull request Apr 18, 2023
@emillon
[new release] dune (15 packages) (3.8.0~alpha1)
8f04d31 
CHANGES:

- When a rule's action is interrupted, delete any leftover directory targets.
  This is consistent with how we treat file targets. (@rgrinberg, 7564)

- Fix plugin loading with findlib. The functionality was broken in 3.7.0.
  (ocaml/dune#7556, @anmonteiro)

- Introduce a `public_headers` field on libraries. This field is like
  `install_c_headers`, but it allows to choose the extension and choose the
  paths for the installed headers. (ocaml/dune#7512, @rgrinberg)

- Load the host context `findlib.conf` when cross-compiling (ocaml/dune#7428, fixes
  ocaml/dune#1701, @rgrinberg, @anmonteiro)

- Resolve `ppx_runtime_libraries` in the target context when cross compiling
  (ocaml/dune#7450, fixes ocaml/dune#2794, @anmonteiro)

- Use `$PKG_CONFIG`, when set, to find the `pkg-config` binary  (ocaml/dune#7469, fixes
  ocaml/dune#2572, @anmonteiro)

- Preliminary support for Coq compiled intefaces (`.vos` files) enabled via
  `(mode vos)` in `coq.theory` stanzas. This can be used in combination with
  `dune coq top` to obtain fast re-building of dependencies (with no checking
  of proofs) prior to stepping into a file. (ocaml/dune#7406, @rlepigre)

- Fix dune crashing on MacOS in watch mode whenever `$PATH` contains `$PWD`
  (ocaml/dune#7441, fixes ocaml/dune#6907, @rgrinberg)

- Fix `dune install` when cross compiling (ocaml/dune#7410, fixes ocaml/dune#6191, @anmonteiro,
  @rizo)

- Find `pps` dependencies in the host context when cross-compiling,  (ocaml/dune#7410,
  fixes ocaml/dune#4156, @anmonteiro)

- Dune in watch mode no longer builds concurrent rules in serial (ocaml/dune#7395
  @rgrinberg, @jchavarri)

- `dune coq top` now correctly respects the project root when called from a
  subdirectory. However, absolute filenames passed to `dune coq top` are no
  longer supported (due to being buggy) (ocaml/dune#7357, fixes ocaml/dune#7344, @rlepigre and
  @Alizter)

- Added a `--no-build` option to `dune coq top` for avoiding rebuilds (ocaml/dune#7380,
  fixes ocaml/dune#7355, @Alizter)

- RPC: Ignore SIGPIPE when clients suddenly disconnect (ocaml/dune#7299, ocaml/dune#7319, fixes
  ocaml/dune#6879, @rgrinberg)

- Always clean up the UI on exit. (ocaml/dune#7271, fixes ocaml/dune#7142 @rgrinberg)

- Bootstrap: remove reliance on shell. Previously, we'd use the shell to get
  the number of processors. (ocaml/dune#7274, @rgrinberg)

- Bootstrap: correctly detect the number of processors by allowing `nproc` to be
  looked up in `$PATH` (ocaml/dune#7272, @Alizter)

- Speed up file copying on macos by using `clonefile` when available
  (@rgrinberg, ocaml/dune#7210)

- Adds support for loading plugins in toplevels (ocaml/dune#6082, fixes ocaml/dune#6081,
  @ivg, @richardlford)

- Support commands that output 8-bit and 24-bit colors in the terminal (ocaml/dune#7188,
  @Alizter)

- Speed up rule generation for libraries and executables with many modules
  (ocaml/dune#7187, @jchavarri)

- Add `--watch-exclusions` to Dune build options (ocaml/dune#7216, @jonahbeckford)

- Do not re-render UI on every frame if the UI doesn't change (ocaml/dune#7186, fix
  ocaml/dune#7184, @rgrinberg)

- Make coq_db creation in scope lazy (@ejgallego, ocaml/dune#7133)

- Non-user proccesses such as version control or config checking are now run
  silently. (ocaml/dune#6994, fixes ocaml/dune#4066, @Alizter)

- Add the `--display-separate-messages` flag to separate the error messages
  produced by commands with a blank line. (ocaml/dune#6823, fixes ocaml/dune#6158, @esope)

- Accept the Ordered Set Language for the `modes` field in `library` stanzas
  (ocaml/dune#6611, @anmonteiro).

- dune install now respects --display quiet mode (ocaml/dune#7116, fixes ocaml/dune#4573, fixes
  ocaml/dune#7106, @Alizter)

- Stub shared libraries (dllXXX_stubs.so) in Dune-installed libraries could not
  be used as dependencies of libraries in the workspace (eg when compiling to
  bytecode and/or Javascript).  This is now fixed. (ocaml/dune#7151, @nojb)

- Allow the main module of a library with `(stdlib ...)` to depend on other
  libraries (ocaml/dune#7154, @anmonteiro).

- Bytecode executables built for JSOO are linked with `-noautolink` and no
  longer depend on the shared stubs of their dependent libraries (ocaml/dune#7156, @nojb)

- Added a new user action `(concurrent )` which is like `(progn )` but runs the
  actions concurrently. (ocaml/dune#6933, @Alizter)

- Allow `(stdlib ...)` to be used with `(wrapped false)` in library stanzas
  (ocaml/dune#7139, @anmonteiro).

- Allow parallel execution of inline tests partitions (ocaml/dune#7012, @hhugo)

- Support `(link_flags ...)` in `(cinaps ...)` stanza. (ocaml/dune#7423, fixes ocaml/dune#7416,
  @nojb)

- Allow `(package ...)` in any position within `(rule ...)` stanza (ocaml/dune#7445,
  @Leonidas-from-XIV)

- Always include `opam` files in the generated `.install` file. Previously, it
  would not be included whenever `(generate_opam_files true)` was set and the
  `.install` file wasn't yet generated. (ocaml/dune#7547, @rgrinberg)
@emillon emillon mentioned this pull request May 23, 2023
Merged
emillon added a commit to emillon/opam-repository that referenced this pull request May 23, 2023
@emillon
[new release] dune (15 packages) (3.8.0)
df1ab22 
CHANGES:

- Fix string quoting in the json file written by `--trace-file` (ocaml/dune#7773,
  @rleshchinskiy)

- Read `pkg-config` arguments from the `PKG_CONFIG_ARGN` environment variable
  (ocaml/dune#1492, ocaml/dune#7734, @anmonteiro)

- Correctly set `MANPATH` in `dune exec`. Previously, we would use the `bin/`
  directory of the context. (ocaml/dune#7655, @rgrinberg)

- Allow overriding the `ocaml` binary with findlib configuration (ocaml/dune#7648,
  @rgrinberg)

- merlin: ignore instrumentation settings for preprocessing. (ocaml/dune#7606, fixes
  ocaml/dune#7465, @Alizter)

- When a rule's action is interrupted, delete any leftover directory targets.
  This is consistent with how we treat file targets. (ocaml/dune#7564, @rgrinberg)

- Fix plugin loading with findlib. The functionality was broken in 3.7.0.
  (ocaml/dune#7556, @anmonteiro)

- Introduce a `public_headers` field on libraries. This field is like
  `install_c_headers`, but it allows to choose the extension and choose the
  paths for the installed headers. (ocaml/dune#7512, @rgrinberg)

- Load the host context `findlib.conf` when cross-compiling (ocaml/dune#7428, fixes
  ocaml/dune#1701, @rgrinberg, @anmonteiro)

- Add a `coqdoc_flags` field to the `coq.theory` stanza allowing the user to
  pass extra arguments to `coqdoc`. (ocaml/dune#7676, fixes ocaml/dune#7954 @Alizter)

- Resolve `ppx_runtime_libraries` in the target context when cross compiling
  (ocaml/dune#7450, fixes ocaml/dune#2794, @anmonteiro)

- Use `$PKG_CONFIG`, when set, to find the `pkg-config` binary  (ocaml/dune#7469, fixes
  ocaml/dune#2572, @anmonteiro)

- Modules that were declared in `(modules_without_implementation)`,
  `(private_modules)` or `(virtual_modules)` but not declared in `(modules)`
  will cause Dune to emit a warning which will become an error in 3.9. (ocaml/dune#7608,
  fixes ocaml/dune#7026, @Alizter)

- Preliminary support for Coq compiled intefaces (`.vos` files) enabled via
  `(mode vos)` in `coq.theory` stanzas. This can be used in combination with
  `dune coq top` to obtain fast re-building of dependencies (with no checking
  of proofs) prior to stepping into a file. (ocaml/dune#7406, @rlepigre)

- Fix dune crashing on MacOS in watch mode whenever `$PATH` contains `$PWD`
  (ocaml/dune#7441, fixes ocaml/dune#6907, @rgrinberg)

- Fix `dune install` when cross compiling (ocaml/dune#7410, fixes ocaml/dune#6191, @anmonteiro,
  @rizo)

- Find `pps` dependencies in the host context when cross-compiling,  (ocaml/dune#7410,
  fixes ocaml/dune#4156, @anmonteiro)

- Dune in watch mode no longer builds concurrent rules in serial (ocaml/dune#7395
  @rgrinberg, @jchavarri)

- Dune can now detect Coq theories from outside the workspace. This allows for
  composition with installed theories (not necessarily installed with Dune).
  (ocaml/dune#7047, @Alizter, @ejgallego)

- `dune coq top` now correctly respects the project root when called from a
  subdirectory. However, absolute filenames passed to `dune coq top` are no
  longer supported (due to being buggy) (ocaml/dune#7357, fixes ocaml/dune#7344, @rlepigre and
  @Alizter)

- Added a `--no-build` option to `dune coq top` for avoiding rebuilds (ocaml/dune#7380,
  fixes ocaml/dune#7355, @Alizter)

- RPC: Ignore SIGPIPE when clients suddenly disconnect (ocaml/dune#7299, ocaml/dune#7319, fixes
  ocaml/dune#6879, @rgrinberg)

- Always clean up the UI on exit. (ocaml/dune#7271, fixes ocaml/dune#7142 @rgrinberg)

- Bootstrap: remove reliance on shell. Previously, we'd use the shell to get
  the number of processors. (ocaml/dune#7274, @rgrinberg)

- Bootstrap: correctly detect the number of processors by allowing `nproc` to be
  looked up in `$PATH` (ocaml/dune#7272, @Alizter)

- Speed up file copying on macos by using `clonefile` when available
  (@rgrinberg, ocaml/dune#7210)

- Adds support for loading plugins in toplevels (ocaml/dune#6082, fixes ocaml/dune#6081,
  @ivg, @richardlford)

- Support commands that output 8-bit and 24-bit colors in the terminal (ocaml/dune#7188,
  @Alizter)

- Speed up rule generation for libraries and executables with many modules
  (ocaml/dune#7187, @jchavarri)

- Add `--watch-exclusions` to Dune build options (ocaml/dune#7216, @jonahbeckford)

- Do not re-render UI on every frame if the UI doesn't change (ocaml/dune#7186, fix
  ocaml/dune#7184, @rgrinberg)

- Make coq_db creation in scope lazy (@ejgallego, ocaml/dune#7133)

- Non-user proccesses such as version control or config checking are now run
  silently. (ocaml/dune#6994, fixes ocaml/dune#4066, @Alizter)

- Add the `--display-separate-messages` flag to separate the error messages
  produced by commands with a blank line. (ocaml/dune#6823, fixes ocaml/dune#6158, @esope)

- Accept the Ordered Set Language for the `modes` field in `library` stanzas
  (ocaml/dune#6611, @anmonteiro).

- dune install now respects --display quiet mode (ocaml/dune#7116, fixes ocaml/dune#4573, fixes
  ocaml/dune#7106, @Alizter)

- Stub shared libraries (dllXXX_stubs.so) in Dune-installed libraries could not
  be used as dependencies of libraries in the workspace (eg when compiling to
  bytecode and/or Javascript).  This is now fixed. (ocaml/dune#7151, @nojb)

- Allow the main module of a library with `(stdlib ...)` to depend on other
  libraries (ocaml/dune#7154, @anmonteiro).

- Bytecode executables built for JSOO are linked with `-noautolink` and no
  longer depend on the shared stubs of their dependent libraries (ocaml/dune#7156, @nojb)

- Added a new user action `(concurrent )` which is like `(progn )` but runs the
  actions concurrently. (ocaml/dune#6933, @Alizter)

- Allow `(stdlib ...)` to be used with `(wrapped false)` in library stanzas
  (ocaml/dune#7139, @anmonteiro).

- Allow parallel execution of inline tests partitions (ocaml/dune#7012, @hhugo)

- Support `(link_flags ...)` in `(cinaps ...)` stanza. (ocaml/dune#7423, fixes ocaml/dune#7416,
  @nojb)

- Allow `(package ...)` in any position within `(rule ...)` stanza (ocaml/dune#7445,
  @Leonidas-from-XIV)

- Always include `opam` files in the generated `.install` file. Previously, it
  would not be included whenever `(generate_opam_files true)` was set and the
  `.install` file wasn't yet generated. (ocaml/dune#7547, @rgrinberg)

- Fix regression where Merlin was unable to handle filenames with uppercase
  letters under Windows. (ocaml/dune#7577, @nojb)

- On nix+macos, pass `-f` to the codesign hook to avoid errors when the binary
  is already signed (ocaml/dune#7183, fixes ocaml/dune#6265, @greedy)

- Fix bug where RPC clients built with dune-rpc-lwt would crash when closing
  their connection to the server (ocaml/dune#7581, @gridbugs)

- Introduce mdx stanza 0.4 requiring mdx >= 2.3.0 which updates the default
  list of files to include `*.mld` files (ocaml/dune#7582, @Leonidas-from-XIV)

- Fix RPC server on Windows (used for OCaml-LSP). (ocaml/dune#7666, @nojb)

- Coq language versions less 0.8 are deprecated, and will be removed
  in an upcoming Dune version. All users are required to migrate to
  `(coq lang 0.8)` which provides the right semantics for theories
  that have been globally installed, such as those coming from opam
  (@ejgallego, @Alizter)

- Bump minimum version of the dune language for the melange syntax extension
  from 3.7 to 3.8 (ocaml/dune#7665, @jchavarri)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@rlepigre rlepigre rlepigre left review comments

@christinerose christinerose Awaiting requested review from christinerose christinerose is a code owner

Assignees

@ejgallego ejgallego

Labels
coq
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Option to make "dune coq top" more permissive
3 participants
@Alizter @rlepigre @ejgallego