## Stream: new members

### Topic: mathlib tactics

#### Jalex Stark (Dec 09 2019 at 10:34):

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 (Dec 09 2019 at 10:35):

Did you "open folder" in vscode?

#### Jalex Stark (Dec 09 2019 at 10:36):

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

#### Mario Carneiro (Dec 09 2019 at 10:36):

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 (Dec 09 2019 at 10:36):

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

#### Mario Carneiro (Dec 09 2019 at 10:37):

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

#### Mario Carneiro (Dec 09 2019 at 10:38):

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 (Dec 09 2019 at 10:39):

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

#### Rob Lewis (Dec 09 2019 at 10:41):

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

#### Jalex Stark (Dec 09 2019 at 10:42):

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

#### Jalex Stark (Dec 09 2019 at 10:43):

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

#### Kevin Buzzard (Dec 09 2019 at 10:43):

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

#### Kevin Buzzard (Dec 09 2019 at 10:44):

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 (Dec 09 2019 at 10:45):

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 (Dec 09 2019 at 10:45):

Then things are functioning correctly ;-)

#### Kevin Buzzard (Dec 09 2019 at 10:46):

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 (Dec 09 2019 at 10:46):

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 (Dec 09 2019 at 10:47):

i don't have suggest

#### Rob Lewis (Dec 09 2019 at 10:47):

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 (Dec 09 2019 at 10:47):

i do have linarith

#### Rob Lewis (Dec 09 2019 at 10:48):

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

#### Kevin Buzzard (Dec 09 2019 at 10:48):

import tactic.suggest  seems to fix it

#### Mario Carneiro (Dec 09 2019 at 10:48):

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

#### Mario Carneiro (Dec 09 2019 at 10:49):

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

#### Kevin Buzzard (Dec 09 2019 at 10:49):

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

#### Mario Carneiro (Dec 09 2019 at 10:49):

I mean grep for it

#### Kevin Buzzard (Dec 09 2019 at 10:49):

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

#### Rob Lewis (Dec 09 2019 at 10:50):

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

#### Mario Carneiro (Dec 09 2019 at 10:50):

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

#### Jalex Stark (Dec 09 2019 at 10:50):

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

#### Mario Carneiro (Dec 09 2019 at 10:51):

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

#### Kevin Buzzard (Dec 09 2019 at 10:51):

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 (Dec 09 2019 at 10:52):

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

#### Kevin Buzzard (Dec 09 2019 at 10:52):

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

#### Kevin Buzzard (Dec 09 2019 at 10:52):

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

#### Mario Carneiro (Dec 09 2019 at 10:53):

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

#### Johan Commelin (Dec 09 2019 at 10:53):

How often is mathlib bumped in the tutorial project?

#### Kevin Buzzard (Dec 09 2019 at 10:54):

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

#### Rob Lewis (Dec 09 2019 at 10:55):

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 (Dec 09 2019 at 10:55):

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

#### Mario Carneiro (Dec 09 2019 at 10:56):

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

#### Mario Carneiro (Dec 09 2019 at 10:56):

we have a search now!

#### Rob Lewis (Dec 09 2019 at 10:57):

Yep, Google got around to indexing the doc pages.

#### Mario Carneiro (Dec 09 2019 at 10:57):

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

#### Mario Carneiro (Dec 09 2019 at 10:57):

or how to import it into my project

#### Mario Carneiro (Dec 09 2019 at 10:58):

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

#### Rob Lewis (Dec 09 2019 at 10:58):

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 (Dec 09 2019 at 11:00):

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

#### Mario Carneiro (Dec 09 2019 at 11:00):

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 (Dec 09 2019 at 11:00):

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

#### Mario Carneiro (Dec 09 2019 at 11:02):

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 (Dec 09 2019 at 11:06):

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>


#### Rob Lewis (Dec 09 2019 at 11:09):

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 (Dec 09 2019 at 11:11):

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 (Dec 09 2019 at 11:14):

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 (Dec 09 2019 at 11:14):

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

#### Mario Carneiro (Dec 09 2019 at 11:17):

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 (Dec 09 2019 at 11:37):

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 (Dec 09 2019 at 11:37):

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

#### Johan Commelin (Dec 09 2019 at 11:38):

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

#### Johan Commelin (Dec 09 2019 at 11:41):

@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 (Dec 09 2019 at 12:03):

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

#### Rob Lewis (Dec 09 2019 at 12:16):

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 (Dec 09 2019 at 12:17):

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

#### Rob Lewis (Dec 09 2019 at 12:17):

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

#### Rob Lewis (Dec 09 2019 at 12:18):

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

#### Rob Lewis (Dec 09 2019 at 12:20):

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 (Dec 09 2019 at 12:23):

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 (Dec 09 2019 at 12:25):

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 (Dec 09 2019 at 12:27):

the current lean docs already look pretty good!

#### Kevin Buzzard (Dec 09 2019 at 12:28):

(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 (Dec 09 2019 at 12:29):

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 (Dec 09 2019 at 12:35):

[...] 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 (Dec 09 2019 at 12:36):

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

#### Mario Carneiro (Dec 09 2019 at 12:37):

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

#### Rob Lewis (Dec 09 2019 at 12:37):

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

#### Mario Carneiro (Dec 09 2019 at 12:38):

lol, you should try to do the search in CSS

#### Mario Carneiro (Dec 09 2019 at 12:38):

surely it's turing complete by now

#### Rob Lewis (Dec 09 2019 at 12:40):

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

#### Rob Lewis (Dec 09 2019 at 12:40):

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

#### Rob Lewis (Dec 09 2019 at 12:47):

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 (Dec 09 2019 at 12:53):

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 (Dec 09 2019 at 13:20):

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 (Dec 09 2019 at 13:21):

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 (Dec 09 2019 at 15:47):

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 (Dec 09 2019 at 15:49):

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

#### Mario Carneiro (Dec 09 2019 at 15:50):

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

#### Rob Lewis (Dec 09 2019 at 15:51):

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 (Dec 09 2019 at 15:52):

by blurb I mean cut off at ~20 characters

#### Mario Carneiro (Dec 09 2019 at 15:52):

I don't think you are doing that now

#### Rob Lewis (Dec 09 2019 at 15:53):

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

#### Rob Lewis (Dec 09 2019 at 15:53):

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

#### Mario Carneiro (Dec 09 2019 at 15:53):

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

#### Mario Carneiro (Dec 09 2019 at 15:54):

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 (Dec 09 2019 at 15:57):

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

#### Rob Lewis (Dec 09 2019 at 15:58):

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 (Dec 09 2019 at 15:58):

"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 (Dec 09 2019 at 16:13):

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

#### Mario Carneiro (Dec 09 2019 at 16:13):

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

#### Mario Carneiro (Dec 09 2019 at 16:14):

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

#### Mario Carneiro (Dec 09 2019 at 16:15):

oh wait, maybe it doesn't highlight

#### Rob Lewis (Dec 09 2019 at 16:17):

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

#### Rob Lewis (Dec 09 2019 at 16:19):

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 (Dec 09 2019 at 16:53):

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

#### Mario Carneiro (Dec 09 2019 at 17:07):

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

#### Mario Carneiro (Dec 09 2019 at 17:08):

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

#### Rob Lewis (Dec 09 2019 at 17:25):

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 (Dec 09 2019 at 17:26):

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

#### Rob Lewis (Dec 09 2019 at 17:36):

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

#### Rob Lewis (Dec 09 2019 at 17:37):

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

Last updated: May 11 2021 at 21:10 UTC