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

Cheri Coq dependecy issues #736

Closed
dc-mak opened this issue Dec 4, 2024 · 2 comments · Fixed by #737
Closed

Cheri Coq dependecy issues #736

dc-mak opened this issue Dec 4, 2024 · 2 comments · Fixed by #737
Assignees
Labels
CI Related to CI infrastructure

Comments

@dc-mak
Copy link
Contributor

dc-mak commented Dec 4, 2024

from https://github.com/rems-project/cerberus/actions/runs/12141123884/job/33852477899#step:5:191

 Error:  Package conflict!
  * No agreement on the version of coq:
    - cerberus-cheri → coq-bbv < 1.5 → coq < 8.14~
    - cerberus-cheri → coq-cheri-capabilities → coq = 8.19.0
  * No agreement on the version of ocaml:
    - (invariant) → ocaml-base-compiler = 4.14.1 → ocaml = 4.14.1
    - cerberus-cheri → coq-bbv < 1.5 → coq < 8.11~ → ocaml < 4.02.0
No solution found, exiting
    You can temporarily relax the switch invariant with `--update-invariant'
@dc-mak dc-mak added the CI Related to CI infrastructure label Dec 4, 2024
@ZippeyKeys12
Copy link
Collaborator

If you make coq-bbv >= "1.5", it becomes:

#=== ERROR while compiling cerberus-cheri.~dev ================================#
# context              2.1.2 | linux/x86_64 | ocaml-base-compiler.4.14.1 | pinned(git+file:///home/runner/work/cerberus/cerberus#HEAD#e04776a3)
# path                 ~/.opam/with_coq/.opam-switch/build/cerberus-cheri.~dev
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p cerberus-cheri --profile=release -j 3 @install
# exit-code            1
# env-file             ~/.opam/log/cerberus-cheri-2055-992432.env
# output-file          ~/.opam/log/cerberus-cheri-2055-992432.out
### output ###
# [...]
# (cd _build/default/coq/Morello && /home/runner/.opam/with_coq/bin/coqdep -boot -I /home/runner/.opam/with_coq/lib/coq/../coq-core/plugins/btauto -I /home/runner/.opam/with_coq/lib/coq/../coq-core/plugins/cc -I /home/runner/.opam/with_coq/lib/coq/../coq-core/plugins/derive -I /home/runner/.opam/with_coq/lib/coq/../coq-core/plugins/extraction -I /home/runner/.opam/with_coq/lib/coq/../coq-core/p[...]
# Warning: in file MorelloCapsGS.v, library
#          Coq.ZArith.Zdigits is required and has not been found in the loadpath!
#          [module-not-found,filesystem,default]
# (cd _build/default && /home/runner/.opam/with_coq/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /home/runner/.opam/with_coq/lib/coq/../coq-core/plugins/btauto -I /home/runner/.opam/with_coq/lib/coq/../coq-core/plugins/cc -I /home/runner/.opam/with_coq/lib/coq/../coq-core/plugins/derive -I /home/runner/.opam/with_coq/lib/coq/.[...]
# File "./coq/Common/Utils.v", line 7, characters 0-[34](https://github.com/rems-project/cerberus/actions/runs/12153602944/job/33893044811?pr=735#step:5:35):
# Error: Cannot find a physical path bound to logical path Coq.ZArith.Zdigits.
# 
# (cd _build/default && /home/runner/.opam/with_coq/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /home/runner/.opam/with_coq/lib/coq/../coq-core/plugins/btauto -I /home/runner/.opam/with_coq/lib/coq/../coq-core/plugins/cc -I /home/runner/.opam/with_coq/lib/coq/../coq-core/plugins/derive -I /home/runner/.opam/with_coq/lib/coq/.[...]
# File "./coq/Morello/MorelloCapsGS.v", line 6, characters 0-34:
# Error: Cannot find a physical path bound to logical path Coq.ZArith.Zdigits.
# 



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build cerberus-cheri ~dev
└─ 
┌─ The following changes have been performed
│ ∗ install cerberus-lib ~dev
└─

from https://github.com/rems-project/cerberus/actions/runs/12153602944/job/33893044811?pr=735#step:5:33

@vzaliva
Copy link
Member

vzaliva commented Dec 4, 2024

Initial analysis shows that it is due to a change in the coq-cheri-capabilities package. Before, there was no coq version restriction. I am considering how to fix it. Last working commit for coq-cheri-capabilities was 2f02c44ad061d4da30136dc9dbc06c142c94fdaf. Because it is not released via OPAM we depend on the latest version. Perhaps we should make it depend on the last known commit?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CI Related to CI infrastructure
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants