`Search` gives Not_found

[JasonGross]

Description of the problem

(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,unsupported-attributes" "-R" "/home/jgross/Documents/GitHub/fiat-crypto/src" "Crypto" "-Q" "/home/jgross/Documents/GitHub/fiat-crypto/coqprime/src/Coqprime" "Coqprime" "-Q" "/home/jgross/Documents/GitHub/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil" "coqutil" "-Q" "/home/jgross/Documents/GitHub/fiat-crypto/rewriter/src/Rewriter" "Rewriter" "-I" "/home/jgross/Documents/GitHub/fiat-crypto/rewriter/src/Rewriter/Util/plugins" "-top" "Crypto.Arithmetic.SolinasReduction" "-R" "." "Top" "-native-compiler" "ondemand" "-native-compiler" "ondemand" "-native-compiler" "ondemand" "-native-compiler" "ondemand" "-native-compiler" "ondemand" "-native-compiler" "ondemand" "-native-compiler" "ondemand") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 2016 lines to 52 lines, then from 57 lines to 8 lines, then from 21 lines to 1807 lines, then from 1812 lines to 446 lines, then from 452 lines to 391 lines, then from 19 lines to 5 lines, then from 18 lines to 3763 lines, then from 3765 lines to 645 lines, then from 322 lines to 243 lines, then from 22 lines to 9 lines, then from 22 lines to 153 lines, then from 158 lines to 19 lines, then from 32 lines to 824 lines, then from 828 lines to 260 lines, then from 273 lines to 618 lines, then from 623 lines to 429 lines, then from 442 lines to 715 lines, then from 720 lines to 459 lines, then from 472 lines to 600 lines, then from 605 lines to 492 lines, then from 505 lines to 554 lines, then from 559 lines to 499 lines, then from 512 lines to 1177 lines, then from 1181 lines to 683 lines, then from 696 lines to 926 lines, then from 931 lines to 130 lines, then from 143 lines to 540 lines, then from 545 lines to 256 lines, then from 269 lines to 486 lines, then from 491 lines to 335 lines, then from 348 lines to 646 lines, then from 651 lines to 345 lines, then from 358 lines to 830 lines, then from 835 lines to 508 lines, then from 521 lines to 727 lines, then from 732 lines to 586 lines, then from 599 lines to 1027 lines, then from 1031 lines to 595 lines, then from 608 lines to 949 lines, then from 954 lines to 722 lines, then from 735 lines to 827 lines, then from 832 lines to 843 lines, then from 842 lines to 36 lines, then from 41 lines to 36 lines *)
(* coqc version 8.17+alpha compiled with OCaml 4.11.2
   coqtop version 8.17+alpha
   Expected coqc runtime on this file: 0.963 sec *)
Require Coq.FSets.FMapPositive.
Import Coq.ZArith.ZArith.

Module Export Crypto_DOT_Util_DOT_Structures_DOT_OrdersEx_WRAPPED.
Module Export OrdersEx.
Module Export NIsoOptionPositiveCommon.
  Definition t := N.
End NIsoOptionPositiveCommon.
Module Export NIsoOptionPositive.
  Include NIsoOptionPositiveCommon.
End NIsoOptionPositive.
Module Export NIsoOptionPositiveOrig.
End NIsoOptionPositiveOrig.
Module NOrderedTypeBitsOrig := NIsoOptionPositiveOrig.
End OrdersEx.
Include Crypto_DOT_Util_DOT_Structures_DOT_OrdersEx_WRAPPED.OrdersEx.
Search Z.eqb.
(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *)

Coq Version

master (85092c51e1bc2a123831c7ab4f5efa86d93116cd) (works fine on 8.16.0)

[JasonGross]

Backtrace

``` Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. Raised at Int.Map.find in file "clib/int.ml", line 39, characters 14-29 Called from HMap.Make.find in file "clib/hMap.ml", line 357, characters 12-28 Called from Dumpglob.constant_kind in file "interp/dumpglob.ml" (inlined), line 119, characters 23-49 Called from Search.generic_search.iter_constant in file "vernac/search.ml", line 72, characters 15-41 Called from Stdlib__map.Make.iter in file "map.ml", line 296, characters 20-25 Called from Stdlib__map.Make.iter in file "map.ml", line 296, characters 20-25 Called from Stdlib__map.Make.iter in file "map.ml", line 296, characters 10-18 Called from Stdlib__map.Make.iter in file "map.ml", line 296, characters 10-18 Called from Stdlib__map.Make.iter in file "map.ml", line 296, characters 10-18 Called from Stdlib__map.Make.iter in file "map.ml", line 296, characters 10-18 Called from Search.generic_search in file "vernac/search.ml", line 89, characters 2-47 Called from Search.prioritize_search in file "vernac/search.ml", line 148, characters 11-19 Called from ComSearch.interp_search in file "vernac/comSearch.ml" (inlined), line 136, characters 6-129 Called from ComSearch.interp_search in file "vernac/comSearch.ml", line 136, characters 6-139 Called from Vernacextend.vtreadproofopt.(fun) in file "vernac/vernacextend.ml", line 159, characters 29-44 Called from Vernacinterp.interp_typed_vernac in file "vernac/vernacinterp.ml", line 20, characters 20-113 Called from Vernacinterp.interp_control.(fun) in file "vernac/vernacinterp.ml", line 207, characters 24-69 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.(fun) in file "vernac/vernacinterp.ml", line 257, characters 18-43 Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 255, characters 6-279 Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38 Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2177, characters 16-43 Called from Stm.State.define in file "stm/stm.ml", line 964, 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", line 2319, characters 4-105 Called from Stm.observe in file "stm/stm.ml", line 2420, characters 4-60 Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38 Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 68, characters 31-52 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" (inlined), line 123, characters 2-60 Called from Coqloop.process_toplevel_command in file "toplevel/coqloop.ml", line 431, characters 17-62 Called from Coqloop.read_and_execute_base in file "toplevel/coqloop.ml", line 462, characters 4-39 Called from Coqloop.read_and_execute in file "toplevel/coqloop.ml", line 468, characters 6-34 ```

[SkySkimmer]

Reduced

Module Outer.
  Module Simple.
    Definition t := nat.
  End Simple.
  Module Contain.
    Include Simple.
  End Contain.
  Module E.
  End E.
  Module Def := E.
End Outer.

Include Outer.
Search Nat.add.
(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *)

[ejgallego]

Maybe related to https://github.com/coq/coq/pull/16300

[SkySkimmer]

For some reason with the Def := E while including Outer constant_of_delta_kn produces (Contain.t, Simple.t) from Contain.t, so the dumpglob map (which is a canord map) does not have an element for Contain.t. I have no clue what is happening in this code so the easiest fix is probably to switch the dumpglob map to cmap_env (userord)

[JasonGross]

This is making Search essentially unusable in fiat-crypto on master, and should plausibly be a blocker for 8.17?