Elpi Db mydb lp:{{ <code> }} not the same as Elpi Db mydb lp:{{ }}. Elpi Accumulate mydb lp:{{ <code> }}

[Janno]

(This came up again this week in https://coq.zulipchat.com/#narrow/channel/253928-Elpi-users-.26-devs/topic/Elpi.202.2E0.20.28beta.20testers.29/near/484771703 and also featured (less prominently) in https://coq.zulipchat.com/#narrow/channel/253928-Elpi-users-.26-devs/topic/Unknown.20Db.20in.20clients.20of.20elpi.20command.20in.208.2E19 at the beginning of the year.)

It seems counter-intuitive that the following two snippets do not have the same effect in clients that Require (but do not Import) the file.

Elpi Db mydb lp:{{ <code> }}.

versus

Elpi Db mydb lp::{{  }}.
Elpi Accumulate mydb lp:{{ <code > }}.

The former will make <code> available to all clients that can see or otherwise interact with mydb but the latter only does so for clients that actually Import the effect.

The correct incantation seems to be

Elpi Db mydb lp::{{  }}.
#[superglobal] Elpi Accumulate mydb lp:{{ <code > }}.

While this works, it is also somewhat surprising because I would expect #[global] to play the role of #[superglobal] here. But maybe that could easily be changed. Or maybe there is a good reason for not using #[global]?

In any case, I wonder if it might be more consistent to separate the effect of having created the database from the effect of putting code into it and allowing/requiring #[superglobal] (or just #[global]) on both Elpi Db and Elpi Accumulate to make the effect of putting the code into the database truly global. The creation of the database should likely always be global. Of course, there is a danger of this being differently confusing when people expect the omission of #[global] on Elpi Db to also affect the effect of creating the database.

[gares]

About global/superglobal, I always forget it, but IIRC with superglobal you obtain that if the db exists, then the extra code is also there, even if you don't require the file defining the db directly. Global would work if you require it, but not if it is required transitively.

[SkySkimmer]

I doubt that, libobject does not tell you if a load is from a transitive or direct Require.

[gares]

This is what we wrote recently, but I can't understand it no more

    let load i ((_,kn),s as o) =
      if Int.equal i 1 ||
        (s.scope = Coq_elpi_utils.Global && is_inside_current_library kn) ||
        s.scope = Coq_elpi_utils.SuperGlobal then cache o in

[gares]

So I think we made "global" only apply to the current library

[SkySkimmer]

There is also the open function.
We made it so that Global gets hoisted to the toplevel of the current library then becomes export. ie

Module M.
Module N.
Global foo.
End N.
End M.

should be equivalent to

Module M.
Module N.
Local foo.
End N.
Local foo.
End M.
#[export] foo.

[gares]

thanks, this explain why global is not enough for @Janno
but maybe we got it wrong, since when foo is generated, elpi.accumulate takes both a locality and a scope. IIRC this is what we need for the scope library, but it should be orthogonal to the locality once it has been hoisted.

[Janno]

We made it so that Global gets hoisted to the toplevel of the current library then becomes export. ie

I do not understand your two equivalent examples at all. It seems intuitively wrong to me. Could you make it more concrete with Hint Resolve or some other effect that supports local/export/global?

[SkySkimmer]

The example works when foo is a command which uses the elpi interpretation of global, so Hint Resolve doesn't work.

[Janno]

Oh, now I understand. What is the reason for that behavior? Why does it make sense to deviate from the usual interpretation of these locality annotations?

[gares]

Note that modules M and N are generated in elpi, and once both are still ongoing, one does an elpi.accumulate-clauses with scope library. The idea was to make the clauses available on Import of the file, not the sub modules.
If the code behaves like @SkySkimmer says even if the @global! => option was used, then I believe it is a bug since after the hoist the hint should #[global] and not `#[export].

If the scope is not library nor exec (equivalent in the example above), and @global! is used, then the hint should just live in the inner module and the visibility semantics should match the #[global] one of Coq (whatever that is).