search

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
211 stars 31 forks source link

Dune tests error: permission denied #93

Closed lukaszcz closed 3 years ago

lukaszcz commented 3 years ago

I run "dune runtest" (after installing CoqHammer with "dune install") and get:

    coqc alias tests/plugin/runtest (exit 1)

(cd _build/default/tests/plugin && /Users/rkw886/.opam/default/bin/coqc plugin_test.v) CoqHammer (dev) for Coq 8.12 Found 9907 accessible Coq objects. (...) Error: System error: "./plugin_test.vos: Permission denied"

    coqc alias tests/tactics/runtest (exit 1)

(cd _build/default/tests/tactics && /Users/rkw886/.opam/default/bin/coqc tactics_test.v) Error: System error: "./tactics_test.vos: Permission denied"

palmskog commented 3 years ago

@lukaszcz Dune is very particular about there not being any "compiled" files in the source tree, such as .vo and .vos. In this case, make clean is seemingly not doing its job to remove all compiled files (it omits *.vos in the tests directory). I will do a pull request to fix this later today.