How to use my own version of ProofWidgets with Mathlib?

Stream: new members

[mars0i]

I'm experimenting with modifications of ProofWidgets (adding things to the Recharts module). I learned from this post that I can get in trouble if I require ProofWidgets separately and in addition to Mathlib, since requiring Mathlib gets ProofWidgets as well.

What's a good way to use a modified version of ProofWidgets with Mathlib? (Hopefully I don't have to have my own copy of Mathlib and everything else.) I can either pull it from my cloned ProofWidgets repo at github, or use a local copy, if there's an easy way to do that (maybe by copying the files into the project where I'm using ProofWidgets??). Thanks.

[Floris van Doorn]

I think you do want a modified version of Mathlib, but the only change that is required (hopefully) is that you update Mathlib's lakefile.lean, and modify the version of proofwidgets it uses, to your own branch/fork.
Then in your own project, you can require your own branch/fork of Mathlib.

If you're a Mathlib contributor, you have write access to branches of Mathlib, which means Github CI will automatically build Mathlib for you, so that you don't have to do this yourself.

[Eric Wieser]

Floris van Doorn said:

I think you do want a modified version of Mathlib, but the only change that is required (hopefully) is that you update Mathlib's lakefile.lean, and modify the version of proofwidgets it uses, to your own branch/fork.

You'll want to push this to github so that you get a cache you can download

[Eric Wieser]

Another option would be to just make your own copy of the Recharts module in your own project, since mathlib doesn't use it anyway.

[mars0i]

Thanks @Floris van Doorn , @Eric Wieser. I'm a little bit confused. Maybe I should have said more about my goals. I'm working on a simple PR for the Recharts part of ProofWidgets. I want to test the modified ProofWidgets before I submit the PR. I want to test it using my own project, which also imports Mathlib.

I'm not sure what your advice is. Is it that rather than submit a PR on github to ProofWidgets, I need to choose or create a branch of Mathlib as a whole to write to it? I don't know the process of adding theorems and such to Mathlib. Maybe it's different from common software package contribution techniques?

Note that since I'm not contributing theorems, but rather contributing code that does something when it runs, the fact that it type checks is not sufficient. So passing CI wouldn't show that my PR is ready.

[Ruben Van de Velde]

I think the easiest approach is to make a branch of mathlib that depends on your branch of proof widgets, and then have your own project depend on that branch of mathlib

[mars0i]

OK, thanks @Ruben Van de Velde

[mars0i]

It feels like a lot to require for a simple 10-line PR to what appears to be a relatively small library (ProofWidgets), though. That's a thought for long-term consideration, maybe. No need for anyone to respond. It makes no difference now. Putting the idea into the air.

[Eric Wieser]

My advice would be to write a test inside the Demos folder of ProofWidgets that doesn't rely on mathlib and your downstream project, because the next contributor to ProofWidgets is otherwise not going to be able to check if they broke anything.

[mars0i]

Yes, that makes sense. First I want to test it on my own project, though.

[mars0i]

And I want to make sure that importing ProofWidgets works with an outside project.

[mars0i]

I forked mathlib. (Maybe I'll ask for write access, but I'd rather start on my own copy.) The original source tree for mathlib doesn't include ProofWidgets; ProofWidgets4 is in a separate repo on github. However, ProofWidgets gets pulled in by lake update, and then it appears in my local copy of mathlib as.lake/packages/proofwidgets/ProofWidgets.

But that's not part of the original mathlib source tree, and a git commit doesn't commit packages under .lake, because the .gitignore file specifies .lake as a directory to be ignored. That makes sense to me, but it doesn't seem that modifying that copy of ProofWidgets under .lakeis the way to contribute to ProofWidgets.

I read through the "How to contribute to mathlib" page, and unless I missed something, it doesn't cover this case. Maybe I don't understand something (quite plausible), but I'm thinking that contributing to an external repo like ProofWidgets or Batteries might involve a different procedure than contributing to the main mathlib source tree. Not sure.

