Anomaly in Trakt

[patrick-nicodemus]

I am trying to bring Trakt into compatibility with more recent versions of math-comp and I am encountering the following anomaly. I will do my best to dig into it but I am hoping that a Coq-Elpi maintainer will be better able to determine whether there is a problem with the Trakt code or a bug in Elpi, and isolate the problem.

Here is the failure in CI, I hope this is locally reproducible just by manually following the attached Github workflow.
https://github.com/patrick-nicodemus/trakt/actions/runs/17658540508/job/50187106381

Here is my debug log:

Error:
Anomaly
"File "src/compiler/compiler_data.ml", line 87, characters 11-17: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
Raised at Elpi_compiler__Compiler_data.TypeAssignment.compare_tmode in file "src/compiler/compiler_data.ml", line 87, characters 11-23
Called from Elpi_compiler__Compiler_data.TypeAssignment.compare_t_ in file "src/compiler/compiler_data.ml", line 135, characters 6-22
Called from Elpi_compiler__Compiler_data.TypeAssignment.check_same_mode in file "src/compiler/compiler_data.ml", line 335, characters 7-95
Called from Elpi_compiler__Compiler_data.TypeAssignment.undup_skemas.eq_skema in file "src/compiler/compiler_data.ml", line 343, characters 16-87
Called from Stdlib__List.exists in file "list.ml", line 176, characters 12-15
Called from Elpi_compiler__Compiler_data.TypeAssignment.undup_skemas.undup in file "src/compiler/compiler_data.ml", line 349, characters 33-60
Called from Elpi_compiler__Compiler_data.TypeAssignment.undup_skemas in file "src/compiler/compiler_data.ml", line 351, characters 6-13
Called from Elpi_compiler__Compiler_data.TypingEnv.merge_envs.(fun) in file "src/compiler/compiler_data.ml", line 537, characters 20-108
Called from Stdlib__Map.Make.union in file "map.ml", line 420, characters 45-57
Called from Stdlib__Map.Make.union in file "map.ml", line 417, characters 42-55
Called from Stdlib__Map.Make.union in file "map.ml", line 417, characters 20-33
Called from Stdlib__Map.Make.union in file "map.ml", line 417, characters 42-55
Called from Stdlib__Map.Make.union in file "map.ml", line 417, characters 20-33
Called from Stdlib__Map.Make.union in file "map.ml", line 417, characters 20-33
Called from Stdlib__Map.Make.union in file "map.ml", line 417, characters 20-33
Called from Stdlib__Map.Make.union in file "map.ml", line 417, characters 20-33
Called from Stdlib__Map.Make.union in file "map.ml", line 417, characters 42-55
Called from Stdlib__Map.Make.union in file "map.ml", line 417, characters 20-33
Called from Stdlib__Map.Make.union in file "map.ml", line 417, characters 20-33
Called from Stdlib__Map.Make.union in file "map.ml", line 417, characters 20-33
Called from Elpi_compiler__Compiler_data.TypingEnv.merge_envs in file "src/compiler/compiler_data.ml", lines 535-540, characters 22-13
Called from Elpi_compiler__Compiler.Assemble.extend1_signature in file "src/compiler/compiler.ml", line 2017, characters 14-53
Called from Elpi_compiler__Compiler.Assemble.extend1 in file "src/compiler/compiler.ml", line 2027, characters 9-91
Called from Elpi_plugin__Rocq_elpi_utils.handle_elpi_compiler_errors in file "src/rocq_elpi_utils.ml", line 86, characters 6-10
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Elpi_plugin__Rocq_elpi_programs.SourcesStorage.compile.compile_chunk in file "src/rocq_elpi_programs.ml", line 802, characters 21-68
Called from Elpi_plugin__Rocq_elpi_programs.SourcesStorage.compile.compile_code in file "src/rocq_elpi_programs.ml", line 784, characters 21-38
Called from Elpi_plugin__Rocq_elpi_programs.SourcesStorage.compile.compile_code in file "src/rocq_elpi_programs.ml", line 784, characters 21-38
Called from Elpi_plugin__Rocq_elpi_programs.SourcesStorage.compile.compile_code in file "src/rocq_elpi_programs.ml", line 784, characters 21-38
Called from Elpi_plugin__Rocq_elpi_programs.SourcesStorage.get_and_compile.(fun) in file "src/rocq_elpi_programs.ml", line 811, characters 15-31
Called from Option.map in file "clib/option.ml", line 102, characters 19-24
Called from Elpi_plugin__Rocq_elpi_programs.SourcesStorage.get_and_compile in file "src/rocq_elpi_programs.ml", lines 809-821, characters 12-23
Called from Elpi_plugin__Rocq_elpi_vernacular.Compiler.get_and_compile in file "src/rocq_elpi_vernacular.ml" (inlined), line 445, characters 32-77
Called from Elpi_plugin__Rocq_elpi_vernacular.Interp.run_program in file "src/rocq_elpi_vernacular.ml", line 535, characters 4-29
Called from Elpi_plugin__Rocq_elpi_vernacular.Interp.run_program in file "src/rocq_elpi_vernacular.ml", line 679, characters 21-94
Called from Vernactypes.vtdefault.(fun) in file "vernac/vernactypes.ml", line 173, characters 34-38
Called from Vernactypes.typed_vernac.(fun) in file "vernac/vernactypes.ml", line 170, characters 65-71
Called from Vernactypes.run.(fun) in file "vernac/vernactypes.ml", line 164, characters 15-32
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", line 126, characters 16-23
Called from Vernactypes.OpaqueAccess.runner.(fun) in file "vernac/vernactypes.ml", line 114, characters 30-34
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", lines 125-127, characters 14-41
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", line 126, characters 16-23
Called from Vernactypes.Proof.runner.(fun) in file "vernac/vernactypes.ml", line 69, characters 30-34
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", lines 125-127, characters 14-41
Called from Vernactypes.Prog.runner.(fun) in file "vernac/vernactypes.ml", line 27, characters 30-34
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", lines 124-128, characters 12-39
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", lines 124-128, characters 12-39
Called from Vernactypes.run in file "vernac/vernactypes.ml", lines 163-164, characters 14-47
Called from Vernacinterp.interp_expr_core in file "vernac/vernacinterp.ml", lines 80-84, characters 60-7
Called from Vernacinterp.interp_expr in file "vernac/vernacinterp.ml", lines 49-50, characters 19-47
Called from VernacControl.under_control in file "vernac/vernacControl.ml", line 203, characters 14-18
Called from Vernacinterp.interp_control_gen in file "vernac/vernacinterp.ml", lines 36-40, characters 4-7
Called from Util.try_finally in file "lib/util.ml", line 133, characters 16-19
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Util.try_finally in file "lib/util.ml", line 137, characters 6-32
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 151, characters 16-41
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp in file "vernac/vernacinterp.ml", line 165, characters 15-115
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2034, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 963, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", lines 2203-2204, characters 4-74
Called from Stm.observe in file "stm/stm.ml", line 2295, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.process_transaction in file "stm/stm.ml", line 2540, characters 25-92
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.add in file "stm/stm.ml", line 2639, characters 8-50
Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 76, characters 28-90
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 157, characters 6-46

Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Util.try_finally in file "lib/util.ml", line 133, characters 16-19
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Util.try_finally in file "lib/util.ml", line 137, characters 6-32
Called from Coqloop.process_toplevel_command in file "toplevel/coqloop.ml", line 480, characters 17-62
Called from Coqloop.read_and_execute in file "toplevel/coqloop.ml", line 507, characters 6-41

