`coq.extraction` + `coq.theory` raises internal errors

jmadiot commented 1 month ago

Expected Behavior

Starting with the files:

foo.v containing Require Extraction. Extraction "bar.ml" nat. (it can also be empty)
dune-project with a standard
```
(lang dune 3.16)
(using coq 0.8)
```
dune with an incorrect but not completely absurd:
```
(coq.theory
(name baz))
(coq.extraction
(prelude foo)
(extracted_modules bar))
```
it would have been quite helpful to have dune build telling me that one cannot have coq.theory and coq.extraction in the same dune file/directory.

Alternatively (but it would be less helpful in understanding the issue) I would have expected an error such as Error: Duplicate Coq module "foo". because I did not add the exclude directive (modules :standard \ foo) to exclude foo from the theory, such as is done in https://github.com/ocaml/dune/issues/4158 .

Actual Behavior

I get the i_must_not_crash message, with an error message that I understand only in hindsight:

Internal error, please report upstream including the contents of _build/log.
Description:
  ("Map.add_exn: key already exists",
  { key =
      { source = In_build_dir "default/foo.v"; prefix = []; name = "foo" }
  })
Raised at Stdune__Code_error.raise in file
  "otherlibs/stdune/src/code_error.ml", line 10, characters 30-62
Called from Stdlib__Map.Make.update in file "map.ml", line 287, characters
  18-28
Called from Dune_rules__Coq_sources.of_dir.(fun) in file
  "src/dune_rules/coq/coq_sources.ml", line 100, characters 20-75
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters
  24-34
Called from Fiber__Core.O.(>>|).(fun) in file "vendor/fiber/src/core.ml",
  line 253, characters 36-41
Called from Fiber__Scheduler.exec in file "vendor/fiber/src/scheduler.ml",
  line 76, characters 8-11
-> required by ("<unnamed>", ())
-> required by ("<unnamed>", ())
-> required by ("load-dir", In_build_dir "default")
-> required by
   ("build-alias", { dir = In_build_dir "default"; name = "default" })
-> required by ("toplevel", ())

I must not crash.  Uncertainty is the mind-killer. Exceptions are the
little-death that brings total obliteration.  I will fully express my cases. 
Execution will pass over me and through me.  And when it has gone past, I
will unwind the stack along its path.  Where the cases are handled there will
be nothing.  Only I will remain.

(I did not include _build/log as it seems to have little relevant information)

The documentation explains coq.extraction somewhat, but I think it would be very helpful to provide to add extraction in the examples projects. Issue 4158 is helpful in understanding what went wrong and what is supposed to be allowed, for example.

I also notice now, in hindsight, the documentation's sentence "the common placement for the OCaml stanzas is in the same dune file." which would suggest no mixing of coq.theory and coq.extraction, but it was a note about where the extraction happens, which was a concern I would have been happy to have at the time.

Reproduction

(Instructions in first section.)

Specifications

dune 3.16.0
ocaml 5.2.0
ubuntu 22.04.5 LTS

ejgallego commented 1 month ago

Thanks @jmadiot for the careful report and test case. I agree on all counts, we need to add the test case to our test suite and proceed to improve the error message.

Improving the error message should be easy if someone is up to the task.

jmadiot commented 1 month ago

For lack of anything proper and better in the documentation, here is an example repository that would have helped me at the time https://github.com/jmadiot/coq-extraction-example

ocaml / dune