search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
143 stars 31 forks source link

[fleche] New `InjectRequire` plugin API #679

Closed ejgallego closed 4 months ago

ejgallego commented 4 months ago

This way plugins can specify a list of extra imports for each file.

This may compose poorly, so note that in the documentation.

Alizter commented 4 months ago

Are these Coq plugins or coq-lsp plugins? I'm guessing the use-case is for the visualizer extensions to easily import the parts they need when working on a file?

ejgallego commented 4 months ago

This is a Fleche plugin, so they work both for coq-lsp, jsCoq, fcc.

The use case here is more for running baselines so far, we have a plugin that will replace all proofs by some concrete text, but sometimes we need to inject some extra requires, for example in order to support Tactician, or From Hammer Require Import Hammer

This API is far from final form tho.