Stream: Elpi users & devs

Topic: Elpi does not find database

Enzo Crance (Jun 02 2021 at 13:49):

Hello, it's me again... I have a Database.v file containing elpi database declarations such as

Elpi Db blah.db lp:{{
  % ...
}}.

and a Tactic.v file importing the previous one:

From elpi Require Import elpi.

Elpi Tactic mytactic.

Require Import Database.
Elpi Accumulate Db blah.db.
Elpi Accumulate Db blah2.db.

Elpi Accumulate lp:{{
  solve [] [G] NG :-
    % ...
}}.
Elpi Typecheck.

Ltac mytactic := elpi mytactic.

This file typechecks when I execute it line by line as well as using coqc. Now Test.v imports Tactic.v to have access to the freshly declared tactic.

Require Import Tactic.

Goal (* ... *).
Proof.
  mytactic.

The call to the tactic results in Unknown Db blah.db and I cannot find the cause of the error. I don't want to import Database.v in Test.v because this is supposed to be a file that is private to the tactic, and not accessible to the end user. :thinking:

Enrico Tassi (Jun 02 2021 at 14:13):

Try using Require Export Database in Tactic.v

Enrico Tassi (Jun 02 2021 at 14:13):

Sorry for my brevity, I'm on VAC

Enzo Crance (Jun 02 2021 at 14:19):

Enrico Tassi said:

Try using Require Export Database in Tactic.v

Thanks, that fixed it. :pray:
However it's weird that it needs to be visible to the user, as it is visible to the tactic and Coq did not complain when compiling the tactic.

Enzo Crance (Jun 02 2021 at 14:19):

Enrico Tassi said:

Sorry for my brevity, I'm on VAC

Sorry for all my questions :sweat_smile: Thanks again

Enrico Tassi (Jun 02 2021 at 14:23):

You are right, It may be possible to fix that at the elpi side. Given you minimized it, please open a issue so that I don't forget about it.

Last updated: Oct 13 2024 at 01:02 UTC