LPCIC / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
134 stars 50 forks source link

Accumulating into programs across several Coq files isn't idempotent #627

Open swasey opened 3 months ago

swasey commented 3 months ago

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:

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 commented 3 months ago

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.