Deriving Repr when there are dependent proofs

Stream: new members

[Vivek Rajesh Joshi]

I'm unable to use deriving Repr here:

inductive ElemOp : Type where
| scalarMul (c : Rat) (hc : c≠0) (i : Fin m) : ElemOp
| rowSwap (i : Fin m) (j : Fin m) : ElemOp
| rowMulAdd (c : Rat) (i : Fin m) (j : Fin m) : ElemOp
--deriving Repr

And it's because of hc : c≠0 (if removed, I can use it). Does anyone know a way around this, or another way to make this function "eval-friendly"?

[Kyle Miller]

What does #eval Lean.versionString say? This should be fixed in 4.8.0

[Vivek Rajesh Joshi]

"4.8.0-rc1"

[Kyle Miller]

Oh right, this was fixed after 4.8.0 (lean4#3944). It's in 4.9.0-rc1 (which is what the current mathlib uses).

[Vivek Rajesh Joshi]

Is 4.9.0 now the latest release?

[Yaël Dillies]

4.9.0 doesn't exist yet. It will in a month, once 4.9.0-rc1 has been battle-tested

[Vivek Rajesh Joshi]

Ahh, I see

[Yaël Dillies]

(rc stands for Release Candidate, if you hadn't clocked it)

[Vivek Rajesh Joshi]

Yeah I got that

[Yaël Dillies]

So right now the latest release in 4.9.0-rc1, and the latest stable is 4.8.0

[Vivek Rajesh Joshi]

On a side note, do you have instructions for updating Mathlib? I keep encountering outdated instructions whenever I search for it

[Kevin Buzzard]

Always look on leanprover-community or the mathlib README for questions like that

[Yaël Dillies]

This scripts has been failsafe for the two years I've used it: https://github.com/YaelDillies/LeanAPAP/blob/master/scripts/update_mathlib.sh

[Yaël Dillies]

Kevin Buzzard said:

Always look on leanprover-community or the mathlib README for questions like that

In that specific case, it seems my script is strictly better

[Kyle Miller]

Three options for getting a Repr instance here:

1. Write a Repr instance manually.
2. Copy the core Repr derive handler into your own project in the meantime.
3. Upgrade to 4.9.0-rc1.

[Kevin Buzzard]

I think that pointing users to "random code I wrote once" is unwise, as in two years' time when you've stopped working on the project and users are randomly searching Zulip the script might fail. If you're not happy with the community instructions then make a PR

[Kevin Buzzard]

(@Yaël)

[Yaël Dillies]

My point is I haven't updated this script for two years and it still works

[Yaël Dillies]

I personally think we should make it a script available in mathlib so that downstream users don't have to think about it

[Kevin Buzzard]

My point is that you should be wary of advertising your script as "the right way and better than the community website" because it might not work in 2 years' time whereas the community web pages will work.

[Yaël Dillies]

Sure, which is why I suggest we make my script the community version

[Kevin Buzzard]

I once saw someone posting here some time ago saying "I followed the installation instructions on some random xenaproject blog post and now everything is broken" and I looked at the page and it said in big letters at the top "THIS PAGE IS OUT OF DATE" but someone was reading it anyway. I deleted the post entirely.

[Kevin Buzzard]

Yaël Dillies said:

Sure, which is why I suggest we make my script the community version

And I'm saying that the canonical way to do this isn't just to say that here but to pass your exam tomorrow (good luck!) and then make a PR

[Vivek Rajesh Joshi]

Kyle Miller said:

Upgrade to 4.9.0-rc1.

Again, not very familiar with the code used to manage Lean and Mathlib versions so I'll have to ask: How do I upgrade Lean4 manually? The VS Code extension says that it was last updated on 2024-06-07. Is there a way to update it using VS Code itself?

[Yaël Dillies]

The vscode extension has a completely different versioning system to Lean/Mathlib. You shouldn't worry about it

[Vivek Rajesh Joshi]

Okay, but how do I update it to 4.90 rc1?

[Yaël Dillies]

You look at https://github.com/leanprover-community/mathlib4/blob/master/lean-toolchain, copy-paste the content to your lean-toolchain file, run lake -R update

[Vivek Rajesh Joshi]

Okay, I did exactly that and now my imports have failed. Any fix?

[Yaël Dillies]

Can you be more precise in how they failed?

[Yaël Dillies]

Sorry btw the last command should lake -R -K update. It's always incorrect to run -R without -K

[Vivek Rajesh Joshi]

Yaël Dillies said:

Can you be more precise in how they failed?

image.png

[Vivek Rajesh Joshi]

Yaël Dillies said:

Sorry btw the last command should lake -R -K update. It's always incorrect to run -R without -K

error : missing command

[Yaël Dillies]

Can you undo the last few operations, bust the .lake folder and run the following commands: https://github.com/YaelDillies/LeanAPAP/blob/master/scripts/update_mathlib.sh

[Vivek Rajesh Joshi]

Is it possible to undo commands from the command line?

[Yaël Dillies]

No, but surely you are working on some git repository?

[Vivek Rajesh Joshi]

Yes

[Vivek Rajesh Joshi]

I haven't pushed any of these changes though

[Yaël Dillies]

Great, discard them

[Yaël Dillies]

(assuming "these changes" doesn't include anything but the failed update)

[Vivek Rajesh Joshi]

I don't know why, but pulling changes from the online repo isn't working. I copy-pasted the config files from the online repo (hadn't been updated in 3 weeks) and I'm still getting the same error

[Vivek Rajesh Joshi]

I think my mathlib is messed up. Should I copy-paste another mathlib that I have downloaded in a different folder?

[Yaël Dillies]

Can you delete the local copy of your project and start afresh?

[Vivek Rajesh Joshi]

Like create a new repository or rewrite all of the code?

[Yaël Dillies]

Delete the local copy of your repository and clone it again

[Vivek Rajesh Joshi]

Alright, looks like everything is back in working condition again. Thanks for the help!