Stream: Coq devs & plugin devs

Topic: ✔ Making plugin by modifying official template


view this post on Zulip Julin Shaji (Jan 10 2024 at 04:28):

Thanks!
That made it work.

view this post on Zulip Notification Bot (Jan 10 2024 at 04:28):

Julin Shaji has marked this topic as resolved.

view this post on Zulip Julin Shaji (Jan 10 2024 at 05:23):

The loader file at https://github.com/coq-community/coq-plugin-template/blob/v8.16/theories/MyPlugin.v
Still uses that legacy syntax (hadn't even known before that there was such a syntax).

Should that be changed?

view this post on Zulip Julin Shaji (Jan 10 2024 at 07:05):

And how could a _CoqProject to use the plugin look like? For the plugin-template.

view this post on Zulip Julin Shaji (Jan 10 2024 at 07:06):

Julin Shaji said:

Thanks!
That made it work.

I'm still confused as to which name should appear where. The relation between name in dune-project or opam file or dune file, etc.

Tried to recreate the template with a different name, couldn't make it work. So sticking to template coq-my-plugin now.

view this post on Zulip Julin Shaji (Mar 16 2024 at 12:09):

If I use the legacy loading way, I can Import the plugin interactively from editor.
But if I change the Declare ML Module to remove the prefix associated with legacy loading, I can't use it from editor.

I guess it's due to something that needs to changed in the _CoqProject file?


Last updated: Oct 13 2024 at 01:02 UTC