Base image should try to install Coq deps.

[ejgallego]

While trying to understand why the Coq build in docker takes so long, I realized that installing the dependencies in the coq images takes a very long time.

A big part of this is due to dune, which requires ocaml-secondary-compiler in 4.05.0 which is a quite heavy package.

I suggest to follow the approach used in Coq's CI docker an preinstall a set of dependencies, in particular BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.0.8 odoc.1.4.2" [or newer if you wish].

By the way, how is the number of cores / -j option determined for docker hub builds?

[erikmd]

Thanks @ejgallego, I'll have a look − you're right that installing all this could speedup the docker-coq build if this is already done in docker-base.

But, is it an issue if some of these dependencies are not being used for most Coq versions? (as IINM, dune is currently required for coqorg/coq:dev only?)

While trying to understand why the Coq build in docker takes so long

BTW as a disclaimer of "the Coq build in docker takes so long", see my comment in that other issue:

coq-community/bignums#36 (comment)

[ejgallego]

But, is it an issue if some of these dependencies are not being used for most Coq versions? (as IINM, dune is currently required for coqorg/coq:dev only?)

Yes, it is a superset. But in particular building dune in 4.05 is taking a very long time per N times so the processing power savings are considerable.

BTW as a disclaimer of "the Coq build in docker takes so long", see my comment in that other issue:

I see that info is from 2015, I'd be surprised the specs hadn't gone a bit better, maybe we could try getting some worker information as we do in Coq's CI docker?

I'd definitively try -j 2 [we do that in Coq's docker even if one CPU only], The current time of close to 120 minutes is just too long IMO, my gut feeling is that a build should take around 30 minutes per Coq switch.

A significant slowdown is using opam :/ for whatever reason, opam install is very very slow with the large amount of files Coq has.

[erikmd]

Yes, it is a superset. But in particular building dune in 4.05 is taking a very long time per N times so the processing power savings are considerable.

OK.

BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.0.8 odoc.1.4.2"

I propose:

• not to install ounit and odoc because they seem to be testsuite/doc dependencies;
• to install (and pin) the latest version of dune that is currently implied by the coqorg/coq:dev image: 2.3.1; unless you prefer to install the minimal required version of dune, 2.0.1 (WDYT?);
• to install num and ocamlfind without constraints because Coq 8.4→8.11 doesn't have constraints on these (but note that num is not a {build} dependency, and ocamlfind is only a {build} dependency from Coq 8.8.0+) → so the question is, should we pin num (and/or ocamlfind)?

maybe we could try getting some worker information as we do in Coq's CI docker?

Good idea, we can do this. Which shell commands would you suggest?

[ejgallego]

• not to install ounit and odoc because they seem to be testsuite/doc dependencies;

sound good.

• to install (and pin) the latest version of dune that is currently implied by the coqorg/coq:dev image: 2.3.1; unless you prefer to install the minimal required version of dune, 2.0.1 (WDYT?);

even 2.4.0 would work better, while 2.0.1 is the minimal supported version for now, it won't be long until we require 2.5.0 for dev; 2.4.0 is much better also for image users that use dune to build Coq developments.

That should save ~20 minutes build time [or more] I think.

• to install num and ocamlfind without constraints because Coq 8.4→8.11 doesn't have constraints on these (but note that num is not a {build} dependency, and ocamlfind is only a {build} dependency from Coq 8.8.0+) → so the question is, should we pin num (and/or ocamlfind)?

yes, we should ping both, ocamlfind will become soon a non-build dependency due to the plugin loader being improved with dependency tracking.

[erikmd]

Thanks @ejgallego !

Also, regarding your other suggestion

[to get] some worker information as we do in Coq's CI docker

do you have specific shell commands in mind?

[ejgallego]

Thanks to you @erikmd

do you have specific shell commands in mind?

That's what we use in gitlab as to debug:

  - cat /proc/{cpu,mem}info || true
  - ls -a # figure out if artifacts are around
  - printenv -0 | sort -z | tr '\0' '\n'

I'm not sure this would help with docker, but at least we get a good idea of what kind of machine builds are running [as it is quite variable]

[ejgallego]

of course careful with the printenv, as it may leak protected variables [we only run that on non-deploy builds]

[erikmd]

