slimcheck tactic for lean 4?

Stream: lean4

[Daniel Patterson]

I see that the bulk of SlimCheck has been ported to Lean 4 (both inside of Mathlib4, and also existing sort of independently in LSpec). It doesn't seem to have the tactic that existed in the Lean 3 version, that ran it and, if no counter-example was found, admited the proof. Does anyone have an implementation of that floating around?

[Mario Carneiro]

not as far as I know

[Mario Carneiro]

it is on the todo list, it should not be too hard

[Alex J. Best]

I've not used it but maybe Lspec is helpful here in the interim https://github.com/lurk-lab/LSpec#integration-with-slimcheck

[Daniel Patterson]

@Alex J. Best I can _run_ the tests fine, I just was hoping for the tactic connection.

@Mario Carneiro Yes, doesn't seem like it would be hard with knowledge of elab / etc... which I was hoping to not have to learn, at least not _right now_ :)

[Scott Morrison]

!4#1103 is the issue tracking this. Maybe soon, perhaps. :-)

[Daniel Patterson]

@Scott Morrison thanks :) Though hoped for in Dec and not yet done... :(

[Scott Morrison]

@Daniel Patterson , please review !4#3114.

[Daniel Patterson]

@Scott Morrison Wow! This looks amazing! I haven't been able to try it though as my binary search for a toolchain that'll build it hasn't been successful (tried latest, 2023-03-25, then 2023-03-17, whats in mathlib4 repo, then 2023-02-22, what's in aesop, then 2023-02-24, whats in std4, and then I gave up -- each had build errors on different modules, all in dependencies before Mathlib.Tactic.SlimCheck...)

[Scott Morrison]

That's strange, and surely something messed up on your system, given that it builds in CI.

[Scott Morrison]

In that branch I have

% cat lean-toolchain
leanprover/lean4:nightly-2023-03-17

so you certainly shouldn't be trying anything except that.

[Scott Morrison]

I would checkout the branch, maybe try some of:

• git clean -xfd
• rm -rf lake-packages/
• lake exe cache get
• lake exe cache get!

[Scott Morrison]

@Daniel Patterson, did you ever get this sorted? I don't like the idea of leaving you without a working toolchain. :-)

[Daniel Patterson]

@Scott Morrison Sorry for the delay. It's been a very busy week! I just rebuilt stuff, and obviously there was some stale cached thing that was breaking stuff, as it all built fine, and the tactic works, so thanks!

So, really, thanks again -- it'll be in front of a couple hundred students next week (as a demo, not in their hands...). It allows me to sort of come full circle in a nice way, as we _started_ with property-based testing (not in Lean), then moved to lean (in order to do _proofs_), and being able to circle back to PBT as we get to the last few weeks of class is really nice.

[Scott Morrison]

@Daniel Patterson, are you missing the functionality for testing lists? I noticed that this was missing from the existing port of the core slim_check code, but didn't investigate adding it. If this is useful I can either try it myself or prod someone with better comparative advantage. :-)

[Daniel Patterson]

It would certainly be nice (for examples) but I can probably work around it. It’s not just a matter of declaring type class instances for them?

[Scott Morrison]

Yes, presumably it's easy.