Absolute value for Float

Stream: lean4

[Henrik Böving]

Do we have an absolute value function for float right now? I grepped around in the Lean4 repo for abs absolute and fabs a bit but couldn't find anything.

[Xubai Wang]

Shall we create a new repo to hold some common utility functions for Lean types (as standard library may not be Lean 4's current focus)? It's very distractive to think about their implementation each time when we need them.

[František Silváši]

I am more than happy to contribute an arbitrary assortment of... stuff that I write.

[Henrik Böving]

Yeah having some external (collection) of libraries of things one might expect in Std seems reasonable while the focus is on mathlib4.

[Mac]

Creating a stop gap lean4-stdlib repository seems like a great idea to me! (I have some stuff that may be worth tossing in there as well.)

[Henrik Böving]

Sooo I guess the question that remains is who makes the repo and where?

[Mario Carneiro]

I would suggest that folks put such things in mathlib4 for the present. It will get split up into more packages when it reaches critical mass - I think there is plenty of space for such a thing in lean 4 - but for now it simplifies maintenance to keep things together, and at least for now the concerns about mathlib being too big don't apply since the vast majority of mathlib is still not ported

[Xubai Wang]

Do these utility functions meet the purpose of mathlib4?

I think most of the stuff is about general programming (e.g. Float.abs, String.isInfixOf), so a "stdgap" and mathlib4 will be independent of each other.

There is also a difference in the pace of development: a stop gap means a lot of issues for discussion and we may "port" a large number of functions from other languages.

We may also need a simple doc (which may go against the previous discussed doc-gen4, which mathlib4 may use in the future), which can show users what it provides and how these functions are similar to those in other languages (e.g. Float.abs to fabs, String.isInfixOf to Haskell's isInfixOf and other languages' String.contains), so programmers can quickly find what they need. A simple lake script would suffice.

[Mario Carneiro]

I think most of the stuff is about general programming (e.g. Float.abs, String.isInfixOf), so a "stdgap" and mathlib4 will be independent of each other.

I've said this on many occasions, but mathlib was always intended to be an std-like library. The math stuff came later, and came to dominate due to our particular clientele, but mathlib already contains lots of programmy stuff like lists, hashmaps and other data structures. For various reasons, I believe that mathlib4 will be able to deliver on the CS goals much more effectively than mathlib could, so expect to see much more of this programmy stuff in mathlib4.

[Mario Carneiro]

There is also a difference in the pace of development: a stop gap means a lot of issues for discussion and we may "port" a large number of functions from other languages.

I don't see how this conflicts with mathlib4's model at all.

We may also need a simple doc (which may go against the previous discussed doc-gen4, which mathlib4 may use in the future), which can show users what it provides and how these functions are similar to those in other languages (e.g. Float.abs to fabs, String.isInfixOf to Haskell's isInfixOf and other languages' String.contains), so programmers can quickly find what they need. A simple lake script would suffice.

No, that sounds very much in scope for what we would want doc-gen4 to support. Doc-gen is not all that different from the documentation generators in other programming languages, and all the things you mention sound fairly standard as far as documentation goes, but don't really even need any support from the tool - you write what you want in the doc comment and it renders that.

[Yakov Pechersky]

I loved contributing proofs of the validity of the natural number parser to mathlib, which is extremely CS and practical operational semantics, no deep mathematical content. It taught me a lot about how mathlib is set up to make any proving easier.

[Mac]

Mario Carneiro said:

I would suggest that folks put such things in mathlib4 for the present.

Mario Carneiro said:

I've said this on many occasions, but mathlib was always intended to be an std-like library. The math stuff came later, and came to dominate due to our particular clientele, but mathlib already contains lots of programmy stuff like lists, hashmaps and other data structures.

As I have stated elsewhere I am very much opposed to this proposal. I think the situation should be the other way around. The stdlib should be focused on the CS stuff with some maths sprinkled in when necessary / useful. Mathlib can then expand on this library in its own way.

Some problems with sticking this stuff in mathlib:

• It does not abide by CS style in a lot of its code and it has linters to enforce this (e.g., braces).
• It puts a lot of things into the root namespace that many user packages may not want (and would be forced to acquire if they wanted the stdlib and it was merged with mathlib) whereas the stdlib would have (most) everything under Std (fitting much better with standard CS packaging style)
• There would be a large clash in scope (with a hefty mix of expert mathematicians and computer scientists) that would be very confusing to new users (a CS person would likely be put off by the mathematical branding and large amount of mathematics related PRs to such a joint repo). A split between mathlib and stdlib would keep the balance clearer (with mostly mathematicians and some CS people maintaining mathlib and mostly CS people and maybe some mathematicians maintaining the stdlib).

While I will grant that @Mario Carneiro is just suggesting to do this "at present" (and not all these criticism currently apply to mathlib4), I personally think it is starting off on the wrong foot and thought it worthwhile to mention why.

[Mario Carneiro]

I didn't say mathlib, I said mathlib4, which is for the present a very different library

[Mario Carneiro]

Once we start moving material from mathlib to mathlib4 in bulk, we will need to split this material off. But importantly, the stuff to split off will not all be added stuff, at least half of it will be material currently in mathlib. So that's why I'm suggesting to mix it together and find a natural split point later, because the two don't coincide

[Mario Carneiro]

Even if a std++ library is developed as a separate package from lean's POV, I would still want it to be developmentally integrated with mathlib. For example, one would expect data structures in std++ being proven correct in mathlib, which puts some design constraints on the std++ stuff (e.g. no private, no partial except as a stopgap solution), plus any changes in one would have to be reflected in the other in order to preserve overall cohesiveness

[Mario Carneiro]

It does not abide by CS style in a lot of its code and it has linters to enforce this (e.g., braces).

What is "CS style"? I want mathlib and std++ to follow the same style guide, determined based on how lean 4 syntax works and with consensus among all lean 4 users. Diverging styles helps no one and splits the ecosystem

[Mac]

Mario Carneiro said:

with consensus among all lean 4 users

This is infeasible. I do not believe there is any way that we are going to get all users to agree on a single style to lint. Even Sebastian and Leo disagree on style in some areas (e.g., parentheses around the argument to match).

[Mac]

Furthermore, a lot of developers have very strong opinions on style. So while it may be feasible to get a consistent style for a single project with a clear lead team which can enforce the style on others (e.g., mathlib, the Lean core, etc.), once there are multiple packages with different lead maintainer, they are inevitably going to require different styles.

[Mario Carneiro]

It's certainly possible to have a language style guide, even when there are many users. Just consider the style guide of any major language (rustfmt comes to mind). Plenty of people will disagree on the fine points, but not enough to make the proposition worthless

[Scott Morrison]

Given that we will have a round-tripping pretty printer, and at least early on the entirety of the mathlib port will be run through that pretty printer, in some sense the style guide should basically be documentation of the pretty printer.

[Mac]

@Mario Carneiro true, however, most language style guides tend to be rather flexible and general and linters based around them are customizable whereas most project style guides are much more specific and fixed.

[Scott Morrison]

Frankly I couldn't care less about where the braces go. On the other hand, the uniformity in mathlib is just wonderful for easy reading of others' code.

[Mac]

I, on the other hand, care immensely about where braces go (to a certain extent).

[Mario Carneiro]

that's entirely language dependent. Style guides vary hugely in the extent to which they allow flexibility

[Mario Carneiro]

some are just AST pretty printers

[Mario Carneiro]

and I think lean will be one of these

[Mario Carneiro]

Obviously an inflexible pretty printer has to be very good, or else you will get riots in the streets

[Mac]

Mario Carneiro said:

that's entirely language dependent. Style guides vary hugely in the extent to which they allow flexibility

true, but they are also varying hugely as to whether programs within the language follow the style guide (e.g., Python).

[Mario Carneiro]

People who are 'opinionated' about style will generally want to opt out of the whole endeavor, but they still have to play by the rules when it comes to contributing to "that one big project"

[Mac]

Yes, hence why I don't contribute to mathlib. :stuck_out_tongue_wink: (That is half a joke and half not.)

[Mac]

I would, however, very much like to contribute to the standard library.

[Mac]

While it is possible I am alone on this matter, I suspect that is unlikely the case.

[Mario Carneiro]

My guess is that you @Mac are not going to be satisfied with any style guide we come up with, even if you are taking part in the discussion, so I think you should approach this with the understanding that you won't be using the style guide and don't try to filibuster things too much

[Mac]

@Mario Carneiro And I would do so, if we were just talking about mathlib. However, the current trend of this discussion seems to imply that you are suggesting enforcing this style guide on all core Lean projects (of which, I should note, Lake is currently one), which is a very different matter.

[Mario Carneiro]

but the big projects absolutely have to be using the style guide, I don't see how that's even an option

[Mac]

Hence my argument about what the style guide should be...

[Xubai Wang]

Mario Carneiro said:

I've said this on many occasions, but mathlib was always intended to be an std-like library.

I have another question, do you think these functions will eventually go to mathlib4 rather than Std(I think it's the latter one)? A separate repo may be easier to cope with when lean is moving towards a better Std, without changing the mathlib4

[Mario Carneiro]

Not necessarily all lean projects, just the big ones that need community support

[Mario Carneiro]

@Xubai Wang Std is in a bit of an awkward position because it is part of the lean bootstrap. I don't know whether what I'm calling std++ will be able to merge with Std, but it would be nice if we could do something like that

[Mac]

@Mario Carneiro that was previously the plan as discussed in the original proposal for the standard library (#528)

[Mario Carneiro]

So as I see it now, in the far future there will probably be three packages, for Std, StdExtra and Mathlib (Mathlib might also break into more packages, we'll see), unless we find a way to merge StdExtra into Std

[Mario Carneiro]

StdExtra might also be split into more packages if needed

[Mac]

@Mario Carneiro what is the problem with the stdlib just adding more stuff to Std?

[Mario Carneiro]

Well, last time we talked about this you were pretty adamantly against that kind of namespace pollution

[Mario Carneiro]

I do think that it would make more sense for the current Std to be renamed to StdCore and StdExtra -> Std though

[Mario Carneiro]

but none of this changes my views on integration between Std and Mathlib

[Mario Carneiro]

this is not a license to have it run off and be completely disconnected from mathlib

[Mac]

Yes, but the idea here is that stdlib will (be the canonical owner of Std, so I don't have a problem with it in this case. Also as a core Lean library, I am willingly to give it more leeway than I would a user library.

[Mario Carneiro]

Are you saying that StdExtra should also be shipped with lean?

[Mac]

Ideally, Lake would also eventually depend on the stdlib (or at the very least make it available in the lakefile).

[Mac]

@Mario Carneiro that was the original plan, yes (again see #528).

[Mario Carneiro]

I suppose that can work, but it's going to be pretty hefty

[Mac]

Most languages ship with a standard library, I don't think Lean doing would be all too weird.

[Mario Carneiro]

well, languages differ on how full featured they want the standard library to be. Are we following the java/python model or the rust model?

[Mario Carneiro]

The advantage of the StdExtra package is that you can basically choose either one

[Mac]

I would assume closer to the Java model. Especially given the current less than pure modularity of Lean.

[Mario Carneiro]

but it's true that lakefiles have some unique constraints that would encourage putting more stuff in the base package

[Xubai Wang]

Mac said:

Ideally, Lake would also eventually depend on the stdlib (or at the very least make it available in the lakefile).

Mario Carneiro said:

but it's true that lakefiles have some unique constraints that would encourage putting more stuff in the base package

It's important to make all packages(build dependencies) available in the lakefile (although the current import mechanism does not support this). So if there is a StdExtra, it doesn't matter whether it's shipped with lean (if build dependency is available).

[Mario Carneiro]

All packages? That's a big chicken and egg problem

[Mario Carneiro]

I would like to keep lakefiles to a bootstrap-like collection of packages only. You shouldn't need that much infrastructure to describe what you want to build. Worst case scenario you describe how to download some package to power a second-tier lakefile that can do fancier stuff

[Xubai Wang]

But what if when e.g. we want to parse markdown, run cargo, or call emscripten as build process or lake script? It's ridiculous to rewrite everything in a single lakefile, which should be a package otherwise.

[Mario Carneiro]

isn't the lakefile for that just a bunch of "call process X, call process Y" etc?

[Mario Carneiro]

probably you won't be able to parse markdown with the default set of packages but like I said you can have a lakefile to build another lakefile

[Mario Carneiro]

the point is that we don't want to have to resolve dependencies in order to resolve dependencies

[Mario Carneiro]

the lakefile should be as "declarative" as possible, and not do too much fancy stuff

[Scott Morrison]

Let's please not have the monstrosities that build.sbt seems to inevitably turn into.

[Henrik Böving]

What's build.sbt?

[Mario Carneiro]

https://en.wikipedia.org/wiki/Sbt_(software)

[Mario Carneiro]

oh, here's a fun fact:

The sbt project uses sbt to build itself, and considers that dogfooding is a positive feature. To the Debian project, however, that is considered a circular dependency, that they try to minimize. As a result, sbt is not yet in Debian.

That's definitely what you don't want in a build tool

[Mario Carneiro]

I wonder if sbt supports building projects that require themselves

[Mac]

Mario Carneiro said:

oh, here's a fun fact:

The sbt project uses sbt to build itself, and considers that dogfooding is a positive feature. To the Debian project, however, that is considered a circular dependency, that they try to minimize. As a result, sbt is not yet in Debian.

That's definitely what you don't want in a build tool

Are you sure? I use Lake to build Lake these days. :laughing:

[Henrik Böving]

It appears even good old GNU make builds itself: https://git.savannah.gnu.org/cgit/make.git/tree/README.git so I don't think that should be tooo much of an issue?

[Gabriel Ebner]

Let's please not have the monstrosities that build.sbt seems to inevitably turn into.

I've maintained a largeish scala project for a couple of years, and in my experience the main problem with sbt is not that people write large build scripts but the fact that the sbt dsl sucks. Virtually nothing works like you'd expect from vanilla scala. There's dynamically scoped variables which have several namespaces (project, target, etc.). Go-to-definition is broken because it takes you to the variable declaration instead of anything useful. Dependencies are implicit (iirc?). Pretty much everything (writing files, resolving paths, etc.) uses sbt-specific functions and not Scala ones. Did I mention that there are two+ different dsls? See here for a longer discussion on the many ways that sbt sucks: https://www.lihaoyi.com/post/SowhatswrongwithSBT.html

In other words, as long as lakefiles remain reasonably close to vanilla lean and all the standard tooling works then I'm confident that even large lakefiles can stay maintainable.