Installation Issues

[wangfuco]

Hi! I'm trying to install coq-ext-check which depends on this. I use opam 2.0.1, Coq 8.5.3 and ocaml 4.05.0. This package always fails to install with the following message.

install: cannot change permissions of ‘/home/wangfuco/.opam/ocaml-base-compiler.4.05.0/lib/coq/user-contrib/PluginUtils’: No such file or directory

install: cannot create regular file '/home/wangfuco/.opam/ocaml-base-compiler.4.05.0/lib/coq/user-contrib/PluginUtils/plugin_utils.cmxs': No such file or directory

Makefile.coq:322: recipe for target 'install-natdynlink' failed

make[1]: *** [install-natdynlink] Error 1

make[1]: Leaving directory '/home/wangfuco/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-plugin-utils.1.2.0'

Makefile:12: recipe for target 'install' failed

make: *** [install] Error 2

Could you provide some tips or comments on what might be the issue? Thanks so much!

[gmalecha]

Hmmm. And the installation of this completed successfully? Where did it get installed?

[wangfuco]

No, it didn't. After this error, opam terminated the installation. I didn't change the directory, so it should be at the default location. Would this be the issue?

[gmalecha]

Can you include a pointer to coq-ext-check? I can try to reproduce the problem.

On another note though, Coq 8.5 is pretty old at this point. May I ask what your motivation for using it is?

[wangfuco]

Sorry, I'm new to opam, so how do I generate a pointer to it? I did run opam config report and it gives the following.

opam config report
# opam config report
# opam-version      2.0.2 
# self-upgrade      no
# system            arch=x86_64 os=linux os-distribution=ubuntu os-version=16.04
# solver            builtin-mccs+glpk
# install-criteria  -removed,-count[version-lag,request],-count[version-lag,changed],-changed
# upgrade-criteria  -removed,-count[version-lag,solution],-new
# jobs              3
# repositories      2 (http) (default repo at 34f81c06)
# pinned            1 (version)
# current-switch    ocaml-base-compiler.4.05.0

I use Coq 8.5 because I'm trying to compile and utilize the VeriDrone library which builds on Coq 8.5 and coq-smt-check.

[wangfuco]

Actually, since my opam installed list is still relatively short, I can start from scratch. If you succeed in installing '''coq-plugin-utils''', could you please share your opam installed list so that I could look into it? Thank you so much!