Cannot check the coq proof after build the whole project

[chan-bing]

Hello,
I recently followed these steps to set up and build Velus:

$ cd $VELUS_DIR
$ mkdir opam
$ opam init --root=opam --compiler=4.13.1
$ eval `opam config env --root=$VELUS_DIR/opam`
$ opam install -j4 ocamlbuild coq.8.16.1 menhir.20230608 ocamlgraph
$ cd $VELUS
$ ./configure aarch64-macos
$ make

However, after completing the build, I am unable to check Coq proofs in VSCode, as I keep encountering the error:
"coqtop is not running."
But coqtop can run normally in other projects. I would really appreciate any guidance on resolving this issue.

[RatCornu]

Hello! Did you try to create a new opam switch then setup vscoq-legacy to use it? Maybe the issue come from the fact that you're using an other version of coq in your other projects