loogle on newly renamed Batteries

Stream: Is there code for X?

[Shreyas Srinivas]

On a different note: @Joachim Breitner : does loogle work with the renamed Batteries?

[Joachim Breitner]

@loogle "Batteries"

[loogle]

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

[Shreyas Srinivas]

But as you can see above, the results for essentially the same data structure are different depending on whether the prefix is Std or Batteries. (Also this thread about loogle should probably be separated)

[Notification Bot]

4 messages were moved here from #Is there code for X? > computable breadth first traversal by Shreyas Srinivas.

[Shreyas Srinivas]

For reference : @loogle Std.Queue

[loogle]

:search: Std.Queue, Std.Queue.empty, and 17 more

[Shreyas Srinivas]

@loogle Std.Queue

[loogle]

:search: Std.Queue, Std.Queue.empty, and 17 more

[Shreyas Srinivas]

@loogle Batteries.Queue

[loogle]

:exclamation: unknown identifier 'Batteries.Queue'
Did you mean "Batteries.Queue"?

[Shreyas Srinivas]

@loogle "Batteries.Queue"

[loogle]

:shrug: nothing found

[Mario Carneiro]

I don't understand what point is being made here. Core has a thing called Std.Queue, batteries has a thing called Batteries.Tactic.Alias.alias, and loogle is finding both

[Eric Wieser]

Perhaps it helps to remember that Std wasn't just renamed, it was split into Batteries and core. We renamed the git repo (rather than creating a new one) to preserve the git history.

[Mario Carneiro]

it isn't much of a split so far, but eventually things will be upstreamed to the new std

[Mario Carneiro]

right now there is no actual Std library

[Mario Carneiro]

although there are a handful of definitions in the Std namespace, all in core somewhere

[Mario Carneiro]

I'm actually surprised Std.Queue is there, I thought that was ditched a while ago

[Mario Carneiro]

docs#Std.Format docs#Std.Range

[Joachim Breitner]

So Loogle is fine?

[Shreyas Srinivas]

What's new to me is that there is an Std namespace in core

[Eric Wieser]

Arguably that was the whole reason that we renamed Std to Batteries, to allow core to claim the Std namespace.

[Shreyas Srinivas]

I thought that was to be claimed by the new fro-std

[Shreyas Srinivas]

But yeah the namespace mixup is the answer to my original confusion

[Eric Wieser]

fro-std is core; at least, it resides in leanprover/lean4