>>>> 3. I don't see any boundaries where you describe -- can you say more? >>> >>> Run typed-performance.rkt and see: >> >> This might be related to >> https://github.com/racket/typed-racket/issues/289. >> > > So basically my unsafe-reprovide module should probably use some syntax > trickery to generate new bindings for all typed provides it requires and > re-provide them unsafely renaming them back to original name? I think I > can do something like that using relatively simple syntax macro. > > Do I understand it correctly? > > Of course Ben's hint at unsafe-reprovide is something I'd like to > investigate.
My hint turned into a PR and merged a few years ago. https://github.com/racket/typed-racket/pull/657 Here's the output I see from `typed-performance.rkt` . I'm on a commit from Jan 20. Does this look more like you'd expect? ``` --- typed: cpu time: 2990 real time: 3023 gc time: 65 unsafe: cpu time: 405 real time: 408 gc time: 5 typed, unsafe provided: cpu time: 692 real time: 697 gc time: 10 plain: cpu time: 748 real time: 752 gc time: 3 --- typed: cpu time: 2817 real time: 2825 gc time: 11 unsafe: cpu time: 414 real time: 417 gc time: 3 typed, unsafe provided: cpu time: 671 real time: 675 gc time: 4 plain: cpu time: 750 real time: 754 gc time: 5 === --- typed: cpu time: 1678 real time: 1684 gc time: 0 unsafe: cpu time: 161 real time: 165 gc time: 0 typed, unsafe provided: cpu time: 175 real time: 178 gc time: 0 plain: cpu time: 180 real time: 184 gc time: 0 --- typed: cpu time: 1744 real time: 1755 gc time: 0 unsafe: cpu time: 165 real time: 168 gc time: 0 typed, unsafe provided: cpu time: 164 real time: 167 gc time: 0 plain: cpu time: 195 real time: 198 gc time: 0 ``` -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAFUu9R4SX5BePy%2BNwM76iMrF%2BoMdtjxmZGKcS94USJ%2B8aHR5HQ%40mail.gmail.com.
