New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Proposal for Stdlib Contributions [RFC] #528
Comments
@leodemoura, @Kha please tag this as I've helped with the RFC, am supportive of it, and it seems to align well with various internal conversations we had. |
This is great, but we need to prepare for it. @Kha and I have been discussing a package reorganization. @Kha: How will the module system you are designing impact this RFC? @tydeu: You floated the idea of putting most types and definitions at We should also add guidelines for theorems. I am assuming many will want to contribute theorems about the functions and types being defined at |
@DanielFabian I will add the tag as soon as we figure out the details described in my previous message. |
Since @leodemoura mentioned me, I will reaffirm that I do still very strongly support this idea. I am also willingly to make the changes necessary to do so should that be desired (though I can see that such a change might be too sensitive for someone less experienced, like myself, to make). |
This raises an interesting question. Do we want complex (non- |
I'm not sure it should impact it at all. Certainly partitioning modules into packages should be mostly independent of it, that is a different organization layer. Where to put proofs as well, as long as we keep a non-signature import around (which I'm relatively sure we'll want to), moving them into a separate module or even package should not be any harder than it is right now. If we really want to fine-tune separate compilation of Lean itself, we may want a smaller prelude (i.e. default import). But as Gabriel said, separate compilation of the core lib doesn't really impact users since any change in the core will most likely change the Lean binary as well, so external Lean packages should be recompiled completely either way. So it might make more sense to keep the prelude roughly as it is right now and make use of explicit |
@Kha What about this one?
|
this feels like fairly orthogonal. How are tactics related to I for one am not even convinced it's desirable to have proofs sit next to the basic functions. It might well make sense to have proofs about them sit in a different namespace or package. Also, how could a |
It is natural to have theorems for functions, and theorems use tactics. Moreover, the tactic was just an example. When we improved
We can have them in different files, but it feels too drastic to use a different package. |
I get the argument, but only half way. By having a richer library, you can express some idioms more concisely using a helper and if the code needs to change, it may well only have to change in the implementation of the helper as opposed to each call-site. A classic example is a If a helper is not used at all in the code base, then the argument holds of course. |
@DanielFabian We should continue the discussion in a face-to-face meeting. I am not managing to convey how painful the bootstrapping issues are here, and why we must minimize the number of dependencies we need to build the Lean binary. It is taking to much time to make the point here in asynchronous media. |
I would recommend you spend some time "designing" your "namespaces" first, then this provides a framework for stuff to be filled in. Then the "standard library" needs some really clear "design principles" to help decide what goes in and what doesn't. Then this all needs to be posted someplace so we can all see it. |
The current standard library in the Lean core is lacking many common utility functions. One way to go about fleshing it out is to allow the community to contributed useful utilities. However, such contributions would likely be small and thus not really suited for the current multi-step RFC contributing process. Instead, it would be nice to be able to fast track such small changes. To help make the process less unwieldy, we can provide examples of which contributions would be welcome and which would not. For example, we probably would want functions like
List.nth
, but may wish to relegate syntactic extensions to the formal RFC process.To give an idea of what we want to evolve Lean's standard library into, we can take cues from, for instance, F# and Haskell:
Note: For the Haskell references, it should be observed that Haskell is (usually) lazy and Lean is strict, so some utilities will not translate.
The text was updated successfully, but these errors were encountered: