Stream: Coq users

Topic: Anomaly: bad vernac extend

spaceloop (Nov 21 2023 at 21:38):

I'm using both the equations and QuickChick library in my project, and while trying to upgrade to coq 8.18, I get the following error when importing either of them after the other:

Dynlink error: execution of module initializers in the shared library failed: "Anomaly: bad vernac extend: Derive, 0"

I suspect that both implement a vernac command "Derive". What should I do?

Paolo Giarrusso (Nov 21 2023 at 22:52):

Whatever the reason, this warrants a bug report. As a workaround, do you need to import both together? You can probably import one in some sections and the other in disjoint sections.

Paolo Giarrusso (Nov 21 2023 at 22:53):

But first try if you can require (not require import) both together; if not, you might need separate files in the same project.

Gaëtan Gilbert (Nov 21 2023 at 23:09):

plugins register their commands at require time so they won't be able to be required together

Gaëtan Gilbert (Nov 21 2023 at 23:12):

stdlib derive is likely to cause the same failure if required with either too

Michael Soegtrop (Nov 22 2023 at 08:35):

I see if I can reproduce it in the 8.18 Coq Platform development branch. If I understood you right this did work in 8.17?

spaceloop (Nov 22 2023 at 08:40):

Michael Soegtrop said:

I see if I can reproduce it in the 8.18 Coq Platform development branch. If I understood you right this did work in 8.17?

No, I was a bit unclear I'm afraid. I used to use older versions of both libraries together with coq 8.13. While moving to 8.18 I had to use newer versions of both equations (coq-equations 1.3+8.18 from opam) and quickchick (master branch from github).

spaceloop (Nov 22 2023 at 08:42):

Paolo Giarrusso said:

But first try if you can require (not require import) both together; if not, you might need separate files in the same project.

The error also occurs when only using Require. I will check now for doing it in separate files.

spaceloop (Nov 22 2023 at 08:50):

Splitting it up in different files gives the same problem, if there is a dependency between the files. Here is a minimal example:

I have A.v

From Equations Require Import Equations.

And B.v

From MyProject Require Import A
From QuickChick Require Import QuickChick

I get

COQDEP VFILES
COQC src/A.v
COQC src/B.v
File "./src/B.v", line 2, characters 0-42:
Error:
Dynlink error: execution of module initializers in the shared library failed: "Anomaly: bad vernac extend: Derive, 0"

Perhaps there is some re-export mechanism in A.v that I can disable? I've also tried not using Import or doing the Requires in sections, but no luck.

Paolo Giarrusso (Nov 22 2023 at 09:24):

Sorry, my suggestion won't work: Require is always transitive.

spaceloop (Nov 22 2023 at 09:29):

Ok, thanks. The only option I see then is to manually patch either of the libraries so that these names don't conflict, which I really dislike. Could there be any alternative?

Pierre-Marie Pédrot (Nov 22 2023 at 09:29):

It's easy to fix this issue from the Coq side by disambiguating the vernac depending on the plugin name, but this will require a minor release.

Pierre-Marie Pédrot (Nov 22 2023 at 09:33):

