Skip to content
Snippets Groups Projects

build-coq.8.11.2

Passed Started by
Ralf Jung
@jung
This job is archived. Only the complete pipeline can be retried.
1Running with gitlab-runner 12.4.1 (05161b14)
2 on coop-timing 9b8a64cb
3 Using Docker executor with image ralfjung/opam-ci:opam2 ... 00:03
4Pulling docker image ralfjung/opam-ci:opam2 ...
5Using docker image sha256:460ea3e90f2124074559dd798ee79b26c4c9b48104d5d442544716fdf91ed094 for ralfjung/opam-ci:opam2 ...
6 Running on runner-9b8a64cb-project-178-concurrent-0 via coop... 00:02
7 Fetching changes... 00:04
8Initialized empty Git repository in /builds/iris/lambda-rust/.git/
9Created fresh repository.
10From https://gitlab.mpi-sws.org/iris/lambda-rust
11 * [new ref] refs/pipelines/31478 -> refs/pipelines/31478
12 * [new branch] ci/janno/reduction_no_check -> origin/ci/janno/reduction_no_check
13 * [new branch] ci/places -> origin/ci/places
14 * [new branch] ci/pm_red -> origin/ci/pm_red
15 * [new branch] ci/ralf/const-rf -> origin/ci/ralf/const-rf
16 * [new branch] ci/ralf/lia-experiment -> origin/ci/ralf/lia-experiment
17 * [new branch] ci/ralf/old-timing-data -> origin/ci/ralf/old-timing-data
18 * [new branch] ci/ralf/sections -> origin/ci/ralf/sections
19 * [new branch] ci/robbert/faster_iDestruct2 -> origin/ci/robbert/faster_iDestruct2
20 * [new branch] ci/robbert/iprop_structures -> origin/ci/robbert/iprop_structures
21 * [new branch] ci/robbert/merge_sbi -> origin/ci/robbert/merge_sbi
22 * [new branch] ci/robbert/merge_sbi_new -> origin/ci/robbert/merge_sbi_new
23 * [new branch] ci/robbert/merge_sbi_new_weak -> origin/ci/robbert/merge_sbi_new_weak
24 * [new branch] ci/robbert/merge_sbi_weak -> origin/ci/robbert/merge_sbi_weak
25 * [new branch] ci/robbert/naive_solver -> origin/ci/robbert/naive_solver
26 * [new branch] ci/weak_mem -> origin/ci/weak_mem
27 * [new branch] coqbug/match -> origin/coqbug/match
28 * [new branch] fast_string -> origin/fast_string
29 * [new branch] gpirlea/pinning -> origin/gpirlea/pinning
30 * [new branch] jh/bug -> origin/jh/bug
31 * [new branch] jh/closures -> origin/jh/closures
32 * [new branch] jh/dynamic_masks -> origin/jh/dynamic_masks
33 * [new branch] jh/lifetime_no_dead_trade -> origin/jh/lifetime_no_dead_trade
34 * [new branch] jh/ofe_problems -> origin/jh/ofe_problems
35 * [new branch] jh/typecheck_foo -> origin/jh/typecheck_foo
36 * [new branch] master -> origin/master
37 * [new branch] masters/weak_mem -> origin/masters/weak_mem
38 * [new branch] no-opaque -> origin/no-opaque
39 * [new branch] notations -> origin/notations
40 * [new branch] ralf/acc -> origin/ralf/acc
41 * [new branch] ralf/sections-open -> origin/ralf/sections-open
42 * [new branch] skiplist -> origin/skiplist
43 * [new branch] strong_cas_fail -> origin/strong_cas_fail
44 * [new tag] RBrlx-POPL20-artifact -> RBrlx-POPL20-artifact
45 * [new tag] popl18 -> popl18
46 * [new tag] popl18-aec -> popl18-aec
47Checking out 9041a374 as masters/weak_mem...
48Skipping Git submodules setup
49 Checking cache for build-coq.8.11.2-weak_mem-8... 00:39
50Downloading cache.zip from https://radosgw.mpi-sws.org/fp-science-ci/iris-ci-cache/project/178/build-coq.8.11.2-weak_mem-8
51Successfully extracted cache
52 $ git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2 25:11
53Cloning into 'ci'...
54$ ci/buildjob
55[buildjob] Using CI branch opam2 (0894aff50fedd29f36853535f33f34abb582687d)
56[prepare-opam] Refreshing cached opam root
57# Creating build-dep package.
58[NOTE] Will configure from built-in defaults.
59Checking for available remotes: rsync and local, git.
60 - you won't be able to use mercurial repositories unless you install the hg command on your system.
61 - you won't be able to use darcs repositories unless you install the darcs command on your system.
62<><> Updating repositories ><><><><><><><><><><><><><><><><><><><><><><><><><><>
63[coq-released] synchronised from https://coq.inria.fr/opam/released
64[iris-dev] synchronised from git+https://gitlab.mpi-sws.org/FP/opam-dev.git
65[default] synchronised from https://opam.ocaml.org
66<><> Synchronising development packages <><><><><><><><><><><><><><><><><><><><>
67[coq-lambda-rust-builddep.~dev] synchronised from file:///builds/iris/lambda-rust/build-dep
68[coq-iris.dev.2020-07-03.0.d44afeed] no changes from git+https://gitlab.mpi-sws.org/iris/iris.git#d44afeed8762544c87b79d11156e66b0737c5b06
69[coq-orc11.dev.2020-07-03.0.adeaaee2] no changes from git+https://gitlab.mpi-sws.org/iris/orc11.git#adeaaee2ef4142e24239b2b844bbada238e62863
70[coq-stdpp.dev.2020-07-02.1.c8129a37] no changes from git+https://gitlab.mpi-sws.org/iris/stdpp.git#c8129a3730a309b84b8965f936375d5e16ae3d94
71[coq-gpfsl.dev.2020-07-03.0.ce4c6d6b] no changes from git+https://gitlab.mpi-sws.org/iris/gpfsl.git#ce4c6d6bde8832b24964c8d266eed450287b4936
72[coq-lambda-rust-builddep] Conflicting update of the metadata from file:///builds/iris/lambda-rust/build-dep.
73Override files in /builds/iris/lambda-rust/opamroot/ocaml-base-compiler.4.08.1/.opam-switch/overlay/coq-lambda-rust-builddep (there will be a backup)? [Y/n] n
74Now run 'opam upgrade' to apply any package updates.
75[prepare-opam] opam report
76# opam config report
77# opam-version 2.0.7
78# self-upgrade no
79# system arch=x86_64 os=linux os-distribution=debian os-version=9
80# solver builtin-mccs+glpk
81# install-criteria -removed,-count[version-lag,request],-count[version-lag,changed],-changed
82# upgrade-criteria -removed,-count[version-lag,solution],-new
83# jobs 20
84# repositories 2 (http), 1 (version-controlled) (default repo at 94768e24)
85# pinned 1 (rsync), 1 (version)
86# current-switch ocaml-base-compiler.4.08.1
87[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.
88<><> Repository configuration for switch ocaml-base-compiler.4.08.1 <><><><><><>
89 1 iris-dev git+https://gitlab.mpi-sws.org/FP/opam-dev.git
90 2 coq-released https://coq.inria.fr/opam/released
91 3 default https://opam.ocaml.org
92[prepare-opam] Removing old pins
93Ok, coq is no longer pinned to https://github.com/coq/coq/archive/V8.11.2.tar.gz (version 8.11.2)
94Ok, coq-lambda-rust-builddep is no longer pinned to file:///builds/iris/lambda-rust/build-dep (version ~dev)
95[prepare-opam] Processing pins
96[prepare-opam] version-pinning coq to 8.11.2
97coq is now pinned to version 8.11.2
98[prepare-opam] Pinning and installing build-dep and upgrading everything
99Package coq-lambda-rust-builddep does not exist, create as a NEW package? [Y/n] y
100[coq-lambda-rust-builddep.~dev: rsync]
101[coq-lambda-rust-builddep.~dev] synchronised from file:///builds/iris/lambda-rust/build-dep
102[WARNING] coq-lambda-rust-builddep's opam file has uncommitted changes, using the versioned one
103coq-lambda-rust-builddep is now pinned to file:///builds/iris/lambda-rust/build-dep (version ~dev)
104<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
105[coq-lambda-rust-builddep.~dev] no changes from file:///builds/iris/lambda-rust/build-dep
106The following actions will be performed:
107 - upgrade coq-iris dev.2020-07-03.0.d44afeed to dev.2020-07-15.0.6b0e19f5 [required by coq-gpfsl]
108 - upgrade coq-gpfsl dev.2020-07-03.0.ce4c6d6b to dev.2020-07-15.0.654300d3 [required by coq-lambda-rust-builddep]
109 - recompile coq-lambda-rust-builddep ~dev*
110===== 1 to recompile | 2 to upgrade =====
111<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
112[coq-lambda-rust-builddep.~dev] no changes from file:///builds/iris/lambda-rust/build-dep
113[coq-gpfsl.dev.2020-07-15.0.654300d3] synchronised from git+https://gitlab.mpi-sws.org/iris/gpfsl.git#654300d356c6f806b4b5dcc971abffa9e3dc43f7
114[coq-iris.dev.2020-07-15.0.6b0e19f5] synchronised from git+https://gitlab.mpi-sws.org/iris/iris.git#6b0e19f52d72dcb6d74843510b00d69e5f1826e0
115<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
116-> removed coq-gpfsl.dev.2020-07-03.0.ce4c6d6b
117-> removed coq-iris.dev.2020-07-03.0.d44afeed
118-> removed coq-lambda-rust-builddep.~dev
119-> installed coq-iris.dev.2020-07-15.0.6b0e19f5
120-> installed coq-gpfsl.dev.2020-07-15.0.654300d3
121-> installed coq-lambda-rust-builddep.~dev
122Done.
123Everything as up-to-date as possible (run with --verbose to show unavailable upgrades).
124The following packages are not being upgraded because the new versions conflict with other installed packages:
125 - coq-iris.dev.2020-07-15.1.6ae02201
126 -- coq-gpfsl.dev.2020-07-15.0.654300d3 is installed and requires coq-iris (= dev.2020-07-15.0.6b0e19f5 | = dev)
127 - coq-stdpp.dev.2020-07-15.0.ab7ed0b8
128 -- coq-iris.dev.2020-07-15.1.6ae02201 is installed and requires coq-stdpp (= dev.2020-07-02.1.c8129a37 | = dev)
129 -- coq-orc11.dev.2020-07-03.0.adeaaee2 is installed and requires coq-stdpp (= dev.2020-07-02.1.c8129a37 | = dev)
130However, you may "opam upgrade" these packages explicitly, which will ask permission to downgrade or uninstall the conflicting packages.
131Nothing to do.
132[prepare-opam] Done! Some version information:
133name coq
134version 8.11.2
135source-hash
136The Coq Proof Assistant, version 8.11.2 (June 2020)
137compiled on Jun 19 2020 16:53:07 with OCaml 4.08.1
138[buildjob] Perfoming build
139"coq_makefile" -f _CoqProject -o Makefile.coq
140COQDEP VFILES
141COQC theories/lang/notation.v
142COQC theories/lifetime/lifetime_sig.v
143COQC theories/lang/memcpy.v
144COQC theories/lang/swap.v
145COQC theories/lang/new_delete.v
146COQC theories/lang/spawn.v
147COQC theories/lifetime/model/boxes.v
148COQC theories/lifetime/model/definitions.v
149COQC theories/lang/arc_cmra.v
150COQC theories/lifetime/model/primitive.v
151COQC theories/lifetime/model/faking.v
152COQC theories/lifetime/model/borrow.v
153COQC theories/lifetime/model/creation.v
154COQC theories/lifetime/model/accessors.v
155COQC theories/lifetime/model/in_at_borrow.v
156COQC theories/lifetime/model/reborrow.v
157COQC theories/lifetime/model/borrow_sep.v
158COQC theories/lifetime/lifetime.v
159COQC theories/lifetime/na_borrow.v
160COQC theories/lifetime/at_borrow.v
161COQC theories/lifetime/frac_borrow.v
162COQC theories/typing/base.v
163COQC theories/logic/gps.v
164COQC theories/typing/lft_contexts.v
165COQC theories/lang/lock.v
166COQC theories/typing/type.v
167COQC theories/typing/type_context.v
168COQC theories/typing/util.v
169COQC theories/typing/product.v
170COQC theories/typing/sum.v
171COQC theories/typing/cont_context.v
172COQC theories/typing/uninit.v
173COQC theories/typing/programs.v
174COQC theories/typing/bool.v
175COQC theories/typing/cont.v
176COQC theories/typing/shr_bor.v
177COQC theories/typing/int.v
178COQC theories/typing/fixpoint.v
179COQC theories/typing/uniq_bor.v
180COQC theories/typing/own.v
181COQC theories/typing/product_split.v
182COQC theories/typing/borrow.v
183COQC theories/typing/type_sum.v
184COQC theories/typing/function.v
185COQC theories/typing/typing.v
186COQC theories/typing/lib/panic.v
187COQC theories/typing/soundness.v
188COQC theories/typing/lib/diverging_static.v
189COQC theories/typing/lib/fake_shared.v
190COQC theories/typing/examples/get_x.v
191COQC theories/typing/lib/spawn.v
192COQC theories/typing/lib/take_mut.v
193COQC theories/typing/examples/unbox.v
194COQC theories/typing/lib/refcell/refcell.v
195COQC theories/typing/examples/rebor.v
196COQC theories/typing/lib/join.v
197COQC theories/typing/examples/init_prod.v
198COQC theories/typing/lib/cell.v
199COQC theories/typing/examples/lazy_lft.v
200COQC theories/typing/lib/option.v
201COQC theories/typing/lib/rwlock/rwlock.v
202COQC theories/typing/lib/refcell/ref.v
203COQC theories/typing/lib/refcell/refmut.v
204COQC theories/typing/lib/rwlock/rwlockreadguard.v
205COQC theories/lang/arc.v
206COQC theories/typing/lib/mutex/mutex.v
207COQC theories/typing/lib/rwlock/rwlockwriteguard.v
208COQC theories/typing/examples/nonlexical.v
209COQC theories/typing/lib/rwlock/rwlockreadguard_code.v
210COQC theories/typing/lib/rwlock/rwlockwriteguard_code.v
211COQC theories/typing/lib/mutex/mutexguard.v
212COQC theories/typing/lib/refcell/refcell_code.v
213COQC theories/typing/lib/rwlock/rwlock_code.v
214COQC theories/typing/lib/refcell/ref_code.v
215COQC theories/typing/lib/refcell/refmut_code.v
216COQC theories/typing/lib/rc/rc.v
217COQC theories/typing/lib/arc.v
218COQC theories/typing/lib/rc/weak.v
219real 12m7.609s
220user 42m31.872s
221sys 0m35.164s
222[buildjob] Build performance information
223## theories/typing/type_context.v
22432872118451;;instructions:u;9727099317;100.00;1.04;insn per cycle
22531652195152;;cycles:u;9727099317;100.00;;
226real: 9.78, user: 9.37, sys: 0.38, mem: 646668 kB
227## theories/typing/type_sum.v
228105385879745;;instructions:u;29520103956;100.00;1.06;insn per cycle
22999368774527;;cycles:u;29520103956;100.00;;
230real: 29.63, user: 29.10, sys: 0.45, mem: 784084 kB
231## theories/typing/examples/rebor.v
23232280672150;;instructions:u;8824694546;100.00;1.09;insn per cycle
23329659169101;;cycles:u;8824694546;100.00;;
234real: 8.91, user: 8.46, sys: 0.37, mem: 644800 kB
235## theories/typing/examples/init_prod.v
23626966290091;;instructions:u;7520501547;100.00;1.08;insn per cycle
23724998229288;;cycles:u;7520501547;100.00;;
238real: 7.60, user: 7.15, sys: 0.37, mem: 637732 kB
239## theories/typing/examples/get_x.v
24020739149640;;instructions:u;6100581600;100.00;1.05;insn per cycle
24119766869475;;cycles:u;6100581600;100.00;;
242real: 6.22, user: 5.70, sys: 0.40, mem: 628744 kB
243## theories/typing/examples/lazy_lft.v
24450716160644;;instructions:u;13190300513;100.00;1.11;insn per cycle
24545820777196;;cycles:u;13190300513;100.00;;
246real: 13.24, user: 12.80, sys: 0.39, mem: 645384 kB
247## theories/typing/examples/nonlexical.v
248180518595647;;instructions:u;43125572808;100.00;1.19;insn per cycle
249151638281560;;cycles:u;43125572808;100.00;;
250real: 43.53, user: 42.72, sys: 0.42, mem: 764792 kB
251## theories/typing/examples/unbox.v
25222357411431;;instructions:u;6598171741;100.00;1.04;insn per cycle
25321515839634;;cycles:u;6598171741;100.00;;
254real: 6.70, user: 6.21, sys: 0.38, mem: 630692 kB
255## theories/typing/cont_context.v
25623078652539;;instructions:u;6700533090;100.00;1.09;insn per cycle
25721121483458;;cycles:u;6700533090;100.00;;
258real: 6.75, user: 6.35, sys: 0.36, mem: 601276 kB
259## theories/typing/int.v
26026142530601;;instructions:u;7928078523;100.00;1.05;insn per cycle
26125002751823;;cycles:u;7928078523;100.00;;
262real: 7.98, user: 7.54, sys: 0.40, mem: 632324 kB
263## theories/typing/base.v
26414792082576;;instructions:u;4525481024;100.00;1.14;insn per cycle
26512961574842;;cycles:u;4525481024;100.00;;
266real: 4.56, user: 4.14, sys: 0.39, mem: 613816 kB
267## theories/typing/sum.v
26855363756914;;instructions:u;15471208241;100.00;1.07;insn per cycle
26951708971405;;cycles:u;15471208241;100.00;;
270real: 15.52, user: 15.09, sys: 0.40, mem: 651076 kB
271## theories/typing/lib/rwlock/rwlock_code.v
272278575192919;;instructions:u;75113496917;100.00;1.07;insn per cycle
273260102330348;;cycles:u;75113496917;100.00;;
274real: 75.62, user: 74.54, sys: 0.58, mem: 1058740 kB
275## theories/typing/lib/rwlock/rwlockreadguard.v
27677371143343;;instructions:u;20491565566;100.00;1.10;insn per cycle
27770369278057;;cycles:u;20491565566;100.00;;
278real: 20.57, user: 20.04, sys: 0.45, mem: 711988 kB
279## theories/typing/lib/rwlock/rwlockreadguard_code.v
280129755459061;;instructions:u;35732125756;100.00;1.06;insn per cycle
281121911740277;;cycles:u;35732125756;100.00;;
282real: 36.06, user: 35.25, sys: 0.49, mem: 846904 kB
283## theories/typing/lib/rwlock/rwlockwriteguard_code.v
284114819333081;;instructions:u;32188482396;100.00;1.03;insn per cycle
285111893205068;;cycles:u;32188482396;100.00;;
286real: 32.50, user: 31.68, sys: 0.52, mem: 817128 kB
287## theories/typing/lib/rwlock/rwlock.v
288110281286950;;instructions:u;31101892525;100.00;1.04;insn per cycle
289106175118293;;cycles:u;31101892525;100.00;;
290real: 31.36, user: 30.69, sys: 0.41, mem: 805956 kB
291## theories/typing/lib/rwlock/rwlockwriteguard.v
29291804038622;;instructions:u;24948297943;100.00;1.08;insn per cycle
29385308009076;;cycles:u;24948297943;100.00;;
294real: 25.07, user: 24.55, sys: 0.40, mem: 731424 kB
295## theories/typing/lib/cell.v
29690698209233;;instructions:u;25896658182;100.00;1.00;insn per cycle
29790662693389;;cycles:u;25896658182;100.00;;
298real: 26.22, user: 25.51, sys: 0.43, mem: 746132 kB
299## theories/typing/lib/rc/weak.v
300371647641907;;instructions:u;92957690229;100.00;1.16;insn per cycle
301320546775820;;cycles:u;92957690229;100.00;;
302real: 93.10, user: 92.32, sys: 0.65, mem: 1164924 kB
303## theories/typing/lib/rc/rc.v
3041001529971960;;instructions:u;261944450617;100.00;1.12;insn per cycle
305896970804765;;cycles:u;261944450617;100.00;;
306real: 263.30, user: 260.96, sys: 1.01, mem: 1223784 kB
307## theories/typing/lib/arc.v
3081022612004261;;instructions:u;266505070996;100.00;1.13;insn per cycle
309906422706688;;cycles:u;266505070996;100.00;;
310real: 267.99, user: 265.58, sys: 0.93, mem: 1183684 kB
311## theories/typing/lib/mutex/mutex.v
31290648175742;;instructions:u;26597895309;100.00;1.01;insn per cycle
31389656370042;;cycles:u;26597895309;100.00;;
314real: 26.82, user: 26.13, sys: 0.49, mem: 755148 kB
315## theories/typing/lib/mutex/mutexguard.v
316158420880648;;instructions:u;44160200394;100.00;1.03;insn per cycle
317153634738502;;cycles:u;44160200394;100.00;;
318real: 44.47, user: 43.68, sys: 0.48, mem: 831980 kB
319## theories/typing/lib/take_mut.v
32060941965442;;instructions:u;17090979258;100.00;1.04;insn per cycle
32158720031665;;cycles:u;17090979258;100.00;;
322real: 17.34, user: 16.71, sys: 0.43, mem: 677492 kB
323## theories/typing/lib/fake_shared.v
32443032094325;;instructions:u;12337295792;100.00;1.02;insn per cycle
32542036386247;;cycles:u;12337295792;100.00;;
326real: 12.56, user: 12.00, sys: 0.37, mem: 641816 kB
327## theories/typing/lib/refcell/refcell.v
32868539007190;;instructions:u;19538288820;100.00;1.01;insn per cycle
32967722668691;;cycles:u;19538288820;100.00;;
330real: 19.78, user: 19.13, sys: 0.45, mem: 699052 kB
331## theories/typing/lib/refcell/ref_code.v
332482213834967;;instructions:u;130183666060;100.00;1.09;insn per cycle
333441520834957;;cycles:u;130183666060;100.00;;
334real: 130.90, user: 129.48, sys: 0.72, mem: 1174308 kB
335## theories/typing/lib/refcell/refmut.v
336103762162749;;instructions:u;27961383813;100.00;1.12;insn per cycle
33792960843691;;cycles:u;27961383813;100.00;;
338real: 28.06, user: 27.52, sys: 0.44, mem: 857548 kB
339## theories/typing/lib/refcell/ref.v
340102195744397;;instructions:u;27127354772;100.00;1.11;insn per cycle
34191911256485;;cycles:u;27127354772;100.00;;
342real: 27.21, user: 26.66, sys: 0.48, mem: 869912 kB
343## theories/typing/lib/refcell/refcell_code.v
344251159926097;;instructions:u;69420411061;100.00;1.04;insn per cycle
345241892662711;;cycles:u;69420411061;100.00;;
346real: 69.96, user: 68.88, sys: 0.54, mem: 956816 kB
347## theories/typing/lib/refcell/refmut_code.v
348530824315473;;instructions:u;140233467917;100.00;1.12;insn per cycle
349472165536999;;cycles:u;140233467917;100.00;;
350real: 141.00, user: 139.52, sys: 0.73, mem: 1210888 kB
351## theories/typing/lib/panic.v
35216546196654;;instructions:u;4908781682;100.00;1.06;insn per cycle
35315675176722;;cycles:u;4908781682;100.00;;
354real: 5.03, user: 4.54, sys: 0.41, mem: 624588 kB
355## theories/typing/lib/diverging_static.v
35638427187982;;instructions:u;10754025840;100.00;1.06;insn per cycle
35736212856730;;cycles:u;10754025840;100.00;;
358real: 10.96, user: 10.38, sys: 0.43, mem: 642024 kB
359## theories/typing/lib/join.v
36078928294506;;instructions:u;20924922400;100.00;1.09;insn per cycle
36172482114152;;cycles:u;20924922400;100.00;;
362real: 21.28, user: 20.56, sys: 0.42, mem: 709356 kB
363## theories/typing/lib/spawn.v
36449170401677;;instructions:u;14037215831;100.00;1.03;insn per cycle
36547848645269;;cycles:u;14037215831;100.00;;
366real: 14.24, user: 13.69, sys: 0.40, mem: 641684 kB
367## theories/typing/lib/option.v
36858431268107;;instructions:u;15509516331;100.00;1.11;insn per cycle
36952692432124;;cycles:u;15509516331;100.00;;
370real: 15.56, user: 15.13, sys: 0.38, mem: 641756 kB
371## theories/typing/shr_bor.v
37233206653877;;instructions:u;9336405185;100.00;1.07;insn per cycle
37330898432611;;cycles:u;9336405185;100.00;;
374real: 9.39, user: 8.99, sys: 0.39, mem: 641668 kB
375## theories/typing/own.v
37687950916345;;instructions:u;24405775047;100.00;1.08;insn per cycle
37781748295193;;cycles:u;24405775047;100.00;;
378real: 24.48, user: 23.99, sys: 0.46, mem: 728572 kB
379## theories/typing/function.v
380118799909370;;instructions:u;32783004154;100.00;1.10;insn per cycle
381107829299109;;cycles:u;32783004154;100.00;;
382real: 32.86, user: 32.40, sys: 0.40, mem: 760608 kB
383## theories/typing/product_split.v
38457822177796;;instructions:u;17227152440;100.00;1.02;insn per cycle
38556416800197;;cycles:u;17227152440;100.00;;
386real: 17.34, user: 16.85, sys: 0.40, mem: 671248 kB
387## theories/typing/uniq_bor.v
38877727544367;;instructions:u;21115749535;100.00;1.10;insn per cycle
38970659460097;;cycles:u;21115749535;100.00;;
390real: 21.22, user: 20.73, sys: 0.43, mem: 730960 kB
391## theories/typing/soundness.v
39224388373183;;instructions:u;7642894249;100.00;0.99;insn per cycle
39324642573299;;cycles:u;7642894249;100.00;;
394real: 7.76, user: 7.29, sys: 0.40, mem: 641188 kB
395## theories/typing/uninit.v
39624672543873;;instructions:u;7583372392;100.00;1.07;insn per cycle
39723093141505;;cycles:u;7583372392;100.00;;
398real: 7.63, user: 7.20, sys: 0.40, mem: 628532 kB
399## theories/typing/product.v
40051567980676;;instructions:u;14450139488;100.00;1.06;insn per cycle
40148726971504;;cycles:u;14450139488;100.00;;
402real: 14.51, user: 14.06, sys: 0.42, mem: 650716 kB
403## theories/typing/type.v
40484142456402;;instructions:u;21625192129;100.00;1.13;insn per cycle
40574663704004;;cycles:u;21625192129;100.00;;
406real: 21.67, user: 21.27, sys: 0.37, mem: 649820 kB
407## theories/typing/typing.v
40814853821451;;instructions:u;4019047984;100.00;1.18;insn per cycle
40912576568938;;cycles:u;4019047984;100.00;;
410real: 4.03, user: 3.61, sys: 0.41, mem: 623416 kB
411## theories/typing/util.v
41238086821362;;instructions:u;10452780778;100.00;1.13;insn per cycle
41333680997140;;cycles:u;10452780778;100.00;;
414real: 10.51, user: 10.09, sys: 0.39, mem: 623280 kB
415## theories/typing/bool.v
41621639142957;;instructions:u;6407083810;100.00;1.11;insn per cycle
41719499145068;;cycles:u;6407083810;100.00;;
418real: 6.48, user: 6.08, sys: 0.36, mem: 619840 kB
419## theories/typing/fixpoint.v
42027511728662;;instructions:u;8203829898;100.00;1.07;insn per cycle
42125683800863;;cycles:u;8203829898;100.00;;
422real: 8.26, user: 7.74, sys: 0.48, mem: 646388 kB
423## theories/typing/lft_contexts.v
42442891217594;;instructions:u;11802376928;100.00;1.10;insn per cycle
42538828001046;;cycles:u;11802376928;100.00;;
426real: 11.86, user: 11.44, sys: 0.37, mem: 642076 kB
427## theories/typing/borrow.v
42870943268511;;instructions:u;19650273019;100.00;1.10;insn per cycle
42964547243724;;cycles:u;19650273019;100.00;;
430real: 19.73, user: 19.29, sys: 0.38, mem: 706144 kB
431## theories/typing/programs.v
43280659988624;;instructions:u;21387013858;100.00;1.13;insn per cycle
43371395597982;;cycles:u;21387013858;100.00;;
434real: 21.43, user: 21.02, sys: 0.38, mem: 693596 kB
435## theories/typing/cont.v
43622001757480;;instructions:u;6613323305;100.00;1.07;insn per cycle
43720547741722;;cycles:u;6613323305;100.00;;
438real: 6.67, user: 6.26, sys: 0.39, mem: 627060 kB
439## theories/lifetime/at_borrow.v
44025546688374;;instructions:u;7544480662;100.00;1.12;insn per cycle
44122719305779;;cycles:u;7544480662;100.00;;
442real: 7.58, user: 7.18, sys: 0.38, mem: 602852 kB
443## theories/lifetime/model/creation.v
44481351713632;;instructions:u;23117571666;100.00;1.10;insn per cycle
44573982632865;;cycles:u;23117571666;100.00;;
446real: 23.21, user: 22.71, sys: 0.42, mem: 700544 kB
447## theories/lifetime/model/primitive.v
44863739408581;;instructions:u;18000346144;100.00;1.08;insn per cycle
44959136550395;;cycles:u;18000346144;100.00;;
450real: 18.06, user: 17.60, sys: 0.41, mem: 672620 kB
451## theories/lifetime/model/reborrow.v
452128798235383;;instructions:u;33785893628;100.00;1.13;insn per cycle
453114435182533;;cycles:u;33785893628;100.00;;
454real: 33.92, user: 33.33, sys: 0.46, mem: 839100 kB
455## theories/lifetime/model/definitions.v
45625382185075;;instructions:u;7544143742;100.00;1.09;insn per cycle
45723322908049;;cycles:u;7544143742;100.00;;
458real: 7.58, user: 7.20, sys: 0.36, mem: 602808 kB
459## theories/lifetime/model/in_at_borrow.v
46028743330009;;instructions:u;8218587369;100.00;1.12;insn per cycle
46125673587046;;cycles:u;8218587369;100.00;;
462real: 8.25, user: 7.88, sys: 0.34, mem: 602028 kB
463## theories/lifetime/model/borrow_sep.v
464129798482371;;instructions:u;34978794655;100.00;1.16;insn per cycle
465112182942164;;cycles:u;34978794655;100.00;;
466real: 35.14, user: 34.47, sys: 0.52, mem: 868848 kB
467## theories/lifetime/model/boxes.v
46872472251804;;instructions:u;21087189488;100.00;1.07;insn per cycle
46967732365260;;cycles:u;21087189488;100.00;;
470real: 21.36, user: 20.70, sys: 0.42, mem: 675516 kB
471## theories/lifetime/model/accessors.v
472164115815333;;instructions:u;44304701202;100.00;1.11;insn per cycle
473148496168957;;cycles:u;44304701202;100.00;;
474real: 44.46, user: 43.78, sys: 0.54, mem: 877696 kB
475## theories/lifetime/model/faking.v
47648020846031;;instructions:u;13604479193;100.00;1.09;insn per cycle
47744068093366;;cycles:u;13604479193;100.00;;
478real: 13.65, user: 13.24, sys: 0.38, mem: 627364 kB
479## theories/lifetime/model/borrow.v
48049853587508;;instructions:u;14248395310;100.00;1.09;insn per cycle
48145925235645;;cycles:u;14248395310;100.00;;
482real: 14.34, user: 13.82, sys: 0.45, mem: 642364 kB
483## theories/lifetime/na_borrow.v
48419263177284;;instructions:u;5566368201;100.00;1.12;insn per cycle
48517212018184;;cycles:u;5566368201;100.00;;
486real: 5.60, user: 5.16, sys: 0.43, mem: 601848 kB
487## theories/lifetime/lifetime_sig.v
48812685458015;;instructions:u;3927988326;100.00;1.11;insn per cycle
48911395966547;;cycles:u;3927988326;100.00;;
490real: 4.08, user: 3.59, sys: 0.37, mem: 589372 kB
491## theories/lifetime/frac_borrow.v
49296693639235;;instructions:u;24829871962;100.00;1.14;insn per cycle
49384994794649;;cycles:u;24829871962;100.00;;
494real: 24.92, user: 24.42, sys: 0.43, mem: 768824 kB
495## theories/lifetime/lifetime.v
49651697009040;;instructions:u;14379375774;100.00;1.12;insn per cycle
49746209586328;;cycles:u;14379375774;100.00;;
498real: 14.45, user: 14.06, sys: 0.32, mem: 646292 kB
499## theories/lang/lock.v
50043087959899;;instructions:u;12169316916;100.00;1.15;insn per cycle
50137631302400;;cycles:u;12169316916;100.00;;
502real: 12.23, user: 11.82, sys: 0.36, mem: 641608 kB
503## theories/lang/new_delete.v
50411789243328;;instructions:u;3758386170;100.00;1.14;insn per cycle
50510317464977;;cycles:u;3758386170;100.00;;
506real: 3.81, user: 3.43, sys: 0.33, mem: 586140 kB
507## theories/lang/swap.v
50821432709189;;instructions:u;5992839456;100.00;1.13;insn per cycle
50919000208437;;cycles:u;5992839456;100.00;;
510real: 6.06, user: 5.67, sys: 0.35, mem: 597828 kB
511## theories/lang/arc.v
5121353931055221;;instructions:u;353681382360;100.00;1.13;insn per cycle
5131201084937088;;cycles:u;353681382360;100.00;;
514real: 354.84, user: 352.87, sys: 0.82, mem: 1438628 kB
515## theories/lang/arc_cmra.v
516156897683589;;instructions:u;39032204239;100.00;1.19;insn per cycle
517131632115785;;cycles:u;39032204239;100.00;;
518real: 39.18, user: 38.64, sys: 0.42, mem: 691852 kB
519## theories/lang/notation.v
5203782298817;;instructions:u;1475158467;100.00;1.14;insn per cycle
5213319169767;;cycles:u;1475158467;100.00;;
522real: 1.62, user: 1.18, sys: 0.32, mem: 495768 kB
523## theories/lang/memcpy.v
52419716571512;;instructions:u;5653258477;100.00;1.11;insn per cycle
52517804935883;;cycles:u;5653258477;100.00;;
526real: 5.70, user: 5.30, sys: 0.38, mem: 597716 kB
527## theories/lang/spawn.v
52842369515387;;instructions:u;11656243769;100.00;1.07;insn per cycle
52939712107329;;cycles:u;11656243769;100.00;;
530real: 11.71, user: 11.31, sys: 0.38, mem: 644144 kB
531## theories/logic/gps.v
53295945240293;;instructions:u;24120915841;100.00;1.21;insn per cycle
53379441819464;;cycles:u;24120915841;100.00;;
534real: 24.19, user: 23.65, sys: 0.48, mem: 815008 kB
535[buildjob] Submitting timing information to coq-speed (Project: lambda-rust, Branch: masters/weak_mem, Config: build-coq.8.11.2)
536Inserted 78 log entries
537 Creating cache build-coq.8.11.2-weak_mem-8... 01:32
538opamroot/: found 71109 matching files
539Uploading cache.zip to https://radosgw.mpi-sws.org/fp-science-ci/iris-ci-cache/project/178/build-coq.8.11.2-weak_mem-8
540Created cache
541Job succeeded