[patrick-nicodemus]

The warning beforehand may be relevant:

Warning:
Undeclared globals:
- File "./example/Example.v", line 254, column 0, characters 6192-6223: conversion-allowed.
Please add the following text to your program:
type conversion-allowed term -> pred.
[elpi.missing-types,elpi.typecheck,elpi,default]

but I don't understand what conversion-allowed does.

It's an accumulated clause in a database. conversion-allowed is a Trakt-defined predicate, but it should be in scope, so I'm not sure why the typechecker is unaware of it.

[gares]

I think this should fix the anomaly: LPCIC/elpi#363
I don't have the time to try out trakt myself.
One this is that, from version 1 to 3, Elpi is now way more strict about the order of accumulate.
Accumulating a clause, and later its signature, is not allowed anymore. This may be why conversion-allowed seems to have no declared type, and later the system tries to see if the inferred one (the one in the warning) is the same as the declared one, reaching an incomplete code path that should be fixed by PR363.

[patrick-nicodemus]

I can confirm that the linked PR fixes the anomaly! I will try to understand why the code is accumulating the signature before the clause.

[patrick-nicodemus]

So we have the following situation. There is a master command Trakt that has sub commands. This is implemented as a kind of higher order function, which selects the correct subcomand to apply and then executes it:

  operation "Add" "Conversion" add-conversion-allowed.
  operation "Set" "Verbosity" set-verbosity.

  main [str Command, str Element|RecordData] :-
    operation Command Element Op, !,
    std.assert! (std.map RecordData elaborate-argument ERecordData) "arguments are ill-typed",
    Op ERecordData.

