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.

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

coq 8.15.2 #103724

Closed
wants to merge 1 commit into from
Closed

coq 8.15.2 #103724

wants to merge 1 commit into from

Conversation

PythonCoderAS
Copy link
Contributor

Created by brew bump


Created with brew bump-formula-pr.

@BrewTestBot BrewTestBot added bump-formula-pr PR was created using `brew bump-formula-pr` ocaml OCaml use is a significant feature of the PR or issue labels Jun 15, 2022
@iMichka
Copy link
Member

iMichka commented Jun 15, 2022

Same failure as the previous version, tested in #97561:

==> make world
/usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build world
make[1]: Entering directory '/tmp/coq-20220615-4351-svyfdx/coq-8.15.2'
MKDIR     BUILD_OUT
DUNE      _build/install/default/bin/coqdep
DUNE      sources
COQDEP    VFILES
DUNE      sources
DUNE      _build/install/default/bin/coqc
DUNE      _build/default/plugins/ltac/ltac_plugin.cmxs
File "interp/dune", line 6, characters 12-18:
6 |  (libraries zarith pretyping))
                ^^^^^^
Error: Library "zarith" not found.
-> required by library "coq-core.interp" in _build/default/interp
-> required by executable coqc_bin in topbin/dune:24
-> required by _build/default/topbin/coqc_bin.exe
-> required by _build/install/default/bin/coqc
Makefile.common:130: recipe for target '_build/install/default/bin/coqc' failed
make[1]: *** [_build/install/default/bin/coqc] Error 1
make[1]: *** Waiting for unfinished jobs....
File "interp/dune", line 6, characters 12-18:
6 |  (libraries zarith pretyping))
                ^^^^^^
Error: Library "zarith" not found.
-> required by library "coq-core.interp" in _build/default/interp
-> required by
   _build/default/plugins/ltac/.ltac_plugin.objs/native/ltac_plugin__Coretactics.cmx
-> required by _build/default/plugins/ltac/ltac_plugin.a
-> required by _build/default/plugins/ltac/ltac_plugin.cmxs
Makefile.common:142: recipe for target '_build/default/plugins/ltac/ltac_plugin.cmxs' failed
make[1]: *** [_build/default/plugins/ltac/ltac_plugin.cmxs] Error 1
make[1]: Leaving directory '/tmp/coq-20220615-4351-svyfdx/coq-8.15.2'
Makefile.make:122: recipe for target 'submake' failed
make: *** [submake] Error 2

@iMichka iMichka added the build failure CI fails while building the software label Jun 15, 2022
@github-actions
Copy link
Contributor

This pull request has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. To keep this pull request open, add a help wanted or in progress label.

@github-actions github-actions bot added the stale No recent activity label Jun 18, 2022
@github-actions github-actions bot closed this Jun 22, 2022
@PythonCoderAS PythonCoderAS deleted the bump-coq-8.15.2 branch July 14, 2022 10:44
@chenrui333
Copy link
Member

#104820

@chenrui333 chenrui333 added the superseded PR was replaced by another PR label Aug 20, 2022
@github-actions github-actions bot added the outdated PR was locked due to age label Sep 20, 2022
@github-actions github-actions bot locked as resolved and limited conversation to collaborators Sep 20, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
build failure CI fails while building the software bump-formula-pr PR was created using `brew bump-formula-pr` ocaml OCaml use is a significant feature of the PR or issue outdated PR was locked due to age stale No recent activity superseded PR was replaced by another PR
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants