Cyril Cohen (Feb 18 2022 at 10:45): Cyril Cohen (Feb 18 2022 at 10:45):Hi, what is the make -f Makefile.dune target (or with dune directly?) to build coqtop?
(and then, where is it located so that I can inform vscode?)
Gaëtan Gilbert (Feb 18 2022 at 11:57):I don't think there's a Makefile.dune target to build just coqtop
states will build coqtop and the prelude, coqtop can then be called as _build/default/dev/shim/coqtop-prelude
doesn't vscode want coqidetop though?
Paolo Giarrusso (Feb 18 2022 at 12:02):the gui asks for both, but I'm not sure why — coqidetop is the actually used one
Gaëtan Gilbert (Feb 18 2022 at 12:08):for coqidetop dune build coqide-server.install should work and put it in _build/install/default/bin/
you may need to also run dune build or dune build coq-stdlib.install long enough to get the prelude and whatever files you Require in _build/install
Cyril Cohen (Feb 18 2022 at 12:30):Thanks
Notification Bot (Feb 18 2022 at 12:30):Cyril Cohen has marked this topic as resolved.
Théo Zimmermann (Feb 18 2022 at 13:11):Paolo Giarrusso said:
the gui asks for both, but I'm not sure why —
coqidetopis the actually used one
It might need it just to run coqtop --version.
Last updated: Apr 16 2024 at 08:02 UTC