[0KRunning with gitlab-runner 12.4.1 (05161b14)
[0;m[0K on coop-timing 9b8a64cb
[0;msection_start:1594815045:prepare_executor
[0K[0KUsing Docker executor with image ralfjung/opam-ci:opam2 ...
[0;m[0KPulling docker image ralfjung/opam-ci:opam2 ...
[0;m[0KUsing docker image sha256:460ea3e90f2124074559dd798ee79b26c4c9b48104d5d442544716fdf91ed094 for ralfjung/opam-ci:opam2 ...
[0;msection_end:1594815048:prepare_executor
[0Ksection_start:1594815048:prepare_script
[0KRunning on runner-9b8a64cb-project-178-concurrent-0 via coop...
section_end:1594815050:prepare_script
[0Ksection_start:1594815050:get_sources
[0K[32;1mFetching changes...[0;m
Initialized empty Git repository in /builds/iris/lambda-rust/.git/
[32;1mCreated fresh repository.[0;m
From https://gitlab.mpi-sws.org/iris/lambda-rust
* [new ref] refs/pipelines/31478 -> refs/pipelines/31478
* [new branch] ci/janno/reduction_no_check -> origin/ci/janno/reduction_no_check
* [new branch] ci/places -> origin/ci/places
* [new branch] ci/pm_red -> origin/ci/pm_red
* [new branch] ci/ralf/const-rf -> origin/ci/ralf/const-rf
* [new branch] ci/ralf/lia-experiment -> origin/ci/ralf/lia-experiment
* [new branch] ci/ralf/old-timing-data -> origin/ci/ralf/old-timing-data
* [new branch] ci/ralf/sections -> origin/ci/ralf/sections
* [new branch] ci/robbert/faster_iDestruct2 -> origin/ci/robbert/faster_iDestruct2
* [new branch] ci/robbert/iprop_structures -> origin/ci/robbert/iprop_structures
* [new branch] ci/robbert/merge_sbi -> origin/ci/robbert/merge_sbi
* [new branch] ci/robbert/merge_sbi_new -> origin/ci/robbert/merge_sbi_new
* [new branch] ci/robbert/merge_sbi_new_weak -> origin/ci/robbert/merge_sbi_new_weak
* [new branch] ci/robbert/merge_sbi_weak -> origin/ci/robbert/merge_sbi_weak
* [new branch] ci/robbert/naive_solver -> origin/ci/robbert/naive_solver
* [new branch] ci/weak_mem -> origin/ci/weak_mem
* [new branch] coqbug/match -> origin/coqbug/match
* [new branch] fast_string -> origin/fast_string
* [new branch] gpirlea/pinning -> origin/gpirlea/pinning
* [new branch] jh/bug -> origin/jh/bug
* [new branch] jh/closures -> origin/jh/closures
* [new branch] jh/dynamic_masks -> origin/jh/dynamic_masks
* [new branch] jh/lifetime_no_dead_trade -> origin/jh/lifetime_no_dead_trade
* [new branch] jh/ofe_problems -> origin/jh/ofe_problems
* [new branch] jh/typecheck_foo -> origin/jh/typecheck_foo
* [new branch] master -> origin/master
* [new branch] masters/weak_mem -> origin/masters/weak_mem
* [new branch] no-opaque -> origin/no-opaque
* [new branch] notations -> origin/notations
* [new branch] ralf/acc -> origin/ralf/acc
* [new branch] ralf/sections-open -> origin/ralf/sections-open
* [new branch] skiplist -> origin/skiplist
* [new branch] strong_cas_fail -> origin/strong_cas_fail
* [new tag] RBrlx-POPL20-artifact -> RBrlx-POPL20-artifact
* [new tag] popl18 -> popl18
* [new tag] popl18-aec -> popl18-aec
[32;1mChecking out 9041a374 as masters/weak_mem...[0;m
[32;1mSkipping Git submodules setup[0;m
section_end:1594815054:get_sources
[0Ksection_start:1594815054:restore_cache
[0K[32;1mChecking cache for build-coq.8.11.2-weak_mem-8...[0;m
Downloading cache.zip from https://radosgw.mpi-sws.org/fp-science-ci/iris-ci-cache/project/178/build-coq.8.11.2-weak_mem-8[0;m
[32;1mSuccessfully extracted cache[0;m
section_end:1594815093:restore_cache
[0Ksection_start:1594815093:download_artifacts
[0Ksection_end:1594815095:download_artifacts
[0Ksection_start:1594815095:build_script
[0K[32;1m$ git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2[0;m
Cloning into 'ci'...
[32;1m$ ci/buildjob[0;m
[1;32m[buildjob] Using CI branch opam2 (0894aff50fedd29f36853535f33f34abb582687d)[0m
[1;32m[prepare-opam] Refreshing cached opam root[0m
# Creating build-dep package.
[NOTE] Will configure from built-in defaults.
Checking for available remotes: rsync and local, git.
- you won't be able to use mercurial repositories unless you install the hg command on your system.
- you won't be able to use darcs repositories unless you install the darcs command on your system.
<><> Updating repositories ><><><><><><><><><><><><><><><><><><><><><><><><><><>
[coq-released] synchronised from https://coq.inria.fr/opam/released
[iris-dev] synchronised from git+https://gitlab.mpi-sws.org/FP/opam-dev.git
[default] synchronised from https://opam.ocaml.org
<><> Synchronising development packages <><><><><><><><><><><><><><><><><><><><>
[coq-lambda-rust-builddep.~dev] synchronised from file:///builds/iris/lambda-rust/build-dep
[coq-iris.dev.2020-07-03.0.d44afeed] no changes from git+https://gitlab.mpi-sws.org/iris/iris.git#d44afeed8762544c87b79d11156e66b0737c5b06
[coq-orc11.dev.2020-07-03.0.adeaaee2] no changes from git+https://gitlab.mpi-sws.org/iris/orc11.git#adeaaee2ef4142e24239b2b844bbada238e62863
[coq-stdpp.dev.2020-07-02.1.c8129a37] no changes from git+https://gitlab.mpi-sws.org/iris/stdpp.git#c8129a3730a309b84b8965f936375d5e16ae3d94
[coq-gpfsl.dev.2020-07-03.0.ce4c6d6b] no changes from git+https://gitlab.mpi-sws.org/iris/gpfsl.git#ce4c6d6bde8832b24964c8d266eed450287b4936
[coq-lambda-rust-builddep] Conflicting update of the metadata from file:///builds/iris/lambda-rust/build-dep.
Override 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
Now run 'opam upgrade' to apply any package updates.
[1;32m[prepare-opam] opam report[0m
# opam config report
# opam-version 2.0.7
# self-upgrade no
# system arch=x86_64 os=linux os-distribution=debian os-version=9
# solver builtin-mccs+glpk
# install-criteria -removed,-count[version-lag,request],-count[version-lag,changed],-changed
# upgrade-criteria -removed,-count[version-lag,solution],-new
# jobs 20
# repositories 2 (http), 1 (version-controlled) (default repo at 94768e24)
# pinned 1 (rsync), 1 (version)
# current-switch ocaml-base-compiler.4.08.1
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.
<><> Repository configuration for switch ocaml-base-compiler.4.08.1 <><><><><><>
1 iris-dev git+https://gitlab.mpi-sws.org/FP/opam-dev.git
2 coq-released https://coq.inria.fr/opam/released
3 default https://opam.ocaml.org
[1;32m[prepare-opam] Removing old pins[0m
Ok, coq is no longer pinned to https://github.com/coq/coq/archive/V8.11.2.tar.gz (version 8.11.2)
Ok, coq-lambda-rust-builddep is no longer pinned to file:///builds/iris/lambda-rust/build-dep (version ~dev)
[1;32m[prepare-opam] Processing pins[0m
[1;32m[prepare-opam] version-pinning coq to 8.11.2[0m
coq is now pinned to version 8.11.2
[1;33m[prepare-opam] Pinning and installing build-dep and upgrading everything[0m
Package coq-lambda-rust-builddep does not exist, create as a NEW package? [Y/n] y
[coq-lambda-rust-builddep.~dev: rsync]
[coq-lambda-rust-builddep.~dev] synchronised from file:///builds/iris/lambda-rust/build-dep
[WARNING] coq-lambda-rust-builddep's opam file has uncommitted changes, using the versioned one
coq-lambda-rust-builddep is now pinned to file:///builds/iris/lambda-rust/build-dep (version ~dev)
<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-lambda-rust-builddep.~dev] no changes from file:///builds/iris/lambda-rust/build-dep
The following actions will be performed:
- upgrade coq-iris dev.2020-07-03.0.d44afeed to dev.2020-07-15.0.6b0e19f5 [required by coq-gpfsl]
- upgrade coq-gpfsl dev.2020-07-03.0.ce4c6d6b to dev.2020-07-15.0.654300d3 [required by coq-lambda-rust-builddep]
- recompile coq-lambda-rust-builddep ~dev*
===== 1 to recompile | 2 to upgrade =====
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[coq-lambda-rust-builddep.~dev] no changes from file:///builds/iris/lambda-rust/build-dep
[coq-gpfsl.dev.2020-07-15.0.654300d3] synchronised from git+https://gitlab.mpi-sws.org/iris/gpfsl.git#654300d356c6f806b4b5dcc971abffa9e3dc43f7
[coq-iris.dev.2020-07-15.0.6b0e19f5] synchronised from git+https://gitlab.mpi-sws.org/iris/iris.git#6b0e19f52d72dcb6d74843510b00d69e5f1826e0
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> removed coq-gpfsl.dev.2020-07-03.0.ce4c6d6b
-> removed coq-iris.dev.2020-07-03.0.d44afeed
-> removed coq-lambda-rust-builddep.~dev
-> installed coq-iris.dev.2020-07-15.0.6b0e19f5
-> installed coq-gpfsl.dev.2020-07-15.0.654300d3
-> installed coq-lambda-rust-builddep.~dev
Done.
Everything as up-to-date as possible (run with --verbose to show unavailable upgrades).
The following packages are not being upgraded because the new versions conflict with other installed packages:
- coq-iris.dev.2020-07-15.1.6ae02201
-- coq-gpfsl.dev.2020-07-15.0.654300d3 is installed and requires coq-iris (= dev.2020-07-15.0.6b0e19f5 | = dev)
- coq-stdpp.dev.2020-07-15.0.ab7ed0b8
-- coq-iris.dev.2020-07-15.1.6ae02201 is installed and requires coq-stdpp (= dev.2020-07-02.1.c8129a37 | = dev)
-- coq-orc11.dev.2020-07-03.0.adeaaee2 is installed and requires coq-stdpp (= dev.2020-07-02.1.c8129a37 | = dev)
However, you may "opam upgrade" these packages explicitly, which will ask permission to downgrade or uninstall the conflicting packages.
Nothing to do.
[1;32m[prepare-opam] Done! Some version information:[0m
name coq
version 8.11.2
source-hash
The Coq Proof Assistant, version 8.11.2 (June 2020)
compiled on Jun 19 2020 16:53:07 with OCaml 4.08.1
[1;32m[buildjob] Perfoming build[0m
"coq_makefile" -f _CoqProject -o Makefile.coq
COQDEP VFILES
COQC theories/lang/notation.v
COQC theories/lifetime/lifetime_sig.v
COQC theories/lang/memcpy.v
COQC theories/lang/swap.v
COQC theories/lang/new_delete.v
COQC theories/lang/spawn.v
COQC theories/lifetime/model/boxes.v
COQC theories/lifetime/model/definitions.v
COQC theories/lang/arc_cmra.v
COQC theories/lifetime/model/primitive.v
COQC theories/lifetime/model/faking.v
COQC theories/lifetime/model/borrow.v
COQC theories/lifetime/model/creation.v
COQC theories/lifetime/model/accessors.v
COQC theories/lifetime/model/in_at_borrow.v
COQC theories/lifetime/model/reborrow.v
COQC theories/lifetime/model/borrow_sep.v
COQC theories/lifetime/lifetime.v
COQC theories/lifetime/na_borrow.v
COQC theories/lifetime/at_borrow.v
COQC theories/lifetime/frac_borrow.v
COQC theories/typing/base.v
COQC theories/logic/gps.v
COQC theories/typing/lft_contexts.v
COQC theories/lang/lock.v
COQC theories/typing/type.v
COQC theories/typing/type_context.v
COQC theories/typing/util.v
COQC theories/typing/product.v
COQC theories/typing/sum.v
COQC theories/typing/cont_context.v
COQC theories/typing/uninit.v
COQC theories/typing/programs.v
COQC theories/typing/bool.v
COQC theories/typing/cont.v
COQC theories/typing/shr_bor.v
COQC theories/typing/int.v
COQC theories/typing/fixpoint.v
COQC theories/typing/uniq_bor.v
COQC theories/typing/own.v
COQC theories/typing/product_split.v
COQC theories/typing/borrow.v
COQC theories/typing/type_sum.v
COQC theories/typing/function.v
COQC theories/typing/typing.v
COQC theories/typing/lib/panic.v
COQC theories/typing/soundness.v
COQC theories/typing/lib/diverging_static.v
COQC theories/typing/lib/fake_shared.v
COQC theories/typing/examples/get_x.v
COQC theories/typing/lib/spawn.v
COQC theories/typing/lib/take_mut.v
COQC theories/typing/examples/unbox.v
COQC theories/typing/lib/refcell/refcell.v
COQC theories/typing/examples/rebor.v
COQC theories/typing/lib/join.v
COQC theories/typing/examples/init_prod.v
COQC theories/typing/lib/cell.v
COQC theories/typing/examples/lazy_lft.v
COQC theories/typing/lib/option.v
COQC theories/typing/lib/rwlock/rwlock.v
COQC theories/typing/lib/refcell/ref.v
COQC theories/typing/lib/refcell/refmut.v
COQC theories/typing/lib/rwlock/rwlockreadguard.v
COQC theories/lang/arc.v
COQC theories/typing/lib/mutex/mutex.v
COQC theories/typing/lib/rwlock/rwlockwriteguard.v
COQC theories/typing/examples/nonlexical.v
COQC theories/typing/lib/rwlock/rwlockreadguard_code.v
COQC theories/typing/lib/rwlock/rwlockwriteguard_code.v
COQC theories/typing/lib/mutex/mutexguard.v
COQC theories/typing/lib/refcell/refcell_code.v
COQC theories/typing/lib/rwlock/rwlock_code.v
COQC theories/typing/lib/refcell/ref_code.v
COQC theories/typing/lib/refcell/refmut_code.v
COQC theories/typing/lib/rc/rc.v
COQC theories/typing/lib/arc.v
COQC theories/typing/lib/rc/weak.v
real 12m7.609s
user 42m31.872s
sys 0m35.164s
[1;32m[buildjob] Build performance information[0m
## theories/typing/type_context.v
32872118451;;instructions:u;9727099317;100.00;1.04;insn per cycle
31652195152;;cycles:u;9727099317;100.00;;
real: 9.78, user: 9.37, sys: 0.38, mem: 646668 kB
## theories/typing/type_sum.v
105385879745;;instructions:u;29520103956;100.00;1.06;insn per cycle
99368774527;;cycles:u;29520103956;100.00;;
real: 29.63, user: 29.10, sys: 0.45, mem: 784084 kB
## theories/typing/examples/rebor.v
32280672150;;instructions:u;8824694546;100.00;1.09;insn per cycle
29659169101;;cycles:u;8824694546;100.00;;
real: 8.91, user: 8.46, sys: 0.37, mem: 644800 kB
## theories/typing/examples/init_prod.v
26966290091;;instructions:u;7520501547;100.00;1.08;insn per cycle
24998229288;;cycles:u;7520501547;100.00;;
real: 7.60, user: 7.15, sys: 0.37, mem: 637732 kB
## theories/typing/examples/get_x.v
20739149640;;instructions:u;6100581600;100.00;1.05;insn per cycle
19766869475;;cycles:u;6100581600;100.00;;
real: 6.22, user: 5.70, sys: 0.40, mem: 628744 kB
## theories/typing/examples/lazy_lft.v
50716160644;;instructions:u;13190300513;100.00;1.11;insn per cycle
45820777196;;cycles:u;13190300513;100.00;;
real: 13.24, user: 12.80, sys: 0.39, mem: 645384 kB
## theories/typing/examples/nonlexical.v
180518595647;;instructions:u;43125572808;100.00;1.19;insn per cycle
151638281560;;cycles:u;43125572808;100.00;;
real: 43.53, user: 42.72, sys: 0.42, mem: 764792 kB
## theories/typing/examples/unbox.v
22357411431;;instructions:u;6598171741;100.00;1.04;insn per cycle
21515839634;;cycles:u;6598171741;100.00;;
real: 6.70, user: 6.21, sys: 0.38, mem: 630692 kB
## theories/typing/cont_context.v
23078652539;;instructions:u;6700533090;100.00;1.09;insn per cycle
21121483458;;cycles:u;6700533090;100.00;;
real: 6.75, user: 6.35, sys: 0.36, mem: 601276 kB
## theories/typing/int.v
26142530601;;instructions:u;7928078523;100.00;1.05;insn per cycle
25002751823;;cycles:u;7928078523;100.00;;
real: 7.98, user: 7.54, sys: 0.40, mem: 632324 kB
## theories/typing/base.v
14792082576;;instructions:u;4525481024;100.00;1.14;insn per cycle
12961574842;;cycles:u;4525481024;100.00;;
real: 4.56, user: 4.14, sys: 0.39, mem: 613816 kB
## theories/typing/sum.v
55363756914;;instructions:u;15471208241;100.00;1.07;insn per cycle
51708971405;;cycles:u;15471208241;100.00;;
real: 15.52, user: 15.09, sys: 0.40, mem: 651076 kB
## theories/typing/lib/rwlock/rwlock_code.v
278575192919;;instructions:u;75113496917;100.00;1.07;insn per cycle
260102330348;;cycles:u;75113496917;100.00;;
real: 75.62, user: 74.54, sys: 0.58, mem: 1058740 kB
## theories/typing/lib/rwlock/rwlockreadguard.v
77371143343;;instructions:u;20491565566;100.00;1.10;insn per cycle
70369278057;;cycles:u;20491565566;100.00;;
real: 20.57, user: 20.04, sys: 0.45, mem: 711988 kB
## theories/typing/lib/rwlock/rwlockreadguard_code.v
129755459061;;instructions:u;35732125756;100.00;1.06;insn per cycle
121911740277;;cycles:u;35732125756;100.00;;
real: 36.06, user: 35.25, sys: 0.49, mem: 846904 kB
## theories/typing/lib/rwlock/rwlockwriteguard_code.v
114819333081;;instructions:u;32188482396;100.00;1.03;insn per cycle
111893205068;;cycles:u;32188482396;100.00;;
real: 32.50, user: 31.68, sys: 0.52, mem: 817128 kB
## theories/typing/lib/rwlock/rwlock.v
110281286950;;instructions:u;31101892525;100.00;1.04;insn per cycle
106175118293;;cycles:u;31101892525;100.00;;
real: 31.36, user: 30.69, sys: 0.41, mem: 805956 kB
## theories/typing/lib/rwlock/rwlockwriteguard.v
91804038622;;instructions:u;24948297943;100.00;1.08;insn per cycle
85308009076;;cycles:u;24948297943;100.00;;
real: 25.07, user: 24.55, sys: 0.40, mem: 731424 kB
## theories/typing/lib/cell.v
90698209233;;instructions:u;25896658182;100.00;1.00;insn per cycle
90662693389;;cycles:u;25896658182;100.00;;
real: 26.22, user: 25.51, sys: 0.43, mem: 746132 kB
## theories/typing/lib/rc/weak.v
371647641907;;instructions:u;92957690229;100.00;1.16;insn per cycle
320546775820;;cycles:u;92957690229;100.00;;
real: 93.10, user: 92.32, sys: 0.65, mem: 1164924 kB
## theories/typing/lib/rc/rc.v
1001529971960;;instructions:u;261944450617;100.00;1.12;insn per cycle
896970804765;;cycles:u;261944450617;100.00;;
real: 263.30, user: 260.96, sys: 1.01, mem: 1223784 kB
## theories/typing/lib/arc.v
1022612004261;;instructions:u;266505070996;100.00;1.13;insn per cycle
906422706688;;cycles:u;266505070996;100.00;;
real: 267.99, user: 265.58, sys: 0.93, mem: 1183684 kB
## theories/typing/lib/mutex/mutex.v
90648175742;;instructions:u;26597895309;100.00;1.01;insn per cycle
89656370042;;cycles:u;26597895309;100.00;;
real: 26.82, user: 26.13, sys: 0.49, mem: 755148 kB
## theories/typing/lib/mutex/mutexguard.v
158420880648;;instructions:u;44160200394;100.00;1.03;insn per cycle
153634738502;;cycles:u;44160200394;100.00;;
real: 44.47, user: 43.68, sys: 0.48, mem: 831980 kB
## theories/typing/lib/take_mut.v
60941965442;;instructions:u;17090979258;100.00;1.04;insn per cycle
58720031665;;cycles:u;17090979258;100.00;;
real: 17.34, user: 16.71, sys: 0.43, mem: 677492 kB
## theories/typing/lib/fake_shared.v
43032094325;;instructions:u;12337295792;100.00;1.02;insn per cycle
42036386247;;cycles:u;12337295792;100.00;;
real: 12.56, user: 12.00, sys: 0.37, mem: 641816 kB
## theories/typing/lib/refcell/refcell.v
68539007190;;instructions:u;19538288820;100.00;1.01;insn per cycle
67722668691;;cycles:u;19538288820;100.00;;
real: 19.78, user: 19.13, sys: 0.45, mem: 699052 kB
## theories/typing/lib/refcell/ref_code.v
482213834967;;instructions:u;130183666060;100.00;1.09;insn per cycle
441520834957;;cycles:u;130183666060;100.00;;
real: 130.90, user: 129.48, sys: 0.72, mem: 1174308 kB
## theories/typing/lib/refcell/refmut.v
103762162749;;instructions:u;27961383813;100.00;1.12;insn per cycle
92960843691;;cycles:u;27961383813;100.00;;
real: 28.06, user: 27.52, sys: 0.44, mem: 857548 kB
## theories/typing/lib/refcell/ref.v
102195744397;;instructions:u;27127354772;100.00;1.11;insn per cycle
91911256485;;cycles:u;27127354772;100.00;;
real: 27.21, user: 26.66, sys: 0.48, mem: 869912 kB
## theories/typing/lib/refcell/refcell_code.v
251159926097;;instructions:u;69420411061;100.00;1.04;insn per cycle
241892662711;;cycles:u;69420411061;100.00;;
real: 69.96, user: 68.88, sys: 0.54, mem: 956816 kB
## theories/typing/lib/refcell/refmut_code.v
530824315473;;instructions:u;140233467917;100.00;1.12;insn per cycle
472165536999;;cycles:u;140233467917;100.00;;
real: 141.00, user: 139.52, sys: 0.73, mem: 1210888 kB
## theories/typing/lib/panic.v
16546196654;;instructions:u;4908781682;100.00;1.06;insn per cycle
15675176722;;cycles:u;4908781682;100.00;;
real: 5.03, user: 4.54, sys: 0.41, mem: 624588 kB
## theories/typing/lib/diverging_static.v
38427187982;;instructions:u;10754025840;100.00;1.06;insn per cycle
36212856730;;cycles:u;10754025840;100.00;;
real: 10.96, user: 10.38, sys: 0.43, mem: 642024 kB
## theories/typing/lib/join.v
78928294506;;instructions:u;20924922400;100.00;1.09;insn per cycle
72482114152;;cycles:u;20924922400;100.00;;
real: 21.28, user: 20.56, sys: 0.42, mem: 709356 kB
## theories/typing/lib/spawn.v
49170401677;;instructions:u;14037215831;100.00;1.03;insn per cycle
47848645269;;cycles:u;14037215831;100.00;;
real: 14.24, user: 13.69, sys: 0.40, mem: 641684 kB
## theories/typing/lib/option.v
58431268107;;instructions:u;15509516331;100.00;1.11;insn per cycle
52692432124;;cycles:u;15509516331;100.00;;
real: 15.56, user: 15.13, sys: 0.38, mem: 641756 kB
## theories/typing/shr_bor.v
33206653877;;instructions:u;9336405185;100.00;1.07;insn per cycle
30898432611;;cycles:u;9336405185;100.00;;
real: 9.39, user: 8.99, sys: 0.39, mem: 641668 kB
## theories/typing/own.v
87950916345;;instructions:u;24405775047;100.00;1.08;insn per cycle
81748295193;;cycles:u;24405775047;100.00;;
real: 24.48, user: 23.99, sys: 0.46, mem: 728572 kB
## theories/typing/function.v
118799909370;;instructions:u;32783004154;100.00;1.10;insn per cycle
107829299109;;cycles:u;32783004154;100.00;;
real: 32.86, user: 32.40, sys: 0.40, mem: 760608 kB
## theories/typing/product_split.v
57822177796;;instructions:u;17227152440;100.00;1.02;insn per cycle
56416800197;;cycles:u;17227152440;100.00;;
real: 17.34, user: 16.85, sys: 0.40, mem: 671248 kB
## theories/typing/uniq_bor.v
77727544367;;instructions:u;21115749535;100.00;1.10;insn per cycle
70659460097;;cycles:u;21115749535;100.00;;
real: 21.22, user: 20.73, sys: 0.43, mem: 730960 kB
## theories/typing/soundness.v
24388373183;;instructions:u;7642894249;100.00;0.99;insn per cycle
24642573299;;cycles:u;7642894249;100.00;;
real: 7.76, user: 7.29, sys: 0.40, mem: 641188 kB
## theories/typing/uninit.v
24672543873;;instructions:u;7583372392;100.00;1.07;insn per cycle
23093141505;;cycles:u;7583372392;100.00;;
real: 7.63, user: 7.20, sys: 0.40, mem: 628532 kB
## theories/typing/product.v
51567980676;;instructions:u;14450139488;100.00;1.06;insn per cycle
48726971504;;cycles:u;14450139488;100.00;;
real: 14.51, user: 14.06, sys: 0.42, mem: 650716 kB
## theories/typing/type.v
84142456402;;instructions:u;21625192129;100.00;1.13;insn per cycle
74663704004;;cycles:u;21625192129;100.00;;
real: 21.67, user: 21.27, sys: 0.37, mem: 649820 kB
## theories/typing/typing.v
14853821451;;instructions:u;4019047984;100.00;1.18;insn per cycle
12576568938;;cycles:u;4019047984;100.00;;
real: 4.03, user: 3.61, sys: 0.41, mem: 623416 kB
## theories/typing/util.v
38086821362;;instructions:u;10452780778;100.00;1.13;insn per cycle
33680997140;;cycles:u;10452780778;100.00;;
real: 10.51, user: 10.09, sys: 0.39, mem: 623280 kB
## theories/typing/bool.v
21639142957;;instructions:u;6407083810;100.00;1.11;insn per cycle
19499145068;;cycles:u;6407083810;100.00;;
real: 6.48, user: 6.08, sys: 0.36, mem: 619840 kB
## theories/typing/fixpoint.v
27511728662;;instructions:u;8203829898;100.00;1.07;insn per cycle
25683800863;;cycles:u;8203829898;100.00;;
real: 8.26, user: 7.74, sys: 0.48, mem: 646388 kB
## theories/typing/lft_contexts.v
42891217594;;instructions:u;11802376928;100.00;1.10;insn per cycle
38828001046;;cycles:u;11802376928;100.00;;
real: 11.86, user: 11.44, sys: 0.37, mem: 642076 kB
## theories/typing/borrow.v
70943268511;;instructions:u;19650273019;100.00;1.10;insn per cycle
64547243724;;cycles:u;19650273019;100.00;;
real: 19.73, user: 19.29, sys: 0.38, mem: 706144 kB
## theories/typing/programs.v
80659988624;;instructions:u;21387013858;100.00;1.13;insn per cycle
71395597982;;cycles:u;21387013858;100.00;;
real: 21.43, user: 21.02, sys: 0.38, mem: 693596 kB
## theories/typing/cont.v
22001757480;;instructions:u;6613323305;100.00;1.07;insn per cycle
20547741722;;cycles:u;6613323305;100.00;;
real: 6.67, user: 6.26, sys: 0.39, mem: 627060 kB
## theories/lifetime/at_borrow.v
25546688374;;instructions:u;7544480662;100.00;1.12;insn per cycle
22719305779;;cycles:u;7544480662;100.00;;
real: 7.58, user: 7.18, sys: 0.38, mem: 602852 kB
## theories/lifetime/model/creation.v
81351713632;;instructions:u;23117571666;100.00;1.10;insn per cycle
73982632865;;cycles:u;23117571666;100.00;;
real: 23.21, user: 22.71, sys: 0.42, mem: 700544 kB
## theories/lifetime/model/primitive.v
63739408581;;instructions:u;18000346144;100.00;1.08;insn per cycle
59136550395;;cycles:u;18000346144;100.00;;
real: 18.06, user: 17.60, sys: 0.41, mem: 672620 kB
## theories/lifetime/model/reborrow.v
128798235383;;instructions:u;33785893628;100.00;1.13;insn per cycle
114435182533;;cycles:u;33785893628;100.00;;
real: 33.92, user: 33.33, sys: 0.46, mem: 839100 kB
## theories/lifetime/model/definitions.v
25382185075;;instructions:u;7544143742;100.00;1.09;insn per cycle
23322908049;;cycles:u;7544143742;100.00;;
real: 7.58, user: 7.20, sys: 0.36, mem: 602808 kB
## theories/lifetime/model/in_at_borrow.v
28743330009;;instructions:u;8218587369;100.00;1.12;insn per cycle
25673587046;;cycles:u;8218587369;100.00;;
real: 8.25, user: 7.88, sys: 0.34, mem: 602028 kB
## theories/lifetime/model/borrow_sep.v
129798482371;;instructions:u;34978794655;100.00;1.16;insn per cycle
112182942164;;cycles:u;34978794655;100.00;;
real: 35.14, user: 34.47, sys: 0.52, mem: 868848 kB
## theories/lifetime/model/boxes.v
72472251804;;instructions:u;21087189488;100.00;1.07;insn per cycle
67732365260;;cycles:u;21087189488;100.00;;
real: 21.36, user: 20.70, sys: 0.42, mem: 675516 kB
## theories/lifetime/model/accessors.v
164115815333;;instructions:u;44304701202;100.00;1.11;insn per cycle
148496168957;;cycles:u;44304701202;100.00;;
real: 44.46, user: 43.78, sys: 0.54, mem: 877696 kB
## theories/lifetime/model/faking.v
48020846031;;instructions:u;13604479193;100.00;1.09;insn per cycle
44068093366;;cycles:u;13604479193;100.00;;
real: 13.65, user: 13.24, sys: 0.38, mem: 627364 kB
## theories/lifetime/model/borrow.v
49853587508;;instructions:u;14248395310;100.00;1.09;insn per cycle
45925235645;;cycles:u;14248395310;100.00;;
real: 14.34, user: 13.82, sys: 0.45, mem: 642364 kB
## theories/lifetime/na_borrow.v
19263177284;;instructions:u;5566368201;100.00;1.12;insn per cycle
17212018184;;cycles:u;5566368201;100.00;;
real: 5.60, user: 5.16, sys: 0.43, mem: 601848 kB
## theories/lifetime/lifetime_sig.v
12685458015;;instructions:u;3927988326;100.00;1.11;insn per cycle
11395966547;;cycles:u;3927988326;100.00;;
real: 4.08, user: 3.59, sys: 0.37, mem: 589372 kB
## theories/lifetime/frac_borrow.v
96693639235;;instructions:u;24829871962;100.00;1.14;insn per cycle
84994794649;;cycles:u;24829871962;100.00;;
real: 24.92, user: 24.42, sys: 0.43, mem: 768824 kB
## theories/lifetime/lifetime.v
51697009040;;instructions:u;14379375774;100.00;1.12;insn per cycle
46209586328;;cycles:u;14379375774;100.00;;
real: 14.45, user: 14.06, sys: 0.32, mem: 646292 kB
## theories/lang/lock.v
43087959899;;instructions:u;12169316916;100.00;1.15;insn per cycle
37631302400;;cycles:u;12169316916;100.00;;
real: 12.23, user: 11.82, sys: 0.36, mem: 641608 kB
## theories/lang/new_delete.v
11789243328;;instructions:u;3758386170;100.00;1.14;insn per cycle
10317464977;;cycles:u;3758386170;100.00;;
real: 3.81, user: 3.43, sys: 0.33, mem: 586140 kB
## theories/lang/swap.v
21432709189;;instructions:u;5992839456;100.00;1.13;insn per cycle
19000208437;;cycles:u;5992839456;100.00;;
real: 6.06, user: 5.67, sys: 0.35, mem: 597828 kB
## theories/lang/arc.v
1353931055221;;instructions:u;353681382360;100.00;1.13;insn per cycle
1201084937088;;cycles:u;353681382360;100.00;;
real: 354.84, user: 352.87, sys: 0.82, mem: 1438628 kB
## theories/lang/arc_cmra.v
156897683589;;instructions:u;39032204239;100.00;1.19;insn per cycle
131632115785;;cycles:u;39032204239;100.00;;
real: 39.18, user: 38.64, sys: 0.42, mem: 691852 kB
## theories/lang/notation.v
3782298817;;instructions:u;1475158467;100.00;1.14;insn per cycle
3319169767;;cycles:u;1475158467;100.00;;
real: 1.62, user: 1.18, sys: 0.32, mem: 495768 kB
## theories/lang/memcpy.v
19716571512;;instructions:u;5653258477;100.00;1.11;insn per cycle
17804935883;;cycles:u;5653258477;100.00;;
real: 5.70, user: 5.30, sys: 0.38, mem: 597716 kB
## theories/lang/spawn.v
42369515387;;instructions:u;11656243769;100.00;1.07;insn per cycle
39712107329;;cycles:u;11656243769;100.00;;
real: 11.71, user: 11.31, sys: 0.38, mem: 644144 kB
## theories/logic/gps.v
95945240293;;instructions:u;24120915841;100.00;1.21;insn per cycle
79441819464;;cycles:u;24120915841;100.00;;
real: 24.19, user: 23.65, sys: 0.48, mem: 815008 kB
[1;32m[buildjob] Submitting timing information to coq-speed (Project: lambda-rust, Branch: masters/weak_mem, Config: build-coq.8.11.2)[0m
Inserted 78 log entries
section_end:1594816606:build_script
[0Ksection_start:1594816606:after_script
[0Ksection_end:1594816608:after_script
[0Ksection_start:1594816608:archive_cache
[0K[32;1mCreating cache build-coq.8.11.2-weak_mem-8...[0;m
opamroot/: found 71109 matching files [0;m
Uploading cache.zip to https://radosgw.mpi-sws.org/fp-science-ci/iris-ci-cache/project/178/build-coq.8.11.2-weak_mem-8[0;m
[32;1mCreated cache[0;m
section_end:1594816700:archive_cache
[0Ksection_start:1594816700:upload_artifacts_on_success
[0Ksection_end:1594816702:upload_artifacts_on_success
[0K[32;1mJob succeeded
[0;m