[MLton] HOL on MLton

Joe Hurd joe.hurd@comlab.ox.ac.uk
Tue, 13 Jan 2004 23:06:32 +0000 (GMT) 

  This message is in MIME format.  The first part should be readable text,
  while the remaining parts are likely unreadable without MIME-aware tools.
  Send mail to mime@docserver.cac.washington.edu for more info.

---559023410-1804928587-1074035192=:29598
Content-Type: TEXT/PLAIN; charset=US-ASCII

Hi Stephen,

thanks for your help with IntInf, everything's working fine now.
That is, except for profiling...

marlin:~/dev/sml/metis$ mlton
MLton 20040106 (built Tue Jan  6 15:53:18 2004 on redhat71)
marlin:~/dev/sml/metis$ mlton -basis 1997 t.sml
Warning: -basis is deprecated
marlin:~/dev/sml/metis$ mlton -basis 1997 -profile time t.sml
Warning: -basis is deprecated
shrinker raised mismatched Leave

The offending source file is attached to this email.

> > BTW, the HOL4 developers would like to move to the new basis library,
> > but we can't do anything until Moscow ML supports it.
>
> I hope this doesn't become too much of a problem.  I have no idea what
> the upgrade plans and timetable for Moscow ML are.  In all
> seriousness, what features is MLton missing that make it impossible to
> switch over to it completely?  Is it the lack of a byte-code compiler?
> Something else?  I understand it may not be feasible to do in the
> short term, but it will help our long term plans if we understand
> what's missing from MLton.  Thanks.

Theorem proving in HOL4 consists of interacting with the ML top-level
interpreter, so this is why we can't simply switch over to MLton. At
the moment I'm trying to generate some interest in using MLton for the
kind of proofs that involve costly simulation (e.g., circuits, or
network protocols), so you'd get everything set up just right using
Moscow ML and then do a one-shot MLton run that might take weeks to
complete a simulation. I think Moscow ML will switch over to the new
basis library soon (the incentive has increased now that the mosml
Time structure has just suffered a Y2K problem!), but in the meantime
if the divergence between MLton and Moscow ML gets too big then my
porting task will become infeasible. So please carry on supporting the
1997 basis, at least for the next few months!

Regards,

Joe

---559023410-1804928587-1074035192=:29598
Content-Type: TEXT/PLAIN; charset=US-ASCII; name="t.sml"
Content-Transfer-Encoding: BASE64
Content-ID: <Pine.SOL.4.44.0401132306320.29598@yellow.csi.cam.ac.uk>
Content-Description: 
Content-Disposition: attachment; filename="t.sml"

