Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[core-dev] Adapt to https://github.com/coq/coq/pull/19530 #3240

Merged
merged 1 commit into from
Dec 6, 2024

Adapt to https://github.com/coq/coq/pull/19530

935d67d
Select commit
Loading
Failed to load commit list.
Merged

[core-dev] Adapt to https://github.com/coq/coq/pull/19530 #3240

Adapt to https://github.com/coq/coq/pull/19530
935d67d
Select commit
Loading
Failed to load commit list.
coqbot-app / GitLab CI job opam-build:4.14.0 (pull request) failed Dec 6, 2024 in 0s

Test has failed on GitLab CI

This job has failed. If you need to, you can restart it directly in the GitHub interface using the "Re-run" button.

We show below the last 40 lines of the trace from GitLab (the complete trace is available here).

Details

  - install conf-pkg-config 3      [required by zarith]
  - install ocamlfind       1.9.6  [required by coq-core]
  - install zarith          1.14   [required by coq-core]
  - install coq-core        dev    [required by rocq-core]
  - install rocq-core       dev
===== 7 to install =====
Installing rocq-core.dev
[WARNING] Running as root is not recommended
[ERROR] The compilation of rocq-core.dev failed at "dune build -p rocq-core -j 2 --promote-install-files=false @install @runtest".

#=== ERROR while compiling rocq-core.dev ======================================#
# context              2.1.2 | linux/x86_64 | ocaml-base-compiler.4.14.0 | file:///builds/coq/opam/core-dev
# path                 ~/opam-root-4.14.0-2.1.2-sandbox/4.14.0/.opam-switch/build/rocq-core.dev
# command              ~/opam-root-4.14.0-2.1.2-sandbox/4.14.0/bin/dune build -p rocq-core -j 2 --promote-install-files=false @install @runtest
# exit-code            1
# env-file             ~/opam-root-4.14.0-2.1.2-sandbox/log/rocq-core-25200-5e5e66.env
# output-file          ~/opam-root-4.14.0-2.1.2-sandbox/log/rocq-core-25200-5e5e66.out
### output ###
# File "test-suite/dune", line 30, characters 12-25:
# 30 |    (package coqide-server)
#                  ^^^^^^^^^^^^^
# Error: Package coqide-server does not exist


The former state can be restored with:
    /usr/local/bin/opam switch import "/builds/coq/opam/opam-root-4.14.0-2.1.2-sandbox/4.14.0/.opam-switch/backup/state-20241206094328.export"
'opam install rocq-core.dev -y -v -v --with-test' failed.
Removing rocq-core
[WARNING] Running as root is not recommended
[NOTE] rocq-core is not installed.

Packages that failed to install: coq-stdlib.dev coq.dev rocq-core.dev
Packages that succeeded to install:
Uploading artifacts for failed job
Uploading artifacts...
log/: found 4 matching artifact files and directories 
Uploading artifacts as "archive" to coordinator... 201 Created  id=5042315 responseStatus=201 Created token=glcbt-64
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1
View more details on coqbot-app