[mars0i]

Oh, I see. I forgot about this comment:
Floris van Doorn said:

I think you do want a modified version of Mathlib, but the only change that is required (hopefully) is that you update Mathlib's lakefile.lean, and modify the version of proofwidgets it uses, to your own branch/fork.
Then in your own project, you can require your own branch/fork of Mathlib.

Sorry about the previous post. (I would delete it, but I can't, and it seemed better to leave the text as is, despite it illustrating some ignorance and lack of attention to Floris's earlier, helpful post.)

[mars0i]

I've continued to work on this, but it's frustrating. (It's a small, unimportant contribution, but I'm treating it as a test case for learning.) Maybe there's something I don't understand, or I've made a mistake.

It appears that the basic mismatch between the helpful advice above and my strategy is that I feel that if I'm going to have outside projects depend on something in ProofWidgets4, I want to test using it as a dependency in my project. I do test my changes in the Demos directory of ProofWidgets4, and it works, but I still think that one should test using it as a dependency from outside. That is what makes this difficult, it seems.

I want my project to depend on a version of mathlib that includes my modified ProofWidgets4. I have set up my copy of mathlib, with a lakefile.lean that points to my version of ProofWidgets4. Each have their own branches, so in theory I could ask for write access to mathlib and submit my version of mathlib for CI, as I understand it. However, that would mean that I'm asking to run a version of mathlib that points to an outside library (my ProofWidgets4 repo in github). I don't know whether that would work, but it seems wrong. (Is this incorrect?) But I don't want my PR to be accepted unless I've tested it properly, so I can't wait for the PR to be accepted to do this.

OK, now the problem is that I have to build mathlib on my computer. I did this once, and then accidentally made a change (that was not really a change) in ProofWidgets4, so I had to build mathlib again. Now I have found that in order to use the new ProofWidgets4 in my own project, I am building mathlib again!

I am wondering whether trying to test a modified component of mathlib as a dependency in a separate library is just not something covered by the usual procedures.

I think the reason I have to build mathlib in my project might be because lake exe cache get wants to get executables from the main lean4 site, but my executables aren't there. Or maybe not. I don't understand what lake exe cache get does. Here is what I tried most recently:

~/docs/src/LeanProver/ChaosLean(main)*$ lake exe cache get
warning: proofwidgets: repository '././.lake/packages/proofwidgets' has local changes
warning: proofwidgets: repository '././.lake/packages/proofwidgets' has local changes
✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required builds logged failures:
- proofwidgets:release
error: build failed
uncaught exception: Failed to validate ProofWidgets cloud release: lake failed with error code 1
~/docs/src/LeanProver/ChaosLean(main)*$ lake build
warning: proofwidgets: repository '././.lake/packages/proofwidgets' has local changes
Build completed successfully.
~/docs/src/LeanProver/ChaosLean(main)*$ /bin/rm -Rf .lake/packages/proofwidgets/
~/docs/src/LeanProver/ChaosLean(main)*$ lake build
info: proofwidgets: cloning https://github.com/mars0i/ProofWidgets4.git
info: proofwidgets: checking out revision '70d004a66abec5814fbfe45f30f881c0cb8e17de'
Build completed successfully.
~/docs/src/LeanProver/ChaosLean(main)*$ lake exe cache get
✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required builds logged failures:
- proofwidgets:release
error: build failed
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1

Here is the ChaosLean project's lakefile.lean:

import Lake
open Lake DSL

package "ChaosLean" where
  version := v!"0.1.0"

lean_lib «ChaosLean» where
  require mathlib from git "https://github.com/mars0i/mathlib4.git" @ "ProofWidgetsRechartAxisType"

