coqc scans direct many times (e.g. working directory 33726x in 10 seconds)

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#5067 From: @MSoegtropIMC Reported version: 8.5 CC: @gares, @silene

[coqbot]

Comment author: @MSoegtropIMC

Dear Coq Team,

I am working with Enrico on new build scripts for the Windows version.

The main issue is that my "homebrew" version of 8.5pl2 is many times slower than the official installer version. I compared disassembly dumps of the binaries for coqc and coqtop and they are 99.9% identical.

So I did compile (coqc) a single short file with both versions and anaylzed the system calls done using ProcMon. With the official version this takes 0.4s, with mine it takes 10 seconds.

One major difference is the number of system calls done. The official version of coqtop does 5163 major system calls (like file open close ..., but not including file read/write), while my version does 149643 for the same task.

The majority of the system calls is done scanning directories like .../share. I have more files in there, so it does more calls, but the strange thing is, that it scans the same useless directory many times. E.g. my version scans

\share\locale\si\LC_MESSAGES

79 times compiling a single file. I really wonder what business coqtop has scanning the locales directory for some exotic language 79 times when compiling a single file (in a single process).

The official version is better, but still looks 20x into share\themes\Emacs, which is likely not neccessary either.

Really bad is that my version scans the working directory (in which the compiled file resides) 33726 in 10 seconds. This is 3x per millisecond. The official version still does it 493 times. I really don't know what this shall be good for.

Attached you find the ProcMon logs as CSV file + a file with remarks on what to search for in these files.

One issue I have is that I don't know if coqtop scans directories like mad in some background thread all the time and that my version does more calls because it is slower in the main task and takes longer, or if the more calls are the root cause of the speed difference. Without having this strange behaviour fixed, it is very hard to do performance analysis on coqtop.

Best regards,

Michael

[coqbot]

Comment author: @MSoegtropIMC

Created attachment 760 zip (7zip cause of size) file with ProcMon logs and remarks

Attached file: Dumps.7z (application/octet-stream, 896749 bytes) Description: zip (7zip cause of size) file with ProcMon logs and remarks

[coqbot]

Comment author: @gares

I'm afraid that you configured Coq with -prefix D:\bin\cygwin_coq64_8.5pl2\usr\x86_64-w64-mingw32\sys-root\mingw\ and Coq is scanning $PREFIX/share for silly reasons. In the standard installation, $PREFIX/share contains noting D:\bin\Coq8.5pl2\share or very little. The initial call could be load_rcfile in coqinit.ml, and in particular xdg_dirs in envvars.ml. A quick try can be done by passing -q (small q).

I don't know why it scans more times. I could imagine it following redundant symlinks in .../usr/ that are not there in the official package, but if the app is not linked against cygwin.ddl (which is not the case) then it should not follow symlinks. Or at least, last time I've checked cygwin did emulate symlinks, not using OS symlinks (assuming windows has such notion).

Could you try to check my guess about rcfile loading?

[coqbot]

Comment author: @silene

