fix(coq): Fix performance regression in coqdep unescaping #10115
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
Regression from ocaml#9231 Fixes ocaml#10088 Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
With this PR, zero build for Coq-HoTT: so it seems like reasonable as to consider the original regression closed. I was curious and I did time the And indeed, it seems we are not memoizing the parsing of the .v.d. file, that's gonna be terrible! (cc: @Alizter ) I seem to recall we had this properly covered, I wonder what happened? But def we should store the |
|
This PR is pretty trivial so I will merge soon, anyways the regression fixed is not observable after #10116 is merged, which solves the real culprit. |
rlepigre
pushed a commit
to rlepigre/dune
that referenced
this pull request
Feb 29, 2024
fix(coq): Fix performance regression in coqdep unescaping
rlepigre
pushed a commit
to rlepigre/dune
that referenced
this pull request
Feb 29, 2024
fix(coq): Fix performance regression in coqdep unescaping
rlepigre
pushed a commit
to rlepigre/dune
that referenced
this pull request
Feb 29, 2024
fix(coq): Fix performance regression in coqdep unescaping
This was referenced Mar 5, 2024
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.
Regression from #9231
Fixes #10088