Std -> Boost migration

Stream: batteries

[Kim Morrison]

We're making plans for the rename of Std to Boost. W'd like to do it shortly after the release of v4.8.0-rc1. @Mac Malone is going to make some changes to lake to help the transition, ensuring that there are custom error messages explaining what to do when updating.

An important question that w'd like to put open to Mario / the @admin team / Boost contributors is whether to leave boost in the leanprover organization or migrate it to the leanprover-community organization.

We've checked that in either case (i.e. leanprover/std4 -> leanprover/boost or leanprover-community/boost) the redirects that Github sets up will mean that repositories using v4.7.0 or earlier will still find the dependency, so as far as we can tell there is no user-experience difference between the two. (And indeed we think this is still the case even if it is done in two steps, at different times.) There will of course be user experience problems when people update their repositories, and this is what Mac will work on to make smoother.

My recommendation is to move it leanprover-community/boost in a single step. I think this best reflects:

• its open development model
• that the FRO isn't responsible for it
• and that future responsibility for its management ultimately lands with @admin team, rather than the Lean FRO.

There are still a bunch of open questions about boost (does it need additional maintainers? could it be split into smaller packages? should parts of it be folded back into Aesop/ProofWidgets/Mathlib? etc), but I'd prefer that we address those questions separately from the migration process, or at least afterwards, in particular because these are questions for the maintainers and the admin team, rather than the FRO.

[Mario Carneiro]

I'm inclined to agree that it should move to leanprover-community

[Mario Carneiro]

(Although there are some weird and surprising repos in the leanprover org...)

[Mario Carneiro]

Before we do that though, I'd like to get the bikeshed out of the way and poll people's opinions on the name. Is Boost actually a good choice? (For those who don't know, Boost is the name of a popular C++ megapackage with a relatively open development model, not unlike mathlib. So it's not a bad name, quite on-the-nose as it were, although it might have a bit too much brand recognition, resulting in confusion and SEO difficulties.)

[Mario Carneiro]

/poll What should the "mathlib for CS" library be called?
Boost
Std2
More
Extra
Plus
Proglib

[David Renshaw]

What about "Bolster"?

[Yury G. Kudryashov]

Should we use a word associated with getting fatter? Or muscle? I'm thinking what is a natural addition to lean.

[Thomas Murrills]

Re: muscle: "Flex"? (Also connotes "greater flexibility" thanks to all the extra functionality.)

[Thomas Murrills]

Another (unrelated) option I'll throw into the mix is "Amp" (as in amplify, like boost), which is nice and short.

[Eric Wieser]

Is everything in Std namespaces/ imports going to change too?

[Mario Carneiro]

There will of course be user experience problems when people update their repositories, and this is what Mac will work on to make smoother.

I take that to be a 'yes'

[Mario Carneiro]

this will be the biggest deprecation/rename job we've ever attempted (assuming we don't just transition cold-turkey), and it's working at a level we historically have not had good support for (import renames and require renames)

[Mario Carneiro]

I'd love it if Boost v1 could just populate the Std import namespace with files which produce a warning telling you to change your imports

[Kim Morrison]

Yes, the import renames we're not going to be able to help with. require Mac is working on.

[Kim Morrison]

Mario Carneiro said:

I'd love it if Boost v1 could just populate the Std import namespace with files which produce a warning telling you to change your imports

That's a good idea, and there's no obstacle to doing that.

[Mario Carneiro]

and then we add Std for real at the same time as removing those shims

[Kim Morrison]

(just a heads up that I will shortly disappear from this thread for about 72 hours)

[Mario Carneiro]

I think the current obstacle is that packages can't populate multiple top level namespaces?

[Mario Carneiro]

unless boost actually has a package in it named Std, which would conflict with the nascent Std library in core during the transition

[Alok Singh]

i tried to click in the poll to no avail, so i'm manually voting batteries. boost seo interferes and bad memories of boost

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

The leanest kind of cylindrical battery appears to be AAAA. One could name the library LeAAAAn, or Le4An for short.

[James Gallicchio]

LeAAAAnis how i feel when something is missing in the standard library

[Mac Malone]

Kim Morrison said:

Mac Malone is going to make some changes to lake to help the transition, ensuring that there are custom error messages explaining what to do when updating.

