{"action":"closed","issue":{"url":"https://api.github.com/repos/Whiley/WhileyTheoremProver/issues/110","repository_url":"https://api.github.com/repos/Whiley/WhileyTheoremProver","labels_url":"https://api.github.com/repos/Whiley/WhileyTheoremProver/issues/110/labels{/name}","comments_url":"https://api.github.com/repos/Whiley/WhileyTheoremProver/issues/110/comments","events_url":"https://api.github.com/repos/Whiley/WhileyTheoremProver/issues/110/events","html_url":"https://github.com/Whiley/WhileyTheoremProver/issues/110","id":231695175,"number":110,"title":"Performance of Type Checking","user":{"login":"DavePearce","id":484459,"avatar_url":"https://avatars1.githubusercontent.com/u/484459?v=3","gravatar_id":"","url":"https://api.github.com/users/DavePearce","html_url":"https://github.com/DavePearce","followers_url":"https://api.github.com/users/DavePearce/followers","following_url":"https://api.github.com/users/DavePearce/following{/other_user}","gists_url":"https://api.github.com/users/DavePearce/gists{/gist_id}","starred_url":"https://api.github.com/users/DavePearce/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DavePearce/subscriptions","organizations_url":"https://api.github.com/users/DavePearce/orgs","repos_url":"https://api.github.com/users/DavePearce/repos","events_url":"https://api.github.com/users/DavePearce/events{/privacy}","received_events_url":"https://api.github.com/users/DavePearce/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":9,"created_at":"2017-05-26T17:58:07Z","updated_at":"2017-05-28T17:20:55Z","closed_at":"2017-05-28T17:20:55Z","body":"Some test cases are taking a long time to verify because of the type checker.  It's going extremely slowly at times for reasons unknown.  Here are some stats from `BoolList_Valid_3`:\r\n```\r\nASSERT #1...17, 225ms\r\nASSERT #2...25, 330ms\r\nASSERT #3...25, 224ms\r\nASSERT #4...56, 390ms\r\nASSERT #5...65, 423ms\r\nASSERT #6...65, 340ms\r\nASSERT #7...65, 386ms\r\nASSERT #8...116, 680ms\r\nASSERT #9...116, 699ms\r\nASSERT #10...116, 699ms\r\nASSERT #11...119, 755ms\r\nASSERT #12...132, 821ms\r\nASSERT #13...133, 830ms\r\nASSERT #14...132, 840ms\r\nASSERT #15...135, 851ms\r\nASSERT #16...152, 874ms\r\nASSERT #17...155, 885ms\r\nASSERT #18...156, 926ms\r\nASSERT #19...155, 945ms\r\nASSERT #20...158, 960ms\r\nASSERT #21...155, 976ms\r\nASSERT #22...156, 998ms\r\nASSERT #23...301, 1106ms\r\nASSERT #24...314, 1181ms\r\nASSERT #25...314, 1196ms\r\nASSERT #26...314, 1228ms\r\nASSERT #27...118, 955ms\r\nASSERT #28...130, 1011ms\r\nASSERT #29...130, 1027ms\r\nASSERT #30...56, 432ms\r\nASSERT #31...4, 1ms\r\nASSERT #32...6, 0ms\r\nASSERT #33...6, 0ms\r\nASSERT #34...13, 18ms\r\nASSERT #35...28, 64ms\r\nASSERT #36...30, 81ms\r\nASSERT #37...28, 69ms\r\nASSERT #38...35, 110ms\r\nASSERT #39...53, 182ms\r\nASSERT #40...55, 173ms\r\nASSERT #41...55, 183ms\r\nASSERT #42...62, 196ms\r\nASSERT #43...84, 234ms\r\nASSERT #44...84, 242ms\r\nASSERT #45...86, 237ms\r\nASSERT #46...91, 279ms\r\nASSERT #47...109, 347ms\r\nASSERT #48...109, 352ms\r\nASSERT #49...111, 355ms\r\nASSERT #50...116, 411ms\r\nASSERT #51...134, 484ms\r\nASSERT #52...136, 482ms\r\nASSERT #53...136, 482ms\r\nASSERT #54...143, 493ms\r\nASSERT #55...165, 548ms\r\nASSERT #56...167, 553ms\r\nASSERT #57...165, 565ms\r\nASSERT #58...172, 607ms\r\nASSERT #59...190, 676ms\r\nASSERT #60...192, 684ms\r\nASSERT #61...192, 699ms\r\nASSERT #62...199, 728ms\r\nASSERT #63...221, 780ms\r\nASSERT #64...5, 1ms\r\nASSERT #65...39, 2ms\r\nASSERT #66...36, 2ms\r\nASSERT #67...37, 3ms\r\nASSERT #68...36, 3ms\r\nASSERT #69...77, 3ms\r\nASSERT #70...74, 4ms\r\nASSERT #71...75, 5ms\r\nASSERT #72...74, 4ms\r\nASSERT #73...77, 5ms\r\nASSERT #74...86, 14ms\r\nASSERT #75...86, 9ms\r\nASSERT #76...3, 0ms\r\nASSERT #77...6, 25ms\r\nASSERT #78...6, 38ms\r\nASSERT #79...4, 0ms\r\nASSERT #80...5, 31ms\r\nDONE\r\n```\r\n\r\nThe first column is the number of subtype operations, and the second is the overall time for that assert to be type checked.  The generic stats are:\r\n```\r\nParsed 1 source file(s). ...................................................... [101ms+5mb]\r\nTyped 1 source file(s). ................................................... [36594ms-452mb]\r\n```"}}
{"actor":{"display_login":"DavePearce"}}