Open Zimmi48 opened 2 years ago
Actually, I realize that I've completely misread the above. Sorry. It is copying the repository to the store which takes so long!
FWIW, this is also what takes the longest on my computer, but just not as long (it might be due to the size of the repo, or to the type of hardware).
[2022-10-04 17:21:23] instantiated 'jsonAction' -> '/nix/store/lw4sm4gc14n88jza66f81wx2pzran7l4-jsonAction.drv'
[2022-10-04 17:21:31] copied source '/home/theo/git/coq' -> '/nix/store/1l9kgdk619ghb08z2rx0hhcblhmzg93y-coq'
The explanation was that @Alizter's repository was full of build artifacts. Still, copying the sources to the store should not be needed. Before my PR, this was excluded when in nix-shell
:
https://github.com/coq/coq/blob/96cf2fd5444b44bfd41b9f2fe50d27496da135a7/default.nix#L99-L100
Would there be a way of achieving the same in the Coq Nix Toolbox?
Looking further, we noticed that the excluding function that was implemented in the Coq repository does not work:
src =
with builtins; filterSource
(path: _:
!elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci" "_build_vo" ".nix"]) ../../..;
This does not exclude .git
or _build
for instance.
So this seems to be something that we could fix to make things faster for the Coq case.
Still, having a way of skipping the copying of the source when getting into nix-shell
would be nice to have.
I tried to fix the source filtering function by using another technique only to discover that my first filtering function was actually fine. It's just that during the evaluation of nix-shell
we get something like:
copied source '/home/theo/git/coq' -> '/nix/store/kgzkcn8y3wmxcdw8jwqr58n6fx8lgrfj-coq'
even though the source that is used by the coq-full
derivation is: /nix/store/8b1p4awf64r19lyplhlcilg3ddpkpgww-coq
.
The former store path has copied everything included filtered out directories, while the latter has the filters applied correctly.
In the current Nix setup in the Coq repository (without the Toolbox), we don't have this issue that the source is copied to the store once without the filters (even when running nix-shell default.nix
so that src
is not set to null
).
So indeed, the Coq Nix Toolbox needs to import the current directory as a source, and we cannot apply exactly the same filters (in particular, we cannot filter out the .nix
repository). If we try to filter out the .git
directory, it also leads to some error:
error: a string that refers to a store path cannot be appended to a path
at /nix/store/0fhbpysgjrayi9nzsh3i4qngdm8a5dch-source/config-parser-1.0.0/normalize.nix:42:21:
41| src = config.src or
42| (if pathExists (/. + initial.src)
| ^
43| -> pathExists (/. + initial.src + "/.git")
(use '--show-trace' to show detailed location information)
@CohenCyril Can you tell me what this was supposed to do:
I guess it was precisely some attempt at doing some filtering? And thus, it cannot be composed with a call to filterSource
. Maybe we should have some basic filtering predicate by default in the Toolbox and provide a way to extend them? Or what about just loading the .nix/
directory and nothing else as the source for the Toolbox's use?
I guess it was precisely some attempt at doing some filtering?
No this was an attempt to have shallow git clones to avoid time consuming source fetching when faced with potentially git repos.
And thus, it cannot be composed with a call to
filterSource
. Maybe we should have some basic filtering predicate by default in the Toolbox and provide a way to extend them? Or what about just loading the.nix/
directory and nothing else as the source for the Toolbox's use?
I prefer to be able to pass the a predicate... but, actually, I'd prefer the source filtering to be done by each derivation (and that hashes of the various sources take the filtering into account), so that for example changing .nix/*
or README
in many derivation does not affect the result of the build.
Since the Coq Nix Toolbox does need the .nix
directory, but a standard derivation should filter it out from its sources, we obviously need two sources, one for the internal functions of the Coq Nix Toolbox and one from the actual package. Would it work if the sources used by the Coq Nix Toolbox were limited to only the .nix
directory?
While testing my PR using the Coq Nix Toolbox on the Coq repo (https://github.com/coq/coq/pull/14435), @Alizter noticed that getting into
nix-shell
takes extremely long compared tomaster
(it's close to a minute vs 4 seconds for him, and it is about 12 vs 3 seconds for me).Using
nix-shell --debug --run exit 2>&1 | ts '[%Y-%m-%d %H:%M:%S]' | xclip -selection clipboard
, he was able to obtain a log with timings (https://ctxt.io/2/AAAQEsEJEw), from which we learn that most of the time is spent there:So it looks like instantiating thejsonAction
on every call tonix-shell
(and everynix-build
) is seriously impacting the performance of the Coq Nix Toolbox.Could we find a way of not instantiating it or making it trivially faster?What I'm considering is adding agen-action ? false
parameter todefault.nix
and changing the value of an attribute based on this.@CohenCyril WDYT?