The draft for the improved error message for a mismatched require (i.e., require std from <boost>) is up at lean4#3999. However, from this thread, it sounds like there might be more Lake magic desired here to assist with this transition. Feel free to suggest additional changes!

[Eric Wieser]

What's the plan for lakefiles which currently download std from leanprover/std4, which at some point will start downloading an entirely different library called std?

[Eric Wieser]

Or will the new std live at a 4-less url, which avoids this issue?

[Mac Malone]

@Eric Wieser The new Std will live in core and not in a separate repoisotry, so that should hopefully avoid the issue.

[Kim Morrison]

Okay, it seems that Boost / Batteries / Amp are the only viable candidates. @Mario Carneiro, will you decide how this is going to be decided (you decide, another polll between those three, whatever). If it's possible to have a final decision on this asap that would be lovely. :-)

[Mario Carneiro]

Okay @stream, let's have a runoff election: Please vote for only one this time.

[Mario Carneiro]

/poll What should the "mathlib for CS" library be called?
Boost
Batteries
Amp

[Mario Carneiro]

@Kim Morrison Can you set the time limit?

[Kim Morrison]

I think 2024-04-29T23:00:00+10:00 or thereabouts should be fine.

The dependency here is that Mac will need a moment to push a commit to Lake that knows about the new name, in time for v4.8.0-rc1, and I'm hoping that if all goes well (i.e. better than expected right now!) we can be cutting v.4.8.0-rc1 from the nightly that lands at 2024-04-30T18:00:00+10:00 or so.

[Kim Morrison]

