search

sbp / idris-bi

Idris Binary Integer Arithmetic, porting PArith, NArith, and ZArith from Coq
https://github.com/idris-lang/Idris-dev/issues/3976
36 stars 5 forks source link

The Last BIP #15

Closed clayrat closed 7 years ago

clayrat commented 7 years ago
clayrat commented 7 years ago

Only "compatibility facts" from Pnat.v now remain, let's maybe do those another time.

clayrat commented 7 years ago

@sbp What do you think?

sbp commented 7 years ago

Good work, as usual! It's a shame that you had to split the proofs up, but they were getting extremely slow to type check. Do you think it's worth opening an issue for slow type checking, if there isn't one already? There are probably some low-hanging-fruit optimisations that can be done, it might be worth profiling to see what's taking all the time. As for Pnat.v, that's fine to kick into the long grass for now. I think concentrating on Bin would be good. For the most part I was hoping that these would be largely defined in terms of congruences with Bip since Bin is effectively just a Bip wrapper with an extra constructor for the zero case, but it didn't turn out to be that way and exceeded my capabilities to prove. At that point I figured I should study your Bip proofs to understand how to move forward with some of the Bin proofs that were missing, but I just haven't had the time to do that sort of analysis yet. Instead I figured I should at least work on some of the easier Biz proofs, but I haven't had time to do that either. And I also wanted to document the whole thing, in ReST, in some nice documentation that would lead the way in showing how Idris should be implemented but sadly isn't. And of course I didn't have time for that yet either! In summary, you are working far more efficiently and persistently than I am, and I feel somewhat sheepish that I am now so far behind in terms of overall effort contributed to the project that I am so interested in bringing forward to completion. I'll give it as much time as I'm able to!

P.S. make check was broken by this PR, but I'll just fix that in a later commit.