KCojbGluZSAwLjAgInNyYy9wcmUvTUQ1LnNpZyIqKQ0KKCogPT09PT09PT09
PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09
PT09PT09PT09PT09PT09PT09PSAqKQ0KKCogTUQ1IGNyeXB0b2dyYXBoaWMg
aGFzaGluZyBpbiBTTUwgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
ICAgICAgICAgICAqKQ0KKCogQ29weXJpZ2h0IChDKSAyMDAxIERhbmllbCBX
YW5nLiBBbGwgcmlnaHRzIHJlc2VydmVkLiAgICAgICAgICAgICAgICAgICAg
ICAqKQ0KKCogRGVyaXZlZCBmcm9tIHRoZSBSU0EgRGF0YSBTZWN1cml0eSwg
SW5jLiBNRDUgTWVzc2FnZS1EaWdlc3QgQWxnb3JpdGhtLiAgICAqKQ0KKCog
PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09
PT09PT09PT09PT09PT09PT09PT09PT09PT09PSAqKQ0KDQpzaWduYXR1cmUg
TUQ1ID0NCnNpZw0KDQogIHR5cGUgbWQ1c3RhdGUNCg0KICB2YWwgaW5pdCA6
IG1kNXN0YXRlDQogIHZhbCB1cGRhdGUgOiAobWQ1c3RhdGUgKiBXb3JkOFZl
Y3Rvci52ZWN0b3IpIC0+IG1kNXN0YXRlDQogIHZhbCBmaW5hbCA6IG1kNXN0
YXRlIC0+IFdvcmQ4VmVjdG9yLnZlY3Rvcg0KICB2YWwgdG9IZXhTdHJpbmcg
OiBXb3JkOFZlY3Rvci52ZWN0b3IgLT4gc3RyaW5nDQogIHZhbCB0b0Jhc2U2
NFN0cmluZyA6IFdvcmQ4VmVjdG9yLnZlY3RvciAtPiBzdHJpbmcNCg0KZW5k
DQooKiNsaW5lIDAuMCAic3JjL3ByZS9NRDUuc21sIiopDQooKiA9PT09PT09
PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09
PT09PT09PT09PT09PT09PT09PT09ICopDQooKiBNRDUgY3J5cHRvZ3JhcGhp
YyBoYXNoaW5nIGluIFNNTCAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
ICAgICAgICAgICAgICopDQooKiBDb3B5cmlnaHQgKEMpIDIwMDEgRGFuaWVs
IFdhbmcuIEFsbCByaWdodHMgcmVzZXJ2ZWQuICAgICAgICAgICAgICAgICAg
ICAgICopDQooKiBEZXJpdmVkIGZyb20gdGhlIFJTQSBEYXRhIFNlY3VyaXR5
LCBJbmMuIE1ENSBNZXNzYWdlLURpZ2VzdCBBbGdvcml0aG0uICAgICopDQoo
KiA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09
PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09ICopDQoNCnN0cnVjdHVy
ZSBNRDUgOj4gTUQ1ID0NCnN0cnVjdA0KDQpzdHJ1Y3R1cmUgVzMyID0gV29y
ZDMyDQpzdHJ1Y3R1cmUgVzhWID0gDQpzdHJ1Y3QNCiAgb3BlbiBXb3JkOFZl
Y3Rvcg0KCWZ1biBleHRyYWN0ICh2ZWMsIHMsIGwpID0NCgkgICBsZXQNCgkg
ICAgICB2YWwgbiA9DQoJCSBjYXNlIGwgb2YNCgkJICAgIE5PTkUgPT4gbGVu
Z3RoIHZlYyAtIHMNCgkJICB8IFNPTUUgaSA9PiBpDQoJICAgaW4NCgkgICAg
ICB0YWJ1bGF0ZSAobiwgZm4gaSA9PiBzdWIgKHZlYywgcyArIGkpKQ0KCSAg
IGVuZA0KICAgICAgZW5kDQogICAgdHlwZSB3b3JkNjQgID0ge2hpOlczMi53
b3JkLGxvOlczMi53b3JkfQ0KICAgIHR5cGUgd29yZDEyOCA9IHtBOlczMi53
b3JkLCBCOlczMi53b3JkLCBDOlczMi53b3JkLCAgRDpXMzIud29yZH0NCiAg
ICB0eXBlIG1kNXN0YXRlID0ge2RpZ2VzdDp3b3JkMTI4LA0KCQkgICAgICAg
bWxlbjp3b3JkNjQsIA0KCQkgICAgICAgIGJ1ZjpXb3JkOFZlY3Rvci52ZWN0
b3J9DQoNCg0KDQogICAgdmFsIHc2NF96ZXJvID0gKHtoaT0wdzAsbG89MHcw
fTp3b3JkNjQpDQogICAgZnVuIG11bDhhZGQgKHtoaSxsb30sbikgPSBsZXQN
CiAgICAgIHZhbCBtdWw4bG8gPSBXMzIuPDwgKFczMi5mcm9tSW50IChuKSww
dzMpDQogICAgICB2YWwgbXVsOGhpID0gVzMyLj4+IChXMzIuZnJvbUludCAo
biksMHcyOSkNCiAgICAgIHZhbCBsbyA9IFczMi4rIChsbyxtdWw4bG8pDQog
ICAgICB2YWwgY291dCA9IGlmIFczMi48IChsbyxtdWw4bG8pIHRoZW4gMHcx
IGVsc2UgMHcwDQogICAgICB2YWwgaGkgPSBXMzIuKyAobXVsOGhpLFczMi4r
IChoaSxjb3V0KSkNCiAgICBpbiB7aGk9aGksbG89bG99DQogICAgZW5kDQog
IA0KICAgIGZ1biBwYWNrTGl0dGxlIHdyZHMgPSBsZXQNCiAgICAgIGZ1biBs
b29wIFtdID0gW10NCgl8IGxvb3AgKHc6OndzKSA9IGxldA0KCSAgICB2YWwg
YjAgPSBXb3JkOC5mcm9tTGFyZ2VXb3JkIChXMzIudG9MYXJnZVdvcmQgdykN
CgkgICAgdmFsIGIxID0gV29yZDguZnJvbUxhcmdlV29yZCAoVzMyLnRvTGFy
Z2VXb3JkIChXMzIuPj4gKHcsMHc4KSkpDQoJICAgIHZhbCBiMiA9IFdvcmQ4
LmZyb21MYXJnZVdvcmQgKFczMi50b0xhcmdlV29yZCAoVzMyLj4+ICh3LDB3
MTYpKSkNCgkgICAgdmFsIGIzID0gV29yZDguZnJvbUxhcmdlV29yZCAoVzMy
LnRvTGFyZ2VXb3JkIChXMzIuPj4gKHcsMHcyNCkpKQ0KCSAgaW4gYjA6OmIx
OjpiMjo6YjM6OiAobG9vcCB3cykNCgkgIGVuZA0KICAgIGluIFc4Vi5mcm9t
TGlzdCAobG9vcCB3cmRzKQ0KICAgIGVuZA0KICAgIA0KICAgIHZhbCBTMTEg
PSAwdzcNCiAgICB2YWwgUzEyID0gMHcxMg0KICAgIHZhbCBTMTMgPSAwdzE3
DQogICAgdmFsIFMxNCA9IDB3MjINCiAgICB2YWwgUzIxID0gMHc1DQogICAg
dmFsIFMyMiA9IDB3OQ0KICAgIHZhbCBTMjMgPSAwdzE0DQogICAgdmFsIFMy
NCA9IDB3MjANCiAgICB2YWwgUzMxID0gMHc0DQogICAgdmFsIFMzMiA9IDB3
MTENCiAgICB2YWwgUzMzID0gMHcxNg0KICAgIHZhbCBTMzQgPSAwdzIzDQog
ICAgdmFsIFM0MSA9IDB3Ng0KICAgIHZhbCBTNDIgPSAwdzEwDQogICAgdmFs
IFM0MyA9IDB3MTUNCiAgICB2YWwgUzQ0ID0gMHcyMQ0KICAgICAgDQogICAg
ZnVuIFBBRERJTkcgaSA9ICBXOFYudGFidWxhdGUgKGksKGZuIDAgPT4gMHd4
ODAgfCBfID0+IDB3eDApKQ0KDQogICAgZnVuIEYgKHgseSx6KSA9IFczMi5v
cmIgKFczMi5hbmRiICh4LHkpLA0KCQkJICAgVzMyLmFuZGIgKFczMi5ub3Ri
IHgseikpDQogICAgZnVuIEcgKHgseSx6KSA9IFczMi5vcmIgKFczMi5hbmRi
ICh4LHopLA0KCQkJICAgVzMyLmFuZGIgKHksVzMyLm5vdGIgeikpDQogICAg
ZnVuIEggKHgseSx6KSA9IFczMi54b3JiICh4LFczMi54b3JiICh5LHopKQ0K
ICAgIGZ1biBJICh4LHkseikgPSBXMzIueG9yYiAoeSxXMzIub3JiICh4LFcz
Mi5ub3RiIHopKQ0KICAgIGZ1biBST1RBVEVfTEVGVCAoeCxuKSA9DQogICAg
ICBXMzIub3JiIChXMzIuPDwgKHgsbiksIFczMi4+PiAoeCwwdzMyIC0gbikp
DQoNCiAgICBmdW4gWFggZiAoYSxiLGMsZCx4LHMsYWMpID0gbGV0DQogICAg
ICB2YWwgYSA9IFczMi4rIChhLFczMi4rIChXMzIuKyAoZiAoYixjLGQpLHgp
LGFjKSkNCiAgICAgIHZhbCBhID0gUk9UQVRFX0xFRlQgKGEscykNCiAgICBp
biBXMzIuKyAoYSxiKQ0KICAgIGVuZA0KCQkJICAgIA0KICAgIHZhbCBGRiA9
IFhYIEYNCiAgICB2YWwgR0cgPSBYWCBHDQogICAgdmFsIEhIID0gWFggSA0K
ICAgIHZhbCBJSSA9IFhYIEkNCg0KICAgIHZhbCBlbXB0eV9idWYgPSBXOFYu
dGFidWxhdGUgKDAsKGZuIHggPT4gcmFpc2UgKEZhaWwgImJ1ZiIpKSkNCiAg
ICB2YWwgaW5pdCA9IHtkaWdlc3Q9IHtBPTB3eDY3NDUyMzAxLA0KCQkJQj0w
d3hlZmNkYWI4OSwNCgkJCUM9MHd4OThiYWRjZmUsDQoJCQlEPTB3eDEwMzI1
NDc2fSwNCgkJbWxlbj13NjRfemVybywNCgkJYnVmPWVtcHR5X2J1Zn0gOiBt
ZDVzdGF0ZQ0KDQogICAgZnVuIHVwZGF0ZSAoe2J1ZixkaWdlc3QsbWxlbn06
bWQ1c3RhdGUsaW5wdXQpID0gbGV0DQogICAgICB2YWwgaW5wdXRMZW4gPSBX
OFYubGVuZ3RoIGlucHV0DQogICAgICB2YWwgbmVlZEJ5dGVzID0gNjQgLSBX
OFYubGVuZ3RoIGJ1Zg0KICAgICAgZnVuIGxvb3AgKGksZGlnZXN0KSA9DQoJ
aWYgaSArIDYzIDwgaW5wdXRMZW4gdGhlbg0KCSAgbG9vcCAoaSArIDY0LHRy
YW5zZm9ybSAoZGlnZXN0LGksaW5wdXQpKQ0KCWVsc2UgKGksZGlnZXN0KQ0K
ICAgICAgdmFsIChidWYsKGksZGlnZXN0KSkgPQ0KCWlmIGlucHV0TGVuID49
IG5lZWRCeXRlcyB0aGVuICBsZXQNCgkgIHZhbCBidWYgPSBXOFYuY29uY2F0
IFtidWYsVzhWLmV4dHJhY3QgKGlucHV0LDAsU09NRSBuZWVkQnl0ZXMpXQ0K
CSAgdmFsIGRpZ2VzdCA9IHRyYW5zZm9ybSAoZGlnZXN0LDAsYnVmKQ0KCWlu
IChlbXB0eV9idWYsbG9vcCAobmVlZEJ5dGVzLGRpZ2VzdCkpDQoJZW5kDQoJ
ZWxzZSAoYnVmLCgwLGRpZ2VzdCkpDQogICAgICB2YWwgYnVmID0gVzhWLmNv
bmNhdCBbYnVmLCBXOFYuZXh0cmFjdCAoaW5wdXQsaSxTT01FIChpbnB1dExl
bi1pKSldDQogICAgICB2YWwgbWxlbiA9IG11bDhhZGQgKG1sZW4saW5wdXRM
ZW4pDQogICAgaW4ge2J1Zj1idWYsZGlnZXN0PWRpZ2VzdCxtbGVuPW1sZW59
DQogICAgZW5kDQogICAgYW5kIGZpbmFsIChzdGF0ZTptZDVzdGF0ZSkgPSBs
ZXQNCiAgICAgIHZhbCB7bWxlbj0ge2xvLGhpfSxidWYsLi4ufSA9IHN0YXRl
DQogICAgICB2YWwgYml0cyA9IHBhY2tMaXR0bGUgW2xvLGhpXQ0KICAgICAg
dmFsIGluZGV4ID0gVzhWLmxlbmd0aCBidWYNCiAgICAgIHZhbCBwYWRMZW4g
PSBpZiBpbmRleCA8IDU2IHRoZW4gNTYgLSBpbmRleCBlbHNlIDEyMCAtIGlu
ZGV4DQogICAgICB2YWwgc3RhdGUgPSB1cGRhdGUgKHN0YXRlLFBBRERJTkcg
cGFkTGVuKQ0KICAgICAgdmFsIHtkaWdlc3Q9IHtBLEIsQyxEfSwuLi59ID0g
dXBkYXRlIChzdGF0ZSxiaXRzKQ0KICAgIGluIHBhY2tMaXR0bGUgW0EsQixD
LERdDQogICAgZW5kDQogICAgYW5kIHRyYW5zZm9ybSAoe0EsQixDLER9LGks
YnVmKSA9IGxldA0KICAgICAgdmFsIG9mZiA9IGkgZGl2IFBhY2szMkxpdHRs
ZS5ieXRlc1BlckVsZW0NCiAgICAgIGZ1biB4IChuKSA9IFdvcmQzMi5mcm9t
TGFyZ2VXb3JkIChQYWNrMzJMaXR0bGUuc3ViVmVjIChidWYsbiArIG9mZikp
DQogICAgICB2YWwgKGEsYixjLGQpID0gKEEsQixDLEQpDQogICAgICAoKiBm
ZXRjaCB0byBhdm9pZCByYW5nZSBjaGVja3MgKikNCiAgICAgIHZhbCB4XzAw
ID0geCAoMCkgIHZhbCB4XzAxID0geCAoMSkgIHZhbCB4XzAyID0geCAoMikg
IHZhbCB4XzAzID0geCAoMykNCiAgICAgIHZhbCB4XzA0ID0geCAoNCkgIHZh
bCB4XzA1ID0geCAoNSkgIHZhbCB4XzA2ID0geCAoNikgIHZhbCB4XzA3ID0g
eCAoNykNCiAgICAgIHZhbCB4XzA4ID0geCAoOCkgIHZhbCB4XzA5ID0geCAo
OSkgIHZhbCB4XzEwID0geCAoMTApIHZhbCB4XzExID0geCAoMTEpDQogICAg
ICB2YWwgeF8xMiA9IHggKDEyKSB2YWwgeF8xMyA9IHggKDEzKSB2YWwgeF8x
NCA9IHggKDE0KSB2YWwgeF8xNSA9IHggKDE1KQ0KDQogICAgICB2YWwgYSA9
IEZGIChhLCBiLCBjLCBkLCB4XzAwLCBTMTEsIDB3eGQ3NmFhNDc4KSAoKiAx
ICopDQogICAgICB2YWwgZCA9IEZGIChkLCBhLCBiLCBjLCB4XzAxLCBTMTIs
IDB3eGU4YzdiNzU2KSAoKiAyICopDQogICAgICB2YWwgYyA9IEZGIChjLCBk
LCBhLCBiLCB4XzAyLCBTMTMsIDB3eDI0MjA3MGRiKSAoKiAzICopDQogICAg
ICB2YWwgYiA9IEZGIChiLCBjLCBkLCBhLCB4XzAzLCBTMTQsIDB3eGMxYmRj
ZWVlKSAoKiA0ICopDQogICAgICB2YWwgYSA9IEZGIChhLCBiLCBjLCBkLCB4
XzA0LCBTMTEsIDB3eGY1N2MwZmFmKSAoKiA1ICopDQogICAgICB2YWwgZCA9
IEZGIChkLCBhLCBiLCBjLCB4XzA1LCBTMTIsIDB3eDQ3ODdjNjJhKSAoKiA2
ICopDQogICAgICB2YWwgYyA9IEZGIChjLCBkLCBhLCBiLCB4XzA2LCBTMTMs
IDB3eGE4MzA0NjEzKSAoKiA3ICopDQogICAgICB2YWwgYiA9IEZGIChiLCBj
LCBkLCBhLCB4XzA3LCBTMTQsIDB3eGZkNDY5NTAxKSAoKiA4ICopDQogICAg
ICB2YWwgYSA9IEZGIChhLCBiLCBjLCBkLCB4XzA4LCBTMTEsIDB3eDY5ODA5
OGQ4KSAoKiA5ICopDQogICAgICB2YWwgZCA9IEZGIChkLCBhLCBiLCBjLCB4
XzA5LCBTMTIsIDB3eDhiNDRmN2FmKSAoKiAxMCAqKQ0KICAgICAgdmFsIGMg
PSBGRiAoYywgZCwgYSwgYiwgeF8xMCwgUzEzLCAwd3hmZmZmNWJiMSkgKCog
MTEgKikNCiAgICAgIHZhbCBiID0gRkYgKGIsIGMsIGQsIGEsIHhfMTEsIFMx
NCwgMHd4ODk1Y2Q3YmUpICgqIDEyICopDQogICAgICB2YWwgYSA9IEZGIChh
LCBiLCBjLCBkLCB4XzEyLCBTMTEsIDB3eDZiOTAxMTIyKSAoKiAxMyAqKQ0K
ICAgICAgdmFsIGQgPSBGRiAoZCwgYSwgYiwgYywgeF8xMywgUzEyLCAwd3hm
ZDk4NzE5MykgKCogMTQgKikNCiAgICAgIHZhbCBjID0gRkYgKGMsIGQsIGEs
IGIsIHhfMTQsIFMxMywgMHd4YTY3OTQzOGUpICgqIDE1ICopDQogICAgICB2
YWwgYiA9IEZGIChiLCBjLCBkLCBhLCB4XzE1LCBTMTQsIDB3eDQ5YjQwODIx
KSAoKiAxNiAqKQ0KCSAgDQogICAgICAoKiBSb3VuZCAyICopDQogICAgICB2
YWwgYSA9IEdHIChhLCBiLCBjLCBkLCB4XzAxLCBTMjEsIDB3eGY2MWUyNTYy
KSAoKiAxNyAqKQ0KICAgICAgdmFsIGQgPSBHRyAoZCwgYSwgYiwgYywgeF8w
NiwgUzIyLCAwd3hjMDQwYjM0MCkgKCogMTggKikNCiAgICAgIHZhbCBjID0g
R0cgKGMsIGQsIGEsIGIsIHhfMTEsIFMyMywgMHd4MjY1ZTVhNTEpICgqIDE5
ICopDQogICAgICB2YWwgYiA9IEdHIChiLCBjLCBkLCBhLCB4XzAwLCBTMjQs
IDB3eGU5YjZjN2FhKSAoKiAyMCAqKQ0KICAgICAgdmFsIGEgPSBHRyAoYSwg
YiwgYywgZCwgeF8wNSwgUzIxLCAwd3hkNjJmMTA1ZCkgKCogMjEgKikNCiAg
ICAgIHZhbCBkID0gR0cgKGQsIGEsIGIsIGMsIHhfMTAsIFMyMiwgIDB3eDI0
NDE0NTMpICgqIDIyICopDQogICAgICB2YWwgYyA9IEdHIChjLCBkLCBhLCBi
LCB4XzE1LCBTMjMsIDB3eGQ4YTFlNjgxKSAoKiAyMyAqKQ0KICAgICAgdmFs
IGIgPSBHRyAoYiwgYywgZCwgYSwgeF8wNCwgUzI0LCAwd3hlN2QzZmJjOCkg
KCogMjQgKikNCiAgICAgIHZhbCBhID0gR0cgKGEsIGIsIGMsIGQsIHhfMDks
IFMyMSwgMHd4MjFlMWNkZTYpICgqIDI1ICopDQogICAgICB2YWwgZCA9IEdH
IChkLCBhLCBiLCBjLCB4XzE0LCBTMjIsIDB3eGMzMzcwN2Q2KSAoKiAyNiAq
KQ0KICAgICAgdmFsIGMgPSBHRyAoYywgZCwgYSwgYiwgeF8wMywgUzIzLCAw
d3hmNGQ1MGQ4NykgKCogMjcgKikNCiAgICAgIHZhbCBiID0gR0cgKGIsIGMs
IGQsIGEsIHhfMDgsIFMyNCwgMHd4NDU1YTE0ZWQpICgqIDI4ICopDQogICAg
ICB2YWwgYSA9IEdHIChhLCBiLCBjLCBkLCB4XzEzLCBTMjEsIDB3eGE5ZTNl
OTA1KSAoKiAyOSAqKQ0KICAgICAgdmFsIGQgPSBHRyAoZCwgYSwgYiwgYywg
eF8wMiwgUzIyLCAwd3hmY2VmYTNmOCkgKCogMzAgKikNCiAgICAgIHZhbCBj
ID0gR0cgKGMsIGQsIGEsIGIsIHhfMDcsIFMyMywgMHd4Njc2ZjAyZDkpICgq
IDMxICopDQogICAgICB2YWwgYiA9IEdHIChiLCBjLCBkLCBhLCB4XzEyLCBT
MjQsIDB3eDhkMmE0YzhhKSAoKiAzMiAqKQ0KCSAgDQogICAgICAoKiBSb3Vu
ZCAzICopDQogICAgICB2YWwgYSA9IEhIIChhLCBiLCBjLCBkLCB4XzA1LCBT
MzEsIDB3eGZmZmEzOTQyKSAoKiAzMyAqKQ0KICAgICAgdmFsIGQgPSBISCAo
ZCwgYSwgYiwgYywgeF8wOCwgUzMyLCAwd3g4NzcxZjY4MSkgKCogMzQgKikN
CiAgICAgIHZhbCBjID0gSEggKGMsIGQsIGEsIGIsIHhfMTEsIFMzMywgMHd4
NmQ5ZDYxMjIpICgqIDM1ICopDQogICAgICB2YWwgYiA9IEhIIChiLCBjLCBk
LCBhLCB4XzE0LCBTMzQsIDB3eGZkZTUzODBjKSAoKiAzNiAqKQ0KICAgICAg
dmFsIGEgPSBISCAoYSwgYiwgYywgZCwgeF8wMSwgUzMxLCAwd3hhNGJlZWE0
NCkgKCogMzcgKikNCiAgICAgIHZhbCBkID0gSEggKGQsIGEsIGIsIGMsIHhf
MDQsIFMzMiwgMHd4NGJkZWNmYTkpICgqIDM4ICopDQogICAgICB2YWwgYyA9
IEhIIChjLCBkLCBhLCBiLCB4XzA3LCBTMzMsIDB3eGY2YmI0YjYwKSAoKiAz
OSAqKQ0KICAgICAgdmFsIGIgPSBISCAoYiwgYywgZCwgYSwgeF8xMCwgUzM0
LCAwd3hiZWJmYmM3MCkgKCogNDAgKikNCiAgICAgIHZhbCBhID0gSEggKGEs
IGIsIGMsIGQsIHhfMTMsIFMzMSwgMHd4Mjg5YjdlYzYpICgqIDQxICopDQog
ICAgICB2YWwgZCA9IEhIIChkLCBhLCBiLCBjLCB4XzAwLCBTMzIsIDB3eGVh
YTEyN2ZhKSAoKiA0MiAqKQ0KICAgICAgdmFsIGMgPSBISCAoYywgZCwgYSwg
YiwgeF8wMywgUzMzLCAwd3hkNGVmMzA4NSkgKCogNDMgKikNCiAgICAgIHZh
bCBiID0gSEggKGIsIGMsIGQsIGEsIHhfMDYsIFMzNCwgIDB3eDQ4ODFkMDUp
ICgqIDQ0ICopDQogICAgICB2YWwgYSA9IEhIIChhLCBiLCBjLCBkLCB4XzA5
LCBTMzEsIDB3eGQ5ZDRkMDM5KSAoKiA0NSAqKQ0KICAgICAgdmFsIGQgPSBI
SCAoZCwgYSwgYiwgYywgeF8xMiwgUzMyLCAwd3hlNmRiOTllNSkgKCogNDYg
KikNCiAgICAgIHZhbCBjID0gSEggKGMsIGQsIGEsIGIsIHhfMTUsIFMzMywg
MHd4MWZhMjdjZjgpICgqIDQ3ICopDQogICAgICB2YWwgYiA9IEhIIChiLCBj
LCBkLCBhLCB4XzAyLCBTMzQsIDB3eGM0YWM1NjY1KSAoKiA0OCAqKQ0KCSAg
DQogICAgICAoKiBSb3VuZCA0ICopDQogICAgICB2YWwgYSA9IElJIChhLCBi
LCBjLCBkLCB4XzAwLCBTNDEsIDB3eGY0MjkyMjQ0KSAoKiA0OSAqKQ0KICAg
ICAgdmFsIGQgPSBJSSAoZCwgYSwgYiwgYywgeF8wNywgUzQyLCAwd3g0MzJh
ZmY5NykgKCogNTAgKikNCiAgICAgIHZhbCBjID0gSUkgKGMsIGQsIGEsIGIs
IHhfMTQsIFM0MywgMHd4YWI5NDIzYTcpICgqIDUxICopDQogICAgICB2YWwg
YiA9IElJIChiLCBjLCBkLCBhLCB4XzA1LCBTNDQsIDB3eGZjOTNhMDM5KSAo
KiA1MiAqKQ0KICAgICAgdmFsIGEgPSBJSSAoYSwgYiwgYywgZCwgeF8xMiwg
UzQxLCAwd3g2NTViNTljMykgKCogNTMgKikNCiAgICAgIHZhbCBkID0gSUkg
KGQsIGEsIGIsIGMsIHhfMDMsIFM0MiwgMHd4OGYwY2NjOTIpICgqIDU0ICop
DQogICAgICB2YWwgYyA9IElJIChjLCBkLCBhLCBiLCB4XzEwLCBTNDMsIDB3
eGZmZWZmNDdkKSAoKiA1NSAqKQ0KICAgICAgdmFsIGIgPSBJSSAoYiwgYywg
ZCwgYSwgeF8wMSwgUzQ0LCAwd3g4NTg0NWRkMSkgKCogNTYgKikNCiAgICAg
IHZhbCBhID0gSUkgKGEsIGIsIGMsIGQsIHhfMDgsIFM0MSwgMHd4NmZhODdl
NGYpICgqIDU3ICopDQogICAgICB2YWwgZCA9IElJIChkLCBhLCBiLCBjLCB4
XzE1LCBTNDIsIDB3eGZlMmNlNmUwKSAoKiA1OCAqKQ0KICAgICAgdmFsIGMg
PSBJSSAoYywgZCwgYSwgYiwgeF8wNiwgUzQzLCAwd3hhMzAxNDMxNCkgKCog
NTkgKikNCiAgICAgIHZhbCBiID0gSUkgKGIsIGMsIGQsIGEsIHhfMTMsIFM0
NCwgMHd4NGUwODExYTEpICgqIDYwICopDQogICAgICB2YWwgYSA9IElJIChh
LCBiLCBjLCBkLCB4XzA0LCBTNDEsIDB3eGY3NTM3ZTgyKSAoKiA2MSAqKQ0K
ICAgICAgdmFsIGQgPSBJSSAoZCwgYSwgYiwgYywgeF8xMSwgUzQyLCAwd3hi
ZDNhZjIzNSkgKCogNjIgKikNCiAgICAgIHZhbCBjID0gSUkgKGMsIGQsIGEs
IGIsIHhfMDIsIFM0MywgMHd4MmFkN2QyYmIpICgqIDYzICopDQogICAgICB2
YWwgYiA9IElJIChiLCBjLCBkLCBhLCB4XzA5LCBTNDQsIDB3eGViODZkMzkx
KSAoKiA2NCAqKQ0KDQogICAgICB2YWwgQSA9IFdvcmQzMi4rIChBLGEpDQog
ICAgICB2YWwgQiA9IFdvcmQzMi4rIChCLGIpDQogICAgICB2YWwgQyA9IFdv
cmQzMi4rIChDLGMpDQogICAgICB2YWwgRCA9IFdvcmQzMi4rIChELGQpDQog
ICAgaW4ge0E9QSxCPUIsQz1DLEQ9RH0NCiAgICBlbmQNCg0KICAgIHZhbCBo
eGQgPSAiMDEyMzQ1Njc4OWFiY2RlZiINCiAgICBmdW4gdG9IZXhTdHJpbmcg
diA9IGxldA0KICAgICAgZnVuIGJ5dGUyaGV4IChiLGFjYykgPQ0KCShTdHJp
bmcuc3ViIChoeGQsKFdvcmQ4LnRvSW50IGIpIGRpdiAxNikpOjoNCgkoU3Ry
aW5nLnN1YiAoaHhkLChXb3JkOC50b0ludCBiKSBtb2QgMTYpKTo6YWNjDQog
ICAgICB2YWwgZGlnaXRzID0gV29yZDhWZWN0b3IuZm9sZHIgYnl0ZTJoZXgg
W10gdg0KICAgIGluIFN0cmluZy5pbXBsb2RlIGRpZ2l0cw0KICAgIGVuZA0K
DQogIHZhbCBiNjQgPSAiQUJDREVGR0hJSktMTU5PUFFSU1RVVldYWVphYmNk
ZWZnaGlqa2xtbm9wcXJzdHV2d3h5ejAxMjM0NTY3ODkrLyI7DQogIGZ1biBi
NjRpIG4gPSBTdHJpbmcuc3ViIChiNjQsIFdvcmQ4LnRvSW50IG4pOw0KICBk
YXRhdHlwZSBic3RhdGUgPSBCMCB8IEIyIG9mIFdvcmQ4LndvcmQgfCBCNCBv
ZiBXb3JkOC53b3JkOw0KICBmdW4gdG9CYXNlNjRTdHJpbmcgdiA9DQogICAg
bGV0DQogICAgICBmdW4gYnl0ZXMyYjY0IChiLChCMCxhY2MpKSA9DQogICAg
ICAgIGxldA0KICAgICAgICAgIHZhbCBibSA9IFdvcmQ4Lj4+IChiLDB3MikN
CiAgICAgICAgICB2YWwgYmwgPSBXb3JkOC48PCAoV29yZDguYW5kYiAoYiww
d3gwMyksIDB3NCkNCiAgICAgICAgaW4NCiAgICAgICAgICAoQjIgYmwsIGJt
IDo6IGFjYykNCiAgICAgICAgZW5kDQogICAgICAgIHwgYnl0ZXMyYjY0IChi
LCAoQjIgeCwgYWNjKSkgPQ0KICAgICAgICBsZXQNCiAgICAgICAgICB2YWwg
Ym0gPSBXb3JkOC5vcmIgKHgsIFdvcmQ4Lj4+IChiLDB3NCkpDQogICAgICAg
ICAgdmFsIGJsID0gV29yZDguPDwgKFdvcmQ4LmFuZGIgKGIsMHd4MGYpLCAw
dzIpDQogICAgICAgIGluDQogICAgICAgICAgKEI0IGJsLCBibSA6OiBhY2Mp
DQogICAgICAgIGVuZA0KICAgICAgICB8IGJ5dGVzMmI2NCAoYiwgKEI0IHgs
IGFjYykpID0NCiAgICAgICAgbGV0DQogICAgICAgICAgdmFsIGJtID0gV29y
ZDgub3JiICh4LCBXb3JkOC4+PiAoYiwwdzYpKQ0KICAgICAgICAgIHZhbCBi
bCA9IFdvcmQ4LmFuZGIgKGIsMHd4M2YpDQogICAgICAgIGluDQogICAgICAg
ICAgKEIwLCBibCA6OiBibSA6OiBhY2MpDQogICAgICAgIGVuZA0KICAgICAg
ZnVuIGZpbmFsIChCMCwgYWNjKSA9IGFjYw0KICAgICAgICB8IGZpbmFsIChC
MiB4LCBhY2MpID0geCA6OiBhY2MNCiAgICAgICAgfCBmaW5hbCAoQjQgeCwg
YWNjKSA9IHggOjogYWNjDQogICAgICB2YWwgY2hycyA9IGZpbmFsIChXb3Jk
OFZlY3Rvci5mb2xkbCBieXRlczJiNjQgKEIwLFtdKSB2KQ0KICAgIGluDQog
ICAgICBTdHJpbmcuaW1wbG9kZSAoZm9sZGwgKGZuIChoLHQpID0+IGI2NGkg
aCA6OiB0KSBbXSBjaHJzKQ0KICAgIGVuZDsNCg0KZW5kDQoNCigqI2xpbmUg
MC4wICJzcmMvYmFzaWMvVXNlZnVsLnNpZyIqKQ0KKCogPT09PT09PT09PT09
PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09
PT09PT09PT09PT09PT09PSAqKQ0KKCogTUwgVVRJTElUWSBGVU5DVElPTlMg
ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
ICAgICAgICAqKQ0KKCogQ29weXJpZ2h0IChjKSAyMDAxLTIwMDQgSm9lIEh1
cmQsIGRpc3RyaWJ1dGVkIHVuZGVyIHRoZSBHTlUgR1BMIHZlcnNpb24gMiAq
KQ0KKCogPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09
PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PSAqKQ0KDQpzaWdu
YXR1cmUgVXNlZnVsID0NCnNpZw0KDQoNCmVuZA0KKCojbGluZSAwLjAgInNy
Yy9iYXNpYy9Vc2VmdWwuc21sIiopDQooKiA9PT09PT09PT09PT09PT09PT09
PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09
PT09PT09PT09ICopDQooKiBNTCBVVElMSVRZIEZVTkNUSU9OUyAgICAgICAg
ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
ICopDQooKiBDb3B5cmlnaHQgKGMpIDIwMDEtMjAwNCBKb2UgSHVyZCwgZGlz
dHJpYnV0ZWQgdW5kZXIgdGhlIEdOVSBHUEwgdmVyc2lvbiAyICopDQooKiA9
PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09
PT09PT09PT09PT09PT09PT09PT09PT09PT09ICopDQoNCnN0cnVjdHVyZSBV
c2VmdWwgOj4gVXNlZnVsID0NCnN0cnVjdA0KDQp2YWwgcmVhbF90b19zdHJp
bmcgPSBSZWFsLnRvU3RyaW5nOw0KDQplbmQNCg0KZnVuIG1kNSBzID0NCiAg
bGV0DQogICAgdmFsIG1zdGF0ZSA9IE1ENS51cGRhdGUgKE1ENS5pbml0LCBC
eXRlLnN0cmluZ1RvQnl0ZXMgcykNCiAgICB2YWwgaGFzaCA9IE1ENS5maW5h
bCBtc3RhdGUNCiAgaW4NCiAgICBNRDUudG9CYXNlNjRTdHJpbmcgaGFzaA0K
ICBlbmQ7DQoNCmZ1biB0ZXN0X2Z1biBwIHIgYSA9DQogIGlmIHIgPSBhIHRo
ZW4gcCBhIF4gIlxuIiBlbHNlDQogICAgKHByaW50ICgiXG5cbiIgXg0KICAg
ICAgICAgICAgInRlc3Q6IHNob3VsZCBoYXZlICAgLS0+IiBeIHAgciBeICI8
LS1cbiIgXg0KICAgICAgICAgICAgInRlc3Q6IGFjdHVhbGx5IGhhdmUgLS0+
IiBeIHAgYSBeICI8LS1cbiIpOw0KICAgICByYWlzZSBGYWlsICJ0ZXN0OiBm
YWlsZWQgYSB0ZXN0Iik7DQoNCmZ1biB0ZXN0IHAgciBhID0gcHJpbnQgKHRl
c3RfZnVuIHAgciBhIF4gIlxuIik7DQoNCnZhbCBtZDV0ZXN0cyA9DQogIFso
IiIsICIxQjJNMlk4QXNnVHBnQW1ZN1BoQ2ZnIiksDQogICAoImEiLCAiRE1G
MXVjRHh0cWd4dzVuaWFYY21ZUSIpLA0KICAgKCJhYmMiLCAia0FGUW1EelNU
N0RXbGo5OUtPRi9jZyIpLA0KICAgKCJtZXNzYWdlIGRpZ2VzdCIsICIrV3Rw
Zlh5M2s0MVNXaTh4cXZGaDBBIiksDQogICAoImFiY2RlZmdoaWprbG1ub3Bx
cnN0dXZ3eHl6IiwgIncvelQxMkdTNUFCOSswbHN5bWZoT3ciKSwNCiAgICgi
QUJDREVGR0hJSktMTU5PUFFSU1RVVldYWVphYmNkZWZnaGlqa2xtbm9wcXJz
dHV2d3h5ejAxMjM0NTY3ODkiLA0KICAgICIwWFNybU5KMzJmV2xZUndzbjBH
ZG53IiksDQogICAoIjEyMzQ1Njc4OTAxMjM0NTY3ODkwMTIzNDU2Nzg5MDEy
MzQ1Njc4OTAiIF4NCiAgICAiMTIzNDU2Nzg5MDEyMzQ1Njc4OTAxMjM0NTY3
ODkwMTIzNDU2Nzg5MCIsDQogICAgIlYrMzBvaXZqeVZXc1Nkb3VJUWUyZWci
KV07DQoNCnZhbCAoKSA9IGFwcCAoZm4gKHgseSkgPT4gdGVzdCAoZm4geCA9
PiB4KSB5IChtZDUgeCkpIG1kNXRlc3RzOw0K
---559023410-1804928587-1074035192=:29598--