Prevent a quadratic blowup in Micromega annotations.

[ppedrot]

The previous code used lists and repeatedly appended them in the wrong order, leading to O(n²) behaviour, or even worse. Since the result is only used in the end to build an unordered set, we simply create the annotation trace as the free datatype closed under concatenation and singleton, i.e. a binary tree.

The quadratic behaviour was observed in coqprime.

[ppedrot]

Bench: https://gitlab.com/coq/coq/-/jobs/1304591833

[ppedrot]

Given the partial result of the bench, this is ready to be reviewed.

[ppedrot]

FTR:

┌─────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬─────────────────┐
│                             │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │   mem faults    │
│                             │                         │                                       │                                       │                         │                 │
│                package_name │     NEW      OLD  PDIFF │            NEW             OLD  PDIFF │            NEW             OLD  PDIFF │     NEW      OLD  PDIFF │ NEW  OLD  PDIFF │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                coq-coqprime │ 1051.21  1137.62  -7.60 │  2925285456095   3160503588764  -7.44 │  4807668903703   5103445962648  -5.80 │  940192  1036884  -9.33 │   0    0    nan │
│                    coq-core │  110.93   111.29  -0.32 │   310531808880    310422361789   0.04 │   457113633868    457113124336   0.00 │  311056   311124  -0.02 │   0    0    nan │
│       coq-engine-bench-lite │  336.11   336.58  -0.14 │   944150975087    944993127192  -0.09 │  1654602748347   1656403240127  -0.11 │ 3507164  3507044   0.00 │   0    0    nan │
│  coq-performance-tests-lite │ 1688.42  1690.72  -0.14 │  4722813667628   4721967351859   0.02 │  7469311908485   7472852057010  -0.05 │ 2084944  2084936   0.00 │   0    0    nan │
│                 coq-unimath │ 4185.30  4190.06  -0.11 │ 11627678724456  11642056251252  -0.12 │ 21289108409446  21287750844503   0.01 │ 1130880  1130972  -0.01 │   0    0    nan │
│                   coq-color │  528.92   529.46  -0.10 │  1468424421904   1468965274519  -0.04 │  1730887058264   1729984659500   0.05 │ 1138724  1106724   2.89 │   0    0    nan │
│          coq-mathcomp-field │  239.85   240.04  -0.08 │   668058719868    668300704094  -0.04 │   955669368768    955564339335   0.01 │  659556   659388   0.03 │   0    0    nan │
│             coq-fiat-crypto │ 5146.69  5149.11  -0.05 │ 14331313707837  14325399664691   0.04 │ 24026802428732  24023012375258   0.02 │ 2218032  2218856  -0.04 │   0    0    nan │
│                         coq │    4.58     4.58   0.00 │    12692436234     12597460754   0.75 │    23634777448     23642336451  -0.03 │  284848   284832   0.01 │   0    0    nan │
│       coq-mathcomp-solvable │  185.79   185.78   0.01 │   516371926589    516339187828   0.01 │   683616647638    683654160993  -0.01 │  674104   674172  -0.01 │   0    0    nan │
│              coq-verdi-raft │ 1247.94  1247.66   0.02 │  3464167511375   3465024031301  -0.02 │  4627786752037   4625477064301   0.05 │  902040   902452  -0.05 │   0    0    nan │
│                    coq-corn │ 1593.18  1592.43   0.05 │  4417074963660   4416697510568   0.01 │  6041297321254   6040428815352   0.01 │  810668   810792  -0.02 │   0    0    nan │
│                coq-bedrock2 │  331.22   330.96   0.08 │   918941107556    918032598018   0.10 │  1521052077762   1520135870587   0.06 │  799940   769236   3.99 │   0    0    nan │
│            coq-fiat-parsers │  647.49   646.68   0.13 │  1799792558515   1795406282291   0.24 │  2567660949004   2567615899128   0.00 │ 3584764  3584796  -0.00 │   0    0    nan │
│      coq-mathcomp-odd-order │ 1141.02  1139.58   0.13 │  3172241840735   3169308837873   0.09 │  4723611908453   4723908357411  -0.01 │  941224   905656   3.93 │   0    0    nan │
│               coq-perennial │ 7303.41  7293.70   0.13 │ 20318562783996  20314780878361   0.02 │ 29189083747022  29192810534765  -0.01 │ 3098676  3124232  -0.82 │   0    0    nan │
│               coq-fiat-core │  117.10   116.94   0.14 │   329086671770    328196698956   0.27 │   412075928118    410915879430   0.28 │  479776   479800  -0.01 │   0    0    nan │
│        coq-mathcomp-algebra │  151.52   151.30   0.15 │   420702562285    419901946431   0.19 │   509574410360    509559718172   0.00 │  554216   554208   0.00 │   0    0    nan │
│ coq-rewriter-perf-SuperFast │  813.73   812.52   0.15 │  2269210781707   2265065892023   0.18 │  3347449159432   3346851662645   0.02 │ 1089044  1089036   0.00 │   0    0    nan │
│       coq-mathcomp-fingroup │   52.40    52.32   0.15 │   145108643137    145204436753  -0.07 │   189835621235    189795096624   0.02 │  480136   479992   0.03 │   0    0    nan │
│                coq-rewriter │  740.86   739.41   0.20 │  2058589396795   2056294307767   0.11 │  2979968968569   2977769124761   0.07 │ 1089328  1089368  -0.00 │   0    0    nan │
│              coq-coquelicot │   74.39    74.22   0.23 │   205617513440    204972288965   0.31 │   242371927587    241653411056   0.30 │  559728   559740  -0.00 │   0    0    nan │
│               coq-fourcolor │ 2723.56  2717.23   0.23 │  7577727040482   7558633307415   0.25 │ 12250690715128  12252584295570  -0.02 │  732928   732852   0.01 │   0    0    nan │
│            coq-math-classes │  189.28   188.83   0.24 │   520172159371    520058982917   0.02 │   654760253439    654781754470  -0.00 │  481220   481304  -0.02 │   0    0    nan │
│             coq-lambda-rust │ 1367.76  1364.35   0.25 │  3807777057459   3793008852940   0.39 │  5136079626275   5136492527769  -0.01 │ 1077456  1099484  -2.00 │   0    0    nan │
│                    coq-hott │  366.55   365.56   0.27 │   994470521356    996833231384  -0.24 │  1410588290272   1410579901406   0.00 │  566232   566324  -0.02 │   0    0    nan │
│                 coq-bignums │   59.86    59.69   0.28 │   164635750609    164375351381   0.16 │   210014492576    209997549279   0.01 │  467212   467012   0.04 │   0    0    nan │
│                  coq-stdlib │  429.12   427.85   0.30 │  1201995547388   1198055479144   0.33 │  1492867525419   1492954108146  -0.01 │  570900   570660   0.04 │   0    0    nan │
│      coq-mathcomp-character │  164.42   163.91   0.31 │   457056079674    455874166245   0.26 │   598866668913    598904960650  -0.01 │  732540   716248   2.27 │   0    0    nan │
│                  coq-geocoq │ 1463.28  1458.74   0.31 │  4058189677070   4046480147208   0.29 │  5645895989960   5644486819668   0.02 │  983816   984184  -0.04 │   0    0    nan │
│      coq-mathcomp-ssreflect │   58.49    58.27   0.38 │   160607025696    160244390620   0.23 │   190754588270    190725369656   0.02 │  522596   522760  -0.03 │   0    0    nan │
│                 coq-coqutil │   62.52    62.21   0.50 │   172229976220    171497948346   0.43 │   214972875092    214556479160   0.19 │  601732   601300   0.07 │   0    0    nan │
│                   coq-verdi │  106.65   106.12   0.50 │   294027689906    292760721346   0.43 │   388690265397    387996448041   0.18 │  544524   544540  -0.00 │   0    0    nan │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴─────────────────┘

[fajb]

Well done @ppedrot . Thanks.