search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
347 stars 70 forks source link

Cannot dynlink to the Stm in `vscoqtop` #678

Open LasseBlaauwbroek opened 1 year ago

LasseBlaauwbroek commented 1 year ago

The Tactician plugin depends on the coq-core.stm library. However, it seems that this library is not linked into the vscoqtop executable. As such, Tactician is not functional in VsCode 2.

Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"<opam-root>/lib/coq/user-contrib/Tactician/tactician_ltac1_record_plugin.cmxs: undefined symbol: camlStm\")")

Any chance that the STM can be put in?

gares commented 1 year ago

Nope, the document manager in vscoqtop is, morally, the STM 2.0, so we won't link the stm.

Can you tell me what you actually use of the old STM?

rtetley commented 3 months ago

@gares what should we do here ?

SkySkimmer commented 3 months ago

IIRC tactician uses the stm because they redeclare the tactic syntax classified as sideeffect and then they want to detect when running those commands whether it's the "real" run or if it's being replayed at Qed (a STM behaviour which I'm not sure if non-stm ides do). They do this by looking at the "get_ast" in stm.mli (if it's a Qed then the code is running from being replayed).

LasseBlaauwbroek commented 3 months ago

Yes, that is mostly accurate. Note that Tactician works fine on coq-lsp, even though it doesn't use the STM (but still links to it). Because coq-lsp doesn't have the complex 'replaying at QED' behavior, Tactician's code paths that use the STM are never actually exercised. I'd hope that the same is true for Vscoq.

If so, then just linking to the STM would be enough. When the STM is removed upstream, Tactician can remove the code-paths as well.