search

Toxaris / pts

Interpreter for functional pure type systems.
BSD 3-Clause "New" or "Revised" License
21 stars 7 forks source link

Changes performed on vacation in Austria #106

Closed Toxaris closed 9 years ago

Toxaris commented 9 years ago

I changed quite a bit about the pts interpreter while on vacation (not so much from work, but certainly from the internet). Most importantly, see f4c65a0a88b5a978b0c17fdec54b703062b4bcfb and 3d3be1db5fcdee2171466808c38df524fbf1287c.

Not sure what to do about this. I'm not super motivated to split it up into multiple pull requests.

Toxaris commented 9 years ago

Teaser: With these changes, checking UU.lpts takes less than 1sec on my laptop -- I hope everything is actually checked ;)

Blaisorblade commented 9 years ago

Not sure what to do about this. I'm not super motivated to split it up into multiple pull requests.

Can relate to that. Do you want me to try reviewing this at all?

Blaisorblade commented 9 years ago

Do you want me to try reviewing this at all?

I'll take at least a look at the commit messages, and maybe sample-review them — later. Up to now, this looks like lots of stuff you had already proposed and which makes sense :-)

Toxaris commented 9 years ago

At some point (maybe after merging?) we should look at the two commits mentioned in the description of the pull request above. Everything else is reasonably straight-forward.

Blaisorblade commented 9 years ago

I've taken a cursory look at everything but 3d3be1db5fcdee2171466808c38df524fbf1287c. I'd be a bit more comfortable to test this at least on all of tsr-experiments (by writing a shell script with the right options) — but we have few negative tests anyway.

Also, this seems to fix #99.

Let's just merge this, and deal with any unlikely breakage later.

Blaisorblade commented 9 years ago

Teaser: With these changes, checking UU.lpts takes less than 1sec on my laptop -- I hope everything is actually checked ;)

I hadn't realized, but that's compared to ~10 s without these changes (because there's much more code now). Congratulations on a 10x speedup while even reducing the amount of code (the core code is probably still a bit more, given the amount of dropped dead code, but still very cool).