Fixes #15221: a case of invalid eta-expansion in notation printing #17841
coqbot-app / GitLab CI job library:ci-geocoq (pull request)
completed
Jul 11, 2023 in 0s
Test has failed on GitLab CI
This job is allowed to fail.
This job ran on the Docker image registry.gitlab.com/coq/coq:bionic_coq-V2023-06-29-2b9dca3152, depended on the build job build:edge+flambda with OCaml 4.14.1+flambda.
We show below an excerpt from the trace from GitLab starting around the last detected "Error" (the complete trace is available here).
Details
File "./Meta_theory/Models/POF_to_Tarski.v", line 21, characters 0-64:
Error: Cannot find a physical path bound to logical path
GeoCoq.Meta_theory.Counter_models.nD.coplanarity.
Command exited with non-zero status 1
Meta_theory/Models/POF_to_Tarski.vo (real: 2.46, user: 1.16, sys: 0.37, mem: 600592 ko)
Makefile:823: recipe for target 'Meta_theory/Models/POF_to_Tarski.vo' failed
make[2]: *** [Meta_theory/Models/POF_to_Tarski.vo] Error 1
make[2]: *** Waiting for unfinished jobs....
Tarski_dev/Annexes/inscribed_angle.vo (real: 9.22, user: 8.88, sys: 0.32, mem: 578004 ko)
COQNATIVE Tarski_dev/Annexes/inscribed_angle.vo
Tarski_dev/Annexes/inscribed_angle.vo.native (real: 0.72, user: 0.52, sys: 0.19, mem: 158716 ko)
Makefile:408: recipe for target 'all' failed
make[1]: *** [all] Error 2
make[1]: Leaving directory '/builds/coq/coq/_build_ci/geocoq'
Aggregating timing log...
Time | Peak Mem | File Name
------------------------------------------------------------------------------------------------------------------------------------
14m59.38s | 714924 ko | Total Time / Peak Mem
------------------------------------------------------------------------------------------------------------------------------------
0m37.52s | 668488 ko | Tarski_dev/Ch13_1.vo
0m29.70s | 714924 ko | Meta_theory/Models/hilbert_to_tarski.vo
0m26.28s | 596036 ko | Meta_theory/Continuity/aristotle.vo
0m22.30s | 653096 ko | Tarski_dev/Ch11_angles.vo
0m19.06s | 599772 ko | Tarski_dev/Annexes/saccheri.vo
0m18.32s | 500332 ko | Meta_theory/Counter_models/Planar/counter_model_cong_inner_transitivity.vo
0m17.29s | 416516 ko | Elements/OriginalProofs/lemma_planeseparation.vo
0m16.14s | 620184 ko | Highschool/orientation.vo
0m14.14s | 454496 ko | Meta_theory/Counter_models/Planar/counter_model_bet_inner_transitivity.vo
0m12.57s | 608700 ko | Tarski_dev/Annexes/quadrilaterals_inter_dec.vo
0m12.23s | 568912 ko | Tarski_dev/Ch09_plane.vo
0m11.62s | 568948 ko | Tarski_dev/Annexes/suma.vo
0m09.79s | 568048 ko | Tarski_dev/Ch08_orthogonality.vo
0m08.88s | 578004 ko | Tarski_dev/Annexes/inscribed_angle.vo
0m08.85s | 414340 ko | Elements/OriginalProofs/proposition_30.vo
0m07.63s | 572916 ko | Meta_theory/Models/tarski_to_euclid.vo
0m07.59s | 430092 ko | Elements/OriginalProofs/lemma_paste5.vo
0m07.36s | 547840 ko | Meta_theory/Dimension_axioms/upper_dim_3.vo
0m07.19s | 532860 ko | Meta_theory/Models/tarski_to_beeson.vo
0m07.18s | 560468 ko | Tarski_dev/Annexes/circles.vo