Zulip Chat Archive

Stream: new members

Topic: mathlib tactics


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Dec 09 2019 at 10:35):

Did you "open folder" in vscode?

view this post on Zulip Jalex Stark (Dec 09 2019 at 10:36):

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

view this post on Zulip 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"

view this post on Zulip Jalex Stark (Dec 09 2019 at 10:36):

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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 10:37):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 09 2019 at 10:39):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Jalex Stark (Dec 09 2019 at 10:43):

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

view this post on Zulip 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).

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 09 2019 at 10:45):

Then things are functioning correctly ;-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jalex Stark (Dec 09 2019 at 10:47):

i don't have suggest

view this post on Zulip 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.

view this post on Zulip Jalex Stark (Dec 09 2019 at 10:47):

i do have linarith

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 09 2019 at 10:48):

import tactic.suggest seems to fix it

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 10:49):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 10:49):

I mean grep for it

view this post on Zulip 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)

view this post on Zulip Rob Lewis (Dec 09 2019 at 10:50):

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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 10:50):

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

view this post on Zulip Kevin Buzzard (Dec 09 2019 at 10:50):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 10:51):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 09 2019 at 10:52):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Dec 09 2019 at 10:53):

How often is mathlib bumped in the tutorial project?

view this post on Zulip 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 ;-)

view this post on Zulip 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.

view this post on Zulip Jalex Stark (Dec 09 2019 at 10:55):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 10:56):

we have a search now!

view this post on Zulip Rob Lewis (Dec 09 2019 at 10:57):

Yep, Google got around to indexing the doc pages.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 10:57):

or how to import it into my project

view this post on Zulip Mario Carneiro (Dec 09 2019 at 10:58):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Rob Lewis (Dec 09 2019 at 11:00):

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

view this post on Zulip 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

view this post on Zulip 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>
file header...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Dec 09 2019 at 11:14):

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

view this post on Zulip 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)

view this post on Zulip 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, ...

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Dec 09 2019 at 11:38):

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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Dec 09 2019 at 12:17):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Dec 09 2019 at 12:27):

the current lean docs already look pretty good!

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 12:37):

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

view this post on Zulip Rob Lewis (Dec 09 2019 at 12:37):

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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 12:38):

lol, you should try to do the search in CSS

view this post on Zulip Mario Carneiro (Dec 09 2019 at 12:38):

surely it's turing complete by now

view this post on Zulip Rob Lewis (Dec 09 2019 at 12:40):

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

view this post on Zulip Rob Lewis (Dec 09 2019 at 12:40):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 15:50):

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

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Dec 09 2019 at 15:52):

by blurb I mean cut off at ~20 characters

view this post on Zulip Mario Carneiro (Dec 09 2019 at 15:52):

I don't think you are doing that now

view this post on Zulip Rob Lewis (Dec 09 2019 at 15:53):

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

view this post on Zulip Rob Lewis (Dec 09 2019 at 15:53):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Dec 09 2019 at 16:13):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 16:15):

oh wait, maybe it doesn't highlight

view this post on Zulip Rob Lewis (Dec 09 2019 at 16:17):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Dec 09 2019 at 16:53):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 09 2019 at 17:08):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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."

view this post on Zulip 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