mathlib tactics

Stream: new members

[Jalex Stark]

I have a local copy of the tutorial project. In the first_proofs.lean file, I have access to tactics define in mathlib such as library_search. When I make a new file in the same folder, I don't. Is there a magic incantation I am missing?

[Mario Carneiro]

Did you "open folder" in vscode?

[Jalex Stark]

Hmm I think so; let me close the VSCode instance and try again.

[Mario Carneiro]

You can tell because the explorer sidebar should show a listing of files in the folder rather than a button saying "open folder"

[Jalex Stark]

yes, my sidebar has a listing of folders that includes a bunch of the mathlib source

[Mario Carneiro]

You should open the tutorial folder, the one with leanpkg.toml in it

[Mario Carneiro]

I believe the tutorial files are in a src directory inside it. If you create another file in the src directory with extension .lean, it should work

[Kevin Buzzard]

vscode.png Here's what my VS Code looks like right now, if it helps.

[Rob Lewis]

An important "magic incantation" is import tactic at the top of the file, or some import that will transitively include tactic.

[Jalex Stark]

I have included import tactic and things now work the way I expect them to. Thanks all!

[Jalex Stark]

The first_proofs.lean file has import data.real.basic which i guess transitively includes tactic

[Kevin Buzzard]

Yes, essentially any import from mathlib imports a whole lot of tactics (but not all of them).

[Kevin Buzzard]

There are "core" tactics imported automatically (like simp and rw), which will get you only so far, and then the community writes other tactics (like ring or linarith) which get put into mathlib and which must be imported manually. [it's analogous to groups being in core so being imported automatically, but modules needing a manual import]

[Jalex Stark]

I seem to have some but not all of the tactics listed at https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md

[Kevin Buzzard]

Then things are functioning correctly ;-)

[Kevin Buzzard]

Perhaps that list should explicitly flag which ones are not imported by import tactic. If you type import tactic.linarith you will get a bunch more.

[Rob Lewis]

I seem to have some but not all of the tactics listed at https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md

import tactic should get you essentially all of them. Which are you missing? It's likely they should be there.

[Jalex Stark]

i don't have suggest

[Rob Lewis]

Perhaps that list should explicitly flag which ones are not imported by import tactic. If you type import tactic.linarith you will get a bunch more.

linarith should be included in import tactic.

[Jalex Stark]

i do have linarith

[Rob Lewis]

Yeah, suggest was added pretty recently and I'm guessing we forgot to add it to the relevant list.

[Kevin Buzzard]

import tactic.suggest seems to fix it

[Mario Carneiro]

If you don't have a tactic, you can always search mathlib for it and import the relevant file

[Mario Carneiro]

the naming is usually pretty obvious though, e.g. tactic.suggest

[Kevin Buzzard]

New users find it hard to search mathlib because by default VS Code doesn't search dependencies

[Mario Carneiro]

I mean grep for it

[Kevin Buzzard]

New users tend not to be command-line savvy either (at least if they're coming from a maths background)

[Rob Lewis]

Or search here: https://leanprover-community.github.io/mathlib_docs/ :slight_smile:

[Mario Carneiro]

If you have mathlib in the _target folder, will vscode's file search look in there?

[Kevin Buzzard]

Rob link: Now that does work! We should perhaps advertise this.

[Jalex Stark]

I do happen to know how to use grep, but I like rob lewis's answer a lot

[Mario Carneiro]

I actually mean vscode's file search; I don't actually use grep

[Kevin Buzzard]

If you have mathlib in the _target folder, will vscode's file search look in there?

If you have followed all the instructions in the mathlib readme to the letter as a new user, then the answer is no

[Mario Carneiro]

does it work if you specify it in the "search within" area? (Don't have a lean project to test atm)

[Kevin Buzzard]

and the reason is this: blue.png -- the button "ignore system files in your search" is checked by default

[Kevin Buzzard]

What makes things worse is that the button is also hidden by default

[Mario Carneiro]

It's not necessarily a bad default - mathlib is big and you should probably only search in it deliberately

[Johan Commelin]

How often is mathlib bumped in the tutorial project?

[Kevin Buzzard]

That's also a good question -- a new user might not have suggest because it's not there ;-)

[Rob Lewis]

I guess it's bumped whenever someone bumps it. There's nothing automatic set up. It can't really hurt to do it regularly.

[Jalex Stark]

(to confirm kevin's suspicion, import tactic.suggest doesn't do anything for me)

[Mario Carneiro]

Oh, I checked out Rob's link, and it's a lot better than I last saw

[Mario Carneiro]

we have a search now!

[Rob Lewis]

Yep, Google got around to indexing the doc pages.

[Mario Carneiro]

I might suggest putting tactic.suggest as the main header though, it's not obvious what file I'm looking at

[Mario Carneiro]

or how to import it into my project

[Mario Carneiro]

looks like it's in the <title> but that's not copyable

[Rob Lewis]

The module doc at https://github.com/leanprover-community/mathlib/blob/1c4a2966ef25ec82e65337022a0764e87a81d992/src/tactic/suggest.lean is malformed, which is why it's missing a header. But yeah, the path should probably be formatted as an import somewhere on the page.

[Rob Lewis]

If you want these doc pages to really look good, and search to really work, the library needs to be documented correctly!

[Mario Carneiro]

the header on the sidebar should also have the full path. https://leanprover-community.github.io/mathlib_docs/tactic/rewrite_all/basic.html has header "basic" which isn't so helpful

[Rob Lewis]

Yup. I'll change that to be the full import path.

[Mario Carneiro]

You could put the path in the file header, but that's just going to make the quality dependent on good doc headers, whereas this is something that can be applied uniformly by the doc tool itself

[Mario Carneiro]

I think it actually looks a bit weird that there is no h1 header in the main pane, it just jumps right into the file header. I'm thinking something like:

<h1>tactic.suggest</h1>
file header...

[Rob Lewis]

I think it looks pretty natural on files like https://leanprover-community.github.io/mathlib_docs/geometry/manifold/real_instances.html where the file name isn't a great description of the file contents.

[Mario Carneiro]

I see, you want the file header to actually have an h1 in it. In that case, I would suggest putting the file name as <h2><code>file.name</code></h2> above the main header

[Rob Lewis]

I'm not sure. I'll add the full path to the right sidebar for sure. Putting it at the top of the page would be duplicating info. It's also visible in the cascading menu on the left, in a slightly different format.

[Rob Lewis]

I'll experiment, but it'll have to wait until after lunch.

[Mario Carneiro]

That's true. I like the Rust docs: https://doc.rust-lang.org/std/convert/trait.AsRef.html . The path is the main header, while the sidebar only contains subfunctions and a short name. The source link is also on the main header (the [src] link)

[Johan Commelin]

Here's the top 10 results when I search for manifold:

mathlib docs: geometry.manifold.real_instances
https://leanprover-community.github.io/.../manifold/real_instances.html
We introduce the necessary bits to be able to define manifolds modelled over ℝ^ n, boundaryless or with boundary or with corners. As a concrete example, we ...
mathlib docs: tactic.rcases
https://leanprover-community.github.io/mathlib_docs/.../rcases.html
The parser/printer uses an "inverted" meaning for the many constructor: rather than representing a sum of products, here it represents a product of sums.
mathlib docs: tactic.scc
https://leanprover-community.github.io/mathlib_docs/.../scc.html
Strongly Connected Components. This file defines tactics to construct proofs of equivalences between a set of mutually equivalent propositions. The tactics use ...
mathlib docs: tactic.lint
https://leanprover-community.github.io/mathlib_docs/.../lint.html
lint command. This file defines the following user commands to spot common mistakes in the code. #lint : check all declarations in the current file; #lint_mathlib  ...
mathlib docs: topology.metric_space.gromov_hausdorff
https://leanprover-community.github.io/.../gromov_hausdorff.html
Gromov-Hausdorff distance. This file defines the Gromov-Hausdorff distance on the space of nonempty compact metric spaces up to isometry. We introduces the  ...
mathlib docs: tactic.abel
https://leanprover-community.github.io/mathlib_docs/.../abel.html
n₁ + n₂ = n' → a₁ + a₂ = a' → tactic.abel.term n₁ x a₁ + tactic.abel.term n₂ x a₂ = tactic.abel.term n' x a'. Implicit arguments: {α : Type u_1} ...
mathlib docs: set_theory.surreal
https://leanprover-community.github.io/mathlib_docs/.../surreal.html
Surreal numbers. The basic theory of surreal numbers, built on top of the theory of combinatorial (pre-)games. A pregame is numeric if all the Left options are ...
mathlib docs: tactic.ring
https://leanprover-community.github.io/mathlib_docs/.../ring.html
tactic.ring.horner a₁ x n₁ b₁ * a₂ = aa → tactic.ring.horner aa x n₂ 0 = haa → a₁ * b₂ = ab → b₁ * b₂ = bb → haa + tactic.ring.horner ab x n₁ bb = t ...
mathlib docs: data.pnat.xgcd
https://leanprover-community.github.io/mathlib_docs/.../xgcd.html
A term of xgcd_type is a system of six naturals. They should be thought of as representing the matrix [[w, x], [y, z]] = [[wp + 1, x], [y, zp + 1]] together with the vector ...
mathlib docs: data.num.basic
https://leanprover-community.github.io/mathlib_docs/.../basic.html
Alternative representation of integers using a sign bit at the end. The convention on sign here is to have the argument to msb denote the sign of the MSB itself, ...

[Johan Commelin]

The first one is certainly relevant, but the others not so much. I would have expected more relevant results...

[Johan Commelin]

After all, there are 3 files with "manifold" in their name

[Johan Commelin]

@Simon Hudon Didn't you have some method to bump mathlib in projects that depend on it? You were working on something like that recently. Could that be used to keep the tutorial project up to date with mathlib? (Bump it once a month, or once week, or so.)

[Mario Carneiro]

A google search will try to use pagerank which will be pretty close to useless for us

[Rob Lewis]

I actually find the Rust docs a little confusing, but I don't know the Rust ontology, so maybe that's not surprising. I suspect we're tied more closely to our file structure than they are. There doesn't seem to be a version of our collapsible menu in their docs. But this structure is the main method of organization in mathlib right now.

[Rob Lewis]

I swapped the sides of the two nav menus, so now the file name appears in full in the top left.

[Rob Lewis]

It seems more like a title there than in the top right.

[Rob Lewis]

The collapsible menu is a little bare at the top. Maybe the search box should move over there?

[Rob Lewis]

Search is using Google's "site search," which is more specific than a generic Google search but much worse than a dedicated search tool. Ideally we'd return results at the declaration level, not at the page level. But we'd have to change the whole hosting setup for that, GitHub Pages only supports static sites.

[Rob Lewis]

Oh, the left menu isn't a consistent size anymore. I messed something up swapping the sides. Pretend it's always the same width for now.

[Marc Huisinga]

i also find the rust docs to be a bit confusing, but that's perhaps just the fact that i'm not used to them.
personally, i've always liked the go docs (e.g. https://godoc.org/github.com/gorilla/websocket), but i'm not sure how well this general style applies to lean.

[Marc Huisinga]

the current lean docs already look pretty good!

[Kevin Buzzard]

(to confirm kevin's suspicion, import tactic.suggest doesn't do anything for me)

@Jalex Stark If you installed the tutorial project from the command line with something like

git clone https://github.com/leanprover-community/tutorials.git
cd tutorials
leanpkg configure
update-mathlib

then you could go back to the command line, find your way back into the tutorials directory, and this time type

leanpkg upgrade
update-mathlib

and you should magically get access to suggest (although it sounds like you'll have to import it still).

[Mario Carneiro]

I admit that hierarchical navigation in the Rust docs is not so easy (you can navigate "modules" in the left nav but you have to go through a lot of pages), but the search is good enough that I don't really need it most of the time. The main pages talk about a struct and its functions, but that distinction is less clear for us so having file based navigation seems fine. But a good search (even just within identifiers) is very helpful for getting around

[Gabriel Ebner]

[...] Ideally we'd return results at the declaration level, not at the page level. But we'd have to change the whole hosting setup for that, GitHub Pages only supports static sites.

We could also implement the search part in javascript, this still works using static hosting. IIRC sphinx also uses this approach.

[Mario Carneiro]

That is my thought as well. I'd volunteer but I don't think I can find the time right now

[Mario Carneiro]

so I'll just make zero-effort suggestions here :P

[Rob Lewis]

This is way out of my wheelhouse too, heh. CSS is bad enough.

[Mario Carneiro]

lol, you should try to do the search in CSS

[Mario Carneiro]

surely it's turing complete by now

[Rob Lewis]

https://stackoverflow.com/questions/2497146/is-css-turing-complete

[Rob Lewis]

But I got annoyed enough trying to make the three columns scroll separately.

[Rob Lewis]

To do JS search, we'd have to have the whole declaration database in JS, right? Or is there some way to pre-index it?

[Gabriel Ebner]

To do JS search, we'd have to have the whole declaration database in JS, right? Or is there some way to pre-index it?

I think the usual approach is to store a precomputed index as a separate (e.g. JSON) file that is generated when building the documentation, and then load it on demand.

[Mario Carneiro]

I looked at how the rust docs do it: At the end of view-source:https://doc.rust-lang.org/core/panicking/index.html there is a script tag going to search-index1.39.0.js which is precomputed during doc generation

[Mario Carneiro]

It's marked <script defer src="../../search-index1.39.0.js"> and placed at the end of the file, which is a bit unusual for script tags. I guess there is a lazy loading thing going on

[Rob Lewis]

Hmm. The JSON file used to generate the docs is ~15mb and compresses to 2.5mb. Not all of that is needed for indexing of course. The Rust js index is a much more reasonable 200kb, and I assume they have more to index. So that pre-computation is definitely important.

[Mario Carneiro]

They have full paths for objects plus ~20 characters blurb taken from the docs on the object

[Mario Carneiro]

I'm thinking we need the full path, the type, and a doc blurb

[Rob Lewis]

This is effectively what that 15mb json file has. It also has file position info (which we don't need for search) and module docs (which we do).

[Mario Carneiro]

by blurb I mean cut off at ~20 characters

[Mario Carneiro]

I don't think you are doing that now

[Rob Lewis]

Oh, no. But a lot of doc strings contain useful keywords beyond 20 characters...

[Rob Lewis]

By "blurb," do you mean it's only including important-seeming keywords?

[Mario Carneiro]

no, it's just the beginning. But they plan for this, and stick important stuff at the beginning

[Mario Carneiro]

I recall javadoc doing something similar: the first sentence is special and appears in other places so you are encouraged to use it for summary

[Rob Lewis]

It seems like it would be almost as effective to just strip common words from the strings.

[Rob Lewis]

The doc strings are probably a relatively small part of the export right now, too, although hopefully they'll grow. The type info takes a lot more space. We could filter a lot of that too before indexing.

[Rob Lewis]

"We." I'm saying this like it's something I'm going to do, but this is a project I'd much rather hand off to someone else, heh.

[Mario Carneiro]

The doc blurbs are used both for search and display in the rustdoc case

[Mario Carneiro]

when you type, it puts each match on a line with the found instances highlighted in red

[Mario Carneiro]

I'm pretty sure this is why the blurbs are so short - more than 20 chars would bust the line length

[Mario Carneiro]

oh wait, maybe it doesn't highlight

[Rob Lewis]

I'm not sure it even searches the strings at all.

[Rob Lewis]

For a random example, https://doc.rust-lang.org/std/net/enum.SocketAddr.html#method.port shows up if you search sort. But not if you search associated.

[Patrick Massot]

This Rust website explicitly says where it will search: name, parameters or return type.

[Mario Carneiro]

Okay, so I guess the blurbs are just there to give you some context for list items in the search

[Mario Carneiro]

If we display name + type (blurb), we could do away with it entirely

[Rob Lewis]

There are complications with searching types (and parameter types). For instance, the doc generator doesn't know the connection between nat and ℕ. As a start, I think we'd be fine searching just declaration names and doc strings, and displaying declaration name, type, and an initial segment of the doc string. We could filter common words out of the doc strings for indexing. So the search data would be tuples (name, doc string keywords, type, doc string blurb) where the latter two are for display only. I think this would still be a much larger index than the Rust index but I'm not sure.

[Rob Lewis]

Oh, it also needs the source file. That and declaration name are enough to build a link.

[Rob Lewis]

Ah, but it also needs to know about module docs. So I think it's two-sorted, "search declarations" or "search files."

[Rob Lewis]

This feels more and more like a project for not-me.