@[default_target]
lean_exe "chaoslean" where
  root := `Main

That version of mathlib's lakefile.lean includes this:

-- require "leanprover-community" / "proofwidgets" @ git "v0.0.48"
require proofwidgets from git "https://github.com/mars0i/ProofWidgets4.git" @ "RechartsAxisType"

The lakefile.lean in my copy of ProofWidgets4 is unchanged from the original. (Is that what it should be?)

Thanks.

[Ruben Van de Velde]

I suspect the mathlib maintainers would not object to you using the mathlib ci to test mathlib against an in-progress proof widgets pr

[Ruben Van de Velde]

I think your instincts are reasonable, btw, but in practice making changes to mathlib (including in this edge case) outside of the main repo is going to make life harder than necessary

[Anand Rao Tadipatri]

If you have npm installed locally, I think it should be possible to add your modified version of ProofWidgets as a dependency to your repository directly (without modifying Mathlib), and then build the JS files by going to the local copy of your repository within .lake/packages/ and then running lake build widgetJsAll.

[mars0i]

Thanks @Anand Rao Tadipatri! That's very helpful. I didn't know where to start with that process.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Eric Wieser said:

My advice would be to write a test inside the Demos folder of ProofWidgets that doesn't rely on mathlib and your downstream project, because the next contributor to ProofWidgets is otherwise not going to be able to check if they broke anything.

I strongly second this recommendation.

I do test my changes in the Demos directory of ProofWidgets4, and it works, but I still think that one should test using it as a dependency from outside.

You really don't have to do this if you're just adding visualization features :) The only changes that need additional testing in a downstream package are changes that impact cross-package interactions: changes to the build process, packages, pulling in additional dependencies, etc. Since your project depends on mathlib, and building mathlib is very heavy, you are making it unnecessarily difficult for yourself to test the changes by waiting on the combined PW4-mathlib-ChaosLean build.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I think the reason I have to build mathlib in my project might be because lake exe cache get wants to get executables from the main lean4 site, but my executables aren't there. Or maybe not. I don't understand what lake exe cache get does.

lake exe cache getdownloads a prebuilt version of mathlib from a cloud cache so that you don't have to build it locally. But for that prebuilt version to exist in the cloud cache, you first need to push its source code to some branch on leanprover-community/mathlib4. Commits there will be automatically processed by the leanprover-community CI infrastructure and uploaded to the cloud cache. That is why it's always recommended on this Zulip that you push to a branch on leanprover-community/mathlib4.

That version of mathlib's lakefile.lean includes this:

Your lakefile.lean looks reasonable. You need to point to a version of ProofWidgets4 available on GitHub and including your changes, and I guess RechartsAxisType has that.

[mars0i]

Thanks @Wojciech Nawrocki.

Wojciech Nawrocki said:

I do test my changes in the Demos directory of ProofWidgets4, and it works, but I still think that one should test using it as a dependency from outside.

You really don't have to do this if you're just adding visualization features :) The only changes that need additional testing in a downstream package are changes that impact cross-package interactions: changes to the build process, packages, pulling in additional dependencies, etc. Since your project depends on mathlib, and building mathlib is very heavy, you are making it unnecessarily difficult for yourself to test the changes by waiting on the combined PW4-mathlib-ChaosLean build.

Thanks--this is helpful. Thanks also for confirming and clarifying re lake exe cache get.

I'm not worried about breaking something--ProofWidgets4 , mathlib, or my project. It's more that I just want to verify the functionality: to see that the changes behave as expected in a different context. I do think that in this particular case, it's hard to see how things would behave differently in my project as opposed to the modified test I made in Demos/Plot.lean. So testing in my project felt like overkill even from my point of view. However, when dealing with unfamiliar code, even if I think I understand it, I try not to assume that my understanding is correct, especially when contributing to someone else's package. I'd rather err on the side of thinking that I'm ignorant.

[mars0i]

I accept that this isn't necessary, but I'm having trouble getting the branch that I pushed to mathlib to work correctly when I require it in my project. Maybe it would be useful to understand what's going on for future work.

My mathlib branch, ProofWidgetsRechartAxisType, differs from the master branch (at the time I created it) only in that lakefile.lean contains this replacement:

-- require "leanprover-community" / "proofwidgets" @ git "v0.0.48"
require proofwidgets from git "https://github.com/mars0i/ProofWidgets4.git" @ "RechartsAxisType"

The RechartsAxisType branch of ProofWidgets4 contains my changes. My project, ChaosLean, has this in its lakefile.lean (which is otherwise the lakefile generated by lake new):

lean_lib «ChaosLean» where
  require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "ProofWidgetsRechartAxisType"

which I understand should get the version of mathlib generated by CI on my branch ProofWidgetsRechartAxisType.

However, the code behaves as if it was using the unmodified ProofWidgets4. I looked in .lake/packages/proofwidgets/, and the source files there don't reflect my changes in the RechartsAxisType branch on https://github.com/mars0i/ProofWidgets4.

[mars0i]

If I remove .lake/packages/proofwidgets and run lake exe cache get, I see:

info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '2b000e02d50394af68cfb4770a291113d94801b5'
No files to download
Decompressing 5794 file(s)
Unpacked in 1245 ms
Completed successfully!

So it seems that this is not getting my version of ProofWidgets4 from my git account.

[mars0i]

Maybe in the branch I pushed to mathlib4, I also needed to regenerate lake-manifest.json? I see that that file in my ProofWidgetsRechartAxisType branch of mathlib4 references the standard version of ProofWidgets4 in leanprover-community.

[mars0i]

I tried modifying lake-manifest.json, replacing the line that pointed to the leanprover-community version of ProofWidgets4 with

  {"url": "https://github.com/mars0i/ProofWidgets4.git",

and also replaced reference to the ProofWidgets4 version number with

   "inputRev": "RechartsAxisType",

These are pure experiments--no idea whether this was a good idea. I get a CI failure at the step "Get cache":

 ✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
error: build failed
Some required builds logged failures:
- proofwidgets:release
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1

Maybe this means that it can't get a compiled version from the version of the git repo on my account, which makes sense, since that isn't there.

Giving up. I'm not upset about it. Maybe there's a way to do this, but it's not worth the trouble for this contribution, at least, to try to test my modification to ProofWidgets4 with my own project that uses ProofWidgets4.

[Eric Wieser]

You should change the lakefile not the manifest

[Eric Wieser]

(then run lake update)

[Ruben Van de Velde]

The cloud release may still be an issue

[mars0i]

Thanks @Eric Wieser-- Right--I did change the lakefile, but the result was that when I made my own project depend on this branch of mathlib, it got the original version of ProofWidgets4 from leanprover-community, rather than the version in my github account that I had referenced in lakefile.lean. However, I saw that lake-manifest.json was still pointing to the leanprover-community version, so I thought I'd try modifying lake-manifest.json.

[mars0i]

Thanks @Ruben Van de Velde. I've seen references to the cloud release, but I don't know what that refers to.

[mars0i]

@Eric Wieser I didn't try running lake update. Will try that now. Thanks.

[Eric Wieser]

I guess lake update ProofWidgets is the command you actually want

[Eric Wieser]

You are right to look at the manifest to determine if the right library version ended up being used

[mars0i]

lake build did update lake-manifest.json to point to my account's ProofWidgets4, but I'm getting almost the same error as from my hand-edited lake-manifest.json:

✖ [2/2] Running proofwidgets:release
error: build failed
error: failed to fetch GitHub release (run with '-v' for details)
Some required builds logged failures:
- proofwidgets:release
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1

[mars0i]

i.e. first I restored the old lake-manifest.json from before I started editing it, and then I ran lake update.

[Eric Wieser]

I think proofwidgets might have a custom flag you have to pass to say "don't use the github release"

[mars0i]

The ProofWidgets4 README.md says

ProofWidgets is configured to use Lake's cloud releases feature which will automatically fetch pre-built JavaScript files as long as you require a release tag rather than the main branch.

Does that a variant of the custom flag idea? I assume the release tag is "v0.0.48" in

require "leanprover-community" / "proofwidgets" @ git "v0.0.48"

which is what mathlib master branch's lakefile.lean said. But I'm not using a release tag, I guess. My mathlib branch's lakefile.lean says:

require proofwidgets from git "https://github.com/mars0i/ProofWidgets4.git" @ "RechartsAxisType"

(Again, this is probably not worth the trouble for this particular contribution to ProofWidgets4. If it's worth the trouble, that would be for future use.)

[mars0i]

There's also a tip in the README about building ProofWidgets4 using npm, which I could do in theory, but I'd rather not figure out how to do that.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

lake build did update lake-manifest.json to point to my account's ProofWidgets4

Somebody please correct me if this is incorrect, but afaik after changing lakefile.lean you need to run lake update (or specifically lake update proofwidgets to just update the one package) for lake-manifest.json to change. lake build will not do this.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

mars0i said:

There's also a tip in the README about building ProofWidgets4 using npm, which I could do in theory, but I'd rather not figure out how to do that.

The cloud release error you are seeing means that Lake does not even try to build PW4 using npm. If it did try that, you should be good: you need to have npm installed and available, but after that everything is handled for you by the Lake build. Unfortunately I do not understand why after the cloud release fails to download, the ordinary build is not tried.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hm, the following works for me when I try it locally:

1. Replace require "leanprover-community" / "proofwidgets" with require proofwidgets from git "https://github.com/mars0i/ProofWidgets4" @ "RechartsAxisType" in lakefile.lean
2. Run lake update proofwidgets
3. Run lake build - this runs npm as expected

[mars0i]

Wojciech Nawrocki said:

lake build did update lake-manifest.json to point to my account's ProofWidgets4

Somebody please correct me if this is incorrect, but afaik after changing lakefile.lean you need to run lake update (or specifically lake update proofwidgets to just update the one package) for lake-manifest.json to change. lake build will not do this.

Sorry, I meant that I ran lake update.

[mars0i]

I started to run lake build but it looked like it was going to go into the 12-hour process, so I killed it. But I'll try it again and let it run.

[Eric Wieser]

Every time you change ProofWidgets, you do indeed have to rebuild the (large) parts of mathlib downstream of it

[Eric Wieser]

You can get mathlib CI to do the build for you on faster machines if you create a mathlib branch first, which will be a ~1hr process

[mars0i]

That's how I was thinking about it. lake update and then push to mathlib, and wait and see what happens. That's how I got the CI error.

[mars0i]

Wojciech Nawrocki said:

Hm, the following works for me when I try it locally:

1. Replace require "leanprover-community" / "proofwidgets" with require proofwidgets from git "https://github.com/mars0i/ProofWidgets4" @ "RechartsAxisType" in lakefile.lean
2. Run lake update proofwidgets
3. Run lake build - this runs npm as expected

That worked for me, too (although it took a long time). But this won't allow me to require the modified mathlib in my other project. Or in any event, I don't know how to do that, other than by causing lake to get mathlib binaries from leanprover.community/mathlib.

After lake build, I have mathlib binaries on my local machine, right? So in theory it would make sense that there should be a way to set up my ChaosLean project to use those binaries in order to require mathlib. (Or if I downloaded the binaries using lake update or lake exe cache get, I have them on my local machine as well, right?) Why should it be necessary to download the mathlib binaries from leanprover-community/mathlib if I already have them somewhere? But as I understand it, getting mathlib binaries from a local source isn't normally done. Maybe it hasn't been thought necessary for most of what people have been doing with Lean, so there's not a procedure for it. I may misunderstand, though. My lack of understanding is very great.