OK so maybe cat /proc/{cpu,mem}info || true would be enough?

[ejgallego]

As you prefer, for us ENV variables have been useful but indeed they do carry security implications.

[erikmd]

@ejgallego

FYI:

$ cat /proc/cpuinfo /proc/meminfo  # in Docker Hub

processor : 0
vendor_id : GenuineIntel
cpu family : 6
model : 62
model name : Intel(R) Xeon(R) CPU E5-2670 v2 @ 2.50GHz
stepping : 4
microcode : 0x42e
cpu MHz : 2500.084
cache size : 25600 KB
physical id : 0
siblings : 1
core id : 0
cpu cores : 1
apicid : 0
initial apicid : 0
fpu : yes
fpu_exception : yes
cpuid level : 13
wp : yes
flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush mmx fxsr sse sse2 ht syscall nx rdtscp lm constant_tsc rep_good nopl xtopology eagerfpu pni pclmulqdq ssse3 cx16 pcid sse4_1 sse4_2 x2apic popcnt tsc_deadline_timer aes xsave avx f16c rdrand hypervisor lahf_lm kaiser fsgsbase smep erms xsaveopt
bugs : cpu_meltdown spectre_v1 spectre_v2 spec_store_bypass
bogomips : 5000.16
clflush size : 64
cache_alignment : 64
address sizes : 46 bits physical, 48 bits virtual
power management:
MemTotal: 3853036 kB
MemFree: 3032248 kB
MemAvailable: 3487288 kB
Buffers: 19180 kB
Cached: 565044 kB
SwapCached: 0 kB
Active: 443536 kB
Inactive: 294812 kB
Active(anon): 156940 kB
Inactive(anon): 5024 kB
Active(file): 286596 kB
Inactive(file): 289788 kB
Unevictable: 3652 kB
Mlocked: 3652 kB
SwapTotal: 0 kB
SwapFree: 0 kB
Dirty: 79604 kB
Writeback: 0 kB
AnonPages: 157772 kB
Mapped: 151252 kB
Shmem: 5424 kB
Slab: 52128 kB
SReclaimable: 34936 kB
SUnreclaim: 17192 kB
KernelStack: 2992 kB
PageTables: 2960 kB
NFS_Unstable: 0 kB
Bounce: 0 kB
WritebackTmp: 0 kB
CommitLimit: 1926516 kB
Committed_AS: 559604 kB
VmallocTotal: 34359738367 kB
VmallocUsed: 0 kB
VmallocChunk: 0 kB
HardwareCorrupted: 0 kB
AnonHugePages: 49152 kB
CmaTotal: 0 kB
CmaFree: 0 kB
HugePages_Total: 0
HugePages_Free: 0
HugePages_Rsvd: 0
HugePages_Surp: 0
Hugepagesize: 2048 kB
DirectMap4k: 43008 kB
DirectMap2M: 3889152 kB

[ejgallego]

Merci @erikmd ; given that kind of worker I'd say try with -j2 , it can help a bit depending on IO bottlenecks.

[erikmd]

@ejgallego

given that kind of worker I'd say try with -j2

Yes this was already the case in docker-coq's Dockerfile, so I kept that option in docker-base as well:

docker-base/Dockerfile

Line 60 in 8aeecac

ENV NJOBS="2"

docker-base/Dockerfile

Line 76 in 8aeecac

&& opam install -y -v -j ${NJOBS} ocamlfind dune num \

[erikmd]

For the record the base images have been rebuilt with ocamlfind.1.8.1, dune.2.4.0, num, and below are some figures:

tag	switches	size (local) before #7	size (local)	compressed size (Docker Hub)
coqorg/base:latest	4.05.0, 4.07.1+flambda	1.04GB	1.39GB	450MB
coqorg/base:4.02.3	4.02.3	not available	not available	269MB
coqorg/base:4.09.0-flambda	4.09.0+flambda	(not applicable)	not available	295MB

@ejgallego can we close that issue #7 ?

(then I'll resume the plan suggested in #4 (comment) )

[ejgallego]

Looks good, thanks a lot @erikmd ! The size increase is a bit unfortunate due to 4.05.0 having to install ocaml-secondary-compiler, on the other hand that's size we should save from the coq:* overlays [and time].