slow elaboration of `List Nat` literal

Stream: lean4

[David Renshaw]

Why does it take 1.6 seconds to elaborate this list of 960 nats?

set_option trace.profiler true in
def dualEquationIds : List Nat :=
  [  1,   2,   3,   5,   4,   6,   7,  23,  28,  25,  31,  34,  24,  29,  30,  26,  32,  36,  27,  35,
    33,  37,   8,  13,  10,  16,  19,   9,  14,  15,  11,  17,  21,  12,  20,  18,  22,  39,  38,  40,
    41,  45,  43,  44,  42,  46, 255, 270, 260, 280, 290, 257, 273, 276, 263, 283, 298, 266, 294, 286,
   302, 256, 271, 272, 261, 281, 292, 262, 291, 282, 293, 258, 274, 278, 264, 284, 300, 268, 295, 288,
   305, 259, 277, 275, 279, 267, 287, 296, 304, 265, 299, 285, 301, 269, 303, 297, 289, 306, 203, 218,
   208, 228, 238, 205, 221, 224, 211, 231, 246, 214, 242, 234, 250, 204, 219, 220, 209, 229, 240, 210,
   239, 230, 241, 206, 222, 226, 212, 232, 248, 216, 243, 236, 253, 207, 225, 223, 227, 215, 235, 244,
   252, 213, 247, 233, 249, 217, 251, 245, 237, 254, 151, 166, 156, 176, 186, 153, 169, 172, 159, 179,
   194, 162, 190, 182, 198, 152, 167, 168, 157, 177, 188, 158, 187, 178, 189, 154, 170, 174, 160, 180,
   196, 164, 191, 184, 201, 155, 173, 171, 175, 163, 183, 192, 200, 161, 195, 181, 197, 165, 199, 193,
   185, 202,  99, 114, 104, 124, 134, 101, 117, 120, 107, 127, 142, 110, 138, 130, 146, 100, 115, 116,
   105, 125, 136, 106, 135, 126, 137, 102, 118, 122, 108, 128, 144, 112, 139, 132, 149, 103, 121, 119,
   123, 111, 131, 140, 148, 109, 143, 129, 145, 113, 147, 141, 133, 150,  47,  62,  52,  72,  82,  49,
    65,  68,  55,  75,  90,  58,  86,  78,  94,  48,  63,  64,  53,  73,  84,  54,  83,  74,  85,  50,
    66,  70,  56,  76,  92,  60,  87,  80,  97,  51,  69,  67,  71,  59,  79,  88,  96,  57,  91,  77,
    93,  61,  95,  89,  81,  98, 359, 364, 361, 367, 370, 360, 365, 366, 362, 368, 372, 363, 371, 369,
   373, 388, 378, 399, 385, 375, 395, 391, 381, 403, 407, 387, 377, 398, 384, 374, 394, 390, 380, 402,
   406, 389, 379, 400, 401, 386, 376, 396, 397, 392, 382, 404, 409, 393, 383, 408, 405, 410, 307, 312,
   309, 315, 318, 308, 313, 314, 310, 316, 320, 311, 319, 317, 321, 336, 326, 347, 333, 323, 343, 339,
   329, 351, 355, 335, 325, 346, 332, 322, 342, 338, 328, 350, 354, 337, 327, 348, 349, 334, 324, 344,
   345, 340, 330, 352, 357, 341, 331, 356, 353, 358,3050,3102,3065,3139,3176,3055,3112,3122,3075,3149,
  3210,3085,3193,3159,3227,3052,3105,3108,3068,3142,3184,3071,3180,3145,3188,3058,3115,3130,3078,3152,
  3218,3093,3197,3167,3242,3061,3126,3118,3134,3089,3163,3201,3237,3081,3214,3155,3222,3097,3232,3205,
  3171,3247,3051,3103,3104,3066,3140,3178,3067,3177,3141,3179,3056,3113,3124,3076,3150,3212,3087,3194,
  3161,3230,3057,3123,3114,3125,3086,3160,3195,3229,3077,3211,3151,3213,3088,3228,3196,3162,3231,3053,
  3106,3110,3069,3143,3186,3073,3181,3147,3191,3059,3116,3132,3079,3153,3220,3095,3198,3169,3245,3063,
  3127,3120,3137,3090,3164,3203,3239,3083,3215,3157,3225,3100,3233,3208,3174,3251,3054,3109,3107,3111,
  3072,3146,3182,3190,3070,3185,3144,3187,3074,3189,3183,3148,3192,3062,3119,3128,3136,3082,3156,3216,
  3224,3091,3202,3165,3240,3099,3206,3235,3173,3250,3060,3131,3117,3133,3094,3168,3199,3244,3080,3219,
  3154,3221,3096,3243,3200,3170,3246,3064,3135,3129,3121,3138,3098,3172,3234,3207,3249,3092,3238,3166,
  3204,3241,3084,3223,3217,3158,3226,3101,3248,3236,3209,3175,3252,2847,2899,2862,2936,2973,2852,2909,
  2919,2872,2946,3007,2882,2990,2956,3024,2849,2902,2905,2865,2939,2981,2868,2977,2942,2985,2855,2912,
  2927,2875,2949,3015,2890,2994,2964,3039,2858,2923,2915,2931,2886,2960,2998,3034,2878,3011,2952,3019,
  2894,3029,3002,2968,3044,2848,2900,2901,2863,2937,2975,2864,2974,2938,2976,2853,2910,2921,2873,2947,
  3009,2884,2991,2958,3027,2854,2920,2911,2922,2883,2957,2992,3026,2874,3008,2948,3010,2885,3025,2993,
  2959,3028,2850,2903,2907,2866,2940,2983,2870,2978,2944,2988,2856,2913,2929,2876,2950,3017,2892,2995,
  2966,3042,2860,2924,2917,2934,2887,2961,3000,3036,2880,3012,2954,3022,2897,3030,3005,2971,3048,2851,
  2906,2904,2908,2869,2943,2979,2987,2867,2982,2941,2984,2871,2986,2980,2945,2989,2859,2916,2925,2933,
  2879,2953,3013,3021,2888,2999,2962,3037,2896,3003,3032,2970,3047,2857,2928,2914,2930,2891,2965,2996,
  3041,2877,3016,2951,3018,2893,3040,2997,2967,3043,2861,2932,2926,2918,2935,2895,2969,3031,3004,3046,
  2889,3035,2963,3001,3038,2881,3020,3014,2955,3023,2898,3045,3033,3006,2972,3049,2644,2696,2659,2733,
  2770,2649,2706,2716,2669,2743,2804,2679,2787,2753,2821,2646,2699,2702,2662,2736,2778,2665,2774,2739,
  2782,2652,2709,2724,2672,2746,2812,2687,2791,2761,2836,2655,2720,2712,2728,2683,2757,2795,2831,2675,
  2808,2749,2816,2691,2826,2799,2765,2841,2645,2697,2698,2660,2734,2772,2661,2771,2735,2773,2650,2707,
  2718,2670,2744,2806,2681,2788,2755,2824,2651,2717,2708,2719,2680,2754,2789,2823,2671,2805,2745,2807,
  2682,2822,2790,2756,2825,2647,2700,2704,2663,2737,2780,2667,2775,2741,2785,2653,2710,2726,2673,2747,
  2814,2689,2792,2763,2839,2657,2721,2714,2731,2684,2758,2797,2833,2677,2809,2751,2819,2694,2827,2802,
  2768,2845,2648,2703,2701,2705,2666,2740,2776,2784,2664,2779,2738,2781,2668,2783,2777,2742,2786,2656]

[Julian Berman]

There was a thread recently that I think is a similar issue -- https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/Large.20vector.20hangs/near/473252143

in particular Mario I think posted an explanation (some "optimization" for large lists is actually slower) and a way to disable that optimization that you may want to try.

[Kyle Miller]

Reported it as lean4#5683 @David Renshaw