(In reply to Enrico Tassi from comment BZ#2)

I'm afraid that you configured Coq with -prefix D:\bin\cygwin_coq64_8.5pl2\usr\x86_64-w64-mingw32\sys-root\mingw\ and Coq is scanning $PREFIX/share for silly reasons.

It is not for silly reasons; it is because that is where Coq was told user contributions are stored on Windows. Now why one would think it is a good idea to store user contributions there is everyone guess.

[coqbot]

Comment author: @MSoegtropIMC

Dear Enrico,

the logs where with -q (I think coqc adds it to coqtop).

The commands line was:

D:\bin\Coq8.5pl2\bin\coqtop.exe -q -I . -Q . Automation -compile TacBasic.v

I will see what happens, if I relpace the "original" coqc/coqtop in a standard installation.

I will also check how reproducible the logs are.

Any idea what the 33726x reading the working directory is good for?

Best regards,

Michael

[coqbot]

Comment author: @MSoegtropIMC

Created attachment 761 7zip file with logs of "home built" coqtop in "standard" folder structure + repeat tests

Attached file: Log3.7z (application/x-7z-compressed, 164434 bytes) Description: 7zip file with logs of "home built" coqtop in "standard" folder structure + repeat tests

[coqbot]

Comment author: @gares

Oh your are right, then it is not the rcfile loading. But I guess it is still xdg_dirs (that on windows behaves != than linux). Coqinit.init_load_path could be the caller...

Envvars.ml contains a lot of fishy stuff like

let dir = if Coq_config.arch_is_win32 then "lib" else "lib/coq" in

but the only line mentioning /share is the one for xdg_dirs, this is why I think you should try to cut it out.

Anyway, it seems envvars.ml assumes that on windows coq is installed is a non-unix filesystem layout.

[coqbot]

Comment author: @MSoegtropIMC

Dear Enrico,

I copied my binaries (bin + plugin folder) into a fresh "standard" install. Now the difference in number of system calls is minor (5333 vs 5163). Also the speed is about the same.

But there is still the issue that coqtop seems to do redundant directory scans, fewer than before, but still quite a lot:

just an arbitrary example:

4x "QueryDirectory","D:\bin\Coq8.5pl2test\share\themes\Emacs","SUCCESS" 21x "CreateFile","D:\bin\Coq8.5pl2test\share\themes\Emacs","SUCCESS"

working directory:

5x "QueryDirectory","C:\Users\soegtrop__Coq\Automation\Tactics","SUCCESS" 523x "CreateFile","C:\Users\soegtrop__Coq\Automation\Tactics","SUCCESS"

But the speed difference issue is solved, so I lowered this to normal.

Best regards,

Michael

[coqbot]

Comment author: @MSoegtropIMC

P.S.:

just out of curiosity: can someone run on Linux:

strace coqtop -q -I . -compile <whatever simple file.v>

and post the result?

Best regards,

Michael

[coqbot]

Comment author: @gares

Created attachment 762 strace on linux

strace -e trace=file -o /tmp/log.txt -- bin/coqtop -q -I . -compile bug.v

it is coq 8.6, ./configure -local.

Attached file: log.txt (text/plain, 618181 bytes) Description: strace on linux

[coqbot]

Comment author: @gares

Comment on attachment 762 strace on linux

This is the part I think explodes on your PC

stat("/home/gares/COQ/coq/theories/Init/Prelude.vo", {st_mode=S_IFREG|0644, st_size=3267, ...}) = 0 stat("/home/gares/.local/share/coq", 0x7ffefd514f50) = -1 ENOENT (No such file or directory) stat("/usr/share/gnome/coq", 0x7ffefd514f50) = -1 ENOENT (No such file or directory) stat("/usr/local/share//coq", 0x7ffefd514f50) = -1 ENOENT (No such file or directory) stat("/usr/share//coq", {st_mode=S_IFDIR|0755, st_size=4096, ...}) = 0

Just after guessing coqlib (finding Prelude.vo) it scans $SOMETHING/coq and on windows it is just $SOMETHING.

[coqbot]

Comment author: @MSoegtropIMC

Dear Enrico,

it also seems to scan useless folders twice, e.g.

line 5785: stat("/home/gares/COQ/coq/ide/coq_icon.rc" ... : ~ 500 other stats inbetween : line 6266: stat("/home/gares/COQ/coq/ide/coq_icon.rc" ...

but compared to the windows logs it looks relatively sane. Interestingly the useful folders it seems to do only once.

I will look at the code you pointed to and see what I can do.

But first I will finish the build scripts for 8.6.

Best regards,

Michael

[ppedrot]

@MSoegtropIMC is this still a relevant bug?

[MSoegtropIMC]

Windows builds are still several times slower than MacOS / Linux, so let me double check ...

[ejgallego]

Indeed we still scan the whole binding set at start time, that's for sure a drag on Windows, tho some laziness may be there (but that doesn't help in general I think).

I'm unsure if we have already an open bug towards going to improve this, note that fcc as a theory compiler can actually do this scan once per the whole theory, so for sure that's an improvement.