So the higher-order relation operation associates the strings "Add Conversion" to add-conversion-allowed and then we run Op (= add-conversion-allowed) on input ERecordData.

add-conversion-allowed is in commands.elpi:

add-conversion-allowed Args :-
  std.assert! (Args = [trm T]) {std.string.concat "\n" [
    "command syntax error",
    "usage: Trakt Add Conversion (?t)"
  ]},
  when (verbose) (coq.say "Enabled conversion on term" {coq.term->string T}),
  coq.elpi.accumulate _ "conversion.db" (clause _ _ (conversion-allowed T)).

conversion-allowed is declared in types.elpi:

pred conversion-allowed o:term. % head term allowed to trigger Coq conversion

then the conversion.db is declared in Database.v. It is initially empty.

In the definition of the Trakt command, types.elpi is accumulated before commands.elpi, and then in the body of the definition of Trakt we call add-conversion-allowed. It seems right to me?

Elpi Command Trakt.
(* ... *
Elpi Accumulate File types.

From Trakt Require Export Database.
Elpi Accumulate Db embeddings.db.
Elpi Accumulate Db symbols.db.
Elpi Accumulate Db relations.db.
Elpi Accumulate Db conversion.db.

Elpi Accumulate File common.

Elpi Accumulate File commands.

Elpi Accumulate lp:{{
  %....
  operation "Add" "Conversion" add-conversion-allowed.
  operation "Set" "Verbosity" set-verbosity.

  main [str Command, str Element|RecordData] :-
    operation Command Element Op, !,
    std.assert! (std.map RecordData elaborate-argument ERecordData) "arguments are ill-typed",
    Op ERecordData.
  %% ...
}}.
Elpi Typecheck.
Elpi Export Trakt.

I think I don't understand where conversion-allowed has to be in scope for this all to work correctly.

[patrick-nicodemus]

I modified the code as follows:

pred add-conversion-allowed i:(list argument).

add-conversion-allowed Args :-
  Args = [trm T],
  conversion-allowed T,
  coq.say T "is already present".

add-conversion-allowed Args :-
  std.assert! (Args = [trm T]) {std.string.concat "\n" [
    "command syntax error",
    "usage: Trakt Add Conversion (?t)"
  ]},
  when (verbose) (coq.say "Enabled conversion on term" {coq.term->string T}),
  coq.elpi.accumulate _ "conversion.db" (clause _ _ (conversion-allowed T)).

So the code first checks to see if conversion-allowed T. If it is, the goal succeeds and nothing happens. Otherwise, it fails, and we accumulate conversion-allowed T to the database.
Now I execute:

Trakt Add Conversion GRing.add.
Trakt Add Conversion GRing.add.

and it prints:

Enabled conversion on term @GRing.add
File "./example/Example.v", line 256, characters 0-31:
Warning:
Undeclared globals:
- File "./example/Example.v", line 256, column 0, characters 6248-6279: conversion-allowed.
Please add the following text to your program:
type conversion-allowed term -> (pred).
[elpi.missing-types,elpi.typecheck,elpi,default]
global (const «GRing.add») is already present

This is confusing to me. The second line of code gives global ... is already present which suggests that indeed GRing.add was successfully added to conversion.db. Is the warning spurious or am I misunderstanding something?