[0KRunning with gitlab-runner 12.4.1 (05161b14)
[0;m[0K on coop 5118fc3f
[0;msection_start:1594813519: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:1594813522:prepare_executor
[0Ksection_start:1594813522:prepare_script
[0KRunning on runner-5118fc3f-project-178-concurrent-1 via coop...
section_end:1594813524:prepare_script
[0Ksection_start:1594813524: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:1594813528:get_sources
[0Ksection_start:1594813528:restore_cache
[0K[32;1mChecking cache for build-coq.8.12.dev-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.12.dev-weak_mem-8[0;m
[32;1mSuccessfully extracted cache[0;m
section_end:1594813578:restore_cache
[0Ksection_start:1594813578:download_artifacts
[0Ksection_end:1594813579:download_artifacts
[0Ksection_start:1594813579: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-core-dev] synchronised from https://coq.inria.fr/opam/core-dev
[coq-extra-dev] synchronised from https://coq.inria.fr/opam/extra-dev
[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-gpfsl.dev.2020-07-03.0.ce4c6d6b] no changes from git+https://gitlab.mpi-sws.org/iris/gpfsl.git#ce4c6d6bde8832b24964c8d266eed450287b4936
[coq-iris.dev.2020-07-03.0.d44afeed] no changes from git+https://gitlab.mpi-sws.org/iris/iris.git#d44afeed8762544c87b79d11156e66b0737c5b06
[coq-lambda-rust-builddep.~dev] synchronised from file:///builds/iris/lambda-rust/build-dep
[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.8.12.dev] synchronised from git+https://github.com/coq/coq.git#v8.12
[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 4 (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-core-dev https://coq.inria.fr/opam/core-dev
3 coq-extra-dev https://coq.inria.fr/opam/extra-dev
4 coq-released https://coq.inria.fr/opam/released
5 default https://opam.ocaml.org
[1;32m[prepare-opam] Removing old pins[0m
Ok, coq is no longer pinned to git+https://github.com/coq/coq.git#v8.12 (version 8.12.dev)
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.12.dev[0m
coq is now pinned to version 8.12.dev
[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
[coq.8.12.dev] synchronised from git+https://github.com/coq/coq.git#v8.12
The following actions will be performed:
- recompile coq 8.12.dev*
- recompile coq-stdpp dev.2020-07-02.1.c8129a37 [uses coq]
- upgrade coq-iris dev.2020-07-03.0.d44afeed to dev.2020-07-15.0.6b0e19f5 [upstream changes]
- recompile coq-orc11 dev.2020-07-03.0.adeaaee2 [uses coq]
- 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*
===== 4 to recompile | 2 to upgrade =====
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[coq-gpfsl.dev.2020-07-15.0.654300d3] synchronised from git+https://gitlab.mpi-sws.org/iris/gpfsl.git#654300d356c6f806b4b5dcc971abffa9e3dc43f7
[coq-lambda-rust-builddep.~dev] no changes from file:///builds/iris/lambda-rust/build-dep
[coq.8.12.dev] no changes from git+https://github.com/coq/coq.git#v8.12
[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-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
-> removed coq-orc11.dev.2020-07-03.0.adeaaee2
-> removed coq-stdpp.dev.2020-07-02.1.c8129a37
-> removed coq.8.12.dev
-> installed coq.8.12.dev
-> installed coq-stdpp.dev.2020-07-02.1.c8129a37
-> installed coq-orc11.dev.2020-07-03.0.adeaaee2
-> 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.12.dev
source-hash 36468ab7
The Coq Proof Assistant, version 8.12+beta1 (July 2020)
compiled on Jul 15 2020 11:46:52 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
File "./theories/lang/notation.v", line 28, characters 0-120:
Warning: The format modifier is irrelevant for only parsing rules.
[irrelevant-format-only-parsing,parsing]
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/cont.v
COQC theories/typing/bool.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/examples/get_x.v
COQC theories/typing/lib/fake_shared.v
COQC theories/typing/lib/spawn.v
COQC theories/typing/lib/take_mut.v
COQC theories/typing/examples/unbox.v
COQC theories/typing/examples/rebor.v
COQC theories/typing/examples/init_prod.v
COQC theories/typing/lib/refcell/refcell.v
COQC theories/typing/lib/join.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/typing/lib/mutex/mutex.v
COQC theories/typing/lib/rwlock/rwlockwriteguard.v
COQC theories/lang/arc.v
COQC theories/typing/examples/nonlexical.v
COQC theories/typing/lib/rwlock/rwlockwriteguard_code.v
COQC theories/typing/lib/rwlock/rwlockreadguard_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
File "./theories/typing/lib/rwlock/rwlock_code.v", line 249, characters 59-65:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
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 13m23.651s
user 47m2.920s
sys 0m35.808s
section_end:1594815658:build_script
[0Ksection_start:1594815658:after_script
[0Ksection_end:1594815660:after_script
[0Ksection_start:1594815660:archive_cache
[0K[32;1mCreating cache build-coq.8.12.dev-weak_mem-8...[0;m
opamroot/: found 77532 matching files [0;m
Uploading cache.zip to https://radosgw.mpi-sws.org/fp-science-ci/iris-ci-cache/project/178/build-coq.8.12.dev-weak_mem-8[0;m
[32;1mCreated cache[0;m
section_end:1594815771:archive_cache
[0Ksection_start:1594815771:upload_artifacts_on_success
[0Ksection_end:1594815773:upload_artifacts_on_success
[0K[32;1mJob succeeded
[0;m