(Is it too late to suggest that only people who've ever contributed to Std in some way (or at least explicitly used it??) vote?) (edit, whatever, too difficult to set a criterion...)

[Ruben Van de Velde]

It's too bad none of those are searchable :)

[Eric Rodriguez]

I really think that making it unsearchable is not great, as much as I like the name Boost otherwise

[Mario Carneiro]

I don't think it will be a major issue, you'll still be able to find it via "lean boost" or something

[Mario Carneiro]

"std" is of course similarly unsearchable

[Phil de Joux]

Maybe we could pick a combination that doesn't already have a lot of hits in a search? I see that "lean boost" is dominated by health supplements, https://www.google.com/search?q=lean+boost.

[Phil de Joux]

As short as "std" we could use "too". It has meaning too if we pun "lean to" as "lean too";

A lean-to is a type of simple structure originally added to an existing building with the rafters "leaning" against another wall. Free-standing lean-to structures are generally used as shelters.

[Eric Wieser]

Too isn't great for speaking aloud, in terms of ambiguity

[Julian Berman]

Silly question (or one discussed elsewhere) I'm sure but is "Mathlib for CS" a description of Std today, of its aspirations, or of neither and I'm reading too much into "CS"? Specifically today Std is a sort of "missing" programming standard library is it not? Is it aspiring to be a CS formalization project?

[Yaël Dillies]

From my understanding it's supposed to rather be Maths ∩ CS ?

[Shreyas Srinivas]

Julian Berman said:

Silly question (or one discussed elsewhere) I'm sure but is "Mathlib for CS" a description of Std today, of its aspirations, or of neither and I'm reading too much into "CS"? Specifically today Std is a sort of "missing" programming standard library is it not? Is it aspiring to be a CS formalization project?

I am not sure that makes sense for CS. Unlike math, CS is distributed too broadly from a conceptual point of view for a single unified library to make sense. I am guessing calling it "Mathlib for CS" signifies the maintenance strategy going forward.

[Eric Wieser]

Does this mean that abstract CS like "formal grammars" or "complexity theory" is in scope? My understanding was that it was not for theoretical CS, but for things which are actually executed (and lemmas about them).

[Shreyas Srinivas]

From Leo's message I got the following:

1. The new Std is meant to support Lean the programming language.
2. Batteries/Boost is a community maintained version of this new Std with extra features (like boost for CPP)

This suggests it will contain libraries for basic data structures and utilities of the kind rust's standard library has.

[Henrik Böving]

Yaël Dillies said:

From my understanding it's supposed to rather be Maths ∩ CS ?

According to Thorsten Altenkirch that's type theory^^

[Henrik Böving]

Shreyas Srinivas said:

From Leo's message I got the following:

1. The new Std is meant to support Lean the programming language.
2. Batteries/Boost is a community maintained version of this new Std with extra features (like boost for CPP)

This suggests it will contain libraries for basic data structures and utilities of the kind rust's standard library has.

The new std inside of Lean will contain stuff that you would expect from a programming language + enough theory that you can do proofs over datastructures and such.

The scope of batteries/boost/amp is basically up to the maintainer team of it.

[Henrik Böving]

Eric Rodriguez said:

I really think that making it unsearchable is not great, as much as I like the name Boost otherwise

Note that batteries is also a name of one of the OCaml alternative standard libraries: https://ocaml-batteries-team.github.io/batteries-included/hdoc2/ so it's not like this name will not lead to search engine confusion either

[Mario Carneiro]

Eric Wieser said:

Does this mean that abstract CS like "formal grammars" or "complexity theory" is in scope? My understanding was that it was not for theoretical CS, but for things which are actually executed (and lemmas about them).

This is my understanding / intention as well. Theoretical CS is in scope only insofar as it is useful for proving theorems about executable functions with practical application (e.g. automata theory used for correctness proofs of a regex engine). My guess is that theoretical CS for its own sake is better suited for mathlib (e.g. the Computability/ folder), because it benefits more from having access to / contributing to the rest of the mathematical infrastructure there.

[Julian Berman]

Got it, OK, then it's me reading too much into "CS" then it sounds like, I don't personally generally consider programming to be part of CS and basically always assume it means theoretical but sounds like if anything that certainly is not what was intended. While I'm at it with the silly ones, what is the reason Std isn't a good name (personally I like it better than any of the others in the poll).

[Mario Carneiro]

I do too. :( Short answer: FRO wants that for themselves

[Kim Morrison]

@Mario Carneiro, on the assumption that the outcome of the poll above doesn't change in the next 8 hours or so, are you happy if I get the ball rolling with batteries?

[Mario Carneiro]

yes

[Johan Commelin]

Will this stream also be renamed? Or do we start a new one?

[Mario Carneiro]

Renaming sounds best. The stream description is quite clear that it is about the github repo and should move with it

[Mario Carneiro]

For the foreseeable future I'm guessing we can just use #lean4 for questions and suggestions regarding the new std

[Eric Wieser]

Is the new GitHub repo going to be /batteries, /batteries4, /Batteries, ...?

[Kim Morrison]

batteries

[Mario Carneiro]

I think it's safe to drop the 4

[Yaël Dillies]

What's the reasoning for batteries again?

[Mario Carneiro]

"batteries included"

[Mario Carneiro]

it's a set phrase used to suggest the "full featured" version of a thing as opposed to the minimalistic version

[Mario Carneiro]

"Batteries included" (slang), in a product usability (mostly in software) it states that the product comes together with all possible parts required for full usability

[Eric Wieser]

And there is precedent for the name in ocaml, right?

[Mario Carneiro]

wikipedia also mentions it as "the motto of the python programming language" although that sounds like [citation needed] to me

[Eric Wieser]

Mario Carneiro said:

"batteries included"

Though arguably Std is now the included batteries, and batteries are explicitly only the batteries that core decides not to include

[Utensil Song]

Initially, I really can't imagine a standard-ish library with such a long (> 5 characters) and plural name, until seeing ocaml-batteries-team/batteries-included, open Batteries, and Bat* types in OCaml.

Now I can see future projects depending on "Lean with batteries".

[Yaël Dillies]

I quite like Amp for the brevity

[Markus Schmaus]

Me too, but I think the decision has been made and it's going to be batteries

[Matthew Ballard]

It is short for another thing too from an unfortunate area that Lean already has a name collision with. Boost also but from a fictional universe. No one that I know of is doing batteries.

[Mauricio Collares]

Henrik Böving said:

Eric Rodriguez said:

I really think that making it unsearchable is not great, as much as I like the name Boost otherwise

Note that batteries is also a name of one of the OCaml alternative standard libraries: https://ocaml-batteries-team.github.io/batteries-included/hdoc2/ so it's not like this name will not lead to search engine confusion either

[Matthew Ballard]

Less obtuse: AMPhetamines. Boost is slang for that in cyberpunk.

[Eric Wieser]

Though then we can make the "lack of Amp set Mathlib back a month" joke

[Matthew Ballard]

There are many jokes to be made down this path.

[Kim Morrison]

Let's not.

[Matthew Ballard]

My point, yes

[Shreyas Srinivas]

My impression of English slang as a second language speaker is that any word or turn of phrase will acquire alternative meanings sooner or later. It seems to be a hopeless task to try and anticipate every possible alternative meaning. Same goes for google searches.

[Eric Wieser]

Probably encouraging users to start searches with leanprover instead of lean is enough to resolve most search issues

[Eric Wieser]

Just like golang instead of go

[Mac Malone]

Kim Morrison said:

The dependency here is that Mac will need a moment to push a commit to Lake that knows about the new name, in time for v4.8.0-rc1, and I'm hoping that if all goes well (i.e. better than expected right now!) we can be cutting v.4.8.0-rc1 from the nightly that lands at 2024-04-30T18:00:00+10:00 or so.

I have updated lean4#3999 (the special eroor message) to be name agnostic, so deciding on a name is no longer a prerequisite to the merge. :smile:

[Shreyas Srinivas]

Follow up: In which release will this update be applied. I just noticed that the github-actions bot published release 4.8.0-rc1

[Shreyas Srinivas]

But there are no notes yet, whence the question

[Kim Morrison]

lean4#3999 landed in v4.8.0-rc1.

[Kim Morrison]

I have opened std4#780, which attempts the rename to batteries.

[Kim Morrison]

I'd like to merge std4#780, effect the transfer/rename, and then work on whatever cleanup is needed, soon. Ideally this would start at about 2024-05-06T14:00:00+10:00. Happy to delay by up to a day if anyone wants to be on hand to help put out fires. :-)

[Mario Carneiro]

I'm going to be traveling tomorrow so delaying sounds good

[Kim Morrison]

When is good?

[Mario Carneiro]

I'll be on a regular schedule starting 2024-05-07T09:00:00+02:00

[Mario Carneiro]

you can do it before then but I may or may not be around for firefighting

[Kim Morrison]

Okay, I will start a bit before that, but then be out roughly 2024-05-07T17:00:00+10:00 - 2024-05-07T21:00:00+10:00 !

[Kim Morrison]

:start:

[Kim Morrison]

Okay, std4#780 is back up to date, and I've hit merge.

Off to do the transfer/rename.

[Kim Morrison]

Okay, done.

[Kim Morrison]

https://github.com/leanprover/std4 successfully redirects to https://github.com/leanprover-community/batteries

[Kim Morrison]

My local checkout of std continues to work (fetch/pull/push) without changing the URL.

[Kim Morrison]

main (with all the renames) was automatically merged into nightly-testing, and that still builds.

[Kim Morrison]

I tried running lake update in aesop, and received:

% lake update
info: std: updating repository '././.lake/packages/std' to revision '56d2e4ee226603eb6b90b05f6b944bde42672cd5'
error: the 'std' package has been renamed to 'batteries' and moved to the
'leanprover-community' organization; downstream packages which wish to
update to the new std should replace

  require std from
    git "https://github.com/leanprover/std4" @ "main"

in their Lake configuration file with

  require batteries from
    git "https://github.com/leanprover-community/batteries" @ "main"
error: aesop: package 'batteries' was required as 'std'

[Kim Morrison]

This looks great, thanks @Mac Malone!

[Kim Morrison]

After making that change, and running lake update then lake build, we get a million errors, because at present there's nothing we do to help with updating imports.

[Kim Morrison]

I've just done a replacement of s/^import Std\.//import Batteries./.

[Kim Morrison]

Next there are various open statements, e.g. open Std (BinomialHeap).

[Kim Morrison]

Acutally only one, and the tests seem to work, so I've opened https://github.com/leanprover-community/aesop/pull/132 moving aesop to batteries.

[Kim Morrison]

Similarly https://github.com/leanprover-community/ProofWidgets4/pull/56 for ProofWidgets. In fact ProofWidgets barely uses batteries at all -- one import in one demo, apparently.

[Kim Morrison]

https://github.com/leanprover-community/import-graph/pull/6 for the import-graph repository (upstream of mathlib)

[Kim Morrison]

Cutting a v0.0.36 release for ProofWidgets now.

[Kim Morrison]

(Until that is available, I can't update Mathlib, as we'll get Batteries via the direct require, and the old Std via ProofWidgets.)

[Kim Morrison]

But it's ready now. :-)

[Kim Morrison]

(... working on mathlib ...)

[Kim Morrison]

#12720 is building locally; if someone could review and/or delegate that would be great!

[Kim Morrison]

Curiously ToFormat and format are in the Std namespace!

[Mario Carneiro]

Yes, some of the things in the Std namespace are defined in core for some reason

[Mario Carneiro]

Std.Range too is a bit weird

[Bulhwi Cha]

Can someone change the description of the GitHub repository from "Standard Library for Lean 4" to 'The "batteries included" extended library for Lean 4'?

[Kim Morrison]

Shall we rename this stream? I suspect it will break links.

[Bulhwi Cha]

Perhaps we can create a new stream for Batteries and leave this stream for Std.

[Shreyas Srinivas]

If the link redirects to batteries, then older projects would also have to watch out right?

[Shreyas Srinivas]

I could have an older project I share with a colleague, and suddenly lake might complain that when running cache or update it cannot find std

[Eric Wieser]

I think the complaint is a warning not an error

[Kim Morrison]

If you need to update, you will need to change URLs. Otherwise, as far as I'm aware at present, you don't need to do anything.

[Joachim Breitner]

I am running into what seem to be cache-related issues (while updating loogle, so all a bit special), but it seems that cache needs to be be told about batteries in

-- TODO this should be generated automatically from the information in `lakefile.lean`.
private def CacheM.getContext : IO CacheM.Context := do
  let root ← CacheM.mathlibDepPath
  return ⟨root, .ofList [
    ("Mathlib", root),
    ("Archive", root),
    ("Counterexamples", root),
    ("Aesop", LAKEPACKAGESDIR / "aesop"),
    ("Std", LAKEPACKAGESDIR / "std"),
    ("Cli", LAKEPACKAGESDIR / "Cli"),
    ("ProofWidgets", LAKEPACKAGESDIR / "proofwidgets"),
    ("Qq", LAKEPACKAGESDIR / "Qq"),
    ("ImportGraph", LAKEPACKAGESDIR / "importGraph")
  ]⟩

in Cache/IO.lean. Is this already on the right radar? @Mario Carneiro’s most likely?

[Mario Carneiro]

yes, that list needs to reflect any change in the contents of lake-manifest.json

[Mario Carneiro]

hopefully that was in the mathlib std bump?

[Joachim Breitner]

No, doesn’t look like it.

[Notification Bot]

4 messages were moved here from #general > batteries vs. cache by Mario Carneiro.

[Mario Carneiro]

#12725, expedited merging appreciated

[Sebastian Ullrich]

Kim Morrison said:

Shall we rename this stream? I suspect it will break links.

I would hope that the "348111" component is a stream ID preventing that but I haven't tried

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/348111-foobar

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/348111-foobar/topic/Std.20-.3E.20Boost.20migration

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/348111-foobar/topic/Std.20-.3E.20Boost.20migration/near/437399729

[Mario Carneiro]

all three kinds of links seem to work

[Johan Commelin]

Mario Carneiro said:

#12725, expedited merging appreciated

On the queue, even though CI wasn't done yet

[Kim Morrison]

There are some more updates in Mathlib renaming Std -> Batteries in #12727.

[Joachim Breitner]

@loogle "Batteries"

[loogle]

:search: Batteries.Tactic.Alias.AliasInfo, Batteries.Tactic.Alias.alias, and 1499 more

[Mario Carneiro]

is anyone else getting a 404 with broken CSS from that link?

[Henrik Böving]

Yeah the docs are broken because the build process refers to Std:docs, I'll fix it

[Henrik Böving]

https://github.com/leanprover-community/mathlib4_docs/actions/runs/8985851449/job/24680647885 so once a hoskinson machine feels like running this we'll have proper docs

[Mario Carneiro]

but it looks like the 404 page is also broken independently of this

[Henrik Böving]

Right, to be honest I don't even know how we end up at this specific 404 page. doc-gen does generate a 404.html but it is placed at the root of the project. The 404 mechanism of github pages does not appear to be redirecting to this page but instead dynamically grabbing it from 404.html and displaying it at this point??

The reason that the CSS is messed up is that the page is rendered at some path but the CSS is stored at the root path and the HTML has no way to know how to refer to the root path like this (in particular because we wanted to be able to host the entire thing at arbitrary subpaths so it's not like we can just statically refer to domain/style.css if you check the requests you will see it is trying to load ./style.css as 404.html knows it is at the root so the CSS should be accessible but isn't because github pages doesn't redirect me)

I'm not going to invest the time to fix this right now as 404s cannot happen (if doc-gen is bug free) while browsing the website and also not with docs#FooBarFoo (as the JS in the search logic correctly redirects to 404.html) THe only way to trigger this is to statically refer to some path that doesn't exist like above.

[Joachim Breitner]

(Like Loogle would :-))

[Floris van Doorn]

All three links that the loogle bot posted look fine to me.

[Henrik Böving]

Floris van Doorn said:

All three links that the loogle bot posted look fine to me.

They do because I fixed the website, mario is right that they were broken before

[Henrik Böving]

To see what mario saw check out e.g.: https://leanprover-community.github.io/mathlib4_docs/Batteries/Tactic/foobarlala

[Joachim Breitner]

What should be doing the chore: bump to nightly-2024-05-07 commit at batteries, and is it still working?
https://github.com/leanprover-community/batteries/commits/nightly-testing

[Kim Morrison]

.github/workflows/nightly_bump_toolchain.yml

[Kim Morrison]

And indeed the repository_owner field needs updating.

[Kim Morrison]

nightly_merge_master.yml has the same problem.

[Kim Morrison]

std4#785

[Kim Morrison]

Or rather: batteries#785

[Mario Carneiro]

@Kim Morrison This looks like a migration-related issue: https://github.com/leanprover/lean4/actions/runs/8986538224/job/24682889193

[Kim Morrison]

lean#4108

[Utensil Song]

Don't know if this qualifies as an issue, I just did a global replacement of import Std to import Batteries of <10 affected Lean files in a project with one Lean file with such import open, then Lean LSP server crashed:

image.png

[Mario Carneiro]

we'll need a replication to do something about that

[Utensil Song]

Yeah, but I have little idea about how to replicate that or gather more information locally in this situation. (Although I can reproduce this stably locally)

[Utensil Song]

Can I turn some options on to have more debug log or similar? (Debugging this might belong to another topic though)

VSCode log

Watchdog error: cannot find open document 'file:///a_file_that_is_not_open_in_vscode.lean'
[Error - 8:26:25 PM] Client Lean 4: connection to server is erroring. Shutting down server.
[Error - 8:26:25 PM] Sending document notification textDocument/didSave failed.
Error: write EPIPE
at WriteWrap.onWriteComplete [as oncomplete] (node:internal/stream_base_commons:94:16)
[Error - 8:26:25 PM] Request textDocument/codeAction failed.
Message: Cannot call write after a stream was destroyed
Code: -32099
[Error - 8:26:25 PM] Connection to server got closed. Server will not be restarted.
[Error - 8:26:25 PM] Stopping server failed
Message: Cannot call write after a stream was destroyed
Code: -32099
[Error - 8:26:25 PM] Stopping server failed
Message: Cannot call write after a stream was destroyed
Code: -32099

[Mario Carneiro]

You can click on the "Show Output" button to see more information (hopefully)

[Mario Carneiro]

(this is not a migration issue per se, it's most likely a server/lake issue caused by removing or changing olean files while they are still open)

[Agnishom Chattopadhyay]

I thought Std stood for _Standard_ as in "Standard Library". What is the meaning of Boost?

[Mario Carneiro]

• Boost: it gives you a leg up, a boost, over the standard library (see also prior art)
• Batteries: It's the 'batteries included' version of the standard library (see also prior art)

[François G. Dorais]

The batteries repo should be pinned in the leanprover-community landing page (just like std4 was pinned in the leanprover landing page).

[Kim Morrison]

Done

[Mario Carneiro]

What was done and where?

[Kim Morrison]

The leanprover-community organization page https://github.com/leanprover-community has some "pinned" repositories. I removed mathport, and added batteries, aesop, and proofwidgets (snap editorial decision, very happy if a community process overrides it!)