The coq-sail from rems-project

coq-sail's People

Contributors

Stargazers

Watchers

coq-sail's Issues

coq-8.18 support

Compilaiton fails with Coq-8.18. I tried to compile making a development version of coq-bbv package as follows:

opam pin -n coq-bbv https://github.com/vzaliva/bbv.git
opam install coq-bbv

After that, I tried to install coq-sail:

opam pin -n coq-sail https://github.com/rems-project/coq-sail.git
opam install coq-sail

And go the following error:

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of coq-sail.0.16 failed at "make -C src HAVE_OPAM_BBV=yes".

#=== ERROR while compiling coq-sail.0.16 ======================================#
# context     2.1.5 | linux/x86_64 | ocaml-base-compiler.4.14.1 | pinned(git+https://github.com/rems-project/coq-sail.git#c79d1a7c11c38096e57d08cbbf7f441eee8f46d6)
# path        /local/scratch/vz231/.opam/cerberus-new-coq/.opam-switch/build/coq-sail.0.16
# command     /local/scratch/vz231/.opam/opam-init/hooks/sandbox.sh build make -C src HAVE_OPAM_BBV=yes
# exit-code   2
# env-file    /local/scratch/vz231/.opam/log/coq-sail-3374397-f98d79.env
# output-file /local/scratch/vz231/.opam/log/coq-sail-3374397-f98d79.out
### output ###
# [...]
# coqc -Q . "Sail" Prompt_monad.v
# coqc -Q . "Sail" Prompt.v
# File "./Prompt.v", line 168, characters 0-14:
# Error: Cannot infer an instance of type "bool" for the variable r in
# environment:
# P, Q, R : bool -> Prop
# p : P false
# H : forall l r : bool,
#     ArithFactP (P l -> (l = true -> Q r) -> R (l && r)%bool)
# 
# make: *** [Makefile:28: Prompt.vo] Error 1
# make: Leaving directory '/local/scratch/vz231/.opam/cerberus-new-coq/.opam-switch/build/coq-sail.0.16/src'

Couldn't build stdpp variant with latest `stdpp`

Since stdpp 1.10.0, bitvector support has been moved to a new package stdpp.bitvector.
See https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/542

Opam dependencies and module names need to be fixed.

Recommend Projects