Janno (Mar 11 2024 at 09:53): Janno (Mar 11 2024 at 09:53):We are having issues with Dbs not being available in clients of our custom elpi commands. We already had to fix a few of these cases and it seemed odd but not too bad. But now that we can build more of our code base these errors pop up everywhere. I've tried reproducing the exact import/export structure but I cannot reproduce the failure itself. My test cases work just fine. We are wondering if there were any recent changes in elpi that could be responsible for something like this? Or does anybody know changes to Coq that could lead to a difference in behavior compared to 8.18?
Enrico Tassi (Mar 11 2024 at 09:56):Dbs at synterp or interp time?
Enrico Tassi (Mar 11 2024 at 09:57):I think the two libobjects should share the same scope, so there should be no difference.
Rodolphe Lepigre (Mar 11 2024 at 09:57):We generally accumulate Dbs at both phases.
Enrico Tassi (Mar 11 2024 at 09:57):But now we have DB at synterp time, so maybe that is the difference
Enrico Tassi (Mar 11 2024 at 09:57):Hum, what do you mean then by visibility?
Enrico Tassi (Mar 11 2024 at 09:58):I thought you got errors like "db foo.db does not exist".
Enrico Tassi (Mar 11 2024 at 09:58):you mean, some clauses are gone?
Rodolphe Lepigre (Mar 11 2024 at 09:59):For example, we get: Error: Unknown Db NES.db.
Rodolphe Lepigre (Mar 11 2024 at 10:00):That's in a file that has some of our custom commands in scope (that itself accumulates the db for both phases).
Janno (Mar 11 2024 at 10:10):There were also cases where predicates were not populated with clauses. We also fixed them by adding imports/exports.
Enrico Tassi (Mar 11 2024 at 10:10):Hum, something is fishy. The error message is a bit misleading, it means that the Db is empty.
Enrico Tassi (Mar 11 2024 at 10:12):it probably signals a real problem, but should be more clear in its wording.
IMO it means you did not import the file in which the Db was created.
Enrico Tassi (Mar 11 2024 at 10:14):In any case I don't see a relevant change in the code of Coq-Elpi
Janno (Mar 11 2024 at 10:14):Are transitive imports enough to tell elpi about Dbs?
Enrico Tassi (Mar 11 2024 at 10:14):Hum, what is a transitive import ;-)
Enrico Tassi (Mar 11 2024 at 10:15):I don't think "Import" is transitive, but I'm always get confused between Import and Export.
Enrico Tassi (Mar 11 2024 at 10:15):One of the two is kind of... but in general Require is transitive, Import is not.
Enrico Tassi (Mar 11 2024 at 10:17):Export is a way to avoid repeating a bunch of import, see for example https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/all_ssreflect.v where we provide a all_ssreflect so that Require Import all_ssreflect does what you want (recursively import all the files listed there).
Is this what you call recursive import?
Janno (Mar 11 2024 at 10:18):Oh yeah, I should have asked "Is transitive Require enough?"
Enrico Tassi (Mar 11 2024 at 10:18):nope, sorry.
Enrico Tassi (Mar 11 2024 at 10:19):It's a mess, but not elpi specific ;-)
Janno (Mar 11 2024 at 10:19):So why did this work in 8.18?
Enrico Tassi (Mar 11 2024 at 10:19):You can make things transitive by declaring libobjects "superglobal"
Enrico Tassi (Mar 11 2024 at 10:20):but I don't see in_db be declared as such in coq-elpi 1.19.3
Enrico Tassi (Mar 11 2024 at 10:20):(sorry, gotta go)
Rodolphe Lepigre (Mar 11 2024 at 10:20):OK, thanks, we're gonna debug this a bit further and keep you posted.
Janno (Mar 11 2024 at 11:04):We found the problem. Databases created in a single stage/phase are declared (P.declare_db) globally so that they exist in some rudimentary form and cannot be created again in the other stage. But, critically, they are not initialized (P.init_db). It's the initialization step that actually registers the Db in the db_name_src summary (where its absence triggers the Unknown Db error). That only happens for the selected stage(s)/phase(s).
Janno (Mar 11 2024 at 11:06):This makes it possible to write #[synterp] Elpi Db bla {{ <some synterp code> }} and #[interp] Elpi Accumulate bla {{ <some interp code >}} in a single file without actually properly creating the Db in the interp stage.
Janno (Mar 11 2024 at 11:07):BTW: init_db is super global and that's why everything work fine in 8.18 and will continue working in 8.19 with very simple changes.
Janno (Mar 11 2024 at 11:07):One very easy fix is to take the phase separation to its logical conclusion and allow DBs to exist independently. We haven't fully tested this but this diff here fixes the test case (which we finally managed to create):
@@ -455,10 +455,11 @@ let run_in_program ?(program = current_program ()) ?(st_setup=fun x -> x) (loc,
| None -> same_phase Interp P.stage
| Some phase -> same_phase phase P.stage in
let elpi = P.ensure_initialized () in
- P.declare_db n;
- if do_init then
+ if do_init then begin
+ P.declare_db n;
let unit = P.unit_from_string ~elpi loc s in
- P.init_db n unit
+ P.init_db n unit
+ end
An alternative would be to always call init_db but use an empty unit for the stage that isn't active (if one exists).
Janno (Mar 11 2024 at 11:14):I have to admit though that the asymmetry of #[synterp] Elpi Db bla followed by #[interp] Elpi Accumulate bla seems odd to me and actually gave me pause a while ago when we first wrote code like that. Since it seemed to work fine locally and through (Export)*(Import)? chains, I guess, we thought it wasn't to blame for the import/export changes we had to add.
Janno (Mar 11 2024 at 11:14):To me keeping the stages entirely separate looks preferable and restores symmetry
Enrico Tassi (Mar 11 2024 at 12:02):I think I did not realize that there was the asymmetry, please submit a fix. After all the code is functorialized on the stage, as in OCaml's functors, exactly to make the two phases identical...
Janno (Mar 11 2024 at 12:37):Just to clarify: The phases are actually identical and #[interp] Elpi Db bla followed by #[synterp] Elpi Accumulate bla has the same problem. I suppose the asymmetry is between #[phase="both"] Elpi Db bla, which works fine, and #[synterp/interp] Elpi Db bla. #[interp/synterp] Elpi Db bla, in which the second Elpi Db will fail because the first one isn't fully contained to its chosen stage.
Rodolphe Lepigre (Mar 11 2024 at 13:02):Submitted the fix here.
Enrico Tassi (Mar 11 2024 at 14:00):Thanks!
Last updated: Oct 13 2024 at 01:02 UTC