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

feature(coq): call coqdep once per theory #7048

Merged
merged 4 commits into from
Feb 13, 2023
Merged

feature(coq): call coqdep once per theory #7048

merged 4 commits into from
Feb 13, 2023

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Feb 12, 2023 •
edited
Loading

We now call coqdep once per theory. Each theory produces a mytheory.theory.d file which is then further interpreted into an internal dependency map.

This is joint work with @ejgallego.

TODO:

@Alizter Alizter force-pushed the ps/rr/feature_coq___call_coqdep_once_per_theory branch from 659514b to 3f470df Compare February 12, 2023 01:31
@Alizter Alizter added the coq label Feb 12, 2023
@Alizter Alizter added this to the 3.8.0 milestone Feb 12, 2023
@Alizter
feature(coq): call coqdep once per theory
30043d8 
<!-- ps-id: caa26aa8-d2fa-4df5-8f47-58eb642c07d5 -->

Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter Alizter force-pushed the ps/rr/feature_coq___call_coqdep_once_per_theory branch from 3f470df to 30043d8 Compare February 12, 2023 18:28
@Alizter Alizter mentioned this pull request Feb 12, 2023
Open
@SkySkimmer
Copy link

This is still a bit inefficient, however should be much faster than the multiple coqdep calls we had before.

This may be true for building from 0, but is it true for incremental builds?

@Alizter
Copy link
Collaborator Author

Alizter commented Feb 12, 2023

@SkySkimmer In my own testing (on quite a slow laptop), the batched call to coqdep has been negligable compared to running it for each file, as you say from 0. However even when doing an incremental build, the call to coqdep for a large theory such as the stdlib is still quite small and hardly noticeable.

This does scale well, since when we add more theories, we are calling coqdep per theory. It will have difficulty scaling if there are a lot of .v files in a single theory, but that would probably take place in the thousands.

ejgallego and others added 2 commits February 13, 2023 20:13
@ejgallego @Alizter
[coq] Parse coqdep output into a shared dependency map.
ef5b971 
This avoids generating the individual `.v.d` files, and should provide
a modest speedup, and cleaner code.

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
Co-authored-by: Ali Caglayan <alizter@gmail.com>
@Alizter
Merge branch 'main' into ps/rr/feature_coq___call_coqdep_once_per_theory
de6db9b
@Alizter Alizter marked this pull request as ready for review February 13, 2023 20:40
@Alizter
add changelog
d2d5e2e 
Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter
Copy link
Collaborator Author

Alizter commented Feb 13, 2023

I will update the documentation in a followup PR.

@Alizter Alizter modified the milestones: 3.8.0, 3.7.0 Feb 13, 2023
@Alizter Alizter merged commit 20e0b26 into ocaml:main Feb 13, 2023
@Alizter Alizter deleted the ps/rr/feature_coq___call_coqdep_once_per_theory branch February 13, 2023 20:59
@ejgallego
Copy link
Collaborator

This may be true for building from 0, but is it true for incremental builds?

Yes, coqdep can lex .v files very fast, so the whole of coq-universe is like 1.5 MiB of code, that's in the miliseconds, however the scanning of the filesystem is what takes 99% of the coqdep time, so even if you touch 2 files this is faster already.

@ejgallego
Copy link
Collaborator

I will update the documentation in a followup PR.

Great! A few comments inline.

ejgallego
ejgallego reviewed Feb 13, 2023
View reviewed changes
CHANGES.md Show resolved Hide resolved
ejgallego
ejgallego reviewed Feb 13, 2023
View reviewed changes
src/dune_rules/coq/coq_rules.ml
let setup_coqdep_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name ~use_stdlib
~source_rule ~ml_flags ~mlpack_rule coq_module =
let* boot_type = boot_type ~dir ~use_stdlib ~wrapper_name coq_module in
let dep_theory_file ~dir ~wrapper_name =
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess wrapper name is Ok, but we can maybe revisit this at some point.

ejgallego
ejgallego reviewed Feb 13, 2023
View reviewed changes
src/dune_rules/coq/coq_rules.ml
:: deps
in
(target, deps)

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should go to Coq_copdep, and provide a better interface.

ejgallego
ejgallego reviewed Feb 13, 2023
View reviewed changes
src/dune_rules/coq/coq_rules.ml
| Some (basename, deps) ->
let target = List.hd @@ String.extract_blank_separated_words basename in
(* let depname, ext = Filename.split_extension ff in *)
let target = Path.relative (Path.build dir) target in
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

target needs to be handled better, for example to filter .vio files out, also to guard against permuations, the List.hd handling is a bit hacky.

