Stream: Coq users

Topic: Adding a new command to extraction


view this post on Zulip Julin Shaji (Jan 04 2024 at 05:24):

Extraction is currently implemented as a plugin, right?

Is it possible to make slight modifications to an existing plugin?

I was wondering if it is possible to add a new sub-command for the Extraction vernacular.

view this post on Zulip Julin Shaji (Jan 04 2024 at 06:38):

Is it possible to use the .ml files of a plugin from another plugin?

view this post on Zulip Paolo Giarrusso (Jan 07 2024 at 18:36):

Depending on plugins is possible — I haven't done i myself, but they can be used as ocaml(find) libraries with dune

view this post on Zulip Notification Bot (Jan 08 2024 at 09:36):

Julin Shaji has marked this topic as unresolved.

view this post on Zulip Julin Shaji (Jan 08 2024 at 09:37):

Is it possible to add a subcommand to an already existing command made with a plugin?

Saw ways to make totally new commands, but is it possible to augment/modify pre-existing vernacular commands?

view this post on Zulip Matthieu Sozeau (Feb 20 2024 at 17:26):

That’s probably more complex as you have to dive in the grammar extension code. Maybe @Pierre-Marie Pédrot can help here

view this post on Zulip Mario Frank (Feb 23 2024 at 14:31):

Hi, yes, it is possible to extend the commands and I did that myself (see here). But you do have to consider multiple aspects, including CoqIDE syntax highlighting. If you have questions, I can try to help.

view this post on Zulip Mario Frank (Feb 23 2024 at 14:50):

Julin Shaji said:

Is it possible to add a subcommand to an already existing command made with a plugin?

Saw ways to make totally new commands, but is it possible to augment/modify pre-existing vernacular commands?

You have to add the new subcommand in the mlg file, see here.
Then, you also have to patch the CoqIDE specific files (see here and here

view this post on Zulip Mario Frank (Feb 23 2024 at 14:52):

And you should update the grammars with "make doc_gram_rsts" and also extend the documentation (see here)

view this post on Zulip Mario Frank (Feb 23 2024 at 14:59):

Julin Shaji said:

Is it possible to use the .ml files of a plugin from another plugin?

Concerning this point, this is more complicated. In a plugin you only have access to libraries defined in the dune file of the plugin (see here for the extraction plugin). The stanza libraries contains the available ones. So you have to find the public name of the plugin you want to reuse. But depending on another plugin should be done with care. I cannot estimate whether this can lead to problems and I am not sure whether this is good style.

view this post on Zulip Julin Shaji (Feb 23 2024 at 16:00):

I was trying to add extra commands to the Extraction plugin. Just for my use.
Am trying to modify Haskell extraction process. Since haskell is already there, I was hoping to piggy-back on the .ml files of extraction plugin.
But many of the functions that I need are not there in the .mli files.
I guess in such a situation, it simply can't be used, right?

view this post on Zulip Mario Frank (Feb 23 2024 at 16:05):

If I understand correctly, the functions you need are located in some other plugins ml file, but not in exported via the mli file, right?

view this post on Zulip Mario Frank (Feb 23 2024 at 16:11):

If all functionality you need is located in the extraction plugin (in the ml files) but not exported via the mli files, you could just extend the mli files.

view this post on Zulip Julin Shaji (Feb 23 2024 at 16:51):

Mario Frank said:

If all functionality you need is located in the extraction plugin (in the ml files) but not exported via the mli files, you could just extend the mli files.

Does that mean having a copy of the extraction plugin?
I mean, the .mli file is already there as part of coq. Extending .mli files mean modifying them, right?

view this post on Zulip Mario Frank (Feb 24 2024 at 20:23):

Yes, I mean modifying the mli file. I do not know which function you need. But if you, for example, want to reuse the function se_iter (that one) from the modutil.ml in the extraction plugin, this will currently not be possible as there is no definition val se_iter : A -> B -> C -> ResultType in the modutil.mli. The types A, B and C are dummies here - I didn't look up the types. However, if you add that "val" declaration, you get access.

But I have the feeling we might be talking about different things since you first asked about accessing other plugins. So I try to wrap up
a) you want to extend the extraction plugin with new Vernac commands and
b) need some functions that are implemented in a ml file in the extraction plugin but
c) not defined in the respective mli file.
Is that right?

view this post on Zulip Julin Shaji (Feb 25 2024 at 07:47):

I was trying to extend the extraction for haskell by adding a few more functionalities.
It looked as if modifying extraction for haskell itself is not
possible, so I set out to make a copy of haskell extraction with
another language name.
I figured it would be better to make it as a separate plugin.
Then I wanted to know if it is possible to depend on the ml files of
the extraction plugin of coq itself.
Saw that it was possible as long as the functions that I needed are
mentioned in the .mli files.
But some of the functions in table.ml and extract_env.ml that I needed to
use are not exposed via the .mli files.
I am at this point at the moment.

In this situation, does modifying the .mli files still a good way?

view this post on Zulip Mario Frank (Feb 26 2024 at 07:38):

There is sadly no general answer to your questions: If the functionality you want to implement is really incompatible with the way the extraction plugin works, it may be a good approach to do that in another plugin. Making a function from extraction plugin public by adding its declaration to the mli is then one of two possible solutions. The other is just copying the function to your plugin but this may involve copying also other functions. One aspect you must take care of and that is really vital. If the function you want to reuse from extraction has side effects (i.e. sets/modifies some module-global variables in the table.ml, for example), using it may alter the behavior of the extraction plugin in a way that you did not anticipate. Thus, without knowing what exactly you want to accomplish, I cannot estimate what side effects may occur. If you cannot tell more details, you should at least be really cautious what the reused functions do.


Last updated: Jun 13 2024 at 21:01 UTC