import with open_locale

Stream: general

[Kenny Lau]

import data.list
open_locale classical

error:

file 'open_locale' not found in the LEAN_PATH

file 'classical' not found in the LEAN_PATH

invalid import: open_locale
could not resolve import: open_locale

invalid import: classical
could not resolve import: classical

[Kenny Lau]

@Mario Carneiro

[Yury G. Kudryashov]

You need something between import and open_locale

[Yury G. Kudryashov]

AFAIR, a comment will do.

[Yury G. Kudryashov]

There can be no user-defined command after import

[Kenny Lau]

comments don't solve this

[Kenny Lau]

so I settled with #check id

[Yury G. Kudryashov]

Including /-! ... -/?

[Kenny Lau]

oh I didn't know that it exists

[Yury G. Kudryashov]

It is used for module-level docstrings

[Mario Carneiro]

I usually use section end

[Kevin Buzzard]

I think /-! -/ is pretty golfy

[Mario Carneiro]

I worry about other options that they will affect the output

[Mario Carneiro]

for example does that leave something funny in the leandoc?

[Kenny Lau]

let's say the solution is universes u v

[Mario Carneiro]

that's not bad, although you might not want to declare universes

[Mario Carneiro]

aha, variables works

[Mario Carneiro]

import tactic.lint
variables
#lint

[Kevin Buzzard]

I've seen someone use something like tactic.cmd skip or something, but I can never remember the syntax

[Mario Carneiro]

most plural commands like universes require 1 or more names

[Mario Carneiro]

but apparently variables is okay with 0

[Mario Carneiro]

I guess you mean run_cmd tactic.skip

[Kevin Buzzard]

The elephant in the room: can this actually be fixed?

[Mario Carneiro]

It's a grammar definition problem

[Kevin Buzzard]

Yeah but can it actually be fixed?

[Mario Carneiro]

That is, unless you change the lean grammar it is doing exactly what it should be doing

[Kevin Buzzard]

Yeah but can it actually be fixed?

[Mario Carneiro]

My preferred solution is to allow . at the end of an import statement to end it

[Mario Carneiro]

We could do something like stop at newlines but that's a bit hackish

[Mario Carneiro]

plus it would have to be unindented lines since imports are sometimes formatted like

import foo bar
  baz
  quux

[Mario Carneiro]

Another possibility: since #lint is not a valid identifier (because of the hash), we can stop when we see something that isn't a name. This won't work for all user commands though; some of them are just words like alias

[Kevin Buzzard]

I just don't understand why import data.real.basic followed by def x := ... works but you can't follow it by open_locale.

[Yury G. Kudryashov]

open_locale is a user-defined command.

[Yury G. Kudryashov]

It is defined in one of the imports

[Yury G. Kudryashov]

And I think that Lean doesn't start looking into these imports before parsing till the end of import list.

[Yury G. Kudryashov]

How should it know that you're not trying to import a file named 'open_locale'?

[Kevin Buzzard]

How should it know that I'm not trying to import a file named def?

[Kevin Buzzard]

You're talking about technicalities. I just don't understand why the problem can't be solved.

[Mario Carneiro]

A number of words like def, import, variables etc are reserved as "command keywords". You can write these anywhere in the file and lean will stop whatever it is doing and begin a new command

[Mario Carneiro]

this is why you can't have a tactic called set_option

[Mario Carneiro]

These define the high level structure of the lean file, and are about the only thing you can parse with no context

[Kevin Buzzard]

I'm well aware that it doesn't currently work but what I'm saying is why can't it be fixed? That's what I don't understand

[Mario Carneiro]

The problem with user commands is that they are command keywords that require context

[Kevin Buzzard]

Why not just add open_locale to some list

[Mario Carneiro]

If open_locale was built into lean, yes that would work

[Mario Carneiro]

but then it wouldn't be a user command

[Kevin Buzzard]

So why can't we just build it into Lean?

[Mario Carneiro]

The point is that lean needs to know that this is a command before it's even read anything

[Mario Carneiro]

because it's a mathlib command

[Kevin Buzzard]

So def is a command and open_locale is a user command?

[Mario Carneiro]

yes

[Mario Carneiro]

it's a command that was defined in a lean file rather than in C++

[Kevin Buzzard]

What are the other user commands?

[Mario Carneiro]

#lint, alias, open_locale, a few others I'm sure

[Mario Carneiro]

you can grep for @[user_command]

[Kevin Buzzard]

#find?

[Mario Carneiro]

yes

[Bryan Gin-ge Chen]

There's a more or less complete list here: https://leanprover-community.github.io/mathlib_docs/commands.html

[Kevin Buzzard]

And we can't just add these to some list in core lean and say "this is a command which we'll define later"?

[Mario Carneiro]

we could, but that's not being nice to people who write their own user commands and want the same level of support

[Mario Carneiro]

the whole point of user commands is that they are not built in

[Kevin Buzzard]

I see

[Kevin Buzzard]

Now I can see the appeal of the full stop after imports over approach

[Kenny Lau]

btw fintype with open_locale classical is frustratingly slow

[Kenny Lau]

although I'm not sure if open_locale classical is the root cause

[Kevin Buzzard]

We can't make it #open_locale and then tell lean that if it begins with a # then no way is it an import?

[Kenny Lau]

@Mario Carneiro is there a way to make Lean tell me which typeclass it struggles to resolve?

[Mario Carneiro]

@Kevin Buzzard We can, that's one of the options I mentioned

[Mario Carneiro]

but does it mean we have to put # on all user commands? I believe the intended meaning of # is temporary commands for interactive use, while several user commands are not meant to be temporary, such as alias, open_locale, add_decl_doc and others

[Mario Carneiro]

@Kenny Lau You can print out the typeclass search using set_option trace.class_instances true; the hard ones are the ones that print out megabytes of tracing info

[Kevin Buzzard]

So maybe we come up with some other symbol to start a user command. How about ,?

[Kevin Buzzard]

I've heard they're phasing it out in Lean 4 so it's probably going spare.

[Mario Carneiro]

Everything is in use by lean or coveted by mathematicians

[Kevin Buzzard]

How about an emoji?

[Mario Carneiro]

that's probably a legal identifier character

[Kevin Buzzard]

so is the d in def

[Mario Carneiro]

but once lean parses the word it finds it on its list of command keywords

[Mario Carneiro]

it won't find a user command on that list so it assumes it's a file name

[Kevin Buzzard]

Ok so I don't feel too bad about banning file names which start with an emoji

[Kenny Lau]

@Mario Carneiro can I set_option class.instance_max_depth 10 with the same effect?

[Kenny Lau]

(the ones that fail to resolve are the problematic ones)

[Mario Carneiro]

YMMV

[Mario Carneiro]

try it and see

[Kenny Lau]

it can't work out that a group has multiplication

[Gabriel Ebner]

How about parsing indentation-sensitively, like Lean 4:

import foo
  bar
open_locale classical -- runs user command

and

import foo
  bar
 open_locale classical -- imports open_locale and classical modules

[Mario Carneiro]

@Kenny Lau You should probably ask a separate question, this is getting cluttered

[Kevin Buzzard]

The indentation idea is by far the most practical I've heard so far

[Mario Carneiro]

I'm okay with the indentation solution because it will have a basically 100% success rate without any change to mathlib, although it would be a departure from anything we have done in lean parsing elsewhere

[Mario Carneiro]

I would prefer that we support both that and the . option

[Mario Carneiro]

for those who don't like indentation sensitivity

[Gabriel Ebner]

lean#188