slim_check

Stream: PR reviews

[Scott Morrison]

@Eric Wieser, your PR #5796 seems to have made my PR "feat: allow slim_check to do work in MetaM #3838" impossible. Could you have a look? I don't really understand what problem you were fixing in #5796, is there some discussion somewhere?

[Scott Morrison]

Could we perhaps do these in the other order? (Pinging @Johan Commelin as they merged #5796.)

[Johan Commelin]

Huh, sorry for causing a hiccup.

[Johan Commelin]

Where exactly is the problem coming from?

[Johan Commelin]

I saw that the PR was making things more universe polymorphic, and the other changes seemed like "fix downstream breakage"...

[Scott Morrison]

The problem is that making things more universe polymorphic is bad idea in tactics, where MetaM works in Type only.

[Scott Morrison]

So adding this universe polymorphism prevents us from generalizing in the monadic direction.

[Scott Morrison]

And I'm not sure what purpose that universe polymorphism is serving.

[Johan Commelin]

Aah, I didn't realize that.

[Johan Commelin]

In that case we should maybe revert this PR. Unless @Eric Wieser has a strong reason for the universe polymorphism.

[Scott Morrison]

It's okay. My MetaM PR didn't have immediate application, in any case, although I thought some about allowing slim_check to use norm_num, which would require something like this change.

[Eric Wieser]

I'll have a look shortly

[Eric Wieser]

Don't we have an unsafe way to drop down a universe level?

[Eric Wieser]

It would be a bit of a shame if slim_check couldn't test basic statements about ULift Nat

[Eric Wieser]

Can you explain what the advantage of adding a m argument to Rand and Gen is? This feels like it's necessary to do something like use dev/urandom as a source of randomness, but it's not clear why this is needed to make evaluating the sample live in MetaM

[Eric Wieser]

(While trying to fix this in a branch, I made #5998 which is rather tangentially related)

[Scott Morrison]

I'll have to have a look again. I made that PR in trying to enable slim_check to run tactics in MetaM to decide whether sampled elements satisfied predicates. (e.g. norm_num) From what I remember, this inevitably led to threading the monad m (presumably always MetaM) into everything, including Gen. It's been a while though, so I may have missed something.