Skip to content

Evaluate DUNE_IN_FILES eagerly#1263

Merged
gares merged 2 commits into
rocq-prover:mainfrom
shilangyu:mw/faster-makefile
Jun 15, 2026
Merged

Evaluate DUNE_IN_FILES eagerly#1263
gares merged 2 commits into
rocq-prover:mainfrom
shilangyu:mw/faster-makefile

Conversation

@shilangyu

Copy link
Copy Markdown
Contributor

Otherwise it is evaluated multiple times per a single call to make. This is especially slow when find looks through _build and _opam directories which are large. In my case running make would take 15 seconds.

Also I moved some gitignore. Makes it more scoped and the ignores also work in editors if you open only the subfolder.

Otherwise it is evaluated multiple times per a call to `make`. This is
especially slow when `find` looks through `_build` and `_opam`
directories which are large.
@gares gares merged commit 2ad60a8 into rocq-prover:main Jun 15, 2026
34 of 35 checks passed
@shilangyu shilangyu deleted the mw/faster-makefile branch June 15, 2026 07:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants