Evaluation is too slow

[Zimmi48]

While testing my PR using the Coq Nix Toolbox on the Coq repo (coq/coq#14435), @Alizter noticed that getting into nix-shell takes extremely long compared to master (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:

[2022-10-04 16:53:13.782202] instantiated 'jsonAction' -> '/nix/store/lw4sm4gc14n88jza66f81wx2pzran7l4-jsonAction.drv'
[2022-10-04 16:54:03.336866] copied source '/home/ali/coq' -> '/nix/store/r8z94sfdklky20qiwsd1yp9zqmap88zn-coq'

So it looks like instantiating the jsonAction on every call to nix-shell (and every nix-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 a gen-action ? false parameter to default.nix and changing the value of an attribute based on this.

@CohenCyril WDYT?

[Zimmi48]

Actually, I realize that I've completely misread the above. Sorry. It is copying the repository to the store which takes so long!

[Zimmi48]

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'

[Zimmi48]

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?

[Zimmi48]

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.

[Zimmi48]

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).

[Zimmi48]

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:

coq-nix-toolbox/config-parser-1.0.0/normalize.nix

Lines 41 to 48 in 84cb9c4

	src = config.src or
	(if pathExists (/. + initial.src)
	-> pathExists (/. + initial.src + "/.git")
	then fetchGit (
	if false # replace by a version check when supported
	# cf https://github.com/NixOS/nix/issues/1837
	then { url = initial.src; shallow = true; } else initial.src)
	else /. + initial.src);

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?

[CohenCyril]

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.

[Zimmi48]

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?