Accumulating into programs across several Coq files isn't idempotent

[swasey]

It looks to me like accumulating files is meant to be idempotent. I give an example where it is not, using Extra Dependency and accumulating into an Elpi program twice from separate Coq files. (The example uses a type abbreviation and draws the Elpi typecheck error "duplicate type abbreviation".)

There are several files:

• progam.v provides a trivial Elpi program (think derive)
• library.elpi provides some code we'll accumulate twice into the program
• accumulate{1,2}.v each import program, accumulate the library into it, and typecheck the program
• test_accumulate_twice.v requires accumulate{1,2}.v and cannot typecheck the program
• dune sets up context (if you use dune, you'll also need a dune-project file)

The files follow inline. (In case it's simpler, here's a tarball: accumulate_bug.tgz.)

(I believe there are work arounds through either accumulating databases or never duplicating effects as done in this example.)

program.v

Require Import elpi.elpi.

Elpi Command program.
Elpi Accumulate lp:{{ main _ :- coq.say "program". }}.
Elpi Typecheck program.
Elpi Export program.

library.elpi

namespace coq {
	kind tm type -> type.
}
namespace cpp {
	typeabbrev bs (coq.tm int).
}

accumulate1.v

From accumulate_bug Extra Dependency "library.elpi" as library.
Require Import accumulate_bug.program.

Elpi Accumulate program File library.
Elpi Typecheck program.

accumulate2.v

(Identical to accumulate1.v.)

test_accumulate_twice.v

Require Import accumulate_bug.accumulate1.
Require Import accumulate_bug.accumulate2.
Fail Elpi Typecheck program.
(*
Error:
File "ROOT/_build/default/fmdeps/cpp2v/elpi-extra/accumulate_bug/library.elpi", line 5, column 2, character 59:duplicate type abbreviation for cpp.bs. Previous declaration: File "ROOT/_build/default/fmdeps/cpp2v/elpi-extra/accumulate_bug/library.elpi", line 5, column 2, character 59:
*)

dune

(include_subdirs qualified)

(coq.theory
 (name accumulate_bug)
 (theories elpi))

(rule
 (target dummy.v)
 (deps (glob_files_rec *.elpi))
 (action
  (with-stdout-to %{target} (echo "(* copy elpi files to _build *)"))))

[gares]

I will check next week, but there is some code to avoid loading the same file twice. So I guess this is a bug. It is possible I do put the current v file name in the uuid of the unit one accumulates, that would explain the problem.