[coq] Memoize coqdep parsing #10116
Merged
[coq] Memoize coqdep parsing #10116
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ejgallego
force-pushed
the
coq_memo_coqdep
branch
from
adf8dee
to
8a08ba8
Compare
ejgallego
force-pushed
the
coq_memo_coqdep
branch
2 times, most recently
from
08abdb0
to
b615000
Compare
ejgallego
force-pushed
the
coq_memo_coqdep
branch
from
b615000
to
c5fdf4f
Compare
I was under the impression that our current code was taking care of this already, however it was not. Suggestions on what is best w.r.t. `Memo/Action_builder` code dance welcome. Obviously, this has a dramatic effect on most Coq builds, for example HoTT's zero build is now: ``` before: ------- real 0m5,302s user 0m5,197s sys 0m0,056s after: ------ real 0m0,210s user 0m0,143s sys 0m0,034s ``` Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
ejgallego
force-pushed
the
coq_memo_coqdep
branch
from
c5fdf4f
to
175ccfc
Compare
rgrinberg
approved these changes
Feb 22, 2024
rlepigre
pushed a commit
to rlepigre/dune
that referenced
this pull request
Feb 29, 2024
[coq] Memoize coqdep parsing
rlepigre
pushed a commit
to rlepigre/dune
that referenced
this pull request
Feb 29, 2024
[coq] Memoize coqdep parsing
rlepigre
pushed a commit
to rlepigre/dune
that referenced
this pull request
Feb 29, 2024
[coq] Memoize coqdep parsing
Leonidas-from-XIV
added a commit
to Leonidas-from-XIV/opam-repository
that referenced
this pull request
Mar 11, 2024
CHANGES: ### Fixed - When a directory is changed to a file, correctly remove it in subsequent `dune build` runs. (ocaml/dune#9327, fix ocaml/dune#6575, @emillon) - Fix a problem with the doc-new target where transitive dependencies were missed during compile. This leads to missing expansions in the output docs. (ocaml/dune#9955, @jonludlam) - coq: fix performance regression in coqdep unescaping (ocaml/dune#10115, fixes ocaml/dune#10088, @ejgallego, thanks to Dan Christensen for the report) - coq: memoize coqdep parsing, this will reduce build times for Coq users, in particular for those with many .v files (ocaml/dune#10116, @ejgallego, see also ocaml/dune#10088) - on Windows, use an unicode-aware version of `CreateProcess` to avoid crashes when paths contains non-ascii characters. (ocaml/dune#10212, fixes ocaml/dune#10180, @emillon)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I was under the impression that our current code was taking care of this already, however it was not.
Suggestions on what is best w.r.t.
Memo/Action_buildercode dance welcome.Obviously, this has a dramatic effect on most Coq builds, for example HoTT's zero build is now:
Signed-off-by: Emilio Jesus Gallego Arias e+git@x80.org