Paolo G. Giarrusso

Results 324 comments of Paolo G. Giarrusso

TLDR: IIUC, proper caching compositional builds _require_ changes to reported locations — and those might not be trivial. But we shouldn't confuse the issue with my fix. 1. Do we...

For discussion on the long-term solution I've opened https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp/topic/Error.20messages.2C.20locations.20and.20paths.

@Alizter that's what I tried in #6006; my attempt is naive, but it doesn't seem enough yet.

@Alizter What I meant is that the MR doesn't fix caching yet — I don't see how to fix this while still using `Command.run` as-is. I'd worry about that before...

@ejgallego do you mean that `cd _build/default/stdpp/theories &&` might _not_ be included in the hash? I had assumed it was.

I think I'm hit by this issue as well, and it interferers with developing dune itself...

> but it's a good first step if there's no test that attempts to run a substituted binary for now. Not to dissuade you from your plans, but I think...

My 2 cents: - One can ask C compilers to output dependency informations — see the `-M` option in https://gcc.gnu.org/onlinedocs/gcc/Preprocessor-Options.html#Preprocessor-Options. That's a standard approach. > > Maybe for external sources...

Good point; preprocessing depends on the listing of the whole search path. Which is a good argument for ccache or its approach.

FTR, using a cache entry by opening it read-only (as done in copy mode) should _not_ update its `ctime`, unlike creating hardlinks — that's according to the POSIX standard (or...