## Stream: general

### Topic: import with open_locale

#### Kenny Lau (Apr 12 2020 at 06:27):

import data.list
open_locale classical


error:

file 'open_locale' not found in the LEAN_PATH

invalid import: open_locale
could not resolve import: open_locale

invalid import: classical
could not resolve import: classical


@Mario Carneiro

#### Yury G. Kudryashov (Apr 12 2020 at 06:28):

You need something between import and open_locale

#### Yury G. Kudryashov (Apr 12 2020 at 06:28):

AFAIR, a comment will do.

#### Yury G. Kudryashov (Apr 12 2020 at 06:28):

There can be no user-defined command after import

#### Kenny Lau (Apr 12 2020 at 06:32):

so I settled with #check id

#### Yury G. Kudryashov (Apr 12 2020 at 06:36):

Including /-! ... -/?

#### Kenny Lau (Apr 12 2020 at 06:36):

oh I didn't know that it exists

#### Yury G. Kudryashov (Apr 12 2020 at 06:40):

It is used for module-level docstrings

#### Mario Carneiro (Apr 12 2020 at 06:41):

I usually use section end

#### Kevin Buzzard (Apr 12 2020 at 07:05):

I think /-! -/ is pretty golfy

#### Mario Carneiro (Apr 12 2020 at 07:07):

I worry about other options that they will affect the output

#### Mario Carneiro (Apr 12 2020 at 07:07):

for example does that leave something funny in the leandoc?

#### Kenny Lau (Apr 12 2020 at 07:07):

let's say the solution is universes u v

#### Mario Carneiro (Apr 12 2020 at 07:08):

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

#### Mario Carneiro (Apr 12 2020 at 07:09):

aha, variables works

#### Mario Carneiro (Apr 12 2020 at 07:09):

import tactic.lint
variables
#lint


#### Kevin Buzzard (Apr 12 2020 at 07:09):

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

#### Mario Carneiro (Apr 12 2020 at 07:10):

most plural commands like universes require 1 or more names

#### Mario Carneiro (Apr 12 2020 at 07:10):

but apparently variables is okay with 0

#### Mario Carneiro (Apr 12 2020 at 07:11):

I guess you mean run_cmd tactic.skip

#### Kevin Buzzard (Apr 12 2020 at 07:11):

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

#### Mario Carneiro (Apr 12 2020 at 07:11):

It's a grammar definition problem

#### Kevin Buzzard (Apr 12 2020 at 07:12):

Yeah but can it actually be fixed?

#### Mario Carneiro (Apr 12 2020 at 07:12):

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

#### Kevin Buzzard (Apr 12 2020 at 07:12):

Yeah but can it actually be fixed?

#### Mario Carneiro (Apr 12 2020 at 07:12):

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

#### Mario Carneiro (Apr 12 2020 at 07:13):

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

#### Mario Carneiro (Apr 12 2020 at 07:14):

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

import foo bar
baz
quux


#### Mario Carneiro (Apr 12 2020 at 07:16):

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 (Apr 12 2020 at 07:30):

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 (Apr 12 2020 at 07:34):

open_locale is a user-defined command.

#### Yury G. Kudryashov (Apr 12 2020 at 07:35):

It is defined in one of the imports

#### Yury G. Kudryashov (Apr 12 2020 at 07:35):

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

#### Yury G. Kudryashov (Apr 12 2020 at 07:36):

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

#### Kevin Buzzard (Apr 12 2020 at 07:44):

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

#### Kevin Buzzard (Apr 12 2020 at 07:45):

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

#### Mario Carneiro (Apr 12 2020 at 07:46):

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 (Apr 12 2020 at 07:46):

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

#### Mario Carneiro (Apr 12 2020 at 07:47):

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

#### Kevin Buzzard (Apr 12 2020 at 07:47):

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 (Apr 12 2020 at 07:47):

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

#### Kevin Buzzard (Apr 12 2020 at 07:48):

Why not just add open_locale to some list

#### Mario Carneiro (Apr 12 2020 at 07:48):

If open_locale was built into lean, yes that would work

#### Mario Carneiro (Apr 12 2020 at 07:48):

but then it wouldn't be a user command

#### Kevin Buzzard (Apr 12 2020 at 07:48):

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

#### Mario Carneiro (Apr 12 2020 at 07:49):

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

#### Mario Carneiro (Apr 12 2020 at 07:49):

because it's a mathlib command

#### Kevin Buzzard (Apr 12 2020 at 07:49):

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

yes

#### Mario Carneiro (Apr 12 2020 at 07:49):

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

#### Kevin Buzzard (Apr 12 2020 at 07:50):

What are the other user commands?

#### Mario Carneiro (Apr 12 2020 at 07:50):

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

#### Mario Carneiro (Apr 12 2020 at 07:50):

you can grep for @[user_command]

#find?

yes

#### Bryan Gin-ge Chen (Apr 12 2020 at 07:51):

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

#### Kevin Buzzard (Apr 12 2020 at 07:51):

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 (Apr 12 2020 at 07:51):

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 (Apr 12 2020 at 07:52):

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

I see

#### Kevin Buzzard (Apr 12 2020 at 07:52):

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

#### Kenny Lau (Apr 12 2020 at 07:53):

btw fintype with open_locale classical is frustratingly slow

#### Kenny Lau (Apr 12 2020 at 07:54):

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

#### Kevin Buzzard (Apr 12 2020 at 07:55):

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 (Apr 12 2020 at 08:23):

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

#### Mario Carneiro (Apr 12 2020 at 08:23):

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

#### Mario Carneiro (Apr 12 2020 at 08:25):

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 (Apr 12 2020 at 08:26):

@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 (Apr 12 2020 at 08:27):

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

#### Kevin Buzzard (Apr 12 2020 at 08:27):

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

#### Mario Carneiro (Apr 12 2020 at 08:27):

Everything is in use by lean or coveted by mathematicians

#### Mario Carneiro (Apr 12 2020 at 08:28):

that's probably a legal identifier character

#### Kevin Buzzard (Apr 12 2020 at 08:28):

so is the d in def

#### Mario Carneiro (Apr 12 2020 at 08:29):

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

#### Mario Carneiro (Apr 12 2020 at 08:29):

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

#### Kenny Lau (Apr 12 2020 at 08:31):

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

#### Kenny Lau (Apr 12 2020 at 08:31):

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

YMMV

try it and see

#### Kenny Lau (Apr 12 2020 at 08:32):

it can't work out that a group has multiplication

#### Gabriel Ebner (Apr 12 2020 at 08:33):

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 (Apr 12 2020 at 08:33):

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

#### Kevin Buzzard (Apr 12 2020 at 08:34):

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

#### Mario Carneiro (Apr 12 2020 at 08:34):

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 (Apr 12 2020 at 08:35):

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

#### Mario Carneiro (Apr 12 2020 at 08:35):

for those who don't like indentation sensitivity

#### Gabriel Ebner (Apr 12 2020 at 09:26):

lean#188

Last updated: May 16 2021 at 05:21 UTC