You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
AFAICT this was never actually supported and <dbname>|<qname> is always interpreted as an elpi program name in this command:
From elpi RequireImport elpi.
Elpi Db test1 lp:{{ }}.
Elpi Db test2 lp:{{ }}.
Elpi Accumulate test1 Db test2. (* No Elpi Program named test1 *)
I've tried fixing this myself but the fact that all of this goes through mlg files breaks my OCaml backtraces and I cannot figure out the chain from the grammar rules to Interp.accumulate which seems to be responsible for the error message. I tried fixing that function directly but adding support for accumulating a db requires more arguments that I don't know how to get.
Activity
gares commentedon Sep 22, 2025
https://rocq-prover.zulipchat.com/#narrow/channel/253928-Elpi-users-.26-devs/topic/Calling.20.60derive.60.20from.20other.20elpi.20commands/with/540811369