Error: No signature declaration for `open-ns`

[Janno]

I don't even know how to describe what is happening here. It seems certain combinations of importing, re-exporting, and/or using NES eventually trigger this error message:

File "./coq-elpi/apps/NES/tests/nes_signature_bug/print.v", line 3, characters 0-14:
Error:
No signature declaration for open-ns. Did you forget to accumulate a file?

This requires a number of files with 1-2 imports/exports each. To make the problem easier to reproduce, I have made a branch (with just 1 commit) that adds the reproducing example as a (failing )test case to the NES app:
https://github.com/Janno/coq-elpi/tree/janno/open-ns-signature-bug

I am using 646dda5 (master from yesterday) and LPCIC/elpi@141b6fe (tag v3.1.0)

[gares]

Are the MUST and MUST-NOT signalling that, in order to reproduce the bug, one has to follow these instructions.
Or the comments are saying that you need Export here and there because of other reasons (so I can't tweak them to make the bug disappear)?

[Janno]

Are the MUST and MUST-NOT signalling that, in order to reproduce the bug, one has to follow these instructions.

The comments are merely for the bug itself and not related to the original code. The test case is already somewhat removed from the original (which has many more modules). Though I think I have only weakened Exports to Imports during the minimization.. but I am not 100% sure.

Or the comments are saying that you need Export here and there because of other reasons (so I can't tweak them to make the bug disappear)?

Making the bug disappear is very easy because almost all tweaks to the reproducing example change the outcome. I can only hope that the bug is an actual bug in coq-elpi, elpi, or rocq itself. Otherwise, if we are actually mis-using modules somehow, I have to go tweaking imports and exports in the original code and that is generally harder than fixing bugs upstream.

[gares]

I just gave it a quick try, my feeling is that somewhere you expect the database to include the type of ns-open even if you did not import NES.v (or export does it for you).

The declaration of a DB is (super)global, all you put in there is always there, while accumulate directives honor locality.
This patch should kind of explain that.
I'll look better into this issue next week.

diff --git a/apps/NES/theories/NES.v b/apps/NES/theories/NES.v
index ecb0cced..f286725c 100644
--- a/apps/NES/theories/NES.v
+++ b/apps/NES/theories/NES.v
@@ -9,17 +9,13 @@ typeabbrev path (list string).
 
 :index (2)
 pred ns o:list string, o:modpath.
-
-}}.
-
-#[synterp] Elpi Accumulate NES.db lp:{{
-
 pred open-ns o:string, o:list string.
 :name "open-ns:begin"
 open-ns _ _ :- fail.
 
 }}.
 
+
 Elpi Command NES.Status.
 #[synterp] Elpi Accumulate Db NES.db.
 #[synterp] Elpi Accumulate File nes_synterp.
diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi

PS: I don't think the signature being available at interp time too is the issue, but I did not try.

[Janno]

Oh, I see. I had missed this in all the minimization work. There does not seem to be a (Export->)*Import chain from NES.v to the final print.v file.

I'll see where we got it wrong and if that fixes the problem. I should note, though, that the exact same code works just fine on a commit from March this year (5cd165a) that we've been using so far.

EDIT: I should have checked my code before writing a reply. I do actually import NES in print.v. So the problem must be with an earlier file somehow? I am now more confused than before..

[gares]

This this is your fix, IMO:

diff --git a/apps/NES/tests/nes_signature_bug/print.v b/apps/NES/tests/nes_signature_bug/print.v
index 98e7d67f..ab1da7f8 100644
--- a/apps/NES/tests/nes_signature_bug/print.v
+++ b/apps/NES/tests/nes_signature_bug/print.v
@@ -1,3 +1,3 @@
-Require Export elpi.apps.NES.tests.nes_signature_bug.uniproc.
 From elpi.apps Require Import NES.
+Require Export elpi.apps.NES.tests.nes_signature_bug.uniproc.
 NES.Begin bla.

[gares]

The order of imports is important, in your test case (that I'm happy to add to the test suite) what happens is that:

• transitively the super global object "elpi databases" from NES.vo is loaded, so the DB exists and contains its header
• then rules for uniproc.v are added
• then you import NES loading more signatures to the same db

But the rules from uniproc need the signature from NES added at step 3.

Does this make sense?

[gares]

I think Elpi became more strict about the order in which things are assembled.
But this confusion is really inherited from Import/Export...

IMO the right fix is my first patch (or the equivalent one with #[superglobal] to Accumulate).
You want that the signature of open-ns is always in the DB.