ejgallego added a commit to ejgallego/dune that referenced this pull request Feb 13, 2023
@ejgallego
[changes] [coq] Tweaks to ocaml#7048 changelog
2a5d638
ejgallego added a commit to ejgallego/dune that referenced this pull request Feb 13, 2023
@ejgallego
[changes] [coq] Tweaks to ocaml#7048 changelog
a0f11e0 
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
ejgallego added a commit to ejgallego/dune that referenced this pull request Feb 13, 2023
@ejgallego
[changes] [coq] Tweaks to ocaml#7048 changelog
d422b3e 
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
ejgallego added a commit to ejgallego/dune that referenced this pull request Feb 13, 2023
@ejgallego
[changes] [coq] Tweaks to ocaml#7048 changelog
051eba0 
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
Alizter pushed a commit that referenced this pull request Feb 13, 2023
@ejgallego @Alizter
[changes] [coq] Tweaks to #7048 changelog
aca5354 
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
@emillon emillon mentioned this pull request Feb 17, 2023
Merged
emillon added a commit to emillon/opam-repository that referenced this pull request Feb 17, 2023
@emillon
[new release] xdg, stdune, ordering, ocamlc-loc, dyn, dune, dune-site…
c5fc79e 
…, dune-rpc, dune-rpc-lwt, dune-private-libs, dune-glob, dune-configurator, dune-build-info, dune-action-plugin and chrome-trace (3.7.0)

CHANGES:

- Allow running `$ dune exec` in watch mode (with the `-w` flag). In watch mode,
  `$ dune exec` the executed binary whenever it is recompiled. (ocaml/dune#6966,
  @gridbugs)

