Jeff Epler
40ab5c6b21
compression: Implement ciscorn's dictionary approach
...
Massive savings. Thanks so much @ciscorn for providing the initial
code for choosing the dictionary.
This adds a bit of time to the build, both to find the dictionary
but also because (for reasons I don't fully understand), the binary
search in the compress() function no longer worked and had to be
replaced with a linear search.
I think this is because the intended invariant is that for codebook
entries that encode to the same number of bits, the entries are ordered
in ascending value. However, I mis-placed the transition from "words"
to "byte/char values" so the codebook entries for words are in word-order
rather than their code order.
Because this price is only paid at build time, I didn't care to determine
exactly where the correct fix was.
I also commented out a line to produce the "estimated total memory size"
-- at least on the unix build with TRANSLATION=ja, this led to a build
time KeyError trying to compute the codebook size for all the strings.
I think this occurs because some single unicode code point ('ァ') is
no longer present as itself in the compressed strings, due to always
being replaced by a word.
As promised, this seems to save hundreds of bytes in the German translation
on the trinket m0.
Testing performed:
- built trinket_m0 in several languages
- built and ran unix port in several languages (en, de_DE, ja) and ran
simple error-producing codes like ./micropython -c '1/0'
2020-09-12 10:10:45 -05:00
..
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-08-30 11:09:49 -05:00
2020-09-03 16:34:56 -07:00
2020-09-10 11:20:44 -07:00
2020-09-03 16:34:56 -07:00
2020-07-29 10:54:37 -07:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-23 20:40:16 -07:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2018-04-10 15:06:47 +10:00
2020-07-06 19:16:25 +01:00
2018-04-10 15:06:47 +10:00
2018-04-10 15:06:47 +10:00
2018-05-04 20:39:16 +10:00
2018-04-10 15:06:47 +10:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-03-03 10:55:50 -08:00
2018-01-24 10:33:46 -08:00
2020-07-17 17:15:03 -07:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2019-04-05 21:38:32 +02:00
2020-09-12 10:10:45 -05:00
2018-08-09 14:16:28 -07:00
2018-08-07 14:58:57 -07:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-08-02 11:36:38 -04:00
2018-10-18 10:37:42 -07:00
2020-06-25 20:57:17 -04:00
2020-07-06 19:16:25 +01:00
2020-08-19 14:23:28 -07:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-13 22:54:52 -05:00
2020-09-06 09:53:16 -05:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-08-25 11:47:50 -05:00
2020-09-03 16:34:56 -07:00
2020-07-21 15:40:51 -07:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2019-01-18 11:53:09 -08:00
2020-08-04 18:42:09 -05:00
2020-07-06 19:16:25 +01:00
2020-08-19 14:23:28 -07:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-23 20:41:10 -07:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-09-06 09:53:16 -05:00
2020-09-06 09:53:16 -05:00
2020-09-06 09:53:16 -05:00
2020-09-06 09:53:16 -05:00
2020-08-04 18:42:09 -05:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2017-10-04 12:37:50 +11:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-08-04 18:42:09 -05:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-08-04 14:45:45 -05:00
2020-07-22 16:26:46 -07:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-08-04 14:45:45 -05:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-08-04 14:45:45 -05:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-08-04 14:45:45 -05:00
2020-06-03 10:56:35 +01:00
2020-08-02 11:36:38 -04:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-08-12 07:32:18 -05:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2018-05-14 17:41:17 -04:00
2018-05-14 17:41:17 -04:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-04-21 22:40:12 -04:00
2020-04-21 22:40:12 -04:00
2020-07-23 20:40:16 -07:00
2018-07-11 16:45:30 -04:00
2020-08-21 11:00:02 -07:00
2020-08-21 11:00:02 -07:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-06-03 10:56:35 +01:00
2017-08-25 22:17:07 -04:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00
2020-07-06 19:16:25 +01:00