chore: import ProofWidgets, so tests work#11350
Conversation
|
bors d+ |
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
| -- Currently we don't need to import all of ProofWidgets, | ||
| -- but without this, if you don't run `lake build ProofWidgets` then `make test` will fail. | ||
| -- Hopefully `lake` will be able to handle tests later. | ||
| import ProofWidgets |
There was a problem hiding this comment.
This adds an MIT-licensed dependency to Mathlib (threejs and recharts), which is otherwise Apache-licensed; can you use a more fine-grained import?
There was a problem hiding this comment.
Perhaps more pragmatically; do we really want to add dependencies to all mathlib users to save one line in a CI script?
There was a problem hiding this comment.
What's the legal theory here?
There was a problem hiding this comment.
Maybe I'm imagining the legal issue, certainly I misremembered the relative strength of the licenses.
There was a problem hiding this comment.
I'm no lawyer so don't take what I'm saying very seriously, but MIT is extremely permissive, and it says it only requires that the license notice be included with the copy. It's even preserved when cloned by lake as .lake/packages/proofwidgets/LICENSE, in case that matters.
There was a problem hiding this comment.
Does replacing the middle line with lake build Mathlib ProofWidgets work?
There was a problem hiding this comment.
Yes, but that that's still a terrible user experience to need to know that!
There was a problem hiding this comment.
@eric-wieser, did you want to minimize imports? If not I'll merge as is?
There was a problem hiding this comment.
I'm curious what @digama0's thoughts are here (about adding the dependency, I think my license concerns are moot).
Is there a reason that adding lake build into make test is a bad option?
There was a problem hiding this comment.
Adding at least lake build ProofWidgets seems sound. As for adding the dependency, shake is not in the business of prescribing Mathlib's policy toward intentionally broad imports, that's why noshake.json exists (esp. the ignoreImport list). I have no strong opinions regarding whether import Mathlib should imply import ProofWidgets, but I agree that we should make the tests work without this additional step, and the right place to put import ProofWidgets is in the make test target. (The actual right place is in lake but until lake test comes about we have to do it the hard way.)
|
This should have been a bors merge not a regular one, right? |
Currently you need to run ``` lake build ProofWidgets make tests ``` to reliably get tests to work. --- <!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Co-authored-by: Author Name <author@email.com> Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> [](https://gitpod.io/from-referrer/)
Currently you need to run ``` lake build ProofWidgets make tests ``` to reliably get tests to work. --- <!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Co-authored-by: Author Name <author@email.com> Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> [](https://gitpod.io/from-referrer/)
Currently you need to run ``` lake build ProofWidgets make tests ``` to reliably get tests to work. --- <!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Co-authored-by: Author Name <author@email.com> Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> [](https://gitpod.io/from-referrer/)
Currently you need to run ``` lake build ProofWidgets make tests ``` to reliably get tests to work. --- <!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Co-authored-by: Author Name <author@email.com> Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> [](https://gitpod.io/from-referrer/)
Currently you need to run ``` lake build ProofWidgets make tests ``` to reliably get tests to work. --- <!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Co-authored-by: Author Name <author@email.com> Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> [](https://gitpod.io/from-referrer/)
Currently you need to run ``` lake build ProofWidgets make tests ``` to reliably get tests to work. --- <!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Co-authored-by: Author Name <author@email.com> Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> [](https://gitpod.io/from-referrer/)
Currently you need to run
to reliably get tests to work.