(we can still do that preventively for the 8.19 release, but if you stick to 8.18 you're out of luck)

Michael Soegtrop (Nov 22 2023 at 09:53):

I could take a patch for 8.18.0 in Coq Platform until 8.18.1 is there.

Pierre-Marie Pédrot (Nov 22 2023 at 10:11):

I've written a PR for 8.19: https://github.com/coq/coq/pull/18345 but it changes the API for cleanliness reasons. I will try to come up with an API-invariant version for 8.18.1

Pierre-Marie Pédrot (Nov 22 2023 at 10:12):

cc @Enrico Tassi as our 8.18 RM

Karl Palmskog (Nov 22 2023 at 10:12):

but for high-profile packages, it seems highly confusing that they provide the same command, even if they can be differentiated somehow.

So I hope both the technical and social "solutions" (changing/differentiating command name) can be implemented

Pierre-Marie Pédrot (Nov 22 2023 at 10:13):

you might not be able to use both commands at the same time due to parsing issues, but for modularity purposes it's critical that plugins shouldn't have to care about what the others are doing if they're going to be required together

Pierre-Marie Pédrot (Nov 22 2023 at 10:14):

the error here is a purely internal problem that just reflects poor design on our side

Michael Soegtrop (Nov 22 2023 at 10:15):

Would it make sense to more have a patch for one or the other package to rename the command in Coq Platform?

Pierre-Marie Pédrot (Nov 22 2023 at 10:16):

indeed it's the most trivial fix one can think of and it will be completely transparent for the end-user

Pierre-Marie Pédrot (Nov 22 2023 at 10:17):

(and since the platform is monolithic there isn't any risk of conflict with other still unknown plugins)

spaceloop (Nov 22 2023 at 10:23):

Thanks for picking this up so quickly! The PR looks like a good general solution.

Karl Palmskog (Nov 22 2023 at 10:27):

@Michael Soegtrop but the question becomes who should change the command. For example, if the command is changed in Equations, this will break a lot of projects

Michael Soegtrop (Nov 22 2023 at 10:30):

I understood @Pierre-Marie Pédrot comment such that these are internal commands not exposed to the user of a package, say one has to change ML code and some Coq wrapper for it, but no user code. Is this not so? I don't have time right now to look into the details ...

Karl Palmskog (Nov 22 2023 at 10:38):

I could take a patch for 8.18.0 in Coq Platform until 8.18.1 is there.

I think we really want to avoid a situation where the opam 8.18.0 differs from the Platform one, right? The patch could go in the general opam archive for coq.8.18.0.

Pierre-Marie Pédrot (Nov 22 2023 at 10:40):

@Karl Palmskog the problem is internal, the name that clashes has no relation whatsoever with what is exposed to the user, it's basically a uid

Pierre-Marie Pédrot (Nov 22 2023 at 10:42):

So it's essentially a one-line patch in the OCaml code of either Equations or QuickChick. The Coq-side fix is more principled and will make this kind of issue (hopefully) inexistent in the future release.

Karl Palmskog (Nov 22 2023 at 10:42):

but doesn't the uid clash due to the commands being called the same thing to the user?

Pierre-Marie Pédrot (Nov 22 2023 at 10:43):

the uid is decided by the plugin, it's what you write after the VERNAC EXTEND macro in the mlg file

Pierre-Marie Pédrot (Nov 22 2023 at 10:44):

e.g. for Equations this diff is enough

diff --git a/src/g_equations.mlg b/src/g_equations.mlg
index 60d8c41c..a45002e1 100644
--- a/src/g_equations.mlg
+++ b/src/g_equations.mlg
@@ -531,7 +531,7 @@ END

 (** Deriving *)

-VERNAC COMMAND EXTEND Derive CLASSIFIED AS SIDEFF STATE program
+VERNAC COMMAND EXTEND EquationsDerive CLASSIFIED AS SIDEFF STATE program
 | #[ poly = polymorphic ] [ "Derive" ne_ident_list(ds) "for" global_list(c) ] -> {
   Ederive.derive ~poly (List.map Id.to_string ds)
     (List.map (fun x -> x.CAst.loc, Smartlocate.global_with_alias x) c)

Pierre-Marie Pédrot (Nov 22 2023 at 10:45):

this doesn't touch the parsing rules, just the internal name of that command

Karl Palmskog (Nov 22 2023 at 10:47):

QuickChick has this:

VERNAC COMMAND EXTEND Derive CLASSIFIED AS SIDEFF
   | ["Derive" constr(class_name) "for" constr(inductive)] ->

So I guess it should be changed to EXTEND QuickChickDerive.

But my point was that what Derive command you get will still be decided by the Import order, no? If you want to do a file that does both Equations Derive commands and QuickChick Derive, there'd need to be a lot of Imports, right?

Pierre-Marie Pédrot (Nov 22 2023 at 10:47):

indeed the Import will decide which command is used if the parsing rules clash

Pierre-Marie Pédrot (Nov 22 2023 at 10:48):

but the problem at hand is a Require issue, which cannot be avoided

Pierre-Marie Pédrot (Nov 22 2023 at 10:49):

Import contorsions is not restricted to plugins defining the same commands, it's a generic issue with <insert any programming language with qualified names here>

Karl Palmskog (Nov 22 2023 at 10:50):

OK, then I guess the "import contorsion" is basically a Platform-only issue once the VERNAC COMMAND stuff is changed. In this case, it can be avoided if projects can agree to play nice together...

Karl Palmskog (Nov 22 2023 at 10:54):

Coq itself has this, should that stay the same? Or included in the possible 8.18.0 patch?

plugins/derive/g_derive.mlg:25:VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof

Pierre-Marie Pédrot (Nov 22 2023 at 11:01):

this should be fixed (or we rename both QC and Equations entries, this also works)

Michael Soegtrop (Nov 22 2023 at 12:38):

Can't the "which name is used" issue be solved just be doing another Import of the module one wants on top?

Gaëtan Gilbert (Nov 22 2023 at 12:41):

it's Require time not Import
and redoing Require does nothing

Gaëtan Gilbert (Nov 22 2023 at 12:41):

see also https://github.com/coq/coq/issues/17064

Michael Soegtrop (Nov 22 2023 at 12:47):

Can we vote on the preferred solution? Please use "upvote" for "patch names in packages" and "downvote" for "patch coq". @Karl Palmskog : during testing I keep it in Coq Platform, but one of the last release steps is to push opam patches upstream.

Gaëtan Gilbert (Nov 22 2023 at 12:49):

I guess you mean the solution for the 8.18 platform, we're patching coq master regardless

Michael Soegtrop (Nov 22 2023 at 12:52):

@Gaëtan Gilbert : yes, I am talking about the 2023.11 Coq Platform release for 8.18.

Last updated: Oct 13 2024 at 01:02 UTC