- `coqdep` is now called once per theory, instead of one time per Coq
  file. This should significantly speed up some builds, as `coqdep`
  startup time is often heavy (ocaml/dune#7048, @Alizter, @ejgallego)

- Add `map_workspace_root` dune-project stanza to allow disabling of
  mapping of workspace root to `/workspace_root`. (ocaml/dune#6988, fixes ocaml/dune#6929,
  @richardlford)

- Fix handling of support files generated by odoc. (ocaml/dune#6913, @jonludlam)

- Fix parsing of OCaml errors that contain code excerpts with `...` in them.
  (ocaml/dune#7008, @rgrinberg)

- Pre-emptively clear screen in watch mode (ocaml/dune#6987, fixes ocaml/dune#6884, @rgrinberg)

- Fix cross compilation configuration when a context with targets is itself a
  host of another context (ocaml/dune#6958, fixes ocaml/dune#6843, @rgrinberg)

- Fix parsing of the `<=` operator in *blang* expressions of `dune` files.
  Previously, the operator would be interpreted as `<`. (ocaml/dune#6928, @tatchi)

- Fix `--trace-file` output. Dune now emits a single *complete* event for every
  executed process. Unterminated *async* events are no longer written. (ocaml/dune#6892,
  @rgrinberg)

- Fix preprocessing with `staged_pps` (ocaml/dune#6748, fixes ocaml/dune#6644, @rgrinberg)

- Use colored output with MDX when Dune colors are enabled.
  (ocaml/dune#6462, @MisterDA)

- Make `dune describe workspace` return consistent dependencies for
  executables and for libraries. By default, compile-time dependencies
  towards PPX-rewriters are from now not taken into account (but
  runtime dependencies always are). Compile-time dependencies towards
  PPX-rewriters can be taken into account by providing the
  `--with-pps` flag. (ocaml/dune#6727, fixes ocaml/dune#6486, @esope)

- Print missing newline after `$ dune exec`. (ocaml/dune#6821, fixes ocaml/dune#6700, @rgrinberg,
  @Alizter)

- Fix binary corruption when installing or promoting in parallel (ocaml/dune#6669, fixes
  ocaml/dune#6668, @edwintorok)

- Use colored output with GCC and Clang when compiling C stubs. The
  flag `-fdiagnostics-color=always` is added to the `:standard` set of
  flags. (ocaml/dune#4083, @MisterDA)

- Fix the parsing of decimal and hexadecimal escape literals in `dune`,
  `dune-package`, and other dune s-expression based files (ocaml/dune#6710, @shym)

- Report an error if `dune init ...` would create a "dune" file in a location
  which already contains a "dune" directory (ocaml/dune#6705, @gridbugs)

- Fix the parsing of alerts. They will now show up in diagnostics correctly.
  (ocaml/dune#6678, @rginberg)

- Fix the compilation of modules generated at link time when
  `implicit_transitive_deps` is enabled (ocaml/dune#6642, @rgrinberg)

- Allow `$ dune utop` to load libraries defined in data only directories
  defined using `(subdir ..)` (ocaml/dune#6631, @rgrinberg)

- Format dune files when they are named `dune-file`. This occurs when we enable
  the alternative file names project option. (ocaml/dune#6566, @rgrinberg)

- Move `$ dune ocaml-merlin -dump-config=$dir` to `$ dune ocaml merlin
  dump-config $dir`. (ocaml/dune#6547, @rgrinberg)

- Allow compilation rules to be impacted by `(env ..)` stanzas that modify the
  environment or set binaries. (ocaml/dune#6527, @rgrinberg)

- Coq native mode is now automatically detected by Dune starting with Coq lang
  0.7. `(mode native)` has been deprecated in favour of detection from the
  configuration of Coq. (ocaml/dune#6409, @Alizter)

- Print "Leaving Directory" whenever "Entering Directory" is printed. (ocaml/dune#6419,
  fixes ocaml/dune#138, @cpitclaudel, @rgrinberg)

- Allow `$ dune ocaml dump-dot-merlin` to run in watch mode. Also this command
  shouldn't print "Entering Directory" mesages. (ocaml/dune#6497, @rgrinberg)

- `dune clean` should no longer fail under Windows due to the inability to
  remove the `.lock` file. Also, bring the implementation of the global lock
  under Windows closer to that of Unix. (ocaml/dune#6523, @nojb)

- Remove "Entering Directory" messages for `$ dune install`. (ocaml/dune#6513,
  @rgrinberg)

- Stop passing `-q` flag in `dune coq top`, which allows for `.coqrc` to be
  loaded. (ocaml/dune#6848, fixes ocaml/dune#6847, @Alizter)

- Fix missing dependencies when detecting the kind of C compiler we're using
  (ocaml/dune#6610, fixes ocaml/dune#6415, @emillon)

- Allow `(include_subdirs qualified)` for OCaml projects. (ocaml/dune#6594, fixes ocaml/dune#1084,
  @rgrinberg)

- Accurately determine merlin configuration for all sources selected with
  `copy#` and `copy_files#`. The old heuristic of looking for a module in
  parent directories is removed (ocaml/dune#6594, @rgrinberg)

- Fix inline tests with *js_of_ocaml* and whole program compilation mode
  enabled (ocaml/dune#6645, @hhugo)

- Fix *js_of_ocaml* separate compilation rules when `--enable=effects`
  ,`--enable=use-js-string` or `--toplevel` is used. (ocaml/dune#6714, ocaml/dune#6828, ocaml/dune#6920, @hhugo)

- Fix *js_of_ocaml* separate compilation in presence of linkall (ocaml/dune#6832, ocaml/dune#6916, @hhugo)

- Remove spurious build dir created when running `dune init proj ...` (ocaml/dune#6707,
  fixes ocaml/dune#5429, @gridbugs)

- Allow `--sandbox` to affect `ocamldep` invocations. Previously, they were
  wrongly marked as incompatible (ocaml/dune#6749, @rgrinberg)

- Validate the command line arguments for `$ dune ocaml top-module`. This
  command requires one positional argument (ocaml/dune#6796, fixes ocaml/dune#6793, @rgrinberg)

- Add a `dune cache size` command for displaying the size of the cache (ocaml/dune#6638,
  @Alizter)

- Fix dependency cycle when installing files to the bin section with
  `glob_files` (ocaml/dune#6764, fixes ocaml/dune#6708, @gridbugs)

- Handle "Too many links" errors when using Dune cache on Windows (ocaml/dune#6993, @nojb)

- Allow the `cinaps` stanza to set a custom alias. By default, if the alias is
  not set then the cinaps actions will be attached to both `@cinaps` and
  `@runtest` (ocaml/dune#6991, @rgrinberg)

- Add `(using ctypes 0.3)`. When used, paths in `(ctypes)` are interpreted
  relative to where the stanza is defined. (ocaml/dune#6883, fixes ocaml/dune#5325, @emillon)

- Auto-detect `dune-workspace` files as `dune` files in Emacs (ocaml/dune#7061,
  @ilankri)

- Add native support for polling mode on Windows (ocaml/dune#7010, @yams-yams, @nojb)
moyodiallo pushed a commit to moyodiallo/dune that referenced this pull request Apr 3, 2023
@ejgallego @moyodiallo
[changes] [coq] Tweaks to ocaml#7048 changelog
94dd128 
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
@palmskog palmskog mentioned this pull request Jun 24, 2023
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ejgallego ejgallego ejgallego left review comments

Assignees
No one assigned
Labels
coq
Projects
None yet
Milestone
3.7.0
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@Alizter @SkySkimmer @ejgallego